Left ideals generated by subsets of rings

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

Created on 2023-06-08.

module ring-theory.left-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.function-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.powersets
open import foundation.propositional-truncations
open import foundation.propositions
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.left-ideals-rings
open import ring-theory.poset-of-left-ideals-rings
open import ring-theory.rings
open import ring-theory.subsets-rings


Idea

The left ideal generated by a subset S of a ring R is the least left ideal in R containing S.

Definitions

The universal property of left 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 : UUω
is-left-ideal-generated-by-subset-Ring =
{l : Level} (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


The universal property of left ideals generated by a family of subsets of a ring

module _
{l1 l2 l3 l4 : Level} (R : Ring l1) {U : UU l2} (S : U → subset-Ring l3 R)
(I : left-ideal-Ring l4 R) (H : (α : U) → S α ⊆ subset-left-ideal-Ring R I)
where

is-left-ideal-generated-by-family-of-subsets-Ring : UUω
is-left-ideal-generated-by-family-of-subsets-Ring =
{l : Level} (J : left-ideal-Ring l R) →
((α : U) → S α ⊆ subset-left-ideal-Ring R J) →
leq-left-ideal-Ring R I J


The universal property of left ideals generated by a family of elements of a ring

module _
{l1 l2 l3 : Level} (R : Ring l1) {U : UU l2} (a : U → type-Ring R)
(I : left-ideal-Ring l3 R) (H : (α : U) → is-in-left-ideal-Ring R I (a α))
where

is-left-ideal-generated-by-family-of-elements-Ring : UUω
is-left-ideal-generated-by-family-of-elements-Ring =
{l : Level} (J : left-ideal-Ring l R) →
((α : U) → is-in-left-ideal-Ring R J (a α)) →
leq-left-ideal-Ring R I J


Construction of the Galois connection of left ideals generated by subsets

Left ideals generated by subsets

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

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

ev-left-formal-combination-subset-Ring :
left-formal-combination-subset-Ring → type-Ring R
ev-left-formal-combination-subset-Ring nil = zero-Ring R
ev-left-formal-combination-subset-Ring (cons (pair r s) l) =
( mul-Ring R r (inclusion-subset-Ring R S s))
( ev-left-formal-combination-subset-Ring l)

preserves-concat-ev-left-formal-combination-subset-Ring :
(u v : left-formal-combination-subset-Ring) →
ev-left-formal-combination-subset-Ring (concat-list u v) ＝
( ev-left-formal-combination-subset-Ring u)
( ev-left-formal-combination-subset-Ring v)
preserves-concat-ev-left-formal-combination-subset-Ring nil v =
preserves-concat-ev-left-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-left-formal-combination-subset-Ring u v)) ∙
( inv
( mul-Ring R r (inclusion-subset-Ring R S s))
( ev-left-formal-combination-subset-Ring u)
( ev-left-formal-combination-subset-Ring v)))

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

preserves-mul-ev-left-formal-combination-subset-Ring :
(r : type-Ring R) (u : left-formal-combination-subset-Ring) →
ev-left-formal-combination-subset-Ring
( mul-left-formal-combination-subset-Ring r u) ＝
mul-Ring R r (ev-left-formal-combination-subset-Ring u)
preserves-mul-ev-left-formal-combination-subset-Ring r nil =
inv (right-zero-law-mul-Ring R r)
preserves-mul-ev-left-formal-combination-subset-Ring r (cons x u) =
( associative-mul-Ring R r (pr1 x) (inclusion-subset-Ring R S (pr2 x)))
( preserves-mul-ev-left-formal-combination-subset-Ring r u)) ∙
( inv
( mul-Ring R (pr1 x) (inclusion-subset-Ring R S (pr2 x)))
( ev-left-formal-combination-subset-Ring u)))

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

is-in-left-ideal-subset-Ring : type-Ring R → UU (l1 ⊔ l2)
is-in-left-ideal-subset-Ring = is-in-subtype subset-left-ideal-subset-Ring

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)

(x y : type-Ring R) →
subset-left-ideal-subset-Ring' x → subset-left-ideal-subset-Ring' y →
pr1
( pair l p) (pair k q)) =
concat-list l k
pr2
( pair l p) (pair k q)) =
( preserves-concat-ev-left-formal-combination-subset-Ring l k) ∙

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

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

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

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

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


The subset relation is preserved by generating left ideals

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

preserves-order-left-ideal-subset-Ring :
{l2 l3 : Level} (S : subset-Ring l2 A) (T : subset-Ring l3 A) →
S ⊆ T →
leq-left-ideal-Ring A
( left-ideal-subset-Ring A S)
( left-ideal-subset-Ring A T)
preserves-order-left-ideal-subset-Ring S T H =
is-left-ideal-generated-by-subset-left-ideal-subset-Ring A S
( left-ideal-subset-Ring A T)
( transitive-leq-subtype S T
( subset-left-ideal-subset-Ring A T)
( contains-subset-left-ideal-subset-Ring A T)
( H))

