Right 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 2023-11-24.

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

Idea

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

Definitions

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

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

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

The universal property of right 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 : right-ideal-Ring l4 R) (H : (α : U) → S α ⊆ subset-right-ideal-Ring R I)
  where

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

The universal property of right ideals generated by a famiy of elements of a ring

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

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

Construction of right ideals generated by a subset of a ring

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

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

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

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

  mul-right-formal-combination-subset-Ring :
    right-formal-combination-subset-Ring →
    type-Ring R → right-formal-combination-subset-Ring
  mul-right-formal-combination-subset-Ring l r =
    map-list (λ (x , y) → (x , (mul-Ring R y r))) l

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

The subset relation is preserved by generating right ideals

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

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

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

The Galois connection S ↦ (S)

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

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

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

The reflective Galois connection S ↦ (S)

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

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

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

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

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

The right 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-right-ideal-family-of-subsets-Ring :
    subset-Ring (l2 ⊔ l3) R
  generating-subset-right-ideal-family-of-subsets-Ring x =
    union-family-of-subtypes S x

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

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

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

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

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

The right 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-right-ideal-family-of-elements-Ring : subset-Ring l1 R
  generating-subset-right-ideal-family-of-elements-Ring x =
    trunc-Prop (fiber a x)

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

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

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

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

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

Properties

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

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

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

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

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

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

The operation S ↦ (S) preserves least upper bounds

In ring-theory.joins-right-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-right-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
      ( right-ideal-Ring-Large-Poset R)
      ( λ α → right-ideal-subset-Ring R (S α))
      ( right-ideal-subset-Ring R T)
  preserves-least-upper-bounds-right-ideal-subset-Ring =
    preserves-join-lower-adjoint-galois-connection-Large-Poset
      ( powerset-Large-Poset (type-Ring R))
      ( right-ideal-Ring-Large-Poset R)
      ( right-ideal-subset-galois-connection-Ring R)
      ( S)

Recent changes