Ideals of semirings

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

@@ -16,6 +16,7 @@ open import foundation.propositions
 open import foundation.universe-levels
 
 open import ring-theory.ideals-semirings
+open import ring-theory.subsets-semirings
 ```
 
 </details>
@@ -103,7 +104,7 @@ module _
     is-ideal-subset-ideal-Semiring (semiring-Commutative-Semiring A) I
 
   is-additive-submonoid-ideal-Commutative-Semiring :
-    is-additive-submonoid-Semiring
+    is-additive-submonoid-subset-Semiring
       ( semiring-Commutative-Semiring A)
       ( subset-ideal-Commutative-Semiring)
   is-additive-submonoid-ideal-Commutative-Semiring =

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

@@ -52,12 +52,12 @@ is-closed-under-add-nilradical-Commutative-Semiring :
   {l : Level} (A : Commutative-Semiring l) →
   is-closed-under-addition-subset-Commutative-Semiring A
     ( subset-nilradical-Commutative-Semiring A)
-is-closed-under-add-nilradical-Commutative-Semiring A x y =
+is-closed-under-add-nilradical-Commutative-Semiring A =
   is-nilpotent-add-Semiring
     ( semiring-Commutative-Semiring A)
-    ( x)
-    ( y)
-    ( commutative-mul-Commutative-Semiring A x y)
+    ( _)
+    ( _)
+    ( commutative-mul-Commutative-Semiring A _ _)
 ```
 
 ### The nilradical is closed under multiplication with ring elements

src/group-theory/commutative-monoids.lagda.md

@@ -19,6 +19,8 @@ open import foundation.universe-levels
 
 open import group-theory.monoids
 open import group-theory.semigroups
+
+open import structured-types.magmas
 ```
 
 </details>
@@ -66,6 +68,10 @@ module _
   monoid-Commutative-Monoid : Monoid l
   monoid-Commutative-Monoid = pr1 M
 
+  unital-magma-Commutative-Monoid : Unital-Magma l
+  unital-magma-Commutative-Monoid =
+    unital-magma-Monoid monoid-Commutative-Monoid
+
   semigroup-Commutative-Monoid : Semigroup l
   semigroup-Commutative-Monoid = semigroup-Monoid monoid-Commutative-Monoid
 

src/group-theory/invertible-elements-monoids.lagda.md

@@ -19,6 +19,7 @@ open import foundation.injective-maps
 open import foundation.propositions
 open import foundation.sets
 open import foundation.subtypes
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import group-theory.monoids
@@ -289,9 +290,34 @@ module _
     left-unit-law-mul-Monoid M (unit-Monoid M)
   pr2 (pr2 is-invertible-element-unit-Monoid) =
     left-unit-law-mul-Monoid M (unit-Monoid M)
+
+  is-invertible-element-is-unit-Monoid :
+    (x : type-Monoid M) → unit-Monoid M ＝ x →
+    is-invertible-element-Monoid M x
+  is-invertible-element-is-unit-Monoid .(unit-Monoid M) refl =
+    is-invertible-element-unit-Monoid
+```
+
+### The inverse of an invertible element is invertible
+
+```agda
+module _
+  {l : Level} (M : Monoid l)
+  where
+
+  is-invertible-element-inv-is-invertible-element-Monoid :
+    {x : type-Monoid M} (H : is-invertible-element-Monoid M x) →
+    is-invertible-element-Monoid M (inv-is-invertible-element-Monoid M H)
+  pr1 (is-invertible-element-inv-is-invertible-element-Monoid {x} H) = x
+  pr1 (pr2 (is-invertible-element-inv-is-invertible-element-Monoid H)) =
+    is-left-inverse-inv-is-invertible-element-Monoid M H
+  pr2 (pr2 (is-invertible-element-inv-is-invertible-element-Monoid H)) =
+    is-right-inverse-inv-is-invertible-element-Monoid M H
 ```
 
-### Invertible elements are closed under multiplication
+### If two of the three elements `x`, `y`, and `xy` are invertible, then so is the third
+
+#### Invertible elements are closed under multiplication
 
 ```agda
 module _
@@ -349,21 +375,52 @@ module _
         ( is-left-invertible-is-invertible-element-Monoid M y K))
 ```
 
