Joins of radical ideals of commutative rings

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

Created on 2023-06-08.
Last modified on 2023-06-10.

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.intersections-radical-ideals-commutative-rings
open import commutative-algebra.joins-ideals-commutative-rings
open import commutative-algebra.poset-of-radical-ideals-commutative-rings
open import commutative-algebra.products-ideals-commutative-rings
open import commutative-algebra.products-radical-ideals-commutative-rings
open import commutative-algebra.radical-ideals-commutative-rings
open import commutative-algebra.radical-ideals-generated-by-subsets-commutative-rings
open import commutative-algebra.radicals-of-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

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

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

  contains-ideal-is-join-family-of-radical-ideals-Commutative-Ring :
    {l4 : Level} (J : radical-ideal-Commutative-Ring l4 A) 
    is-join-family-of-radical-ideals-Commutative-Ring J 
    {α : U}  leq-radical-ideal-Commutative-Ring A (I α) J
  contains-ideal-is-join-family-of-radical-ideals-Commutative-Ring J H {α} =
    is-upper-bound-is-least-upper-bound-family-of-elements-Large-Poset
      ( radical-ideal-Commutative-Ring-Large-Poset A)
      { 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

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

  join-family-of-radical-ideals-Commutative-Ring :
    radical-ideal-Commutative-Ring (l1  l2  l3) A
  join-family-of-radical-ideals-Commutative-Ring =
    radical-ideal-subset-Commutative-Ring A
      generating-subset-join-family-of-radical-ideals-Commutative-Ring

  forward-inclusion-is-join-join-family-of-radical-ideals-Commutative-Ring :
    {l4 : Level} (K : radical-ideal-Commutative-Ring l4 A) 
    ((i : I)  leq-radical-ideal-Commutative-Ring A (J i) K) 
    leq-radical-ideal-Commutative-Ring A
      ( join-family-of-radical-ideals-Commutative-Ring)
      ( K)
  forward-inclusion-is-join-join-family-of-radical-ideals-Commutative-Ring
    K H =
    is-radical-of-ideal-radical-of-ideal-Commutative-Ring A
      ( 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 α))
        ( ideal-radical-ideal-Commutative-Ring A K)
        ( H))

  backward-inclusion-is-join-join-family-of-radical-ideals-Commutative-Ring :
    {l4 : Level} (K : radical-ideal-Commutative-Ring l4 A) 
    leq-radical-ideal-Commutative-Ring A
      ( join-family-of-radical-ideals-Commutative-Ring)
      ( K) 
    (i : I)  leq-radical-ideal-Commutative-Ring A (J i) K
  backward-inclusion-is-join-join-family-of-radical-ideals-Commutative-Ring
    K H i x p =
    H ( x)
      ( contains-ideal-radical-of-ideal-Commutative-Ring A
        ( 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)))

  is-join-join-family-of-radical-ideals-Commutative-Ring :
    is-join-family-of-radical-ideals-Commutative-Ring A J
      join-family-of-radical-ideals-Commutative-Ring
  pr1 (is-join-join-family-of-radical-ideals-Commutative-Ring K) =
    forward-inclusion-is-join-join-family-of-radical-ideals-Commutative-Ring K
  pr2 (is-join-join-family-of-radical-ideals-Commutative-Ring K) =
    backward-inclusion-is-join-join-family-of-radical-ideals-Commutative-Ring
      K

