Ideals of semirings
Content created by Egbert Rijke, Fredrik Bakke and Maša Žaucer
Created on 2023-03-18.
Last modified on 2023-06-08.
module ring-theory.ideals-semirings where
Imports
open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.propositions open import foundation.universe-levels open import group-theory.submonoids open import ring-theory.semirings open import ring-theory.subsets-semirings
Idea
An ideal (resp. a left/right ideal) of a semiring R is an additive
submodule of R that is closed under multiplication by elements of R (from
the left/right).
Note
This is the standard definition of ideals in semirings. However, such two-sided
ideals do not correspond uniquely to congruences on R. If we ask in addition
that the underlying additive submodule is normal, then we get unique
correspondence to congruences. We will call such ideals normal.
Definitions
Additive submonoids
module _ {l1 : Level} (R : Semiring l1) where is-additive-submonoid-Semiring : {l2 : Level} → subset-Semiring l2 R → UU (l1 ⊔ l2) is-additive-submonoid-Semiring = is-submonoid-Monoid (additive-monoid-Semiring R)
Left ideals
module _ {l1 : Level} (R : Semiring l1) where is-left-ideal-subset-Semiring : {l2 : Level} → subset-Semiring l2 R → UU (l1 ⊔ l2) is-left-ideal-subset-Semiring P = is-additive-submonoid-Semiring R P × is-closed-under-left-multiplication-subset-Semiring R P left-ideal-Semiring : (l : Level) {l1 : Level} (R : Semiring l1) → UU ((lsuc l) ⊔ l1) left-ideal-Semiring l R = Σ (subset-Semiring l R) (is-left-ideal-subset-Semiring R) module _ {l1 l2 : Level} (R : Semiring l1) (I : left-ideal-Semiring l2 R) where subset-left-ideal-Semiring : subset-Semiring l2 R subset-left-ideal-Semiring = pr1 I is-in-left-ideal-Semiring : type-Semiring R → UU l2 is-in-left-ideal-Semiring x = type-Prop (subset-left-ideal-Semiring x) type-left-ideal-Semiring : UU (l1 ⊔ l2) type-left-ideal-Semiring = type-subset-Semiring R subset-left-ideal-Semiring inclusion-left-ideal-Semiring : type-left-ideal-Semiring → type-Semiring R inclusion-left-ideal-Semiring = inclusion-subset-Semiring R subset-left-ideal-Semiring ap-inclusion-left-ideal-Semiring : (x y : type-left-ideal-Semiring) → x ＝ y → inclusion-left-ideal-Semiring x ＝ inclusion-left-ideal-Semiring y ap-inclusion-left-ideal-Semiring = ap-inclusion-subset-Semiring R subset-left-ideal-Semiring is-in-subset-inclusion-left-ideal-Semiring : (x : type-left-ideal-Semiring) → is-in-left-ideal-Semiring (inclusion-left-ideal-Semiring x) is-in-subset-inclusion-left-ideal-Semiring = is-in-subset-inclusion-subset-Semiring R subset-left-ideal-Semiring is-closed-under-eq-left-ideal-Semiring : {x y : type-Semiring R} → is-in-left-ideal-Semiring x → (x ＝ y) → is-in-left-ideal-Semiring y is-closed-under-eq-left-ideal-Semiring = is-closed-under-eq-subset-Semiring R subset-left-ideal-Semiring is-closed-under-eq-left-ideal-Semiring' : {x y : type-Semiring R} → is-in-left-ideal-Semiring y → (x ＝ y) → is-in-left-ideal-Semiring x is-closed-under-eq-left-ideal-Semiring' = is-closed-under-eq-subset-Semiring' R subset-left-ideal-Semiring is-left-ideal-subset-left-ideal-Semiring : is-left-ideal-subset-Semiring R subset-left-ideal-Semiring is-left-ideal-subset-left-ideal-Semiring = pr2 I is-additive-submonoid-left-ideal-Semiring : is-additive-submonoid-Semiring R subset-left-ideal-Semiring is-additive-submonoid-left-ideal-Semiring = pr1 is-left-ideal-subset-left-ideal-Semiring contains-zero-left-ideal-Semiring : is-in-left-ideal-Semiring (zero-Semiring R) contains-zero-left-ideal-Semiring = pr1 is-additive-submonoid-left-ideal-Semiring is-closed-under-addition-left-ideal-Semiring : is-closed-under-addition-subset-Semiring R subset-left-ideal-Semiring is-closed-under-addition-left-ideal-Semiring = pr2 is-additive-submonoid-left-ideal-Semiring is-closed-under-left-multiplication-left-ideal-Semiring : is-closed-under-left-multiplication-subset-Semiring R subset-left-ideal-Semiring is-closed-under-left-multiplication-left-ideal-Semiring = pr2 is-left-ideal-subset-left-ideal-Semiring
Right ideals
module _ {l1 : Level} (R : Semiring l1) where is-right-ideal-subset-Semiring : {l2 : Level} → subset-Semiring l2 R → UU (l1 ⊔ l2) is-right-ideal-subset-Semiring P = is-additive-submonoid-Semiring R P × is-closed-under-right-multiplication-subset-Semiring R P right-ideal-Semiring : (l : Level) {l1 : Level} (R : Semiring l1) → UU ((lsuc l) ⊔ l1) right-ideal-Semiring l R = Σ (subset-Semiring l R) (is-right-ideal-subset-Semiring R) module _ {l1 l2 : Level} (R : Semiring l1) (I : right-ideal-Semiring l2 R) where subset-right-ideal-Semiring : subset-Semiring l2 R subset-right-ideal-Semiring = pr1 I is-in-right-ideal-Semiring : type-Semiring R → UU l2 is-in-right-ideal-Semiring x = type-Prop (subset-right-ideal-Semiring x) type-right-ideal-Semiring : UU (l1 ⊔ l2) type-right-ideal-Semiring = type-subset-Semiring R subset-right-ideal-Semiring inclusion-right-ideal-Semiring : type-right-ideal-Semiring → type-Semiring R inclusion-right-ideal-Semiring = inclusion-subset-Semiring R subset-right-ideal-Semiring ap-inclusion-right-ideal-Semiring : (x y : type-right-ideal-Semiring) → x ＝ y → inclusion-right-ideal-Semiring x ＝ inclusion-right-ideal-Semiring y ap-inclusion-right-ideal-Semiring = ap-inclusion-subset-Semiring R subset-right-ideal-Semiring is-in-subset-inclusion-right-ideal-Semiring : (x : type-right-ideal-Semiring) → is-in-right-ideal-Semiring (inclusion-right-ideal-Semiring x) is-in-subset-inclusion-right-ideal-Semiring = is-in-subset-inclusion-subset-Semiring R subset-right-ideal-Semiring is-closed-under-eq-right-ideal-Semiring : {x y : type-Semiring R} → is-in-right-ideal-Semiring x → (x ＝ y) → is-in-right-ideal-Semiring y is-closed-under-eq-right-ideal-Semiring = is-closed-under-eq-subset-Semiring R subset-right-ideal-Semiring is-closed-under-eq-right-ideal-Semiring' : {x y : type-Semiring R} → is-in-right-ideal-Semiring y → (x ＝ y) → is-in-right-ideal-Semiring x is-closed-under-eq-right-ideal-Semiring' = is-closed-under-eq-subset-Semiring' R subset-right-ideal-Semiring is-right-ideal-subset-right-ideal-Semiring : is-right-ideal-subset-Semiring R subset-right-ideal-Semiring is-right-ideal-subset-right-ideal-Semiring = pr2 I is-additive-submonoid-right-ideal-Semiring : is-additive-submonoid-Semiring R subset-right-ideal-Semiring is-additive-submonoid-right-ideal-Semiring = pr1 is-right-ideal-subset-right-ideal-Semiring contains-zero-right-ideal-Semiring : is-in-right-ideal-Semiring (zero-Semiring R) contains-zero-right-ideal-Semiring = pr1 is-additive-submonoid-right-ideal-Semiring is-closed-under-addition-right-ideal-Semiring : is-closed-under-addition-subset-Semiring R subset-right-ideal-Semiring is-closed-under-addition-right-ideal-Semiring = pr2 is-additive-submonoid-right-ideal-Semiring is-closed-under-right-multiplication-right-ideal-Semiring : is-closed-under-right-multiplication-subset-Semiring R subset-right-ideal-Semiring is-closed-under-right-multiplication-right-ideal-Semiring = pr2 is-right-ideal-subset-right-ideal-Semiring
Two-sided ideals
is-ideal-subset-Semiring : {l1 l2 : Level} (R : Semiring l1) (P : subset-Semiring l2 R) → UU (l1 ⊔ l2) is-ideal-subset-Semiring R P = is-additive-submonoid-Semiring R P × ( is-closed-under-left-multiplication-subset-Semiring R P × is-closed-under-right-multiplication-subset-Semiring R P) ideal-Semiring : (l : Level) {l1 : Level} (R : Semiring l1) → UU ((lsuc l) ⊔ l1) ideal-Semiring l R = Σ (subset-Semiring l R) (is-ideal-subset-Semiring R) module _ {l1 l2 : Level} (R : Semiring l1) (I : ideal-Semiring l2 R) where subset-ideal-Semiring : subset-Semiring l2 R subset-ideal-Semiring = pr1 I is-in-ideal-Semiring : type-Semiring R → UU l2 is-in-ideal-Semiring = is-in-subset-Semiring R subset-ideal-Semiring is-prop-is-in-ideal-Semiring : (x : type-Semiring R) → is-prop (is-in-ideal-Semiring x) is-prop-is-in-ideal-Semiring = is-prop-is-in-subset-Semiring R subset-ideal-Semiring type-ideal-Semiring : UU (l1 ⊔ l2) type-ideal-Semiring = type-subset-Semiring R subset-ideal-Semiring inclusion-ideal-Semiring : type-ideal-Semiring → type-Semiring R inclusion-ideal-Semiring = inclusion-subset-Semiring R subset-ideal-Semiring ap-inclusion-ideal-Semiring : (x y : type-ideal-Semiring) → x ＝ y → inclusion-ideal-Semiring x ＝ inclusion-ideal-Semiring y ap-inclusion-ideal-Semiring = ap-inclusion-subset-Semiring R subset-ideal-Semiring is-in-subset-inclusion-ideal-Semiring : (x : type-ideal-Semiring) → is-in-ideal-Semiring (inclusion-ideal-Semiring x) is-in-subset-inclusion-ideal-Semiring = is-in-subset-inclusion-subset-Semiring R subset-ideal-Semiring is-closed-under-eq-ideal-Semiring : {x y : type-Semiring R} → is-in-ideal-Semiring x → (x ＝ y) → is-in-ideal-Semiring y is-closed-under-eq-ideal-Semiring = is-closed-under-eq-subset-Semiring R subset-ideal-Semiring is-closed-under-eq-ideal-Semiring' : {x y : type-Semiring R} → is-in-ideal-Semiring y → (x ＝ y) → is-in-ideal-Semiring x is-closed-under-eq-ideal-Semiring' = is-closed-under-eq-subset-Semiring' R subset-ideal-Semiring is-ideal-subset-ideal-Semiring : is-ideal-subset-Semiring R subset-ideal-Semiring is-ideal-subset-ideal-Semiring = pr2 I is-additive-submonoid-ideal-Semiring : is-additive-submonoid-Semiring R subset-ideal-Semiring is-additive-submonoid-ideal-Semiring = pr1 is-ideal-subset-ideal-Semiring contains-zero-ideal-Semiring : is-in-ideal-Semiring (zero-Semiring R) contains-zero-ideal-Semiring = pr1 is-additive-submonoid-ideal-Semiring is-closed-under-addition-ideal-Semiring : is-closed-under-addition-subset-Semiring R subset-ideal-Semiring is-closed-under-addition-ideal-Semiring = pr2 is-additive-submonoid-ideal-Semiring is-closed-under-left-multiplication-ideal-Semiring : is-closed-under-left-multiplication-subset-Semiring R subset-ideal-Semiring is-closed-under-left-multiplication-ideal-Semiring = pr1 (pr2 is-ideal-subset-ideal-Semiring) is-closed-under-right-multiplication-ideal-Semiring : is-closed-under-right-multiplication-subset-Semiring R subset-ideal-Semiring is-closed-under-right-multiplication-ideal-Semiring = pr2 (pr2 is-ideal-subset-ideal-Semiring) submonoid-ideal-Semiring : Submonoid l2 (additive-monoid-Semiring R) pr1 submonoid-ideal-Semiring = subset-ideal-Semiring pr1 (pr2 submonoid-ideal-Semiring) = contains-zero-ideal-Semiring pr2 (pr2 submonoid-ideal-Semiring) = is-closed-under-addition-ideal-Semiring
Recent changes
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).
- 2023-06-08. Egbert Rijke, Maša Žaucer and Fredrik Bakke. The Zariski locale of a commutative ring (#619).
- 2023-03-21. Fredrik Bakke. Formatting fixes (#530).
- 2023-03-19. Egbert Rijke. Refactoring ideals in semirings, rings, commutative semirings, and commutative rings; refactoring a corollary of the binomial theorem; constructing the nilradical of an ideal in a commutative ring (#525).
- 2023-03-18. Egbert Rijke and Maša Žaucer. Central elements in semigroups, monoids, groups, semirings, and rings; ideals; nilpotent elements in semirings, rings, commutative semirings, and commutative rings; the nilradical of a commutative ring (#516).