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)