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

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

Imports
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


## Idea

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.

## Definitions

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

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

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

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

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) =
( 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) ＝
( ev-formal-combination-subset-Ring u)
( ev-formal-combination-subset-Ring v)
preserves-concat-ev-formal-combination-subset-Ring nil v =
preserves-concat-ev-formal-combination-subset-Ring (cons (x , s , y) u) v =
( ap
( mul-Ring R (mul-Ring R x (inclusion-subset-Ring R S s)) y))
( preserves-concat-ev-formal-combination-subset-Ring u v)) ∙
( inv
( 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 =
inv
( ( 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 =
( ( 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
( 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
( 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)

(x y : type-Ring R) →
subset-ideal-subset-Ring' x → subset-ideal-subset-Ring' 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) ∙

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' →
unit-trunc-Prop
( 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' →
unit-trunc-Prop
( 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' →
unit-trunc-Prop
( 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 =
tr
( 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 =
subset-ideal-subset-Ring
pr1 (pr1 (pr2 ideal-subset-Ring)) =
contains-zero-ideal-subset-Ring
pr1 (pr2 (pr1 (pr2 ideal-subset-Ring))) =
pr2 (pr2 (pr1 (pr2 ideal-subset-Ring))) =
is-closed-under-negatives-ideal-subset-Ring
pr1 (pr2 (pr2 ideal-subset-Ring)) =
is-closed-under-left-multiplication-ideal-subset-Ring
pr2 (pr2 (pr2 ideal-subset-Ring)) =
is-closed-under-right-multiplication-ideal-subset-Ring

contains-subset-ideal-subset-Ring :
S ⊆ subset-ideal-subset-Ring
contains-subset-ideal-subset-Ring s H =
unit-trunc-Prop
( ( 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-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
where
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)
where

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 :
hom-Large-Poset
( λ 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 =
preserves-order-ideal-subset-Ring


#### The Galois connection S ↦ (S)

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

{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)
is-ideal-generated-by-subset-ideal-subset-Ring A S I

ideal-subset-galois-connection-Ring :
galois-connection-Large-Poset
( _⊔_ 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)
where

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

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

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

abstract
is-ideal-generated-by-family-of-elements-ideal-family-of-elements-Ring :
is-ideal-generated-by-family-of-elements-Ring R a
ideal-family-of-elements-Ring
contains-element-ideal-family-of-elements-Ring
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))


## Properties

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

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

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

preserves-least-upper-bounds-ideal-subset-Ring :
{l4 : Level} (T : subset-Ring l4 R) →
is-least-upper-bound-family-of-elements-Large-Poset
( powerset-Large-Poset (type-Ring R))
( S)
( T) →
is-least-upper-bound-family-of-elements-Large-Poset
( ideal-Ring-Large-Poset R)
( λ α → ideal-subset-Ring R (S α))
( ideal-subset-Ring R T)
preserves-least-upper-bounds-ideal-subset-Ring =