# Joins of radical ideals of commutative rings

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

Created on 2023-06-08.

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

Imports
open import commutative-algebra.commutative-rings
open import commutative-algebra.ideals-commutative-rings
open import commutative-algebra.joins-ideals-commutative-rings
open import commutative-algebra.products-ideals-commutative-rings
open import commutative-algebra.subsets-commutative-rings

open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.universe-levels

open import order-theory.large-suplattices
open import order-theory.least-upper-bounds-large-posets


## Idea

The join of a family of radical ideals α ↦ J α in a commutative ring is the least radical ideal containing each J α.

## Definitions

### The universal property of the join of a family of radical ideals

module _
{l1 l2 l3 : Level} (A : Commutative-Ring l1)
{U : UU l2} (I : U → radical-ideal-Commutative-Ring l3 A)
where

{l4 : Level} (K : radical-ideal-Commutative-Ring l4 A) → UUω
is-least-upper-bound-family-of-elements-Large-Poset
( I)

{l4 : Level} (J : radical-ideal-Commutative-Ring l4 A) →
{l5 : Level} (K : radical-ideal-Commutative-Ring l5 A) →
((α : U) → leq-radical-ideal-Commutative-Ring A (I α) K) →
leq-is-least-upper-bound-family-of-elements-Large-Poset
( I)

{l4 : Level} (J : radical-ideal-Commutative-Ring l4 A) →
{α : U} → leq-radical-ideal-Commutative-Ring A (I α) J
is-upper-bound-is-least-upper-bound-family-of-elements-Large-Poset
{ x = I}
{ y = J}
( H)
( α)


### The join of a family of radical ideals

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

subset-Commutative-Ring (l2 ⊔ l3) A
generating-subset-join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α))

radical-ideal-Commutative-Ring (l1 ⊔ l2 ⊔ l3) A

{l4 : Level} (K : radical-ideal-Commutative-Ring l4 A) →
((i : I) → leq-radical-ideal-Commutative-Ring A (J i) K) →
( K)
K H =
( join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α)))
( K)
( forward-inclusion-is-join-join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α))
( H))

{l4 : Level} (K : radical-ideal-Commutative-Ring l4 A) →
( K) →
(i : I) → leq-radical-ideal-Commutative-Ring A (J i) K
K H i x p =
H ( x)
( join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α)))
( x)
( backward-inclusion-is-join-join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α))
( join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α)))
( λ t → id)
( i)
( x)
( p)))

K


### The large suplattice of radical ideals in a commutative ring

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

is-large-suplattice-Large-Poset l1
sup-has-least-upper-bound-family-of-elements-Large-Poset
is-least-upper-bound-sup-has-least-upper-bound-family-of-elements-Large-Poset

Large-Suplattice (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3) l1
large-poset-Large-Suplattice
is-large-suplattice-Large-Suplattice


## Properties

### Join is an order preserving operation

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

preserves-order-sup-Large-Suplattice
{ x = I}
{ y = J}
( H)


### √ (⋁_α √ I_α) ＝ √ (⋁_α I_α) for any family I of ideals

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

( λ α → radical-of-ideal-Commutative-Ring A (I α)))
( join-family-of-ideals-Commutative-Ring A I))
( join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-of-ideal-Commutative-Ring A (I α)))
( join-family-of-ideals-Commutative-Ring A I))
( forward-inclusion-is-join-join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-of-ideal-Commutative-Ring A (I α))
( join-family-of-ideals-Commutative-Ring A I))
( λ α →
( I α)
( join-family-of-ideals-Commutative-Ring A I))
( λ x p →
( join-family-of-ideals-Commutative-Ring A I)
( x)
( contains-ideal-join-family-of-ideals-Commutative-Ring
A I x p))))

( join-family-of-ideals-Commutative-Ring A I))
( λ α → radical-of-ideal-Commutative-Ring A (I α)))
( join-family-of-ideals-Commutative-Ring A I)
( join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-of-ideal-Commutative-Ring A (I α)))
( preserves-order-join-family-of-ideals-Commutative-Ring A
( I)
( λ α → ideal-radical-of-ideal-Commutative-Ring A (I α))
( λ α → contains-ideal-radical-of-ideal-Commutative-Ring A (I α)))

( λ α → radical-of-ideal-Commutative-Ring A (I α)) ＝
( join-family-of-ideals-Commutative-Ring A I)
( λ α → radical-of-ideal-Commutative-Ring A (I α)))
( join-family-of-ideals-Commutative-Ring A I))


