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
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


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


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)

  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)

  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 α))

  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)

  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))
    ( 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 :
    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) 
      ( 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)
    ( is-closed-under-addition-right-ideal-subset-Ring' x y (l , p) (k , q)) =
    concat-list l k
    ( 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' 
              ( 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)
    ( is-closed-under-right-multiplication-right-ideal-subset-Ring' x r
      ( pair l p)) =
    mul-right-formal-combination-subset-Ring l r
    ( 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
  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' 
          ( 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 =
      ( 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 =
  pr1 (pr1 (pr2 right-ideal-subset-Ring)) =
  pr1 (pr2 (pr1 (pr2 right-ideal-subset-Ring))) =
  pr2 (pr2 (pr1 (pr2 right-ideal-subset-Ring))) =
  pr2 (pr2 right-ideal-subset-Ring) =

  contains-subset-right-ideal-subset-Ring :
    S  subset-right-ideal-subset-Ring
  contains-subset-right-ideal-subset-Ring s H =
      ( ( 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
    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)

  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 :
      ( λ 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 =

The Galois connection S ↦ (S)

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

  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 :
      ( l1 ⊔_)  l  l)
      ( powerset-Large-Poset (type-Ring A))
      ( right-ideal-Ring-Large-Poset A)
    right-ideal-subset-galois-connection-Ring =
    right-ideal-subset-hom-large-poset-Ring A
    right-ideal-subset-galois-connection-Ring =
    subset-right-ideal-hom-large-poset-Ring A
    right-ideal-subset-galois-connection-Ring =

The reflective Galois connection S ↦ (S)

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

  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 :
      ( 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 :
      ( powerset-Large-Poset (type-Ring A))
      ( right-ideal-Ring-Large-Poset A)
    right-ideal-subset-reflective-galois-connection-Ring =
    right-ideal-subset-galois-connection-Ring A
    right-ideal-subset-reflective-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)

  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

  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

  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

  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)
    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)

  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

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

  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

  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))

    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
      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))


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)

  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
    ( 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)

    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)

  preserves-least-upper-bounds-right-ideal-subset-Ring :
    {l4 : Level} (T : subset-Ring l4 R) 
      ( powerset-Large-Poset (type-Ring R))
      ( S)
      ( T) 
      ( 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 =
      ( powerset-Large-Poset (type-Ring R))
      ( right-ideal-Ring-Large-Poset R)
      ( right-ideal-subset-galois-connection-Ring R)
      ( S)

Recent changes