-### The inverse of an invertible element is invertible
+#### If `y` and `xy` are invertible, then so is `x`
 
 ```agda
 module _
-  {l : Level} (M : Monoid l)
+  {l : Level} (M : Monoid l) (x y : type-Monoid M)
   where
 
-  is-invertible-element-inv-is-invertible-element-Monoid :
-    {x : type-Monoid M} (H : is-invertible-element-Monoid M x) →
-    is-invertible-element-Monoid M (inv-is-invertible-element-Monoid M H)
-  pr1 (is-invertible-element-inv-is-invertible-element-Monoid {x} H) = x
-  pr1 (pr2 (is-invertible-element-inv-is-invertible-element-Monoid H)) =
-    is-left-inverse-inv-is-invertible-element-Monoid M H
-  pr2 (pr2 (is-invertible-element-inv-is-invertible-element-Monoid H)) =
-    is-right-inverse-inv-is-invertible-element-Monoid M H
+  is-invertible-element-left-factor-Monoid :
+    is-invertible-element-Monoid M y →
+    is-invertible-element-Monoid M (mul-Monoid M x y) →
+    is-invertible-element-Monoid M x
+  is-invertible-element-left-factor-Monoid H@(y' , Ly , Ry) K =
+    tr
+      ( is-invertible-element-Monoid M)
+      ( associative-mul-Monoid M x y y' ∙
+        ap (mul-Monoid M x) Ly ∙
+        right-unit-law-mul-Monoid M x)
+      ( is-invertible-element-mul-Monoid M
+        ( mul-Monoid M x y)
+        ( y')
+        ( K)
+        ( is-invertible-element-inv-is-invertible-element-Monoid M H))
+```
+
+#### If `x` and `xy` are invertible, then so is `y`
+
+```agda
+module _
+  {l : Level} (M : Monoid l) (x y : type-Monoid M)
+  where
+
+  is-invertible-element-right-factor-Monoid :
+    is-invertible-element-Monoid M x →
+    is-invertible-element-Monoid M (mul-Monoid M x y) →
+    is-invertible-element-Monoid M y
+  is-invertible-element-right-factor-Monoid H@(x' , Lx , Rx) K =
+    tr
+      ( is-invertible-element-Monoid M)
+      ( inv (associative-mul-Monoid M x' x y) ∙
+        ap (mul-Monoid' M y) Rx ∙
+        left-unit-law-mul-Monoid M y)
+      ( is-invertible-element-mul-Monoid M
+        ( x')
+        ( mul-Monoid M x y)
+        ( is-invertible-element-inv-is-invertible-element-Monoid M H)
+        ( K))
 ```
 
 ### An element is invertible if and only if multiplying by it is an equivalence

src/group-theory/monoids.lagda.md

@@ -19,6 +19,7 @@ open import foundation.universe-levels
 open import group-theory.semigroups
 
 open import structured-types.h-spaces
+open import structured-types.magmas
 open import structured-types.wild-monoids
 ```
 
@@ -48,6 +49,9 @@ module _
   semigroup-Monoid : Semigroup l
   semigroup-Monoid = pr1 M
 
+  magma-Monoid : Magma l
+  magma-Monoid = magma-Semigroup semigroup-Monoid
+
   is-unital-Monoid : is-unital-Semigroup semigroup-Monoid
   is-unital-Monoid = pr2 M
 
@@ -94,6 +98,10 @@ module _
   right-unit-law-mul-Monoid : (x : type-Monoid) → mul-Monoid x unit-Monoid ＝ x
   right-unit-law-mul-Monoid = pr2 (pr2 has-unit-Monoid)
 
+  unital-magma-Monoid : Unital-Magma l
+  pr1 unital-magma-Monoid = magma-Monoid
+  pr2 unital-magma-Monoid = has-unit-Monoid
+
   left-swap-mul-Monoid :
     {x y z : type-Monoid} → mul-Monoid x y ＝ mul-Monoid y x →
     mul-Monoid x (mul-Monoid y z) ＝

src/group-theory/powers-of-elements-monoids.lagda.md

@@ -25,9 +25,23 @@ open import group-theory.monoids
 
 ## Idea
 
-The **power operation** on a [monoid](group-theory.monoids.md) is the map
-`n x ↦ xⁿ`, which is defined by [iteratively](foundation.iterating-functions.md)
-multiplying `x` with itself `n` times.
+The {{#concept "power operation" Disambiguation="monoid" Agda=power-Monoid}} on
+a [monoid](group-theory.monoids.md) is the map `n x ↦ xⁿ`, which is defined by
+[iteratively](foundation.iterating-functions.md) multiplying `x` with itself `n`
+times.
+
+We define the power operation such that the following equalities hold by
+definition:
+
+```text
+  x⁰ ≐ 1
+  x¹ ≐ x
+  xⁿ⁺² ≐ xⁿ⁺¹ · x.
+```
+
+This setup requires one extra step for the most basic properties, but it avoids
+having a superficial factor of the multiplicative unit in its definition for
+`n ≥ 1`.
 
 ## Definitions
 

src/group-theory/semigroups.lagda.md

@@ -13,6 +13,8 @@ open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.sets
 open import foundation.universe-levels
+
+open import structured-types.magmas
 ```
 
 </details>