The large suplattice of radical ideals in a commutative ring

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

  is-large-suplattice-radical-ideal-Commutative-Ring :
    is-large-suplattice-Large-Poset l1
      ( radical-ideal-Commutative-Ring-Large-Poset A)
  sup-has-least-upper-bound-family-of-elements-Large-Poset
    ( is-large-suplattice-radical-ideal-Commutative-Ring I) =
    join-family-of-radical-ideals-Commutative-Ring A I
  is-least-upper-bound-sup-has-least-upper-bound-family-of-elements-Large-Poset
    ( is-large-suplattice-radical-ideal-Commutative-Ring I) =
    is-join-join-family-of-radical-ideals-Commutative-Ring A I

  radical-ideal-Commutative-Ring-Large-Suplattice :
    Large-Suplattice  l2  l1  lsuc l2)  l2 l3  l1  l2  l3) l1
  large-poset-Large-Suplattice
    radical-ideal-Commutative-Ring-Large-Suplattice =
    radical-ideal-Commutative-Ring-Large-Poset A
  is-large-suplattice-Large-Suplattice
    radical-ideal-Commutative-Ring-Large-Suplattice =
    is-large-suplattice-radical-ideal-Commutative-Ring

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-join-family-of-radical-ideals-Commutative-Ring :
    leq-radical-ideal-Commutative-Ring A
      ( join-family-of-radical-ideals-Commutative-Ring A I)
      ( join-family-of-radical-ideals-Commutative-Ring A J)
  preserves-order-join-family-of-radical-ideals-Commutative-Ring =
    preserves-order-sup-Large-Suplattice
      ( radical-ideal-Commutative-Ring-Large-Suplattice A)
      { 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

  forward-inclusion-radical-law-join-family-of-radical-ideals-Commutative-Ring :
    leq-radical-ideal-Commutative-Ring A
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  radical-of-ideal-Commutative-Ring A (I α)))
      ( radical-of-ideal-Commutative-Ring A
        ( join-family-of-ideals-Commutative-Ring A I))
  forward-inclusion-radical-law-join-family-of-radical-ideals-Commutative-Ring =
    is-radical-of-ideal-radical-of-ideal-Commutative-Ring A
      ( join-family-of-ideals-Commutative-Ring A
        ( λ α  ideal-radical-of-ideal-Commutative-Ring A (I α)))
      ( radical-of-ideal-Commutative-Ring A
        ( 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 α))
        ( ideal-radical-of-ideal-Commutative-Ring A
          ( join-family-of-ideals-Commutative-Ring A I))
        ( λ α 
          is-radical-of-ideal-radical-of-ideal-Commutative-Ring A
            ( I α)
            ( radical-of-ideal-Commutative-Ring A
              ( join-family-of-ideals-Commutative-Ring A I))
            ( λ x p 
              contains-ideal-radical-of-ideal-Commutative-Ring A
                ( join-family-of-ideals-Commutative-Ring A I)
                ( x)
                ( contains-ideal-join-family-of-ideals-Commutative-Ring
                  A I x p))))

  backward-inclusion-radical-law-join-family-of-radical-ideals-Commutative-Ring :
    leq-radical-ideal-Commutative-Ring A
      ( radical-of-ideal-Commutative-Ring A
        ( join-family-of-ideals-Commutative-Ring A I))
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  radical-of-ideal-Commutative-Ring A (I α)))
  backward-inclusion-radical-law-join-family-of-radical-ideals-Commutative-Ring =
    preserves-order-radical-of-ideal-Commutative-Ring A
      ( 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-law-join-family-of-radical-ideals-Commutative-Ring :
    join-family-of-radical-ideals-Commutative-Ring A
      ( λ α  radical-of-ideal-Commutative-Ring A (I α)) 
    radical-of-ideal-Commutative-Ring A
      ( join-family-of-ideals-Commutative-Ring A I)
  radical-law-join-family-of-radical-ideals-Commutative-Ring =
    antisymmetric-leq-radical-ideal-Commutative-Ring A
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  radical-of-ideal-Commutative-Ring A (I α)))
      ( radical-of-ideal-Commutative-Ring A
        ( join-family-of-ideals-Commutative-Ring A I))
      ( forward-inclusion-radical-law-join-family-of-radical-ideals-Commutative-Ring)
      ( backward-inclusion-radical-law-join-family-of-radical-ideals-Commutative-Ring)

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)
  (I : radical-ideal-Commutative-Ring l2 A)
  {U : UU l3} (J : U  radical-ideal-Commutative-Ring l4 A)
  where

  forward-inclusion-distributive-product-join-family-of-radical-ideals-Commutative-Ring :
    leq-radical-ideal-Commutative-Ring A
      ( product-radical-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-radical-ideals-Commutative-Ring A J))
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  product-radical-ideal-Commutative-Ring A I (J α)))
  forward-inclusion-distributive-product-join-family-of-radical-ideals-Commutative-Ring =
    transitive-leq-radical-ideal-Commutative-Ring A
      ( product-radical-ideal-Commutative-Ring A I
        ( join-family-of-radical-ideals-Commutative-Ring A J))
      ( radical-of-ideal-Commutative-Ring A
        ( product-ideal-Commutative-Ring A
          ( ideal-radical-ideal-Commutative-Ring A I)
          ( join-family-of-ideals-Commutative-Ring A
            ( λ α  ideal-radical-ideal-Commutative-Ring A (J α)))))
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  product-radical-ideal-Commutative-Ring A I (J α)))
      ( transitive-leq-radical-ideal-Commutative-Ring A
        ( radical-of-ideal-Commutative-Ring A
          ( product-ideal-Commutative-Ring A
            ( ideal-radical-ideal-Commutative-Ring A I)
            ( join-family-of-ideals-Commutative-Ring A
              ( λ α  ideal-radical-ideal-Commutative-Ring A (J α)))))
        ( radical-of-ideal-Commutative-Ring A
          ( join-family-of-ideals-Commutative-Ring A
            ( λ α 
              product-ideal-Commutative-Ring A
                ( ideal-radical-ideal-Commutative-Ring A I)
                ( ideal-radical-ideal-Commutative-Ring A (J α)))))
        ( join-family-of-radical-ideals-Commutative-Ring A
          ( λ α  product-radical-ideal-Commutative-Ring A I (J α)))
        ( backward-inclusion-radical-law-join-family-of-radical-ideals-Commutative-Ring
          ( A)
          ( λ α 
            product-ideal-Commutative-Ring A
              ( ideal-radical-ideal-Commutative-Ring A I)
              ( ideal-radical-ideal-Commutative-Ring A (J α))))
        ( preserves-order-radical-of-ideal-Commutative-Ring A
          ( product-ideal-Commutative-Ring A
            ( ideal-radical-ideal-Commutative-Ring 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
                ( ideal-radical-ideal-Commutative-Ring A I)
                ( ideal-radical-ideal-Commutative-Ring A (J α))))
          ( forward-inclusion-distributive-product-join-family-of-ideals-Commutative-Ring
            ( A)
            ( ideal-radical-ideal-Commutative-Ring A I)
            ( λ α  ideal-radical-ideal-Commutative-Ring A (J α)))))
      ( forward-inclusion-right-radical-law-product-radical-ideal-Commutative-Ring
        ( A)
        ( I)
        ( join-family-of-ideals-Commutative-Ring A
          ( λ α  ideal-radical-ideal-Commutative-Ring A (J α))))

  backward-inclusion-distributive-product-join-family-of-radical-ideals-Commutative-Ring :
    leq-radical-ideal-Commutative-Ring A
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  product-radical-ideal-Commutative-Ring A I (J α)))
      ( product-radical-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-radical-ideals-Commutative-Ring A J))
  backward-inclusion-distributive-product-join-family-of-radical-ideals-Commutative-Ring =
    transitive-leq-radical-ideal-Commutative-Ring A
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  product-radical-ideal-Commutative-Ring A I (J α)))
      ( radical-of-ideal-Commutative-Ring A
        ( join-family-of-ideals-Commutative-Ring A
          ( λ α 
            product-ideal-Commutative-Ring A
              ( ideal-radical-ideal-Commutative-Ring A I)
              ( ideal-radical-ideal-Commutative-Ring A (J α)))))
      ( product-radical-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-radical-ideals-Commutative-Ring A J))
      ( transitive-leq-radical-ideal-Commutative-Ring A
        ( radical-of-ideal-Commutative-Ring A
          ( join-family-of-ideals-Commutative-Ring A
            ( λ α 
              product-ideal-Commutative-Ring A
                ( ideal-radical-ideal-Commutative-Ring A I)
                ( ideal-radical-ideal-Commutative-Ring A (J α)))))
        ( radical-of-ideal-Commutative-Ring A
          ( product-ideal-Commutative-Ring A
            ( ideal-radical-ideal-Commutative-Ring A I)
            ( join-family-of-ideals-Commutative-Ring A
              ( λ α  ideal-radical-ideal-Commutative-Ring A (J α)))))
        ( product-radical-ideal-Commutative-Ring A
          ( I)
          ( join-family-of-radical-ideals-Commutative-Ring A J))
        ( backward-inclusion-right-radical-law-product-radical-ideal-Commutative-Ring
          ( A)
          ( I)
          ( join-family-of-ideals-Commutative-Ring A
            ( λ α  ideal-radical-ideal-Commutative-Ring A (J α))))
        ( preserves-order-radical-of-ideal-Commutative-Ring A
          ( join-family-of-ideals-Commutative-Ring A
            ( λ α 
              product-ideal-Commutative-Ring A
                ( ideal-radical-ideal-Commutative-Ring A I)
                ( ideal-radical-ideal-Commutative-Ring A (J α))))
          ( product-ideal-Commutative-Ring A
            ( ideal-radical-ideal-Commutative-Ring A I)
            ( 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 I)
            ( λ α  ideal-radical-ideal-Commutative-Ring A (J α)))))
      ( forward-inclusion-radical-law-join-family-of-radical-ideals-Commutative-Ring
        ( A)
        ( λ α 
          product-ideal-Commutative-Ring A
            ( ideal-radical-ideal-Commutative-Ring A I)
            ( ideal-radical-ideal-Commutative-Ring A (J α))))

  sim-distributive-product-join-family-of-radical-ideals-Commutative-Ring :
    sim-radical-ideal-Commutative-Ring A
      ( product-radical-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-radical-ideals-Commutative-Ring A J))
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  product-radical-ideal-Commutative-Ring A I (J α)))
  pr1 sim-distributive-product-join-family-of-radical-ideals-Commutative-Ring =
    forward-inclusion-distributive-product-join-family-of-radical-ideals-Commutative-Ring
  pr2 sim-distributive-product-join-family-of-radical-ideals-Commutative-Ring =
    backward-inclusion-distributive-product-join-family-of-radical-ideals-Commutative-Ring

  distributive-product-join-family-of-radical-ideals-Commutative-Ring :
    product-radical-ideal-Commutative-Ring A
      ( I)
      ( join-family-of-radical-ideals-Commutative-Ring A J) 
    join-family-of-radical-ideals-Commutative-Ring A
      ( λ α  product-radical-ideal-Commutative-Ring A I (J α))
  distributive-product-join-family-of-radical-ideals-Commutative-Ring =
    antisymmetric-leq-radical-ideal-Commutative-Ring A
      ( product-radical-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-radical-ideals-Commutative-Ring A J))
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  product-radical-ideal-Commutative-Ring A I (J α)))
      ( forward-inclusion-distributive-product-join-family-of-radical-ideals-Commutative-Ring)
      ( backward-inclusion-distributive-product-join-family-of-radical-ideals-Commutative-Ring)

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)
  (I : radical-ideal-Commutative-Ring l2 A)
  {U : UU l3} (J : U  radical-ideal-Commutative-Ring l4 A)
  where

  forward-inclusion-distributive-intersection-join-family-of-radical-ideals-Commutative-Ring :
    leq-radical-ideal-Commutative-Ring A
      ( intersection-radical-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-radical-ideals-Commutative-Ring A J))
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  intersection-radical-ideal-Commutative-Ring A I (J α)))
  forward-inclusion-distributive-intersection-join-family-of-radical-ideals-Commutative-Ring =
    transitive-leq-radical-ideal-Commutative-Ring A
      ( intersection-radical-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-radical-ideals-Commutative-Ring A J))
      ( product-radical-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-radical-ideals-Commutative-Ring A J))
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  intersection-radical-ideal-Commutative-Ring A I (J α)))
      ( transitive-leq-radical-ideal-Commutative-Ring A
        ( product-radical-ideal-Commutative-Ring A
          ( I)
          ( join-family-of-radical-ideals-Commutative-Ring A J))
        ( join-family-of-radical-ideals-Commutative-Ring A
          ( λ α  product-radical-ideal-Commutative-Ring A I (J α)))
        ( join-family-of-radical-ideals-Commutative-Ring A
          ( λ α  intersection-radical-ideal-Commutative-Ring A I (J α)))
        ( preserves-order-join-family-of-radical-ideals-Commutative-Ring A
          ( λ α  product-radical-ideal-Commutative-Ring A I (J α))
          ( λ α  intersection-radical-ideal-Commutative-Ring A I (J α))
          ( λ α 
            backward-inclusion-intersection-radical-ideal-Commutative-Ring A I
              ( J α)))
        ( forward-inclusion-distributive-product-join-family-of-radical-ideals-Commutative-Ring
          ( A)
          ( I)
          ( J)))
      ( forward-inclusion-intersection-radical-ideal-Commutative-Ring A I
        ( join-family-of-radical-ideals-Commutative-Ring A J))

  backward-inclusion-distributive-intersection-join-family-of-radical-ideals-Commutative-Ring :
    leq-radical-ideal-Commutative-Ring A
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  intersection-radical-ideal-Commutative-Ring A I (J α)))
      ( intersection-radical-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-radical-ideals-Commutative-Ring A J))
  backward-inclusion-distributive-intersection-join-family-of-radical-ideals-Commutative-Ring =
    transitive-leq-radical-ideal-Commutative-Ring A
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  intersection-radical-ideal-Commutative-Ring A I (J α)))
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  product-radical-ideal-Commutative-Ring A I (J α)))
      ( intersection-radical-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-radical-ideals-Commutative-Ring A J))
      ( transitive-leq-radical-ideal-Commutative-Ring A
        ( join-family-of-radical-ideals-Commutative-Ring A
          ( λ α  product-radical-ideal-Commutative-Ring A I (J α)))
        ( product-radical-ideal-Commutative-Ring A
          ( I)
          ( join-family-of-radical-ideals-Commutative-Ring A J))
        ( intersection-radical-ideal-Commutative-Ring A
          ( I)
          ( join-family-of-radical-ideals-Commutative-Ring A J))
        ( backward-inclusion-intersection-radical-ideal-Commutative-Ring A I
          ( join-family-of-radical-ideals-Commutative-Ring A J))
        ( backward-inclusion-distributive-product-join-family-of-radical-ideals-Commutative-Ring
          ( A)
          ( I)
          ( J)))
      ( preserves-order-join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  intersection-radical-ideal-Commutative-Ring A I (J α))
        ( λ α  product-radical-ideal-Commutative-Ring A I (J α))
        ( λ α 
          forward-inclusion-intersection-radical-ideal-Commutative-Ring A I
            ( J α)))

  distributive-intersection-join-family-of-radical-ideals-Commutative-Ring :
    intersection-radical-ideal-Commutative-Ring A
      ( I)
      ( join-family-of-radical-ideals-Commutative-Ring A J) 
    join-family-of-radical-ideals-Commutative-Ring A
      ( λ α  intersection-radical-ideal-Commutative-Ring A I (J α))
  distributive-intersection-join-family-of-radical-ideals-Commutative-Ring =
    antisymmetric-leq-radical-ideal-Commutative-Ring A
      ( intersection-radical-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-radical-ideals-Commutative-Ring A J))
      ( join-family-of-radical-ideals-Commutative-Ring A
        ( λ α  intersection-radical-ideal-Commutative-Ring A I (J α)))
      ( forward-inclusion-distributive-intersection-join-family-of-radical-ideals-Commutative-Ring)
      ( backward-inclusion-distributive-intersection-join-family-of-radical-ideals-Commutative-Ring)

Recent changes