Left ideals generated by subsets of rings

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

Created on 2023-06-08.
Last modified on 2024-11-20.

module ring-theory.left-ideals-generated-by-subsets-rings where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.powersets
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.unions-subtypes
open import foundation.universe-levels

open import lists.concatenation-lists
open import lists.functoriality-lists
open import lists.lists

open import order-theory.galois-connections-large-posets
open import order-theory.least-upper-bounds-large-posets
open import order-theory.order-preserving-maps-large-posets
open import order-theory.order-preserving-maps-large-preorders
open import order-theory.reflective-galois-connections-large-posets

open import ring-theory.left-ideals-rings
open import ring-theory.poset-of-left-ideals-rings
open import ring-theory.rings
open import ring-theory.subsets-rings

Idea

The left ideal generated by a subset S of a ring R is the least left ideal in R containing S.

Definitions

The universal property of left ideals generated by a subset of a ring

module _
  {l1 l2 l3 : Level} (R : Ring l1) (S : subset-Ring l2 R)
  (I : left-ideal-Ring l3 R) (H : S ⊆ subset-left-ideal-Ring R I)
  where

  is-left-ideal-generated-by-subset-Ring : UUω
  is-left-ideal-generated-by-subset-Ring =
    {l : Level} (J : left-ideal-Ring l R) →
    S ⊆ subset-left-ideal-Ring R J →
    subset-left-ideal-Ring R I ⊆ subset-left-ideal-Ring R J

The universal property of left ideals generated by a family of subsets of a ring

module _
  {l1 l2 l3 l4 : Level} (R : Ring l1) {U : UU l2} (S : U → subset-Ring l3 R)
  (I : left-ideal-Ring l4 R) (H : (α : U) → S α ⊆ subset-left-ideal-Ring R I)
  where

  is-left-ideal-generated-by-family-of-subsets-Ring : UUω
  is-left-ideal-generated-by-family-of-subsets-Ring =
    {l : Level} (J : left-ideal-Ring l R) →
    ((α : U) → S α ⊆ subset-left-ideal-Ring R J) →
    leq-left-ideal-Ring R I J

The universal property of left ideals generated by a family of elements in a ring

module _
  {l1 l2 l3 : Level} (R : Ring l1) {U : UU l2} (a : U → type-Ring R)
  (I : left-ideal-Ring l3 R) (H : (α : U) → is-in-left-ideal-Ring R I (a α))
  where

  is-left-ideal-generated-by-family-of-elements-Ring : UUω
  is-left-ideal-generated-by-family-of-elements-Ring =
    {l : Level} (J : left-ideal-Ring l R) →
    ((α : U) → is-in-left-ideal-Ring R J (a α)) →
    leq-left-ideal-Ring R I J

Construction of the Galois connection of left ideals generated by subsets

