Ideals generated by subsets of rings

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Maša Žaucer.

Created on 2022-04-07.
Last modified on 2023-11-24.

module ring-theory.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.identity-types
open import foundation.logical-equivalences
open import foundation.powersets
open import foundation.propositional-truncations
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.ideals-rings
open import ring-theory.poset-of-ideals-rings
open import ring-theory.rings
open import ring-theory.subsets-rings


If S is a subset of a ring R, then the (two-sided) ideal generated by S is the least ideal containing S. This idea expresses the universal property of the ideal generated by a subset of a ring. We will construct it as the type of finite linear combinations of elements in S. The operation S ↦ (S) which maps a subset S to the ideal generated by S is the lower adjoint of a galois connection between the large poset of subsets of R and the large poset of ideals of R.


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

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

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

The universal property of ideals generated by families of subsets of a ring

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

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

The universal property of ideals generated by families of elements of a ring

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

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

Construction of the Galois connection of ideals generated by subsets

Ideals generated by subsets

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

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

  ev-formal-combination-subset-Ring :
    formal-combination-subset-Ring  type-Ring R
  ev-formal-combination-subset-Ring nil = zero-Ring R
  ev-formal-combination-subset-Ring (cons (x , s , y) l) =
    add-Ring R
      ( mul-Ring R (mul-Ring R x (inclusion-subset-Ring R S s)) y)
      ( ev-formal-combination-subset-Ring l)

  preserves-concat-ev-formal-combination-subset-Ring :
    (u v : formal-combination-subset-Ring) 
    ev-formal-combination-subset-Ring (concat-list u v) 
    add-Ring R
      ( ev-formal-combination-subset-Ring u)
      ( ev-formal-combination-subset-Ring v)
  preserves-concat-ev-formal-combination-subset-Ring nil v =
    inv (left-unit-law-add-Ring R (ev-formal-combination-subset-Ring v))
  preserves-concat-ev-formal-combination-subset-Ring (cons (x , s , y) u) v =
    ( ap
      ( add-Ring R
        ( mul-Ring R (mul-Ring R x (inclusion-subset-Ring R S s)) y))
      ( preserves-concat-ev-formal-combination-subset-Ring u v)) 
    ( inv
      ( associative-add-Ring R
        ( mul-Ring R (mul-Ring R x (inclusion-subset-Ring R S s)) y)
        ( ev-formal-combination-subset-Ring u)
        ( ev-formal-combination-subset-Ring v)))

  mul-formal-combination-subset-Ring :
    type-Ring R  formal-combination-subset-Ring 
    type-Ring R  formal-combination-subset-Ring
  mul-formal-combination-subset-Ring x l y =
    map-list  (u , s , v)  (mul-Ring R x u , s , mul-Ring R v y)) l

  preserves-mul-ev-formal-combination-subset-Ring :
    (x : type-Ring R) (u : formal-combination-subset-Ring) (y : type-Ring R) 
    ( ev-formal-combination-subset-Ring
      ( mul-formal-combination-subset-Ring x u y)) 
    ( mul-Ring R (mul-Ring R x (ev-formal-combination-subset-Ring u)) y)
  preserves-mul-ev-formal-combination-subset-Ring x nil y =
      ( ( ap
          ( mul-Ring' R y)
          ( right-zero-law-mul-Ring R x)) 
        ( left-zero-law-mul-Ring R y))
  preserves-mul-ev-formal-combination-subset-Ring x
    ( cons (r , (s , H) , t) u) y =
    ( ap-add-Ring R
      ( ( inv
          ( associative-mul-Ring R
            ( mul-Ring R (mul-Ring R x r) s)
            ( t)
            ( y))) 
        ( ap
          ( mul-Ring' R y)
          ( ( ap (mul-Ring' R t) (associative-mul-Ring R x r s)) 
            ( associative-mul-Ring R x (mul-Ring R r s) t))))
      ( preserves-mul-ev-formal-combination-subset-Ring x u y)) 
    ( ( inv
        ( right-distributive-mul-add-Ring R
          ( mul-Ring R x
            ( mul-Ring R (mul-Ring R r s) t))
          ( mul-Ring R x (ev-formal-combination-subset-Ring u))
          ( y))) 
      ( ap
        ( mul-Ring' R y)
        ( inv
          ( left-distributive-mul-add-Ring R x
            ( mul-Ring R (mul-Ring R r s) t)
            ( ev-formal-combination-subset-Ring u)))))

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

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

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

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

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

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

  is-closed-under-multiplication-ideal-subset-Ring' :
    (r s t : type-Ring R)  subset-ideal-subset-Ring' s 
    subset-ideal-subset-Ring' (mul-Ring R (mul-Ring R r s) t)
  pr1 (is-closed-under-multiplication-ideal-subset-Ring' r s t (l , p)) =
    mul-formal-combination-subset-Ring r l t
  pr2 (is-closed-under-multiplication-ideal-subset-Ring' r s t (l , p)) =
    ( preserves-mul-ev-formal-combination-subset-Ring r l t) 
    ( ap  u  mul-Ring R (mul-Ring R r u) t) p)

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

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

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

  ideal-subset-Ring : ideal-Ring (l1  l2) R
  pr1 ideal-subset-Ring =
  pr1 (pr1 (pr2 ideal-subset-Ring)) =
  pr1 (pr2 (pr1 (pr2 ideal-subset-Ring))) =
  pr2 (pr2 (pr1 (pr2 ideal-subset-Ring))) =
  pr1 (pr2 (pr2 ideal-subset-Ring)) =
  pr2 (pr2 (pr2 ideal-subset-Ring)) =

  contains-subset-ideal-subset-Ring :
    S  subset-ideal-subset-Ring
  contains-subset-ideal-subset-Ring s H =
      ( ( cons (one-Ring R , (s , H) , one-Ring R) nil) ,
        ( ( right-unit-law-add-Ring R _) 
          ( right-unit-law-mul-Ring R _  left-unit-law-mul-Ring R _)))

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

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

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

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

The subset relation is preserved by generating ideals

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

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

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

The Galois connection S ↦ (S)

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

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

  ideal-subset-galois-connection-Ring :
      ( _⊔_ l1)  l  l)
      ( powerset-Large-Poset (type-Ring A))
      ( ideal-Ring-Large-Poset A)
    ideal-subset-galois-connection-Ring =
    ideal-subset-hom-large-poset-Ring A
    ideal-subset-galois-connection-Ring =
    subset-ideal-hom-large-poset-Ring A
    ideal-subset-galois-connection-Ring =

The reflective Galois connection S ↦ (S)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

The operation S ↦ (S) preserves least upper bounds

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

Recent changes