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)

Co-authored-by: Masa Zaucer <masa.zaucer@student.fmf.uni-lj.si>

src/commutative-algebra.lagda.md

@@ -17,15 +17,18 @@ open import commutative-algebra.function-commutative-semirings public
 open import commutative-algebra.gaussian-integers public
 open import commutative-algebra.homomorphisms-commutative-rings public
 open import commutative-algebra.ideals-commutative-rings public
+open import commutative-algebra.ideals-commutative-semirings public
 open import commutative-algebra.integral-domains public
 open import commutative-algebra.invertible-elements-commutative-rings public
 open import commutative-algebra.isomorphisms-commutative-rings public
 open import commutative-algebra.local-commutative-rings public
 open import commutative-algebra.maximal-ideals-commutative-rings public
 open import commutative-algebra.nilradical-commutative-rings public
+open import commutative-algebra.nilradicals-commutative-semirings public
 open import commutative-algebra.powers-of-elements-commutative-rings public
 open import commutative-algebra.powers-of-elements-commutative-semirings public
 open import commutative-algebra.prime-ideals-commutative-rings public
+open import commutative-algebra.subsets-commutative-semirings public
 open import commutative-algebra.sums-commutative-rings public
 open import commutative-algebra.sums-commutative-semirings public
 open import commutative-algebra.zariski-topology public

src/commutative-algebra/commutative-rings.lagda.md

@@ -14,6 +14,7 @@ open import elementary-number-theory.natural-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.identity-types
+open import foundation.interchange-law
 open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
@@ -259,6 +260,20 @@ module _
   commutative-semiring-Commutative-Ring : Commutative-Semiring l
   pr1 commutative-semiring-Commutative-Ring = semiring-Commutative-Ring
   pr2 commutative-semiring-Commutative-Ring = commutative-mul-Commutative-Ring
+
+  interchange-mul-mul-Commutative-Ring :
+    (x y z w : type-Commutative-Ring) →
+    mul-Commutative-Ring
+      ( mul-Commutative-Ring x y)
+      ( mul-Commutative-Ring z w) ＝
+    mul-Commutative-Ring
+      ( mul-Commutative-Ring x z)
+      ( mul-Commutative-Ring y w)
+  interchange-mul-mul-Commutative-Ring =
+    interchange-law-commutative-and-associative
+      mul-Commutative-Ring
+      commutative-mul-Commutative-Ring
+      associative-mul-Commutative-Ring
 ```
 
 ### Scalar multiplication of elements of a commutative ring by natural numbers
@@ -277,6 +292,19 @@ module _
   ap-mul-nat-scalar-Commutative-Ring =
     ap-mul-nat-scalar-Ring ring-Commutative-Ring
 
+  left-zero-law-mul-nat-scalar-Commutative-Ring :
+    (x : type-Commutative-Ring) →
+    mul-nat-scalar-Commutative-Ring 0 x ＝ zero-Commutative-Ring
+  left-zero-law-mul-nat-scalar-Commutative-Ring =
+    left-zero-law-mul-nat-scalar-Ring ring-Commutative-Ring
+
+  right-zero-law-mul-nat-scalar-Commutative-Ring :
+    (n : ℕ) →
+    mul-nat-scalar-Commutative-Ring n zero-Commutative-Ring ＝
+    zero-Commutative-Ring
+  right-zero-law-mul-nat-scalar-Commutative-Ring =
+    right-zero-law-mul-nat-scalar-Ring ring-Commutative-Ring
+
   left-unit-law-mul-nat-scalar-Commutative-Ring :
     (x : type-Commutative-Ring) →
     mul-nat-scalar-Commutative-Ring 1 x ＝ x
@@ -315,3 +343,20 @@ module _
   right-distributive-mul-nat-scalar-add-Commutative-Ring =
     right-distributive-mul-nat-scalar-add-Ring ring-Commutative-Ring
 ```
