# Ideals generated by subsets of commutative rings

Content created by Fredrik Bakke, Egbert Rijke and Maša Žaucer.

Created on 2023-05-04.

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.poset-of-ideals-commutative-rings
open import commutative-algebra.subsets-commutative-rings

open import foundation.identity-types
open import foundation.subtypes
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


### The ideal generated by a subset

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) →
( ev-formal-combination-subset-Commutative-Ring (concat-list u v)) ＝
( 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 →
type-Commutative-Ring R →
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)
(t : type-Commutative-Ring R) →
ev-formal-combination-subset-Commutative-Ring
( mul-formal-combination-subset-Commutative-Ring r u t) ＝
mul-Commutative-Ring R
( mul-Commutative-Ring R r
( ev-formal-combination-subset-Commutative-Ring u))
( t)
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-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-ideal-subset-Ring (ring-Commutative-Ring R) S

is-in-ideal-subset-Commutative-Ring : type-Commutative-Ring R → UU (l1 ⊔ l2)
is-in-ideal-subset-Commutative-Ring =
is-in-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-ideal-subset-Ring (ring-Commutative-Ring R) S

subset-ideal-subset-Commutative-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-right-multiplication-ideal-subset-Commutative-Ring :
is-closed-under-right-multiplication-subset-Commutative-Ring R
subset-ideal-subset-Commutative-Ring
is-closed-under-right-multiplication-ideal-subset-Commutative-Ring =
is-closed-under-right-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-ideal-subset-Ring
( ring-Commutative-Ring R)
( S)

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

contains-subset-ideal-subset-Commutative-Ring :
S ⊆ subset-ideal-subset-Commutative-Ring
contains-subset-ideal-subset-Commutative-Ring =
contains-subset-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-ideal-subset-Ring
( ring-Commutative-Ring R)
( S)
( 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 I =
is-ideal-generated-by-subset-ideal-subset-Ring
( ring-Commutative-Ring R)
( S)
( I)

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

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


## Properties

### The subset relation is preserved by generating ideals

module _
{l1 l2 l3 : Level} (A : Commutative-Ring l1)
(S : subset-Commutative-Ring l2 A) (T : subset-Commutative-Ring l3 A)
where

preserves-order-ideal-subset-Commutative-Ring :
S ⊆ T →
leq-ideal-Commutative-Ring A
( ideal-subset-Commutative-Ring A S)
( ideal-subset-Commutative-Ring A T)
preserves-order-ideal-subset-Commutative-Ring =
preserves-order-ideal-subset-Ring (ring-Commutative-Ring A) S T


### The ideal generated by the underlying set of an ideal I is I itself

module _
{l1 l2 : Level} (A : Commutative-Ring l1) (I : ideal-Commutative-Ring l2 A)
where

forward-inclusion-idempotent-ideal-subset-Commutative-Ring :
leq-ideal-Commutative-Ring A
( ideal-subset-Commutative-Ring A (subset-ideal-Commutative-Ring A I))
( I)
forward-inclusion-idempotent-ideal-subset-Commutative-Ring =
forward-inclusion-idempotent-ideal-subset-Ring (ring-Commutative-Ring A) I

backward-inclusion-idempotent-ideal-subset-Commutative-Ring :
leq-ideal-Commutative-Ring A
( I)
( ideal-subset-Commutative-Ring A (subset-ideal-Commutative-Ring A I))
backward-inclusion-idempotent-ideal-subset-Commutative-Ring =
backward-inclusion-idempotent-ideal-subset-Ring (ring-Commutative-Ring A) I

idempotent-ideal-subset-Commutative-Ring :
has-same-elements-ideal-Commutative-Ring A
( ideal-subset-Commutative-Ring A (subset-ideal-Commutative-Ring A I))
( I)
idempotent-ideal-subset-Commutative-Ring =
idempotent-ideal-subset-Ring (ring-Commutative-Ring A) I