Left ideals generated by subsets

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

  left-formal-combination-subset-Ring : UU (l1 ⊔ l2)
  left-formal-combination-subset-Ring =
    list (type-Ring R × type-subset-Ring R S)

  ev-left-formal-combination-subset-Ring :
    left-formal-combination-subset-Ring → type-Ring R
  ev-left-formal-combination-subset-Ring nil = zero-Ring R
  ev-left-formal-combination-subset-Ring (cons (pair r s) l) =
    add-Ring R
      ( mul-Ring R r (inclusion-subset-Ring R S s))
      ( ev-left-formal-combination-subset-Ring l)

  preserves-concat-ev-left-formal-combination-subset-Ring :
    (u v : left-formal-combination-subset-Ring) →
    ev-left-formal-combination-subset-Ring (concat-list u v) ＝
    add-Ring R
      ( ev-left-formal-combination-subset-Ring u)
      ( ev-left-formal-combination-subset-Ring v)
  preserves-concat-ev-left-formal-combination-subset-Ring nil v =
    inv (left-unit-law-add-Ring R (ev-left-formal-combination-subset-Ring v))
  preserves-concat-ev-left-formal-combination-subset-Ring
    ( cons (pair r s) u) v =
    ( ap
      ( add-Ring R (mul-Ring R r (inclusion-subset-Ring R S s)))
      ( preserves-concat-ev-left-formal-combination-subset-Ring u v)) ∙
    ( inv
      ( associative-add-Ring R
        ( mul-Ring R r (inclusion-subset-Ring R S s))
        ( ev-left-formal-combination-subset-Ring u)
        ( ev-left-formal-combination-subset-Ring v)))

  mul-left-formal-combination-subset-Ring :
    type-Ring R →
    left-formal-combination-subset-Ring → left-formal-combination-subset-Ring
  mul-left-formal-combination-subset-Ring r =
    map-list (λ x → pair (mul-Ring R r (pr1 x)) (pr2 x))

  preserves-mul-ev-left-formal-combination-subset-Ring :
    (r : type-Ring R) (u : left-formal-combination-subset-Ring) →
    ev-left-formal-combination-subset-Ring
      ( mul-left-formal-combination-subset-Ring r u) ＝
    mul-Ring R r (ev-left-formal-combination-subset-Ring u)
  preserves-mul-ev-left-formal-combination-subset-Ring r nil =
    inv (right-zero-law-mul-Ring R r)
  preserves-mul-ev-left-formal-combination-subset-Ring r (cons x u) =
    ( ap-add-Ring R
      ( associative-mul-Ring R r (pr1 x) (inclusion-subset-Ring R S (pr2 x)))
      ( preserves-mul-ev-left-formal-combination-subset-Ring r u)) ∙
    ( inv
      ( left-distributive-mul-add-Ring R r
        ( mul-Ring R (pr1 x) (inclusion-subset-Ring R S (pr2 x)))
        ( ev-left-formal-combination-subset-Ring u)))

  subset-left-ideal-subset-Ring' : type-Ring R → UU (l1 ⊔ l2)
  subset-left-ideal-subset-Ring' x =
    fiber ev-left-formal-combination-subset-Ring x

  subset-left-ideal-subset-Ring : subset-Ring (l1 ⊔ l2) R
  subset-left-ideal-subset-Ring x =
    trunc-Prop (subset-left-ideal-subset-Ring' x)

  is-in-left-ideal-subset-Ring : type-Ring R → UU (l1 ⊔ l2)
  is-in-left-ideal-subset-Ring = is-in-subtype subset-left-ideal-subset-Ring

  contains-zero-left-ideal-subset-Ring :
    contains-zero-subset-Ring R subset-left-ideal-subset-Ring
  contains-zero-left-ideal-subset-Ring = unit-trunc-Prop (pair nil refl)

  is-closed-under-addition-left-ideal-subset-Ring' :
    (x y : type-Ring R) →
    subset-left-ideal-subset-Ring' x → subset-left-ideal-subset-Ring' y →
    subset-left-ideal-subset-Ring' (add-Ring R x y)
  pr1
    ( is-closed-under-addition-left-ideal-subset-Ring' x y
      ( pair l p) (pair k q)) =
    concat-list l k
  pr2
    ( is-closed-under-addition-left-ideal-subset-Ring' x y
      ( pair l p) (pair k q)) =
    ( preserves-concat-ev-left-formal-combination-subset-Ring l k) ∙
    ( ap-add-Ring R p q)

  is-closed-under-addition-left-ideal-subset-Ring :
    is-closed-under-addition-subset-Ring R subset-left-ideal-subset-Ring
  is-closed-under-addition-left-ideal-subset-Ring {x} {y} H K =
    apply-universal-property-trunc-Prop H
      ( subset-left-ideal-subset-Ring (add-Ring R x y))
      ( λ H' →
        apply-universal-property-trunc-Prop K
          ( subset-left-ideal-subset-Ring (add-Ring R x y))
          ( λ K' →
            unit-trunc-Prop
              ( is-closed-under-addition-left-ideal-subset-Ring' x y H' K')))

  is-closed-under-left-multiplication-left-ideal-subset-Ring' :
    (r x : type-Ring R) → subset-left-ideal-subset-Ring' x →
    subset-left-ideal-subset-Ring' (mul-Ring R r x)
  pr1
    ( is-closed-under-left-multiplication-left-ideal-subset-Ring' r x
      ( pair l p)) =
    mul-left-formal-combination-subset-Ring r l
  pr2
    ( is-closed-under-left-multiplication-left-ideal-subset-Ring' r x
      ( pair l p)) =
    ( preserves-mul-ev-left-formal-combination-subset-Ring r l) ∙
    ( ap (mul-Ring R r) p)

  is-closed-under-left-multiplication-left-ideal-subset-Ring :
    is-closed-under-left-multiplication-subset-Ring R
      subset-left-ideal-subset-Ring
  is-closed-under-left-multiplication-left-ideal-subset-Ring r x H =
    apply-universal-property-trunc-Prop H
      ( subset-left-ideal-subset-Ring (mul-Ring R r x))
      ( λ H' →
        unit-trunc-Prop
          ( is-closed-under-left-multiplication-left-ideal-subset-Ring' r x H'))

  is-closed-under-negatives-left-ideal-subset-Ring :
    is-closed-under-negatives-subset-Ring R subset-left-ideal-subset-Ring
  is-closed-under-negatives-left-ideal-subset-Ring {x} H =
    tr
      ( type-Prop ∘ subset-left-ideal-subset-Ring)
      ( mul-neg-one-Ring R x)
      ( is-closed-under-left-multiplication-left-ideal-subset-Ring
        ( neg-one-Ring R)
        ( x)
        ( H))

  left-ideal-subset-Ring : left-ideal-Ring (l1 ⊔ l2) R
  pr1 left-ideal-subset-Ring = subset-left-ideal-subset-Ring
  pr1 (pr1 (pr2 left-ideal-subset-Ring)) = contains-zero-left-ideal-subset-Ring
  pr1 (pr2 (pr1 (pr2 left-ideal-subset-Ring))) =
    is-closed-under-addition-left-ideal-subset-Ring
  pr2 (pr2 (pr1 (pr2 left-ideal-subset-Ring))) =
    is-closed-under-negatives-left-ideal-subset-Ring
  pr2 (pr2 left-ideal-subset-Ring) =
    is-closed-under-left-multiplication-left-ideal-subset-Ring

  contains-subset-left-ideal-subset-Ring :
    S ⊆ subset-left-ideal-subset-Ring
  contains-subset-left-ideal-subset-Ring s H =
    unit-trunc-Prop
      ( pair
        ( cons (pair (one-Ring R) (pair s H)) nil)
        ( ( right-unit-law-add-Ring R (mul-Ring R (one-Ring R) s)) ∙
          ( left-unit-law-mul-Ring R s)))

  contains-left-formal-combinations-left-ideal-subset-Ring :
    {l3 : Level} (I : left-ideal-Ring l3 R) → S ⊆ subset-left-ideal-Ring R I →
    (x : left-formal-combination-subset-Ring) →
    is-in-left-ideal-Ring R I (ev-left-formal-combination-subset-Ring x)
  contains-left-formal-combinations-left-ideal-subset-Ring I H nil =
    contains-zero-left-ideal-Ring R I
  contains-left-formal-combinations-left-ideal-subset-Ring I H
    ( cons (pair r (pair s K)) c) =
    is-closed-under-addition-left-ideal-Ring R I
      ( is-closed-under-left-multiplication-left-ideal-Ring R I r s (H s K))
      ( contains-left-formal-combinations-left-ideal-subset-Ring I H c)

  is-left-ideal-generated-by-subset-left-ideal-subset-Ring :
    is-left-ideal-generated-by-subset-Ring R S
      ( left-ideal-subset-Ring)
      ( contains-subset-left-ideal-subset-Ring)
  is-left-ideal-generated-by-subset-left-ideal-subset-Ring {l} J K x H =
    apply-universal-property-trunc-Prop H (subset-left-ideal-Ring R J x) P
    where
    P : subset-left-ideal-subset-Ring' x → is-in-left-ideal-Ring R J x
    P (pair c refl) =
      contains-left-formal-combinations-left-ideal-subset-Ring J K c

  is-closed-under-eq-left-ideal-subset-Ring :
    {x y : type-Ring R} → is-in-left-ideal-subset-Ring x →
    (x ＝ y) → is-in-left-ideal-subset-Ring y
  is-closed-under-eq-left-ideal-subset-Ring =
    is-closed-under-eq-left-ideal-Ring R left-ideal-subset-Ring

  is-closed-under-eq-left-ideal-subset-Ring' :
    {x y : type-Ring R} → is-in-left-ideal-subset-Ring y →
    (x ＝ y) → is-in-left-ideal-subset-Ring x
  is-closed-under-eq-left-ideal-subset-Ring' =
    is-closed-under-eq-left-ideal-Ring' R left-ideal-subset-Ring

The subset relation is preserved by generating left ideals

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

  preserves-order-left-ideal-subset-Ring :
    {l2 l3 : Level} (S : subset-Ring l2 A) (T : subset-Ring l3 A) →
    S ⊆ T →
    leq-left-ideal-Ring A
      ( left-ideal-subset-Ring A S)
      ( left-ideal-subset-Ring A T)
  preserves-order-left-ideal-subset-Ring S T H =
    is-left-ideal-generated-by-subset-left-ideal-subset-Ring A S
      ( left-ideal-subset-Ring A T)
      ( transitive-leq-subtype S T
        ( subset-left-ideal-subset-Ring A T)
        ( contains-subset-left-ideal-subset-Ring A T)
        ( H))

  left-ideal-subset-hom-large-poset-Ring :
    hom-Large-Poset
      ( λ l2 → l1 ⊔ l2)
      ( powerset-Large-Poset (type-Ring A))
      ( left-ideal-Ring-Large-Poset A)
  map-hom-Large-Preorder left-ideal-subset-hom-large-poset-Ring =
    left-ideal-subset-Ring A
  preserves-order-hom-Large-Preorder left-ideal-subset-hom-large-poset-Ring =
    preserves-order-left-ideal-subset-Ring

The Galois connection S ↦ (S)

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

  adjoint-relation-left-ideal-subset-Ring :
    {l2 l3 : Level} (S : subset-Ring l2 A) (I : left-ideal-Ring l3 A) →
    leq-left-ideal-Ring A (left-ideal-subset-Ring A S) I ↔
    (S ⊆ subset-left-ideal-Ring A I)
  pr1 (adjoint-relation-left-ideal-subset-Ring S I) H =
    transitive-leq-subtype S
      ( subset-left-ideal-subset-Ring A S)
      ( subset-left-ideal-Ring A I)
      ( H)
      ( contains-subset-left-ideal-subset-Ring A S)
  pr2 (adjoint-relation-left-ideal-subset-Ring S I) =
    is-left-ideal-generated-by-subset-left-ideal-subset-Ring A S I

  left-ideal-subset-galois-connection-Ring :
    galois-connection-Large-Poset
      ( l1 ⊔_) (λ l → l)
      ( powerset-Large-Poset (type-Ring A))
      ( left-ideal-Ring-Large-Poset A)
  lower-adjoint-galois-connection-Large-Poset
    left-ideal-subset-galois-connection-Ring =
    left-ideal-subset-hom-large-poset-Ring A
  upper-adjoint-galois-connection-Large-Poset
    left-ideal-subset-galois-connection-Ring =
    subset-left-ideal-hom-large-poset-Ring A
  adjoint-relation-galois-connection-Large-Poset
    left-ideal-subset-galois-connection-Ring =
    adjoint-relation-left-ideal-subset-Ring

The reflective Galois connection S ↦ (S)

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

  forward-inclusion-is-reflective-left-ideal-subset-galois-connection-Ring :
    {l2 : Level} (I : left-ideal-Ring l2 A) →
    leq-left-ideal-Ring A
      ( left-ideal-subset-Ring A (subset-left-ideal-Ring A I))
      ( I)
  forward-inclusion-is-reflective-left-ideal-subset-galois-connection-Ring I =
    is-left-ideal-generated-by-subset-left-ideal-subset-Ring A
      ( subset-left-ideal-Ring A I)
      ( I)
      ( refl-leq-left-ideal-Ring A I)

  backward-inclusion-is-reflective-left-ideal-subset-galois-connection-Ring :
    {l2 : Level} (I : left-ideal-Ring l2 A) →
    leq-left-ideal-Ring A I
      ( left-ideal-subset-Ring A (subset-left-ideal-Ring A I))
  backward-inclusion-is-reflective-left-ideal-subset-galois-connection-Ring I =
    contains-subset-left-ideal-subset-Ring A (subset-left-ideal-Ring A I)

  is-reflective-left-ideal-subset-galois-connection-Ring :
    is-reflective-galois-connection-Large-Poset
      ( powerset-Large-Poset (type-Ring A))
      ( left-ideal-Ring-Large-Poset A)
      ( left-ideal-subset-galois-connection-Ring A)
  pr1 (is-reflective-left-ideal-subset-galois-connection-Ring I) =
    forward-inclusion-is-reflective-left-ideal-subset-galois-connection-Ring I
  pr2 (is-reflective-left-ideal-subset-galois-connection-Ring I) =
    backward-inclusion-is-reflective-left-ideal-subset-galois-connection-Ring I

  left-ideal-subset-reflective-galois-connection-Ring :
    reflective-galois-connection-Large-Poset
      ( powerset-Large-Poset (type-Ring A))
      ( left-ideal-Ring-Large-Poset A)
  galois-connection-reflective-galois-connection-Large-Poset
    left-ideal-subset-reflective-galois-connection-Ring =
    left-ideal-subset-galois-connection-Ring A
  is-reflective-reflective-galois-connection-Large-Poset
    left-ideal-subset-reflective-galois-connection-Ring =
    is-reflective-left-ideal-subset-galois-connection-Ring

The left ideal generated by a family of subsets of a ring

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

  generating-subset-left-ideal-family-of-subsets-Ring :
    subset-Ring (l2 ⊔ l3) R
  generating-subset-left-ideal-family-of-subsets-Ring x =
    union-family-of-subtypes S x

  left-ideal-family-of-subsets-Ring : left-ideal-Ring (l1 ⊔ l2 ⊔ l3) R
  left-ideal-family-of-subsets-Ring =
    left-ideal-subset-Ring R generating-subset-left-ideal-family-of-subsets-Ring

  subset-left-ideal-family-of-subsets-Ring : subset-Ring (l1 ⊔ l2 ⊔ l3) R
  subset-left-ideal-family-of-subsets-Ring =
    subset-left-ideal-subset-Ring R
      generating-subset-left-ideal-family-of-subsets-Ring

  is-in-left-ideal-family-of-subsets-Ring : type-Ring R → UU (l1 ⊔ l2 ⊔ l3)
  is-in-left-ideal-family-of-subsets-Ring =
    is-in-left-ideal-subset-Ring R
      generating-subset-left-ideal-family-of-subsets-Ring

  contains-subset-left-ideal-family-of-subsets-Ring :
    {α : U} → (S α) ⊆ subset-left-ideal-family-of-subsets-Ring
  contains-subset-left-ideal-family-of-subsets-Ring {α} x H =
    contains-subset-left-ideal-subset-Ring R
      ( generating-subset-left-ideal-family-of-subsets-Ring)
      ( x)
      ( unit-trunc-Prop (α , H))

  is-left-ideal-generated-by-family-of-subsets-left-ideal-family-of-subsets-Ring :
    is-left-ideal-generated-by-family-of-subsets-Ring R S
      ( left-ideal-family-of-subsets-Ring)
      ( λ α → contains-subset-left-ideal-family-of-subsets-Ring)
  is-left-ideal-generated-by-family-of-subsets-left-ideal-family-of-subsets-Ring
    J H =
    is-left-ideal-generated-by-subset-left-ideal-subset-Ring R
      ( generating-subset-left-ideal-family-of-subsets-Ring)
      ( J)
      ( λ y q →
        apply-universal-property-trunc-Prop q
          ( subset-left-ideal-Ring R J y)
          ( λ (α , K) → H α y K))

The left ideal generated by a family of elements in a ring

module _
  {l1 l2 : Level} (R : Ring l1) {I : UU l1} (a : I → type-Ring R)
  where

  generating-subset-left-ideal-family-of-elements-Ring : subset-Ring l1 R
  generating-subset-left-ideal-family-of-elements-Ring x =
    trunc-Prop (fiber a x)

  left-ideal-family-of-elements-Ring : left-ideal-Ring l1 R
  left-ideal-family-of-elements-Ring =
    left-ideal-subset-Ring R
      generating-subset-left-ideal-family-of-elements-Ring

  subset-left-ideal-family-of-elements-Ring : subset-Ring l1 R
  subset-left-ideal-family-of-elements-Ring =
    subset-left-ideal-subset-Ring R
      generating-subset-left-ideal-family-of-elements-Ring

  is-in-left-ideal-family-of-elements-Ring : type-Ring R → UU l1
  is-in-left-ideal-family-of-elements-Ring =
    is-in-left-ideal-subset-Ring R
      generating-subset-left-ideal-family-of-elements-Ring

  contains-element-left-ideal-family-of-elements-Ring :
    (i : I) → is-in-left-ideal-family-of-elements-Ring (a i)
  contains-element-left-ideal-family-of-elements-Ring i =
    contains-subset-left-ideal-subset-Ring R
      ( generating-subset-left-ideal-family-of-elements-Ring)
      ( a i)
      ( unit-trunc-Prop (i , refl))

  abstract
    is-left-ideal-generated-by-family-of-elements-left-ideal-family-of-elements-Ring :
      is-left-ideal-generated-by-family-of-elements-Ring R a
        left-ideal-family-of-elements-Ring
        contains-element-left-ideal-family-of-elements-Ring
    is-left-ideal-generated-by-family-of-elements-left-ideal-family-of-elements-Ring
      J H =
      is-left-ideal-generated-by-subset-left-ideal-subset-Ring R
        ( generating-subset-left-ideal-family-of-elements-Ring)
        ( J)
        ( λ x p →
          apply-universal-property-trunc-Prop p
            ( subset-left-ideal-Ring R J x)
            ( λ where (i , refl) → H i))

Properties

The left ideal generated by the underlying subset of an left ideal I is I itself

module _
  {l1 l2 : Level} (R : Ring l1) (I : left-ideal-Ring l2 R)
  where

  cases-forward-inclusion-idempotent-left-ideal-subset-Ring :
    (l : left-formal-combination-subset-Ring R (subset-left-ideal-Ring R I)) →
    is-in-left-ideal-Ring R I
      ( ev-left-formal-combination-subset-Ring R (subset-left-ideal-Ring R I) l)
  cases-forward-inclusion-idempotent-left-ideal-subset-Ring nil =
    contains-zero-left-ideal-Ring R I
  cases-forward-inclusion-idempotent-left-ideal-subset-Ring
    ( cons (x , y , u) l) =
    is-closed-under-addition-left-ideal-Ring R I
      ( is-closed-under-left-multiplication-left-ideal-Ring R I x y u)
      ( cases-forward-inclusion-idempotent-left-ideal-subset-Ring l)

  abstract
    forward-inclusion-idempotent-left-ideal-subset-Ring :
      leq-left-ideal-Ring R
        ( left-ideal-subset-Ring R (subset-left-ideal-Ring R I))
        ( I)
    forward-inclusion-idempotent-left-ideal-subset-Ring x H =
      apply-universal-property-trunc-Prop H
        ( subset-left-ideal-Ring R I x)
        ( λ where
          ( l , refl) →
            cases-forward-inclusion-idempotent-left-ideal-subset-Ring l)

  backward-inclusion-idempotent-left-ideal-subset-Ring :
    leq-left-ideal-Ring R
      ( I)
      ( left-ideal-subset-Ring R (subset-left-ideal-Ring R I))
  backward-inclusion-idempotent-left-ideal-subset-Ring =
    contains-subset-left-ideal-subset-Ring R (subset-left-ideal-Ring R I)

  idempotent-left-ideal-subset-Ring :
    has-same-elements-left-ideal-Ring R
      ( left-ideal-subset-Ring R (subset-left-ideal-Ring R I))
      ( I)
  pr1 (idempotent-left-ideal-subset-Ring x) =
    forward-inclusion-idempotent-left-ideal-subset-Ring x
  pr2 (idempotent-left-ideal-subset-Ring x) =
    backward-inclusion-idempotent-left-ideal-subset-Ring x

The operation S ↦ (S) preserves least upper bounds

In ring-theory.joins-left-ideals-rings we will convert this fact to the fact that S ↦ (S) preserves joins.

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

  preserves-least-upper-bounds-left-ideal-subset-Ring :
    {l4 : Level} (T : subset-Ring l4 R) →
    is-least-upper-bound-family-of-elements-Large-Poset
      ( powerset-Large-Poset (type-Ring R))
      ( S)
      ( T) →
    is-least-upper-bound-family-of-elements-Large-Poset
      ( left-ideal-Ring-Large-Poset R)
      ( λ α → left-ideal-subset-Ring R (S α))
      ( left-ideal-subset-Ring R T)
  preserves-least-upper-bounds-left-ideal-subset-Ring =
    preserves-join-lower-adjoint-galois-connection-Large-Poset
      ( powerset-Large-Poset (type-Ring R))
      ( left-ideal-Ring-Large-Poset R)
      ( left-ideal-subset-galois-connection-Ring R)
      ( S)

Recent changes