@@ -99,6 +101,10 @@ module _
     ( associative-mul-Semigroup _ _ _) ∙
     ( ap (mul-Semigroup _) (left-swap-mul-Semigroup H)) ∙
     ( inv (associative-mul-Semigroup _ _ _))
+
+  magma-Semigroup : Magma l
+  pr1 magma-Semigroup = type-Semigroup
+  pr2 magma-Semigroup = mul-Semigroup
 ```
 
 ### The structure of a semigroup

src/ring-theory.lagda.md

@@ -46,11 +46,19 @@ open import ring-theory.joins-left-ideals-rings public
 open import ring-theory.joins-right-ideals-rings public
 open import ring-theory.kernels-of-ring-homomorphisms public
 open import ring-theory.left-ideals-generated-by-subsets-rings public
+open import ring-theory.left-ideals-generated-by-subsets-semirings public
 open import ring-theory.left-ideals-rings public
+open import ring-theory.left-ideals-semirings public
+open import ring-theory.left-linear-combinations-of-elements-rings public
+open import ring-theory.left-linear-combinations-of-elements-semirings public
+open import ring-theory.linear-combinations-of-elements-rings public
+open import ring-theory.linear-combinations-of-elements-semirings public
 open import ring-theory.local-rings public
 open import ring-theory.localizations-rings public
 open import ring-theory.maximal-ideals-rings public
 open import ring-theory.modules-rings public
+open import ring-theory.monoids-with-left-semiring-actions public
+open import ring-theory.monoids-with-right-semiring-actions public
 open import ring-theory.multiples-of-elements-rings public
 open import ring-theory.multiplicative-orders-of-units-rings public
 open import ring-theory.nil-ideals-rings public
@@ -60,11 +68,14 @@ open import ring-theory.opposite-rings public
 open import ring-theory.poset-of-cyclic-rings public
 open import ring-theory.poset-of-ideals-rings public
 open import ring-theory.poset-of-left-ideals-rings public
+open import ring-theory.poset-of-left-ideals-semirings public
 open import ring-theory.poset-of-right-ideals-rings public
+open import ring-theory.poset-of-right-ideals-semirings public
 open import ring-theory.powers-of-elements-rings public
 open import ring-theory.powers-of-elements-semirings public
 open import ring-theory.precategory-of-rings public
 open import ring-theory.precategory-of-semirings public
+open import ring-theory.principal-ideals-semirings public
 open import ring-theory.products-ideals-rings public
 open import ring-theory.products-left-ideals-rings public
 open import ring-theory.products-right-ideals-rings public
@@ -73,11 +84,16 @@ open import ring-theory.products-subsets-rings public
 open import ring-theory.quotient-rings public
 open import ring-theory.radical-ideals-rings public
 open import ring-theory.right-ideals-generated-by-subsets-rings public
+open import ring-theory.right-ideals-generated-by-subsets-semirings public
 open import ring-theory.right-ideals-rings public
+open import ring-theory.right-ideals-semirings public
+open import ring-theory.right-linear-combinations-of-elements-rings public
+open import ring-theory.right-linear-combinations-of-elements-semirings public
 open import ring-theory.rings public
 open import ring-theory.semirings public
 open import ring-theory.subsets-rings public
 open import ring-theory.subsets-semirings public
+open import ring-theory.subtractive-ideals-semirings public
 open import ring-theory.sums-rings public
 open import ring-theory.sums-semirings public
 open import ring-theory.transporting-ring-structure-along-isomorphisms-abelian-groups public

src/ring-theory/full-ideals-rings.lagda.md

@@ -96,8 +96,10 @@ module _
 
   is-left-ideal-full-ideal-Ring :
     is-left-ideal-subset-Ring R subset-full-ideal-Ring
-  pr1 is-left-ideal-full-ideal-Ring =
-    is-additive-subgroup-full-ideal-Ring
+  pr1 (pr1 is-left-ideal-full-ideal-Ring) =
+    contains-zero-full-ideal-Ring
+  pr2 (pr1 is-left-ideal-full-ideal-Ring) {x} {y} =
+    is-closed-under-addition-full-ideal-Ring {x} {y}
   pr2 is-left-ideal-full-ideal-Ring =
     is-closed-under-left-multiplication-full-ideal-Ring
 

src/ring-theory/groups-of-units-rings.lagda.md

@@ -9,8 +9,10 @@ module ring-theory.groups-of-units-rings where
 ```agda
 open import category-theory.functors-large-precategories
 