### Products of radical ideals distribute over joins

Consider a radical ideal I and a family of radical ideals J_α indexed by α : U. To prove distributivity, we make the following calculation where we will write ·r for the product of radical ideals and ⋁r for the join of a family of radical ideals.

  I ·r (⋁r_α J_α) ＝ √ (I · √ (⋁_α J_α))
＝ √ (I · (⋁_α J_α))
＝ √ (⋁_α (I · J_α))
＝ √ (⋁_α √ (I · J_α))
＝ ⋁r_α (I ·r J_α)


The proof below proceeds by proving inclusions in both directions along the computation steps above.

module _
{l1 l2 l3 l4 : Level} (A : Commutative-Ring l1)
{U : UU l3} (J : U → radical-ideal-Commutative-Ring l4 A)
where

( I)
( λ α → product-radical-ideal-Commutative-Ring A I (J α)))
( product-ideal-Commutative-Ring A
( join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α)))))
( λ α → product-radical-ideal-Commutative-Ring A I (J α)))
( product-ideal-Commutative-Ring A
( join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α)))))
( join-family-of-ideals-Commutative-Ring A
( λ α →
product-ideal-Commutative-Ring A
( λ α → product-radical-ideal-Commutative-Ring A I (J α)))
( A)
( λ α →
product-ideal-Commutative-Ring A
( product-ideal-Commutative-Ring A
( join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α))))
( join-family-of-ideals-Commutative-Ring A
( λ α →
product-ideal-Commutative-Ring A
( forward-inclusion-distributive-product-join-family-of-ideals-Commutative-Ring
( A)
( λ α → ideal-radical-ideal-Commutative-Ring A (J α)))))
( A)
( I)
( join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α))))

( λ α → product-radical-ideal-Commutative-Ring A I (J α)))
( I)
( λ α → product-radical-ideal-Commutative-Ring A I (J α)))
( join-family-of-ideals-Commutative-Ring A
( λ α →
product-ideal-Commutative-Ring A
( I)
( join-family-of-ideals-Commutative-Ring A
( λ α →
product-ideal-Commutative-Ring A
( product-ideal-Commutative-Ring A
( join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α)))))
( I)
( A)
( I)
( join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α))))
( join-family-of-ideals-Commutative-Ring A
( λ α →
product-ideal-Commutative-Ring A
( product-ideal-Commutative-Ring A
( join-family-of-ideals-Commutative-Ring A
( λ α → ideal-radical-ideal-Commutative-Ring A (J α))))
( backward-inclusion-distributive-product-join-family-of-ideals-Commutative-Ring
( A)
( λ α → ideal-radical-ideal-Commutative-Ring A (J α)))))
( A)
( λ α →
product-ideal-Commutative-Ring A

( I)
( λ α → product-radical-ideal-Commutative-Ring A I (J α)))

( I)
( λ α → product-radical-ideal-Commutative-Ring A I (J α))
( I)
( λ α → product-radical-ideal-Commutative-Ring A I (J α)))


### Intersections of radical ideals distribute over joins

Since the intersection I ∩ J of two radical ideals is the product IJ of radical ideals, it follows that intersections distribute over joins of radical ideals.

module _
{l1 l2 l3 l4 : Level} (A : Commutative-Ring l1)
{U : UU l3} (J : U → radical-ideal-Commutative-Ring l4 A)
where

( I)
( λ α → intersection-radical-ideal-Commutative-Ring A I (J α)))
( I)
( I)
( λ α → intersection-radical-ideal-Commutative-Ring A I (J α)))
( I)
( λ α → product-radical-ideal-Commutative-Ring A I (J α)))
( λ α → intersection-radical-ideal-Commutative-Ring A I (J α)))
( λ α → product-radical-ideal-Commutative-Ring A I (J α))
( λ α → intersection-radical-ideal-Commutative-Ring A I (J α))
( λ α →
( J α)))
( A)
( I)
( J)))

( λ α → intersection-radical-ideal-Commutative-Ring A I (J α)))
( I)
( λ α → intersection-radical-ideal-Commutative-Ring A I (J α)))
( λ α → product-radical-ideal-Commutative-Ring A I (J α)))
( I)
( λ α → product-radical-ideal-Commutative-Ring A I (J α)))
( I)
( I)
( A)
( I)
( J)))
( λ α → intersection-radical-ideal-Commutative-Ring A I (J α))
( λ α → product-radical-ideal-Commutative-Ring A I (J α))
( λ α →
( J α)))

( I)