Ideals generated by subsets of commutative rings

module commutative-algebra.ideals-generated-by-subsets-commutative-rings where
Imports
open import commutative-algebra.commutative-rings
open import commutative-algebra.ideals-commutative-rings
open import commutative-algebra.subsets-commutative-rings

open import foundation.identity-types
open import foundation.powersets
open import foundation.universe-levels

open import lists.concatenation-lists

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

Idea

The ideal generated by a subset S of a commutative ring R is the least ideal that contains S.

Definitions

The universal property of the ideal generated by a subset

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

  is-ideal-generated-by-subset-Commutative-Ring :
    (l : Level)  UU (l1  l2  l3  lsuc l)
  is-ideal-generated-by-subset-Commutative-Ring l =
    (J : ideal-Commutative-Ring l R) 
    S  subset-ideal-Commutative-Ring R J 
    subset-ideal-Commutative-Ring R I  subset-ideal-Commutative-Ring R J
module _
  {l1 l2 : Level} (R : Commutative-Ring l1) (S : subset-Commutative-Ring l2 R)
  where

  formal-combination-subset-Commutative-Ring : UU (l1  l2)
  formal-combination-subset-Commutative-Ring =
    formal-combination-subset-Ring (ring-Commutative-Ring R) S

  ev-formal-combination-subset-Commutative-Ring :
    formal-combination-subset-Commutative-Ring  type-Commutative-Ring R
  ev-formal-combination-subset-Commutative-Ring =
    ev-formal-combination-subset-Ring (ring-Commutative-Ring R) S

  preserves-concat-ev-formal-combination-subset-Commutative-Ring :
    (u v : formal-combination-subset-Commutative-Ring) 
    Id ( ev-formal-combination-subset-Commutative-Ring (concat-list u v))
       ( add-Commutative-Ring R
         ( ev-formal-combination-subset-Commutative-Ring u)
         ( ev-formal-combination-subset-Commutative-Ring v))
  preserves-concat-ev-formal-combination-subset-Commutative-Ring =
    preserves-concat-ev-formal-combination-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

  mul-formal-combination-subset-Commutative-Ring :
    type-Commutative-Ring R 
    formal-combination-subset-Commutative-Ring 
    formal-combination-subset-Commutative-Ring
  mul-formal-combination-subset-Commutative-Ring =
    mul-formal-combination-subset-Ring (ring-Commutative-Ring R) S

  preserves-mul-ev-formal-combination-subset-Commutative-Ring :
    (r : type-Commutative-Ring R)
    (u : formal-combination-subset-Commutative-Ring) 
    Id ( ev-formal-combination-subset-Commutative-Ring
         ( mul-formal-combination-subset-Commutative-Ring r u))
       ( mul-Commutative-Ring R r
         ( ev-formal-combination-subset-Commutative-Ring u))
  preserves-mul-ev-formal-combination-subset-Commutative-Ring =
    preserves-mul-ev-formal-combination-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

  subset-ideal-subset-Commutative-Ring' : type-Commutative-Ring R  UU (l1  l2)
  subset-ideal-subset-Commutative-Ring' =
    subset-left-ideal-subset-Ring'
      ( ring-Commutative-Ring R)
      ( S)

  subset-ideal-subset-Commutative-Ring : subset-Commutative-Ring (l1  l2) R
  subset-ideal-subset-Commutative-Ring =
    subset-left-ideal-subset-Ring (ring-Commutative-Ring R) S

  contains-zero-ideal-subset-Commutative-Ring :
    contains-zero-subset-Commutative-Ring R subset-ideal-subset-Commutative-Ring
  contains-zero-ideal-subset-Commutative-Ring =
    contains-zero-left-ideal-subset-Ring (ring-Commutative-Ring R) S

  is-closed-under-addition-ideal-subset-Commutative-Ring :
    is-closed-under-addition-subset-Commutative-Ring R
      subset-ideal-subset-Commutative-Ring
  is-closed-under-addition-ideal-subset-Commutative-Ring =
    is-closed-under-addition-left-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

  is-closed-under-left-multiplication-ideal-subset-Commutative-Ring :
    is-closed-under-left-multiplication-subset-Commutative-Ring R
      subset-ideal-subset-Commutative-Ring
  is-closed-under-left-multiplication-ideal-subset-Commutative-Ring =
    is-closed-under-left-multiplication-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

  is-closed-under-negatives-ideal-subset-Commutative-Ring :
    is-closed-under-negatives-subset-Commutative-Ring R
      subset-ideal-subset-Commutative-Ring
  is-closed-under-negatives-ideal-subset-Commutative-Ring =
    is-closed-under-negatives-left-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

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

  contains-subset-ideal-subset-Commutative-Ring :
    S  subset-ideal-subset-Commutative-Ring
  contains-subset-ideal-subset-Commutative-Ring =
    contains-subset-left-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)

  contains-formal-combinations-ideal-subset-Commutative-Ring :
    {l3 : Level} (I : ideal-Commutative-Ring l3 R) 
    S  subset-ideal-Commutative-Ring R I 
    (x : formal-combination-subset-Commutative-Ring) 
    is-in-ideal-Commutative-Ring R I
      ( ev-formal-combination-subset-Commutative-Ring x)
  contains-formal-combinations-ideal-subset-Commutative-Ring I =
    contains-formal-combinations-left-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)
      ( left-ideal-ideal-Commutative-Ring R I)

  is-ideal-generated-by-subset-ideal-subset-Commutative-Ring :
    (l : Level) 
    is-ideal-generated-by-subset-Commutative-Ring R S
      ( ideal-subset-Commutative-Ring)
      ( contains-subset-ideal-subset-Commutative-Ring)
      ( l)
  is-ideal-generated-by-subset-ideal-subset-Commutative-Ring l I =
    is-left-ideal-generated-by-subset-left-ideal-subset-Ring
      ( ring-Commutative-Ring R)
      ( S)
      ( l)
      ( left-ideal-ideal-Commutative-Ring R I)