+
+### Computing multiplication with minus one in a ring
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l)
+  where
+
+  neg-one-Commutative-Ring : type-Commutative-Ring R
+  neg-one-Commutative-Ring = neg-one-Ring (ring-Commutative-Ring R)
+
+  mul-neg-one-Commutative-Ring :
+    (x : type-Commutative-Ring R) →
+    mul-Commutative-Ring R neg-one-Commutative-Ring x ＝
+    neg-Commutative-Ring R x
+  mul-neg-one-Commutative-Ring = mul-neg-one-Ring (ring-Commutative-Ring R)
+```

src/commutative-algebra/commutative-semirings.lagda.md

@@ -265,6 +265,19 @@ module _
   ap-mul-nat-scalar-Commutative-Semiring =
     ap-mul-nat-scalar-Semiring semiring-Commutative-Semiring
 
+  left-zero-law-mul-nat-scalar-Commutative-Semiring :
+    (x : type-Commutative-Semiring) →
+    mul-nat-scalar-Commutative-Semiring 0 x ＝ zero-Commutative-Semiring
+  left-zero-law-mul-nat-scalar-Commutative-Semiring =
+    left-zero-law-mul-nat-scalar-Semiring semiring-Commutative-Semiring
+
+  right-zero-law-mul-nat-scalar-Commutative-Semiring :
+    (n : ℕ) →
+    mul-nat-scalar-Commutative-Semiring n zero-Commutative-Semiring ＝
+    zero-Commutative-Semiring
+  right-zero-law-mul-nat-scalar-Commutative-Semiring =
+    right-zero-law-mul-nat-scalar-Semiring semiring-Commutative-Semiring
+
   left-unit-law-mul-nat-scalar-Commutative-Semiring :
     (x : type-Commutative-Semiring) →
     mul-nat-scalar-Commutative-Semiring 1 x ＝ x

src/commutative-algebra/ideals-commutative-rings.lagda.md

@@ -10,6 +10,7 @@ module commutative-algebra.ideals-commutative-rings where
 open import commutative-algebra.commutative-rings
 
 open import foundation.dependent-pair-types
+open import foundation.identity-types
 open import foundation.propositions
 open import foundation.subtypes
 open import foundation.universe-levels
@@ -44,6 +45,12 @@ module _
   is-prop-is-in-subset-Commutative-Ring =
     is-prop-is-in-subtype S
 
+  is-closed-under-eq-subset-Commutative-Ring :
+    {x y : type-Commutative-Ring R} →
+    is-in-subset-Commutative-Ring x → x ＝ y → is-in-subset-Commutative-Ring y
+  is-closed-under-eq-subset-Commutative-Ring =
+    is-closed-under-eq-subtype S
+
   type-subset-Commutative-Ring : UU (l1 ⊔ l2)
   type-subset-Commutative-Ring = type-subtype S
 
@@ -65,6 +72,21 @@ module _
   {l1 l2 : Level} (R : Commutative-Ring l1) (S : subset-Commutative-Ring l2 R)
   where
 
+  contains-zero-subset-Commutative-Ring : UU l2
+  contains-zero-subset-Commutative-Ring =
+    is-in-subset-Commutative-Ring R S (zero-Commutative-Ring R)
+
+  is-closed-under-add-subset-Commutative-Ring : UU (l1 ⊔ l2)
+  is-closed-under-add-subset-Commutative-Ring =
+    (x y : type-Commutative-Ring R) →
+    is-in-subset-Commutative-Ring R S x → is-in-subset-Commutative-Ring R S y →
+    is-in-subset-Commutative-Ring R S (add-Commutative-Ring R x y)
+
+  is-closed-under-neg-subset-Commutative-Ring : UU (l1 ⊔ l2)
+  is-closed-under-neg-subset-Commutative-Ring =
+    (x : type-Commutative-Ring R) → is-in-subset-Commutative-Ring R S x →
+    is-in-subset-Commutative-Ring R S (neg-Commutative-Ring R x)
+
   is-closed-under-mul-left-subset-Commutative-Ring : UU (l1 ⊔ l2)
   is-closed-under-mul-left-subset-Commutative-Ring =
     is-closed-under-mul-left-subset-Ring (ring-Commutative-Ring R) S
@@ -145,4 +167,38 @@ module _
     is-closed-under-mul-right-two-sided-ideal-Ring
       ( ring-Commutative-Ring R)
       ( I)
+
+ideal-left-ideal-Commutative-Ring :
+  {l1 l2 : Level} (R : Commutative-Ring l1) (S : subset-Commutative-Ring l2 R) →
+  contains-zero-subset-Commutative-Ring R S →
+  is-closed-under-add-subset-Commutative-Ring R S →
+  is-closed-under-neg-subset-Commutative-Ring R S →
+  is-closed-under-mul-left-subset-Commutative-Ring R S →
+  ideal-Commutative-Ring l2 R
+pr1 (ideal-left-ideal-Commutative-Ring R S z a n m) = S
+pr1 (pr1 (pr2 (ideal-left-ideal-Commutative-Ring R S z a n m))) = z
+pr1 (pr2 (pr1 (pr2 (ideal-left-ideal-Commutative-Ring R S z a n m)))) = a
+pr2 (pr2 (pr1 (pr2 (ideal-left-ideal-Commutative-Ring R S z a n m)))) = n
+pr1 (pr2 (pr2 (ideal-left-ideal-Commutative-Ring R S z a n m))) = m
+pr2 (pr2 (pr2 (ideal-left-ideal-Commutative-Ring R S z a n m))) x y H =
+  is-closed-under-eq-subset-Commutative-Ring R S
+    ( m y x H)
+    ( commutative-mul-Commutative-Ring R y x)
+
+ideal-right-ideal-Commutative-Ring :
+  {l1 l2 : Level} (R : Commutative-Ring l1) (S : subset-Commutative-Ring l2 R) →
+  contains-zero-subset-Commutative-Ring R S →
+  is-closed-under-add-subset-Commutative-Ring R S →
+  is-closed-under-neg-subset-Commutative-Ring R S →
+  is-closed-under-mul-right-subset-Commutative-Ring R S →
+  ideal-Commutative-Ring l2 R
+pr1 (ideal-right-ideal-Commutative-Ring R S z a n m) = S
+pr1 (pr1 (pr2 (ideal-right-ideal-Commutative-Ring R S z a n m))) = z
+pr1 (pr2 (pr1 (pr2 (ideal-right-ideal-Commutative-Ring R S z a n m)))) = a
+pr2 (pr2 (pr1 (pr2 (ideal-right-ideal-Commutative-Ring R S z a n m)))) = n
+pr1 (pr2 (pr2 (ideal-right-ideal-Commutative-Ring R S z a n m))) x y H =
+  is-closed-under-eq-subset-Commutative-Ring R S
+    ( m y x H)
+    ( commutative-mul-Commutative-Ring R y x)
+pr2 (pr2 (pr2 (ideal-right-ideal-Commutative-Ring R S z a n m))) = m
 ```