left-ideal-subset-hom-large-poset-Ring :
hom-Large-Poset
( λ l2 → l1 ⊔ l2)
( powerset-Large-Poset (type-Ring A))
( left-ideal-Ring-Large-Poset A)
map-hom-Large-Preorder left-ideal-subset-hom-large-poset-Ring =
left-ideal-subset-Ring A
preserves-order-hom-Large-Preorder left-ideal-subset-hom-large-poset-Ring =
preserves-order-left-ideal-subset-Ring


The Galois connection S ↦ (S)

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

{l2 l3 : Level} (S : subset-Ring l2 A) (I : left-ideal-Ring l3 A) →
leq-left-ideal-Ring A (left-ideal-subset-Ring A S) I ↔
(S ⊆ subset-left-ideal-Ring A I)
pr1 (adjoint-relation-left-ideal-subset-Ring S I) H =
transitive-leq-subtype S
( subset-left-ideal-subset-Ring A S)
( subset-left-ideal-Ring A I)
( H)
( contains-subset-left-ideal-subset-Ring A S)
is-left-ideal-generated-by-subset-left-ideal-subset-Ring A S I

left-ideal-subset-galois-connection-Ring :
galois-connection-Large-Poset
( l1 ⊔_) (λ l → l)
( powerset-Large-Poset (type-Ring A))
( left-ideal-Ring-Large-Poset A)
left-ideal-subset-galois-connection-Ring =
left-ideal-subset-hom-large-poset-Ring A
left-ideal-subset-galois-connection-Ring =
subset-left-ideal-hom-large-poset-Ring A
left-ideal-subset-galois-connection-Ring =


The reflective Galois connection S ↦ (S)

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

forward-inclusion-is-reflective-left-ideal-subset-galois-connection-Ring :
{l2 : Level} (I : left-ideal-Ring l2 A) →
leq-left-ideal-Ring A
( left-ideal-subset-Ring A (subset-left-ideal-Ring A I))
( I)
forward-inclusion-is-reflective-left-ideal-subset-galois-connection-Ring I =
is-left-ideal-generated-by-subset-left-ideal-subset-Ring A
( subset-left-ideal-Ring A I)
( I)
( refl-leq-left-ideal-Ring A I)

backward-inclusion-is-reflective-left-ideal-subset-galois-connection-Ring :
{l2 : Level} (I : left-ideal-Ring l2 A) →
leq-left-ideal-Ring A I
( left-ideal-subset-Ring A (subset-left-ideal-Ring A I))
backward-inclusion-is-reflective-left-ideal-subset-galois-connection-Ring I =
contains-subset-left-ideal-subset-Ring A (subset-left-ideal-Ring A I)

is-reflective-left-ideal-subset-galois-connection-Ring :
is-reflective-galois-connection-Large-Poset
( powerset-Large-Poset (type-Ring A))
( left-ideal-Ring-Large-Poset A)
( left-ideal-subset-galois-connection-Ring A)
pr1 (is-reflective-left-ideal-subset-galois-connection-Ring I) =
forward-inclusion-is-reflective-left-ideal-subset-galois-connection-Ring I
pr2 (is-reflective-left-ideal-subset-galois-connection-Ring I) =
backward-inclusion-is-reflective-left-ideal-subset-galois-connection-Ring I

left-ideal-subset-reflective-galois-connection-Ring :
reflective-galois-connection-Large-Poset
( powerset-Large-Poset (type-Ring A))
( left-ideal-Ring-Large-Poset A)
galois-connection-reflective-galois-connection-Large-Poset
left-ideal-subset-reflective-galois-connection-Ring =
left-ideal-subset-galois-connection-Ring A
is-reflective-reflective-galois-connection-Large-Poset
left-ideal-subset-reflective-galois-connection-Ring =
is-reflective-left-ideal-subset-galois-connection-Ring


The left 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-left-ideal-family-of-subsets-Ring :
subset-Ring (l2 ⊔ l3) R
generating-subset-left-ideal-family-of-subsets-Ring x =
union-family-of-subtypes S x

left-ideal-family-of-subsets-Ring : left-ideal-Ring (l1 ⊔ l2 ⊔ l3) R
left-ideal-family-of-subsets-Ring =
left-ideal-subset-Ring R generating-subset-left-ideal-family-of-subsets-Ring

subset-left-ideal-family-of-subsets-Ring : subset-Ring (l1 ⊔ l2 ⊔ l3) R
subset-left-ideal-family-of-subsets-Ring =
subset-left-ideal-subset-Ring R
generating-subset-left-ideal-family-of-subsets-Ring

is-in-left-ideal-family-of-subsets-Ring : type-Ring R → UU (l1 ⊔ l2 ⊔ l3)
is-in-left-ideal-family-of-subsets-Ring =
is-in-left-ideal-subset-Ring R
generating-subset-left-ideal-family-of-subsets-Ring

contains-subset-left-ideal-family-of-subsets-Ring :
{α : U} → (S α) ⊆ subset-left-ideal-family-of-subsets-Ring
contains-subset-left-ideal-family-of-subsets-Ring {α} x H =
contains-subset-left-ideal-subset-Ring R
( generating-subset-left-ideal-family-of-subsets-Ring)
( x)
( unit-trunc-Prop (α , H))

