Joins of ideals of rings

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

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

module ring-theory.joins-ideals-rings where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.unions-subtypes
open import foundation.universe-levels

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

open import ring-theory.ideals-generated-by-subsets-rings
open import ring-theory.ideals-rings
open import ring-theory.poset-of-ideals-rings
open import ring-theory.rings
open import ring-theory.subsets-rings

Idea

The join of a family of ideals of rings is the least ideal containing all the ideals in the family of ideals. In other words, the join of a family of ideals is the ideal generated by the union of the underlying subsets of the ideals in the family of ideals.

Definitions

The predicate of being the join of a family of ideals

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

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

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

  contains-ideal-is-join-family-of-ideals-Ring :
    {l4 : Level} (J : ideal-Ring l4 R) →
    is-join-family-of-ideals-Ring J →
    {α : U} → leq-ideal-Ring R (I α) J
  contains-ideal-is-join-family-of-ideals-Ring J H {α} =
    pr2 (H J) (refl-leq-ideal-Ring R J) α

The join of a family of ideals

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

  generating-subset-join-family-of-ideals-Ring :
    subset-Ring (l2 ⊔ l3) R
  generating-subset-join-family-of-ideals-Ring =
    union-family-of-subtypes (λ α → subset-ideal-Ring R (I α))

  join-family-of-ideals-Ring :
    ideal-Ring (l1 ⊔ l2 ⊔ l3) R
  join-family-of-ideals-Ring =
    ideal-family-of-subsets-Ring R (λ α → subset-ideal-Ring R (I α))

  forward-inclusion-is-join-join-family-of-ideals-Ring :
    {l4 : Level} (K : ideal-Ring l4 R) →
    ((α : U) → leq-ideal-Ring R (I α) K) →
    leq-ideal-Ring R join-family-of-ideals-Ring K
  forward-inclusion-is-join-join-family-of-ideals-Ring K H =
    is-ideal-generated-by-family-of-subsets-ideal-family-of-subsets-Ring R
      ( λ α → subset-ideal-Ring R (I α))
      ( K)
      ( λ {α} x → H α x)

  backward-inclusion-is-join-join-family-of-ideals-Ring :
    {l4 : Level} (K : ideal-Ring l4 R) →
    leq-ideal-Ring R join-family-of-ideals-Ring K →
    (α : U) → leq-ideal-Ring R (I α) K
  backward-inclusion-is-join-join-family-of-ideals-Ring K H _ x p =
    H ( x)
      ( contains-subset-ideal-family-of-subsets-Ring R
        ( λ α → subset-ideal-Ring R (I α))
        ( x)
        ( p))

  is-join-join-family-of-ideals-Ring :
    is-join-family-of-ideals-Ring R I join-family-of-ideals-Ring
  pr1 (is-join-join-family-of-ideals-Ring K) =
    forward-inclusion-is-join-join-family-of-ideals-Ring K
  pr2 (is-join-join-family-of-ideals-Ring K) =
    backward-inclusion-is-join-join-family-of-ideals-Ring K

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

  contains-ideal-join-family-of-ideals-Ring :
    {α : U} → leq-ideal-Ring R (I α) join-family-of-ideals-Ring
  contains-ideal-join-family-of-ideals-Ring =
    contains-ideal-is-join-family-of-ideals-Ring R I
      ( join-family-of-ideals-Ring)
      ( is-join-join-family-of-ideals-Ring)

The large suplattice of ideals in a ring

module _
  {l1 : Level} (R : Ring l1)
  where

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

  ideal-Ring-Large-Suplattice :
    Large-Suplattice (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3) l1
  large-poset-Large-Suplattice
    ideal-Ring-Large-Suplattice =
    ideal-Ring-Large-Poset R
  is-large-suplattice-Large-Suplattice
    ideal-Ring-Large-Suplattice =
    is-large-suplattice-ideal-Ring-Large-Poset

Properties

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

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

  preserves-order-join-family-of-ideals-Ring :
    leq-ideal-Ring A
      ( join-family-of-ideals-Ring A I)
      ( join-family-of-ideals-Ring A J)
  preserves-order-join-family-of-ideals-Ring =
    preserves-order-sup-Large-Suplattice
      ( ideal-Ring-Large-Suplattice A)
      { x = I}
      { y = J}
      ( H)

The operation S ↦ (S) preserves joins

module _
  {l1 l2 l3 : Level} (R : Ring l1) {U : UU l2} (S : U → subset-Ring l3 R)
  where

  is-least-upper-bound-join-ideal-subset-Ring :
    is-least-upper-bound-family-of-elements-Large-Poset
      ( ideal-Ring-Large-Poset R)
      ( λ α → ideal-subset-Ring R (S α))
      ( ideal-subset-Ring R (union-family-of-subtypes S))
  is-least-upper-bound-join-ideal-subset-Ring =
    preserves-least-upper-bounds-ideal-subset-Ring R S
      ( union-family-of-subtypes S)
      ( is-least-upper-bound-union-family-of-subtypes S)

  sim-preserves-join-ideal-subset-Ring :
    sim-ideal-Ring R
      ( ideal-subset-Ring R (union-family-of-subtypes S))
      ( join-family-of-ideals-Ring R (λ α → ideal-subset-Ring R (S α)))
  sim-preserves-join-ideal-subset-Ring =
    sim-is-least-upper-bound-family-of-elements-Large-Poset
      ( ideal-Ring-Large-Poset R)
      { x = λ α → ideal-subset-Ring R (S α)}
      { y = ideal-subset-Ring R (union-family-of-subtypes S)}
      { z = join-family-of-ideals-Ring R (λ α → ideal-subset-Ring R (S α))}
      ( is-least-upper-bound-join-ideal-subset-Ring)
      ( is-join-join-family-of-ideals-Ring R
        ( λ α → ideal-subset-Ring R (S α)))

  preserves-join-ideal-subset-Ring :
    ideal-subset-Ring R (union-family-of-subtypes S) ＝
    join-family-of-ideals-Ring R (λ α → ideal-subset-Ring R (S α))
  preserves-join-ideal-subset-Ring =
    eq-sim-Large-Poset
      ( ideal-Ring-Large-Poset R)
      ( ideal-subset-Ring R (union-family-of-subtypes S))
      ( join-family-of-ideals-Ring R (λ α → ideal-subset-Ring R (S α)))
      ( sim-preserves-join-ideal-subset-Ring)

Recent changes