Joins of right 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-right-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.poset-of-right-ideals-rings
open import ring-theory.right-ideals-generated-by-subsets-rings
open import ring-theory.right-ideals-rings
open import ring-theory.rings
open import ring-theory.subsets-rings

Idea

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

Definitions

The predicate of being the join of a family of right ideals

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

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

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

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

The join of a family of right ideals

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

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

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

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

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

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

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

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

The large suplattice of right ideals in a ring

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

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

  right-ideal-Ring-Large-Suplattice :
    Large-Suplattice (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3) l1
  large-poset-Large-Suplattice
    right-ideal-Ring-Large-Suplattice =
    right-ideal-Ring-Large-Poset R
  is-large-suplattice-Large-Suplattice
    right-ideal-Ring-Large-Suplattice =
    is-large-suplattice-right-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 → right-ideal-Ring l3 A)
  (J : U → right-ideal-Ring l4 A)
  (H : (α : U) → leq-right-ideal-Ring A (I α) (J α))
  where

  preserves-order-join-family-of-right-ideals-Ring :
    leq-right-ideal-Ring A
      ( join-family-of-right-ideals-Ring A I)
      ( join-family-of-right-ideals-Ring A J)
  preserves-order-join-family-of-right-ideals-Ring =
    preserves-order-sup-Large-Suplattice
      ( right-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-right-ideal-subset-Ring :
    is-least-upper-bound-family-of-elements-Large-Poset
      ( right-ideal-Ring-Large-Poset R)
      ( λ α → right-ideal-subset-Ring R (S α))
      ( right-ideal-subset-Ring R (union-family-of-subtypes S))
  is-least-upper-bound-join-right-ideal-subset-Ring =
    preserves-least-upper-bounds-right-ideal-subset-Ring R S
      ( union-family-of-subtypes S)
      ( is-least-upper-bound-union-family-of-subtypes S)

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

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

Recent changes