# Radicals of ideals of commutative rings

Content created by Egbert Rijke, Fredrik Bakke and Maša Žaucer.

Created on 2023-03-19.

module commutative-algebra.radicals-of-ideals-commutative-rings where

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

open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import order-theory.galois-connections-large-posets
open import order-theory.order-preserving-maps-large-posets
open import order-theory.order-preserving-maps-large-preorders
open import order-theory.reflective-galois-connections-large-posets


## Idea

The radical √ I of an ideal I in a commutative ring A is the least radical ideal of A containing I. The radical √ I is constructed as the ideal consisting of all elements f for which there exists an n such that fⁿ ∈ I.

The operation I ↦ √ I is a reflective Galois connection from the large poset of ideals in A into the large poset of radical ideals in A.

## Definitions

### The condition of being the radical of an ideal

module _
{l1 l2 l3 : Level} (A : Commutative-Ring l1)
(I : ideal-Commutative-Ring l2 A)
(H :
leq-ideal-Commutative-Ring A I (ideal-radical-ideal-Commutative-Ring A J))
where

{l4 : Level} (K : radical-ideal-Commutative-Ring l4 A) →
leq-ideal-Commutative-Ring A I (ideal-radical-ideal-Commutative-Ring A K) →
leq-ideal-Commutative-Ring A


### The radical Galois connection on ideals of a commutative ring

#### The radical of an ideal

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

subset-radical-of-ideal-Commutative-Ring : type-Commutative-Ring A → Prop l2
∃ ℕ (λ n → subset-ideal-Commutative-Ring A I (power-Commutative-Ring A n f))

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

(f : type-Commutative-Ring A) →
is-in-ideal-Commutative-Ring A I f →
contains-ideal-radical-of-ideal-Commutative-Ring f H = intro-exists 1 H

( zero-Commutative-Ring A)
( contains-zero-ideal-Commutative-Ring A I)

apply-universal-property-trunc-Prop H
( λ (n , p) →
apply-universal-property-trunc-Prop K
( λ (m , q) →
intro-exists
( n +ℕ m)
( is-closed-under-eq-ideal-Commutative-Ring' A I
( is-closed-under-right-multiplication-ideal-Commutative-Ring
( A)
( I)
( _)
( _)
( q))
( is-closed-under-right-multiplication-ideal-Commutative-Ring
( A)
( I)
( _)
( _)
( p)))
( is-linear-combination-power-add-Commutative-Ring A n m x y))))

is-closed-under-negatives-subset-Commutative-Ring A
apply-universal-property-trunc-Prop H
( λ (n , p) →
intro-exists n
( is-closed-under-eq-ideal-Commutative-Ring' A I
( is-closed-under-left-multiplication-ideal-Commutative-Ring A I _
( power-Commutative-Ring A n x)
( p))
( power-neg-Commutative-Ring A n x)))

is-closed-under-right-multiplication-subset-Commutative-Ring A
apply-universal-property-trunc-Prop H
( subset-radical-of-ideal-Commutative-Ring (mul-Commutative-Ring A x y))
( λ (n , p) →
intro-exists n
( is-closed-under-eq-ideal-Commutative-Ring' A I
( is-closed-under-right-multiplication-ideal-Commutative-Ring A I
( power-Commutative-Ring A n x)
( power-Commutative-Ring A n y)
( p))
( distributive-power-mul-Commutative-Ring A n x y)))

is-closed-under-left-multiplication-subset-Commutative-Ring A
apply-universal-property-trunc-Prop H
( subset-radical-of-ideal-Commutative-Ring (mul-Commutative-Ring A x y))
( λ (n , p) →
intro-exists n
( is-closed-under-eq-ideal-Commutative-Ring' A I
( is-closed-under-left-multiplication-ideal-Commutative-Ring A I
( power-Commutative-Ring A n x)
( power-Commutative-Ring A n y)
( p))
( distributive-power-mul-Commutative-Ring A n x y)))

ideal-right-ideal-Commutative-Ring A

apply-universal-property-trunc-Prop H
( λ (m , K) →
intro-exists
( mul-ℕ n m)
( is-closed-under-eq-ideal-Commutative-Ring' A I K
( power-mul-Commutative-Ring A n m)))

apply-universal-property-trunc-Prop K
( λ (n , L) →
( H (power-Commutative-Ring A n x) L))


#### The operation I ↦ √ I as an order preserving map

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

{l2 l3 : Level}
(I : ideal-Commutative-Ring l2 A) (J : ideal-Commutative-Ring l3 A) →
leq-ideal-Commutative-Ring A I J →
( transitive-leq-ideal-Commutative-Ring A I J
( H))

hom-Large-Poset
( λ l → l)
( ideal-Commutative-Ring-Large-Poset A)
map-hom-Large-Preorder
preserves-order-hom-Large-Preorder


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

{l2 l3 : Level}
(I : ideal-Commutative-Ring l2 A)
(J : radical-ideal-Commutative-Ring l3 A) →
( J) ↔
leq-ideal-Commutative-Ring A
( I)
transitive-leq-ideal-Commutative-Ring A I
( H)

galois-connection-Large-Poset (λ l → l) (λ l → l)
( ideal-Commutative-Ring-Large-Poset A)


#### The radical reflective Galois connection

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

is-reflective-galois-connection-Large-Poset
( ideal-Commutative-Ring-Large-Poset A)
( I)