Right 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.right-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.poset-of-right-ideals-rings
open import ring-theory.right-ideals-rings
open import ring-theory.rings
open import ring-theory.subsets-rings


Idea

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

Definitions

The universal property of right ideals generated by a subset of a ring

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

is-right-ideal-generated-by-subset-Ring : UUω
is-right-ideal-generated-by-subset-Ring =
{l : Level} (J : right-ideal-Ring l R) → S ⊆ subset-right-ideal-Ring R J →
subset-right-ideal-Ring R I ⊆ subset-right-ideal-Ring R J


The universal property of right 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 : right-ideal-Ring l4 R) (H : (α : U) → S α ⊆ subset-right-ideal-Ring R I)
where

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


The universal property of right ideals generated by a famiy of elements of a ring

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

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


Construction of right ideals generated by a subset of a ring

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

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

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

preserves-concat-ev-right-formal-combination-subset-Ring :
(u v : right-formal-combination-subset-Ring) →
ev-right-formal-combination-subset-Ring (concat-list u v) ＝
( ev-right-formal-combination-subset-Ring u)
( ev-right-formal-combination-subset-Ring v)
preserves-concat-ev-right-formal-combination-subset-Ring nil v =
preserves-concat-ev-right-formal-combination-subset-Ring
( cons (pair s r) u) v =
( ap
( add-Ring R (mul-Ring R (inclusion-subset-Ring R S s) r))
( preserves-concat-ev-right-formal-combination-subset-Ring u v)) ∙
( inv
( mul-Ring R (inclusion-subset-Ring R S s) r)
( ev-right-formal-combination-subset-Ring u)
( ev-right-formal-combination-subset-Ring v)))

mul-right-formal-combination-subset-Ring :
right-formal-combination-subset-Ring →
type-Ring R → right-formal-combination-subset-Ring
mul-right-formal-combination-subset-Ring l r =
map-list (λ (x , y) → (x , (mul-Ring R y r))) l

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

subset-right-ideal-subset-Ring' : type-Ring R → UU (l1 ⊔ l2)
subset-right-ideal-subset-Ring' x =
fiber ev-right-formal-combination-subset-Ring x

subset-right-ideal-subset-Ring : subset-Ring (l1 ⊔ l2) R
subset-right-ideal-subset-Ring x =
trunc-Prop (subset-right-ideal-subset-Ring' x)

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

contains-zero-right-ideal-subset-Ring :
contains-zero-subset-Ring R subset-right-ideal-subset-Ring
contains-zero-right-ideal-subset-Ring = unit-trunc-Prop (pair nil refl)

(x y : type-Ring R) →
subset-right-ideal-subset-Ring' x → subset-right-ideal-subset-Ring' y →
pr1
( is-closed-under-addition-right-ideal-subset-Ring' x y (l , p) (k , q)) =
concat-list l k
pr2
( is-closed-under-addition-right-ideal-subset-Ring' x y (l , p) (k , q)) =
( preserves-concat-ev-right-formal-combination-subset-Ring l k) ∙

is-closed-under-addition-right-ideal-subset-Ring {x} {y} H K =
apply-universal-property-trunc-Prop H
( subset-right-ideal-subset-Ring (add-Ring R x y))
( λ H' →
apply-universal-property-trunc-Prop K
( subset-right-ideal-subset-Ring (add-Ring R x y))
( λ K' →
unit-trunc-Prop
( is-closed-under-addition-right-ideal-subset-Ring' x y H' K')))

is-closed-under-right-multiplication-right-ideal-subset-Ring' :
(x r : type-Ring R) → subset-right-ideal-subset-Ring' x →
subset-right-ideal-subset-Ring' (mul-Ring R x r)
pr1
( is-closed-under-right-multiplication-right-ideal-subset-Ring' x r
( pair l p)) =
mul-right-formal-combination-subset-Ring l r
pr2
( is-closed-under-right-multiplication-right-ideal-subset-Ring' x r
( pair l p)) =
( preserves-mul-ev-right-formal-combination-subset-Ring l r) ∙
( ap (mul-Ring' R r) p)

is-closed-under-right-multiplication-right-ideal-subset-Ring :
is-closed-under-right-multiplication-subset-Ring R
subset-right-ideal-subset-Ring
is-closed-under-right-multiplication-right-ideal-subset-Ring x r H =
apply-universal-property-trunc-Prop H
( subset-right-ideal-subset-Ring (mul-Ring R x r))
( λ H' →
unit-trunc-Prop
( is-closed-under-right-multiplication-right-ideal-subset-Ring'
x r H'))

is-closed-under-negatives-right-ideal-subset-Ring :
is-closed-under-negatives-subset-Ring R subset-right-ideal-subset-Ring
is-closed-under-negatives-right-ideal-subset-Ring {x} H =
tr
( type-Prop ∘ subset-right-ideal-subset-Ring)
( mul-neg-one-Ring' R x)
( is-closed-under-right-multiplication-right-ideal-subset-Ring
( x)
( neg-one-Ring R)
( H))

right-ideal-subset-Ring : right-ideal-Ring (l1 ⊔ l2) R
pr1 right-ideal-subset-Ring =
subset-right-ideal-subset-Ring
pr1 (pr1 (pr2 right-ideal-subset-Ring)) =
contains-zero-right-ideal-subset-Ring
pr1 (pr2 (pr1 (pr2 right-ideal-subset-Ring))) =
pr2 (pr2 (pr1 (pr2 right-ideal-subset-Ring))) =
is-closed-under-negatives-right-ideal-subset-Ring
pr2 (pr2 right-ideal-subset-Ring) =
is-closed-under-right-multiplication-right-ideal-subset-Ring

contains-subset-right-ideal-subset-Ring :
S ⊆ subset-right-ideal-subset-Ring
contains-subset-right-ideal-subset-Ring s H =
unit-trunc-Prop
( ( cons ((s , H) , one-Ring R) nil) ,
( ( right-unit-law-add-Ring R (mul-Ring R s (one-Ring R))) ∙
( right-unit-law-mul-Ring R s)))

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

is-right-ideal-generated-by-subset-right-ideal-subset-Ring :
is-right-ideal-generated-by-subset-Ring R S
( right-ideal-subset-Ring)
( contains-subset-right-ideal-subset-Ring)
is-right-ideal-generated-by-subset-right-ideal-subset-Ring J K x H =
apply-universal-property-trunc-Prop H (subset-right-ideal-Ring R J x) P
where
P : subset-right-ideal-subset-Ring' x → is-in-right-ideal-Ring R J x
P (pair c refl) =
contains-right-formal-combinations-right-ideal-subset-Ring J K c

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

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


The subset relation is preserved by generating right ideals

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

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

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


The Galois connection S ↦ (S)

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

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

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


The reflective Galois connection S ↦ (S)

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

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

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

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

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


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

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

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

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

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

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


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

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

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

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

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

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


Properties

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

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

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

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

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

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


The operation S ↦ (S) preserves least upper bounds

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