# Radical ideals of commutative rings

Content created by Egbert Rijke, Fredrik Bakke, Maša Žaucer and Gregor Perčič.

Created on 2023-03-19.

module commutative-algebra.radical-ideals-commutative-rings where

Imports
open import commutative-algebra.commutative-rings
open import commutative-algebra.ideals-commutative-rings
open import commutative-algebra.powers-of-elements-commutative-rings
open import commutative-algebra.subsets-commutative-rings

open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtype-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels


## Idea

An ideal I in a commutative ring is said to be radical if for every element f : A such that there exists an n such that fⁿ ∈ I, we have f ∈ I. In other words, radical ideals are ideals that contain, for every element u ∈ I, also the n-th roots of u if it has any.

## Definitions

### The condition of being a radical ideal

module _
{l1 l2 : Level} (A : Commutative-Ring l1)
where

(I : ideal-Commutative-Ring l2 A) → Prop (l1 ⊔ l2)
Π-Prop
( type-Commutative-Ring A)
( λ f →
Π-Prop ℕ
( λ n →
function-Prop
( is-in-ideal-Commutative-Ring A I (power-Commutative-Ring A n f))
( subset-ideal-Commutative-Ring A I f)))

(I : ideal-Commutative-Ring l2 A) → UU (l1 ⊔ l2)

(I : ideal-Commutative-Ring l2 A) →


radical-ideal-Commutative-Ring :
{l1 : Level} (l2 : Level) → Commutative-Ring l1 → UU (l1 ⊔ lsuc l2)
Σ (ideal-Commutative-Ring l2 A) (is-radical-ideal-Commutative-Ring A)

module _
{l1 l2 : Level} (A : Commutative-Ring l1)
where

is-in-radical-ideal-Commutative-Ring : type-Commutative-Ring A → UU l2

{x y : type-Commutative-Ring A} → is-in-radical-ideal-Commutative-Ring x →
(x ＝ y) → is-in-radical-ideal-Commutative-Ring y
is-closed-under-eq-subset-Commutative-Ring A

{x y : type-Commutative-Ring A} → is-in-radical-ideal-Commutative-Ring y →
(x ＝ y) → is-in-radical-ideal-Commutative-Ring x
is-closed-under-eq-subset-Commutative-Ring' A

type-radical-ideal-Commutative-Ring : UU (l1 ⊔ l2)

is-ideal-ideal-Commutative-Ring A

is-closed-under-left-multiplication-subset-Commutative-Ring A
is-closed-under-left-multiplication-ideal-Commutative-Ring A

is-closed-under-right-multiplication-subset-Commutative-Ring A
is-closed-under-right-multiplication-ideal-Commutative-Ring A

(n : ℕ) (x : type-Commutative-Ring A) →
is-in-radical-ideal-Commutative-Ring (power-Commutative-Ring A (succ-ℕ n) x)
is-closed-under-powers-ideal-Commutative-Ring A


## Properties

### Characterizing equality of radical ideals

module _
{l1 : Level} (A : Commutative-Ring l1)
where

{l2 l3 : Level} →
radical-ideal-Commutative-Ring l3 A → UU (l1 ⊔ l2 ⊔ l3)
has-same-elements-ideal-Commutative-Ring A

{l2 : Level} (I : radical-ideal-Commutative-Ring l2 A) →
refl-has-same-elements-ideal-Commutative-Ring A

{l2 : Level} (I : radical-ideal-Commutative-Ring l2 A) →
is-torsorial
is-torsorial-Eq-subtype
( is-torsorial-has-same-elements-ideal-Commutative-Ring A

{l2 : Level} (I J : radical-ideal-Commutative-Ring l2 A) →
(I ＝ J) → has-same-elements-radical-ideal-Commutative-Ring I J

{l2 : Level} (I J : radical-ideal-Commutative-Ring l2 A) →
fundamental-theorem-id

{l2 : Level} (I J : radical-ideal-Commutative-Ring l2 A) →
(I ＝ J) ≃ has-same-elements-radical-ideal-Commutative-Ring I J