+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 group-theory.cores-monoids
@@ -32,15 +34,18 @@ open import ring-theory.rings
 
 ## Idea
 
-The **group of units** of a [ring](ring-theory.rings.md) `R` is the
-[group](group-theory.groups.md) consisting of all the
+The {{#concept "group of units" Disambiguation="ring" WD="unit" WDID=Q118084}}
+of a [ring](ring-theory.rings.md) `R` is the [group](group-theory.groups.md)
+consisting of all the
 [invertible elements](ring-theory.invertible-elements-rings.md) in `R`.
 Equivalently, the group of units of `R` is the
 [core](group-theory.cores-monoids.md) of the multiplicative
 [monoid](group-theory.monoids.md) of `R`.
 
 ## Definitions
 
+### The group of units of a ring
+
 ```agda
 module _
   {l : Level} (R : Ring l)
@@ -136,6 +141,13 @@ module _
   inclusion-group-of-units-Ring =
     inclusion-core-Monoid (multiplicative-monoid-Ring R)
 
+  is-invertible-element-inclusion-group-of-units-Ring :
+    (x : type-group-of-units-Ring) →
+    is-invertible-element-Ring R
+      ( inclusion-group-of-units-Ring x)
+  is-invertible-element-inclusion-group-of-units-Ring =
+    is-in-subtype-inclusion-subtype subtype-group-of-units-Ring
+
   preserves-mul-inclusion-group-of-units-Ring :
     {x y : type-group-of-units-Ring} →
     inclusion-group-of-units-Ring (mul-group-of-units-Ring x y) ＝
@@ -210,7 +222,7 @@ module _
       ( hom-multiplicative-monoid-hom-Ring R S f)
 ```
 
-#### The functorial laws of `group-of-units-Ring`
+#### The functorial laws of the group-of-units functor
 
 ```agda
 module _
@@ -245,7 +257,7 @@ module _
       ( hom-multiplicative-monoid-hom-Ring R S f)
 ```
 
-#### The functor `group-of-units-Ring`
+#### The group-of-units functor
 
 ```agda
 group-of-units-ring-functor-Large-Precategory :
@@ -266,3 +278,21 @@ preserves-id-functor-Large-Precategory
   group-of-units-ring-functor-Large-Precategory {X = R} =
   preserves-id-hom-group-of-units-hom-Ring R
 ```
+
+### Negatives of units
+
+```agda
+module _
+  {l : Level} (R : Ring l)
+  where
+
+  neg-group-of-units-Ring :
+    type-group-of-units-Ring R → type-group-of-units-Ring R
+  pr1 (neg-group-of-units-Ring (x , H)) = neg-Ring R x
+  pr2 (neg-group-of-units-Ring (x , H)) = is-invertible-element-neg-Ring R x H
+
+  neg-unit-group-of-units-Ring :
+    type-group-of-units-Ring R
+  neg-unit-group-of-units-Ring =
+    neg-group-of-units-Ring (unit-group-of-units-Ring R)
+```