Joins of ideals of commutative rings

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

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

module commutative-algebra.joins-ideals-commutative-rings where
Imports 
open import commutative-algebra.commutative-rings
open import commutative-algebra.ideals-commutative-rings
open import commutative-algebra.ideals-generated-by-subsets-commutative-rings
open import commutative-algebra.poset-of-ideals-commutative-rings
open import commutative-algebra.products-ideals-commutative-rings
open import commutative-algebra.products-subsets-commutative-rings
open import commutative-algebra.subsets-commutative-rings

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.subtypes
open import foundation.unions-subtypes
open import foundation.universe-levels

open import ring-theory.joins-ideals-rings

Idea

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

Definition

The universal property of the join of a family of ideals

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

  is-join-family-of-ideals-Commutative-Ring :
    {l4 : Level} (K : ideal-Commutative-Ring l4 A) → UUω
  is-join-family-of-ideals-Commutative-Ring =
    is-join-family-of-ideals-Ring (ring-Commutative-Ring A) I

  inclusion-is-join-family-of-ideals-Commutative-Ring :
    {l4 l5 : Level} (J : ideal-Commutative-Ring l4 A) →
    is-join-family-of-ideals-Commutative-Ring J →
    (K : ideal-Commutative-Ring l5 A) →
    ((α : U) → leq-ideal-Commutative-Ring A (I α) K) →
    leq-ideal-Commutative-Ring A J K
  inclusion-is-join-family-of-ideals-Commutative-Ring =
    inclusion-is-join-family-of-ideals-Ring (ring-Commutative-Ring A) I

  contains-ideal-is-join-family-of-ideals-Commutative-Ring :
    {l4 : Level} (J : ideal-Commutative-Ring l4 A) →
    is-join-family-of-ideals-Commutative-Ring J →
    {α : U} → leq-ideal-Commutative-Ring A (I α) J
  contains-ideal-is-join-family-of-ideals-Commutative-Ring =
    contains-ideal-is-join-family-of-ideals-Ring (ring-Commutative-Ring A) I

The join of a family of ideals

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

  generating-subset-join-family-of-ideals-Commutative-Ring :
    subset-Commutative-Ring (l2 ⊔ l3) A
  generating-subset-join-family-of-ideals-Commutative-Ring =
    generating-subset-join-family-of-ideals-Ring
      ( ring-Commutative-Ring A)
      ( I)

  join-family-of-ideals-Commutative-Ring :
    ideal-Commutative-Ring (l1 ⊔ l2 ⊔ l3) A
  join-family-of-ideals-Commutative-Ring =
    join-family-of-ideals-Ring (ring-Commutative-Ring A) I

  forward-inclusion-is-join-join-family-of-ideals-Commutative-Ring :
    {l4 : Level} (K : ideal-Commutative-Ring l4 A) →
    ((α : U) → leq-ideal-Commutative-Ring A (I α) K) →
    leq-ideal-Commutative-Ring A join-family-of-ideals-Commutative-Ring K
  forward-inclusion-is-join-join-family-of-ideals-Commutative-Ring =
    forward-inclusion-is-join-join-family-of-ideals-Ring
      ( ring-Commutative-Ring A)
      ( I)

  backward-inclusion-is-join-join-family-of-ideals-Commutative-Ring :
    {l4 : Level} (K : ideal-Commutative-Ring l4 A) →
    leq-ideal-Commutative-Ring A join-family-of-ideals-Commutative-Ring K →
    (α : U) → leq-ideal-Commutative-Ring A (I α) K
  backward-inclusion-is-join-join-family-of-ideals-Commutative-Ring =
    backward-inclusion-is-join-join-family-of-ideals-Ring
      ( ring-Commutative-Ring A)
      ( I)

  is-join-join-family-of-ideals-Commutative-Ring :
    is-join-family-of-ideals-Commutative-Ring A I
      join-family-of-ideals-Commutative-Ring
  is-join-join-family-of-ideals-Commutative-Ring =
    is-join-join-family-of-ideals-Ring (ring-Commutative-Ring A) I

  inclusion-join-family-of-ideals-Commutative-Ring :
    {l4 : Level} (J : ideal-Commutative-Ring l4 A) →
    ((α : U) → leq-ideal-Commutative-Ring A (I α) J) →
    leq-ideal-Commutative-Ring A join-family-of-ideals-Commutative-Ring J
  inclusion-join-family-of-ideals-Commutative-Ring =
    inclusion-join-family-of-ideals-Ring (ring-Commutative-Ring A) I

  contains-ideal-join-family-of-ideals-Commutative-Ring :
    {α : U} →
    leq-ideal-Commutative-Ring A (I α) join-family-of-ideals-Commutative-Ring
  contains-ideal-join-family-of-ideals-Commutative-Ring =
    contains-ideal-join-family-of-ideals-Ring (ring-Commutative-Ring A) I