is-left-ideal-generated-by-family-of-subsets-left-ideal-family-of-subsets-Ring :
is-left-ideal-generated-by-family-of-subsets-Ring R S
( left-ideal-family-of-subsets-Ring)
( λ α → contains-subset-left-ideal-family-of-subsets-Ring)
is-left-ideal-generated-by-family-of-subsets-left-ideal-family-of-subsets-Ring
J H =
is-left-ideal-generated-by-subset-left-ideal-subset-Ring R
( generating-subset-left-ideal-family-of-subsets-Ring)
( J)
( λ y q →
apply-universal-property-trunc-Prop q
( subset-left-ideal-Ring R J y)
( λ (α , K) → H α y K))


The left 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-left-ideal-family-of-elements-Ring : subset-Ring l1 R
generating-subset-left-ideal-family-of-elements-Ring x =
trunc-Prop (fiber a x)

left-ideal-family-of-elements-Ring : left-ideal-Ring l1 R
left-ideal-family-of-elements-Ring =
left-ideal-subset-Ring R
generating-subset-left-ideal-family-of-elements-Ring

subset-left-ideal-family-of-elements-Ring : subset-Ring l1 R
subset-left-ideal-family-of-elements-Ring =
subset-left-ideal-subset-Ring R
generating-subset-left-ideal-family-of-elements-Ring

is-in-left-ideal-family-of-elements-Ring : type-Ring R → UU l1
is-in-left-ideal-family-of-elements-Ring =
is-in-left-ideal-subset-Ring R
generating-subset-left-ideal-family-of-elements-Ring

contains-element-left-ideal-family-of-elements-Ring :
(i : I) → is-in-left-ideal-family-of-elements-Ring (a i)
contains-element-left-ideal-family-of-elements-Ring i =
contains-subset-left-ideal-subset-Ring R
( generating-subset-left-ideal-family-of-elements-Ring)
( a i)
( unit-trunc-Prop (i , refl))

abstract
is-left-ideal-generated-by-family-of-elements-left-ideal-family-of-elements-Ring :
is-left-ideal-generated-by-family-of-elements-Ring R a
left-ideal-family-of-elements-Ring
contains-element-left-ideal-family-of-elements-Ring
is-left-ideal-generated-by-family-of-elements-left-ideal-family-of-elements-Ring
J H =
is-left-ideal-generated-by-subset-left-ideal-subset-Ring R
( generating-subset-left-ideal-family-of-elements-Ring)
( J)
( λ x p →
apply-universal-property-trunc-Prop p
( subset-left-ideal-Ring R J x)
( λ where (i , refl) → H i))


Properties

The left ideal generated by the underlying subset of an left ideal I is I itself

module _
{l1 l2 : Level} (R : Ring l1) (I : left-ideal-Ring l2 R)
where

cases-forward-inclusion-idempotent-left-ideal-subset-Ring :
(l : left-formal-combination-subset-Ring R (subset-left-ideal-Ring R I)) →
is-in-left-ideal-Ring R I
( ev-left-formal-combination-subset-Ring R (subset-left-ideal-Ring R I) l)
cases-forward-inclusion-idempotent-left-ideal-subset-Ring nil =
contains-zero-left-ideal-Ring R I
cases-forward-inclusion-idempotent-left-ideal-subset-Ring
( cons (x , y , u) l) =
( is-closed-under-left-multiplication-left-ideal-Ring R I x y u)
( cases-forward-inclusion-idempotent-left-ideal-subset-Ring l)

abstract
forward-inclusion-idempotent-left-ideal-subset-Ring :
leq-left-ideal-Ring R
( left-ideal-subset-Ring R (subset-left-ideal-Ring R I))
( I)
forward-inclusion-idempotent-left-ideal-subset-Ring x H =
apply-universal-property-trunc-Prop H
( subset-left-ideal-Ring R I x)
( λ where
( l , refl) →
cases-forward-inclusion-idempotent-left-ideal-subset-Ring l)

backward-inclusion-idempotent-left-ideal-subset-Ring :
leq-left-ideal-Ring R
( I)
( left-ideal-subset-Ring R (subset-left-ideal-Ring R I))
backward-inclusion-idempotent-left-ideal-subset-Ring =
contains-subset-left-ideal-subset-Ring R (subset-left-ideal-Ring R I)

idempotent-left-ideal-subset-Ring :
has-same-elements-left-ideal-Ring R
( left-ideal-subset-Ring R (subset-left-ideal-Ring R I))
( I)
pr1 (idempotent-left-ideal-subset-Ring x) =
forward-inclusion-idempotent-left-ideal-subset-Ring x
pr2 (idempotent-left-ideal-subset-Ring x) =
backward-inclusion-idempotent-left-ideal-subset-Ring x


The operation S ↦ (S) preserves least upper bounds

In ring-theory.joins-left-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-left-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
( left-ideal-Ring-Large-Poset R)
( λ α → left-ideal-subset-Ring R (S α))
( left-ideal-subset-Ring R T)
preserves-least-upper-bounds-left-ideal-subset-Ring =