Ideals generated by subsets of rings

module ring-theory.ideals-generated-by-subsets-rings where

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.fibers-of-maps
open import foundation.functions
open import foundation.identity-types
open import foundation.powersets
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.universe-levels

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

open import ring-theory.ideals-rings
open import ring-theory.rings
open import ring-theory.subsets-rings

Idea

If S is a subset of a ring R, then the left/right/two-sided ideal generated by S is the least left/right/two-sided 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.

Definitions

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 : left-ideal-Ring l3 R) (H : S ⊆ subset-left-ideal-Ring R I)
  where

  is-left-ideal-generated-by-subset-Ring :
    (l : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l)
  is-left-ideal-generated-by-subset-Ring l =
    (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

Construction of ideals generated by a subset of a ring

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

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

  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 (pair r s) l) =
    add-Ring R
      ( mul-Ring R r (inclusion-subset-Ring R S s))
      ( ev-formal-combination-subset-Ring l)

  preserves-concat-ev-formal-combination-subset-Ring :
    (u v : formal-combination-subset-Ring) →
    Id ( 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 (pair r s) u) v =
    ( ap
      ( add-Ring R (mul-Ring R r (inclusion-subset-Ring R S s)))
      ( preserves-concat-ev-formal-combination-subset-Ring u v)) ∙
    ( inv
      ( associative-add-Ring R
        ( mul-Ring R r (inclusion-subset-Ring R S s))
        ( ev-formal-combination-subset-Ring u)
        ( ev-formal-combination-subset-Ring v)))

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

  preserves-mul-ev-formal-combination-subset-Ring :
    (r : type-Ring R) (u : formal-combination-subset-Ring) →
    Id ( ev-formal-combination-subset-Ring
         ( mul-formal-combination-subset-Ring r u))
       ( mul-Ring R r (ev-formal-combination-subset-Ring u))
  preserves-mul-ev-formal-combination-subset-Ring r nil =
    inv (right-zero-law-mul-Ring R r)
  preserves-mul-ev-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-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-formal-combination-subset-Ring u)))

  subset-left-ideal-subset-Ring' : type-Ring R → UU (l1 ⊔ l2)
  subset-left-ideal-subset-Ring' x = fib ev-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)

  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-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-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-ideal-subset-Ring' r x (pair l p)) =
    mul-formal-combination-subset-Ring r l
  pr2 (is-closed-under-left-multiplication-ideal-subset-Ring' r x (pair l p)) =
    ( preserves-mul-ev-formal-combination-subset-Ring r l) ∙
    ( ap (mul-Ring R r) p)

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

  is-left-ideal-generated-by-subset-left-ideal-subset-Ring :
    (l : Level) →
    is-left-ideal-generated-by-subset-Ring R S
      ( left-ideal-subset-Ring)
      ( contains-subset-left-ideal-subset-Ring)
      ( l)
  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-formal-combinations-left-ideal-subset-Ring J K c