src/commutative-algebra/ideals-commutative-semirings.lagda.md

@@ -0,0 +1,164 @@
+# Ideals in commutative semirings
+
+```agda
+module commutative-algebra.ideals-commutative-semirings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-semirings
+open import commutative-algebra.subsets-commutative-semirings
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import ring-theory.ideals-semirings
+open import ring-theory.subsets-semirings
+```
+
+</details>
+
+## Idea
+
+An ideal in a commutative semiring is a two-sided ideal in the underlying
+semiring.
+
+## Definitions
+
+### Ideals in commutative rings
+
+```agda
+module _
+  {l1 l2 : Level} (R : Commutative-Semiring l1)
+  (S : subset-Commutative-Semiring l2 R)
+  where
+
+  is-closed-under-add-subset-Commutative-Semiring : UU (l1 ⊔ l2)
+  is-closed-under-add-subset-Commutative-Semiring =
+    (x y : type-Commutative-Semiring R) →
+    is-in-subset-Commutative-Semiring R S x →
+    is-in-subset-Commutative-Semiring R S y →
+    is-in-subset-Commutative-Semiring R S (add-Commutative-Semiring R x y)
+
+  is-closed-under-mul-left-subset-Commutative-Semiring : UU (l1 ⊔ l2)
+  is-closed-under-mul-left-subset-Commutative-Semiring =
+    is-closed-under-mul-left-subset-Semiring (semiring-Commutative-Semiring R) S
+
+  is-closed-under-mul-right-subset-Commutative-Semiring : UU (l1 ⊔ l2)
+  is-closed-under-mul-right-subset-Commutative-Semiring =
+    is-closed-under-mul-right-subset-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( S)
+
+  is-ideal-subset-Commutative-Semiring : UU (l1 ⊔ l2)
+  is-ideal-subset-Commutative-Semiring =
+    is-two-sided-ideal-subset-Semiring (semiring-Commutative-Semiring R) S
+
+ideal-Commutative-Semiring :
+  {l1 : Level} (l2 : Level) → Commutative-Semiring l1 → UU (l1 ⊔ lsuc l2)
+ideal-Commutative-Semiring l2 R =
+  two-sided-ideal-Semiring l2 (semiring-Commutative-Semiring R)
+
+module _
+  {l1 l2 : Level} (R : Commutative-Semiring l1)
+  (I : ideal-Commutative-Semiring l2 R)
+  where
+
+  subset-ideal-Commutative-Semiring : subset-Commutative-Semiring l2 R
+  subset-ideal-Commutative-Semiring = pr1 I
+
+  is-in-ideal-Commutative-Semiring : type-Commutative-Semiring R → UU l2
+  is-in-ideal-Commutative-Semiring x =
+    type-Prop (subset-ideal-Commutative-Semiring x)
+
+  type-ideal-Commutative-Semiring : UU (l1 ⊔ l2)
+  type-ideal-Commutative-Semiring =
+    type-subset-Commutative-Semiring R subset-ideal-Commutative-Semiring
+
+  inclusion-ideal-Commutative-Semiring :
+    type-ideal-Commutative-Semiring → type-Commutative-Semiring R
+  inclusion-ideal-Commutative-Semiring =
+    inclusion-subset-Commutative-Semiring R subset-ideal-Commutative-Semiring
+
+  is-ideal-subset-ideal-Commutative-Semiring :
+    is-ideal-subset-Commutative-Semiring R subset-ideal-Commutative-Semiring
+  is-ideal-subset-ideal-Commutative-Semiring =
+    is-two-sided-ideal-subset-two-sided-ideal-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( I)
+
+  is-additive-submonoid-ideal-Commutative-Semiring :
+    is-additive-submonoid-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( subset-ideal-Commutative-Semiring)
+  is-additive-submonoid-ideal-Commutative-Semiring =
+    is-additive-submonoid-two-sided-ideal-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( I)
+
+  contains-zero-ideal-Commutative-Semiring :
+    is-in-ideal-Commutative-Semiring (zero-Commutative-Semiring R)
+  contains-zero-ideal-Commutative-Semiring =
+    contains-zero-two-sided-ideal-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( I)
+
+  is-closed-under-add-ideal-Commutative-Semiring :
+    {x y : type-Commutative-Semiring R} →
+    is-in-ideal-Commutative-Semiring x → is-in-ideal-Commutative-Semiring y →
+    is-in-ideal-Commutative-Semiring (add-Commutative-Semiring R x y)
+  is-closed-under-add-ideal-Commutative-Semiring H K =
+    pr2 is-additive-submonoid-ideal-Commutative-Semiring _ _ H K
+
+  is-closed-under-mul-left-ideal-Commutative-Semiring :
+    is-closed-under-mul-left-subset-Commutative-Semiring R
+      subset-ideal-Commutative-Semiring
+  is-closed-under-mul-left-ideal-Commutative-Semiring =
+    is-closed-under-mul-left-two-sided-ideal-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( I)
+
+  is-closed-under-mul-right-ideal-Commutative-Semiring :
+    is-closed-under-mul-right-subset-Commutative-Semiring R
+      subset-ideal-Commutative-Semiring
+  is-closed-under-mul-right-ideal-Commutative-Semiring =
+    is-closed-under-mul-right-two-sided-ideal-Semiring
+      ( semiring-Commutative-Semiring R)
+      ( I)
+
+ideal-left-ideal-Commutative-Semiring :
+  {l1 l2 : Level} (R : Commutative-Semiring l1)
+  (S : subset-Commutative-Semiring l2 R) →
+  contains-zero-subset-Commutative-Semiring R S →
+  is-closed-under-add-subset-Commutative-Semiring R S →
+  is-closed-under-mul-left-subset-Commutative-Semiring R S →
+  ideal-Commutative-Semiring l2 R
+pr1 (ideal-left-ideal-Commutative-Semiring R S z a m) = S
+pr1 (pr1 (pr2 (ideal-left-ideal-Commutative-Semiring R S z a m))) = z
+pr2 (pr1 (pr2 (ideal-left-ideal-Commutative-Semiring R S z a m))) = a
+pr1 (pr2 (pr2 (ideal-left-ideal-Commutative-Semiring R S z a m))) = m
+pr2 (pr2 (pr2 (ideal-left-ideal-Commutative-Semiring R S z a m))) x y H =
+  is-closed-under-eq-subset-Commutative-Semiring R S
+    ( m y x H)
+    ( commutative-mul-Commutative-Semiring R y x)
+
+ideal-right-ideal-Commutative-Semiring :
+  {l1 l2 : Level} (R : Commutative-Semiring l1)
+  (S : subset-Commutative-Semiring l2 R) →
+  contains-zero-subset-Commutative-Semiring R S →
+  is-closed-under-add-subset-Commutative-Semiring R S →
+  is-closed-under-mul-right-subset-Commutative-Semiring R S →
+  ideal-Commutative-Semiring l2 R
+pr1 (ideal-right-ideal-Commutative-Semiring R S z a m) = S
+pr1 (pr1 (pr2 (ideal-right-ideal-Commutative-Semiring R S z a m))) = z
+pr2 (pr1 (pr2 (ideal-right-ideal-Commutative-Semiring R S z a m))) = a
+pr1 (pr2 (pr2 (ideal-right-ideal-Commutative-Semiring R S z a m))) x y H =
+  is-closed-under-eq-subset-Commutative-Semiring R S
+    ( m y x H)
+    ( commutative-mul-Commutative-Semiring R y x)
+pr2 (pr2 (pr2 (ideal-right-ideal-Commutative-Semiring R S z a m))) = m
+```