Properties

If I α ⊆ J α for each α, then ⋁ I ⊆ ⋁ J

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

  preserves-order-join-family-of-ideals-Commutative-Ring :
    leq-ideal-Commutative-Ring A
      ( join-family-of-ideals-Commutative-Ring A I)
      ( join-family-of-ideals-Commutative-Ring A J)
  preserves-order-join-family-of-ideals-Commutative-Ring =
    preserves-order-join-family-of-ideals-Ring
      ( ring-Commutative-Ring A)
      ( I)
      ( J)
      ( H)

Products distribute over joins of families of ideals

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

  forward-inclusion-distributive-product-join-family-of-ideals-Commutative-Ring :
    leq-ideal-Commutative-Ring A
      ( product-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-ideals-Commutative-Ring A J))
      ( join-family-of-ideals-Commutative-Ring A
        ( λ α →
          product-ideal-Commutative-Ring A I (J α)))
  forward-inclusion-distributive-product-join-family-of-ideals-Commutative-Ring
    x p =
    preserves-order-ideal-subset-Commutative-Ring A
      ( product-subset-Commutative-Ring A
        ( subset-ideal-Commutative-Ring A I)
        ( union-family-of-subtypes
          ( λ α → subset-ideal-Commutative-Ring A (J α))))
      ( generating-subset-join-family-of-ideals-Commutative-Ring A
        ( λ α → product-ideal-Commutative-Ring A I (J α)))
      ( transitive-leq-subtype
        ( product-subset-Commutative-Ring A
          ( subset-ideal-Commutative-Ring A I)
          ( union-family-of-subtypes
            ( λ α → subset-ideal-Commutative-Ring A (J α))))
        ( union-family-of-subtypes
          ( λ α →
            generating-subset-product-ideal-Commutative-Ring A I (J α)))
        ( generating-subset-join-family-of-ideals-Commutative-Ring A
          ( λ α → product-ideal-Commutative-Ring A I (J α)))
        ( preserves-order-union-family-of-subtypes
          ( λ α → generating-subset-product-ideal-Commutative-Ring A I (J α))
          ( λ α → subset-product-ideal-Commutative-Ring A I (J α))
          ( λ α →
            contains-subset-ideal-subset-Commutative-Ring A
              ( generating-subset-product-ideal-Commutative-Ring A I (J α))))
        ( forward-inclusion-distributive-product-union-family-of-subsets-Commutative-Ring
          ( A)
          ( subset-ideal-Commutative-Ring A I)
          ( λ α → subset-ideal-Commutative-Ring A (J α))))
      ( x)
      ( backward-inclusion-right-preserves-product-ideal-subset-Commutative-Ring
        ( A)
        ( I)
        ( generating-subset-join-family-of-ideals-Commutative-Ring A J)
        ( x)
        ( p))

  backward-inclusion-distributive-product-join-family-of-ideals-Commutative-Ring :
    leq-ideal-Commutative-Ring A
      ( join-family-of-ideals-Commutative-Ring A
        ( λ α →
          product-ideal-Commutative-Ring A I (J α)))
      ( product-ideal-Commutative-Ring A
        ( I)
        ( join-family-of-ideals-Commutative-Ring A J))
  backward-inclusion-distributive-product-join-family-of-ideals-Commutative-Ring
    =
    forward-implication
      ( is-join-join-family-of-ideals-Commutative-Ring A
        ( λ α → product-ideal-Commutative-Ring A I (J α))
        ( product-ideal-Commutative-Ring A I
          ( join-family-of-ideals-Commutative-Ring A J)))
      ( λ α →
        preserves-order-right-product-ideal-Commutative-Ring A I
          ( J α)
          ( join-family-of-ideals-Commutative-Ring A J)
          ( contains-ideal-join-family-of-ideals-Commutative-Ring A J))

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

  distributive-product-join-family-of-ideals-Commutative-Ring :
    product-ideal-Commutative-Ring A I
      ( join-family-of-ideals-Commutative-Ring A J) ＝
    join-family-of-ideals-Commutative-Ring A
      ( λ α → product-ideal-Commutative-Ring A I (J α))
  distributive-product-join-family-of-ideals-Commutative-Ring =
    eq-sim-ideal-Commutative-Ring A
      ( product-ideal-Commutative-Ring A I
        ( join-family-of-ideals-Commutative-Ring A J))
      ( join-family-of-ideals-Commutative-Ring A
        ( λ α → product-ideal-Commutative-Ring A I (J α)))
      ( sim-distributive-product-join-family-of-ideals-Commutative-Ring)

Recent changes