diff --git a/src/commutative-algebra.lagda.md b/src/commutative-algebra.lagda.md
index 4143d4220b..f8d5216396 100644
--- a/src/commutative-algebra.lagda.md
+++ b/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
diff --git a/src/commutative-algebra/commutative-rings.lagda.md b/src/commutative-algebra/commutative-rings.lagda.md
index 5650fc7aff..9af9baf1c0 100644
--- a/src/commutative-algebra/commutative-rings.lagda.md
+++ b/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)
+```
diff --git a/src/commutative-algebra/commutative-semirings.lagda.md b/src/commutative-algebra/commutative-semirings.lagda.md
index 86e8360c84..dbad014bd9 100644
--- a/src/commutative-algebra/commutative-semirings.lagda.md
+++ b/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
diff --git a/src/commutative-algebra/ideals-commutative-rings.lagda.md b/src/commutative-algebra/ideals-commutative-rings.lagda.md
index 67d1f1670c..17c88fe924 100644
--- a/src/commutative-algebra/ideals-commutative-rings.lagda.md
+++ b/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
```
diff --git a/src/commutative-algebra/ideals-commutative-semirings.lagda.md b/src/commutative-algebra/ideals-commutative-semirings.lagda.md
new file mode 100644
index 0000000000..8b1de1edd3
--- /dev/null
+++ b/src/commutative-algebra/ideals-commutative-semirings.lagda.md
@@ -0,0 +1,164 @@
+# Ideals in commutative semirings
+
+```agda
+module commutative-algebra.ideals-commutative-semirings where
+```
+
+Imports
+
+```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
+```
+
+Imports
```agda
+open import commutative-algebra.binomial-theorem-commutative-rings
open import commutative-algebra.commutative-rings
open import commutative-algebra.ideals-commutative-rings
+open import commutative-algebra.powers-of-elements-commutative-rings
+open import commutative-algebra.sums-commutative-rings
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.binomial-coefficients
+open import elementary-number-theory.distance-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.propositional-truncations
+open import foundation.subtypes
open import foundation.universe-levels
open import ring-theory.nilpotent-elements-rings
+
+open import univalent-combinatorics.coproduct-types
+open import univalent-combinatorics.standard-finite-types
```
Imports
+
+```agda
+open import commutative-algebra.commutative-semirings
+open import commutative-algebra.subsets-commutative-semirings
+
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import ring-theory.nilpotent-elements-semirings
+```
+
+Imports
+
+```agda
+open import commutative-algebra.commutative-semirings
+
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import ring-theory.subsets-semirings
+```
+
+Imports
+
+```agda
+open import elementary-number-theory.divisibility-natural-numbers
+open import elementary-number-theory.modular-arithmetic-standard-finite-types
+open import elementary-number-theory.natural-numbers
+
+open import foundation.decidable-types
+open import foundation.dependent-pair-types
+open import foundation.functions
+open import foundation.identity-types
+open import foundation.negation
+open import foundation.universe-levels
+```
+
+
+
+## Idea
+
+Parity partitions the natural numbers into two classes: the even and the odd
+natural numbers. Even natural numbers are those that are divisible by two, and
+odd natural numbers are those that aren't.
+
+## Definition
+
+```agda
+is-even-ℕ : ℕ → UU lzero
+is-even-ℕ n = div-ℕ 2 n
+
+is-odd-ℕ : ℕ → UU lzero
+is-odd-ℕ n = ¬ (is-even-ℕ n)
+```
+
+## Properties
+
+### Being even or odd is decidable
+
+```agda
+is-decidable-is-even-ℕ : (x : ℕ) → is-decidable (is-even-ℕ x)
+is-decidable-is-even-ℕ x = is-decidable-div-ℕ 2 x
+
+is-decidable-is-odd-ℕ : (x : ℕ) → is-decidable (is-odd-ℕ x)
+is-decidable-is-odd-ℕ x = is-decidable-neg (is-decidable-is-even-ℕ x)
+```
+
+### `0` is an even natural number
+
+```agda
+is-even-zero-ℕ : is-even-ℕ 0
+is-even-zero-ℕ = div-zero-ℕ 2
+
+is-odd-one-ℕ : is-odd-ℕ 1
+is-odd-one-ℕ H = Eq-eq-ℕ (is-one-div-one-ℕ 2 H)
+```
+
+### A natural number `x` is even if and only if `x + 2` is even
+
+```agda
+is-even-is-even-succ-succ-ℕ :
+ (n : ℕ) → is-even-ℕ (succ-ℕ (succ-ℕ n)) → is-even-ℕ n
+pr1 (is-even-is-even-succ-succ-ℕ n (succ-ℕ d , p)) = d
+pr2 (is-even-is-even-succ-succ-ℕ n (succ-ℕ d , p)) =
+ is-injective-succ-ℕ (is-injective-succ-ℕ p)
+
+is-even-succ-succ-is-even-ℕ :
+ (n : ℕ) → is-even-ℕ n → is-even-ℕ (succ-ℕ (succ-ℕ n))
+pr1 (is-even-succ-succ-is-even-ℕ n (d , p)) = succ-ℕ d
+pr2 (is-even-succ-succ-is-even-ℕ n (d , p)) = ap (succ-ℕ ∘ succ-ℕ) p
+```
+
+### A natural number `x` is odd if and only if `x + 2` is odd
+
+```agda
+is-odd-is-odd-succ-succ-ℕ :
+ (n : ℕ) → is-odd-ℕ (succ-ℕ (succ-ℕ n)) → is-odd-ℕ n
+is-odd-is-odd-succ-succ-ℕ n = map-neg (is-even-succ-succ-is-even-ℕ n)
+
+is-odd-succ-succ-is-odd-ℕ :
+ (n : ℕ) → is-odd-ℕ n → is-odd-ℕ (succ-ℕ (succ-ℕ n))
+is-odd-succ-succ-is-odd-ℕ n = map-neg (is-even-is-even-succ-succ-ℕ n)
+```
diff --git a/src/finite-group-theory/subgroups-finite-groups.lagda.md b/src/finite-group-theory/subgroups-finite-groups.lagda.md
index fa290c1d0b..454c2812a9 100644
--- a/src/finite-group-theory/subgroups-finite-groups.lagda.md
+++ b/src/finite-group-theory/subgroups-finite-groups.lagda.md
@@ -332,7 +332,7 @@ module _
( group-Group-𝔽 G)
( inclusion-Subgroup-𝔽 G H)
preserves-mul-inclusion-group-Subgroup-𝔽 =
- preserves-mul-inclusion-group-Decidable-Subgroup (group-Group-𝔽 G) H
+ preserves-mul-inclusion-Decidable-Subgroup (group-Group-𝔽 G) H
preserves-unit-inclusion-group-Subgroup-𝔽 :
preserves-unit-Group
@@ -340,7 +340,7 @@ module _
( group-Group-𝔽 G)
( inclusion-Subgroup-𝔽 G H)
preserves-unit-inclusion-group-Subgroup-𝔽 =
- preserves-unit-inclusion-group-Decidable-Subgroup (group-Group-𝔽 G) H
+ preserves-unit-inclusion-Decidable-Subgroup (group-Group-𝔽 G) H
preserves-inverses-inclusion-group-Subgroup-𝔽 :
preserves-inverses-Group
@@ -348,12 +348,12 @@ module _
( group-Group-𝔽 G)
( inclusion-Subgroup-𝔽 G H)
preserves-inverses-inclusion-group-Subgroup-𝔽 =
- preserves-inverses-inclusion-group-Decidable-Subgroup (group-Group-𝔽 G) H
+ preserves-inverses-inclusion-Decidable-Subgroup (group-Group-𝔽 G) H
inclusion-group-Subgroup-𝔽 :
type-hom-Group (group-Subgroup-𝔽 G H) (group-Group-𝔽 G)
inclusion-group-Subgroup-𝔽 =
- inclusion-group-Decidable-Subgroup (group-Group-𝔽 G) H
+ hom-inclusion-Decidable-Subgroup (group-Group-𝔽 G) H
```
## Properties
diff --git a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md
index 3583aca66a..56118c0a50 100644
--- a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md
+++ b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md
@@ -9,6 +9,7 @@ module foundation.lesser-limited-principle-of-omniscience where
```agda
open import elementary-number-theory.divisibility-natural-numbers
open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.parity-natural-numbers
open import foundation.disjunction
diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md
index a66716dcf5..35fa68f7ce 100644
--- a/src/group-theory.lagda.md
+++ b/src/group-theory.lagda.md
@@ -15,6 +15,11 @@ open import group-theory.category-of-groups public
open import group-theory.category-of-semigroups public
open import group-theory.cayleys-theorem public
open import group-theory.centers-groups public
+open import group-theory.centers-monoids public
+open import group-theory.centers-semigroups public
+open import group-theory.central-elements-groups public
+open import group-theory.central-elements-monoids public
+open import group-theory.central-elements-semigroups public
open import group-theory.commutative-monoids public
open import group-theory.commutators-groups public
open import group-theory.concrete-group-actions public
@@ -88,6 +93,7 @@ open import group-theory.monomorphisms-concrete-groups public
open import group-theory.monomorphisms-groups public
open import group-theory.normal-subgroups public
open import group-theory.normal-subgroups-concrete-groups public
+open import group-theory.normal-submonoids public
open import group-theory.opposite-groups public
open import group-theory.orbit-stabilizer-theorem-concrete-groups public
open import group-theory.orbits-concrete-group-actions public
diff --git a/src/group-theory/abelian-groups.lagda.md b/src/group-theory/abelian-groups.lagda.md
index e89de50845..babdfed587 100644
--- a/src/group-theory/abelian-groups.lagda.md
+++ b/src/group-theory/abelian-groups.lagda.md
@@ -21,6 +21,7 @@ open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels
+open import group-theory.central-elements-groups
open import group-theory.commutative-monoids
open import group-theory.conjugation
open import group-theory.groups
@@ -591,3 +592,19 @@ module _
preserves-concat-add-list-Ab =
preserves-concat-mul-list-Group (group-Ab A)
```
+
+### A group is abelian if and only if every element is central
+
+```agda
+module _
+ {l : Level} (G : Group l)
+ where
+
+ is-abelian-every-element-central-Group :
+ ((x : type-Group G) → is-central-element-Group G x) → is-abelian-Group G
+ is-abelian-every-element-central-Group = id
+
+ every-element-central-is-abelian-Group :
+ is-abelian-Group G → ((x : type-Group G) → is-central-element-Group G x)
+ every-element-central-is-abelian-Group = id
+```
diff --git a/src/group-theory/centers-groups.lagda.md b/src/group-theory/centers-groups.lagda.md
index 5027215aaf..d2047b90c3 100644
--- a/src/group-theory/centers-groups.lagda.md
+++ b/src/group-theory/centers-groups.lagda.md
@@ -10,62 +10,89 @@ module group-theory.centers-groups where
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
-open import foundation.sets
open import foundation.universe-levels
+open import group-theory.central-elements-groups
+open import group-theory.homomorphisms-groups
open import group-theory.groups
+open import group-theory.normal-subgroups
open import group-theory.subgroups
```
-
+
## Idea
-The **center** of a group `G` is the normal subgroup consisting of all elements
-`g : G` that commute with every element of `G`.
+The **center** of a group consists of those elements that are central.
## Definition
```agda
module _
- {l1 : Level} (G : Group l1)
+ {l : Level} (G : Group l)
where
- subtype-center-Group : subset-Group l1 G
- subtype-center-Group g =
- Π-Prop
- ( type-Group G)
- ( λ h → Id-Prop (set-Group G) (mul-Group G g h) (mul-Group G h g))
-
- contains-unit-center-Group : contains-unit-subset-Group G subtype-center-Group
- contains-unit-center-Group h =
- ( left-unit-law-mul-Group G h) ∙
- ( inv (right-unit-law-mul-Group G h))
-
- is-closed-under-mul-center-Group :
- is-closed-under-mul-subset-Group G subtype-center-Group
- is-closed-under-mul-center-Group g1 g2 H1 H2 h =
- ( associative-mul-Group G g1 g2 h) ∙
- ( ( ap (mul-Group G g1) (H2 h)) ∙
- ( ( inv (associative-mul-Group G g1 h g2)) ∙
- ( ( ap (mul-Group' G g2) (H1 h)) ∙
- ( associative-mul-Group G h g1 g2))))
-
- is-closed-under-inv-center-Group :
- is-closed-under-inv-subset-Group G subtype-center-Group
- is-closed-under-inv-center-Group g H h =
- ( inv (inv-inv-Group G (mul-Group G (inv-Group G g) h))) ∙
- ( ( ap (inv-Group G) (distributive-inv-mul-Group G (inv-Group G g) h)) ∙
- ( ( ap
- ( inv-Group G)
- ( ap (mul-Group G (inv-Group G h)) (inv-inv-Group G g))) ∙
- ( ( inv (ap (inv-Group G) (H (inv-Group G h)))) ∙
- ( ( distributive-inv-mul-Group G g (inv-Group G h)) ∙
- ( ap (mul-Group' G (inv-Group G g)) (inv-inv-Group G h))))))
-
- subgroup-center-Group : Subgroup l1 G
+ subtype-center-Group : type-Group G → Prop l
+ subtype-center-Group = is-central-element-group-Prop G
+
+ subgroup-center-Group : Subgroup l G
pr1 subgroup-center-Group = subtype-center-Group
- pr1 (pr2 subgroup-center-Group) = contains-unit-center-Group
- pr1 (pr2 (pr2 subgroup-center-Group)) = is-closed-under-mul-center-Group
- pr2 (pr2 (pr2 subgroup-center-Group)) = is-closed-under-inv-center-Group
+ pr1 (pr2 subgroup-center-Group) = is-central-element-unit-Group G
+ pr1 (pr2 (pr2 subgroup-center-Group)) = is-central-element-mul-Group G
+ pr2 (pr2 (pr2 subgroup-center-Group)) = is-central-element-inv-Group G
+
+ group-center-Group : Group l
+ group-center-Group = group-Subgroup G subgroup-center-Group
+
+ type-center-Group : UU l
+ type-center-Group =
+ type-Subgroup G subgroup-center-Group
+
+ mul-center-Group :
+ (x y : type-center-Group) → type-center-Group
+ mul-center-Group = mul-Subgroup G subgroup-center-Group
+
+ associative-mul-center-Group :
+ (x y z : type-center-Group) →
+ mul-center-Group (mul-center-Group x y) z ＝
+ mul-center-Group x (mul-center-Group y z)
+ associative-mul-center-Group =
+ associative-mul-Subgroup G subgroup-center-Group
+
+ inclusion-center-Group :
+ type-center-Group → type-Group G
+ inclusion-center-Group =
+ inclusion-Subgroup G subgroup-center-Group
+
+ is-central-element-inclusion-center-Group :
+ (x : type-center-Group) →
+ is-central-element-Group G (inclusion-center-Group x)
+ is-central-element-inclusion-center-Group x =
+ is-in-subgroup-inclusion-Subgroup G subgroup-center-Group x
+
+ preserves-mul-inclusion-center-Group :
+ (x y : type-center-Group) →
+ inclusion-center-Group (mul-center-Group x y) ＝
+ mul-Group G
+ ( inclusion-center-Group x)
+ ( inclusion-center-Group y)
+ preserves-mul-inclusion-center-Group =
+ preserves-mul-inclusion-Subgroup G subgroup-center-Group
+
+ hom-inclusion-center-Group :
+ type-hom-Group group-center-Group G
+ hom-inclusion-center-Group =
+ hom-inclusion-Subgroup G subgroup-center-Group
+
+ is-normal-subgroup-center-Group :
+ is-normal-Subgroup G subgroup-center-Group
+ is-normal-subgroup-center-Group x y =
+ is-central-element-conjugation-Group G
+ ( inclusion-center-Group y)
+ ( x)
+ ( is-central-element-inclusion-center-Group y)
+
+ center-Group : Normal-Subgroup l G
+ pr1 center-Group = subgroup-center-Group
+ pr2 center-Group = is-normal-subgroup-center-Group
```
diff --git a/src/group-theory/centers-monoids.lagda.md b/src/group-theory/centers-monoids.lagda.md
new file mode 100644
index 0000000000..74f109ebe1
--- /dev/null
+++ b/src/group-theory/centers-monoids.lagda.md
@@ -0,0 +1,78 @@
+# Center of a monoid
+
+```agda
+module group-theory.centers-monoids where
+```
+
+Imports
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import group-theory.central-elements-monoids
+open import group-theory.homomorphisms-monoids
+open import group-theory.monoids
+open import group-theory.submonoids
+```
+
+
+
+## Idea
+
+The center of a monoid consists of those elements that are central.
+
+## Definition
+
+```agda
+module _
+ {l : Level} (M : Monoid l)
+ where
+
+ subtype-center-Monoid : type-Monoid M → Prop l
+ subtype-center-Monoid = is-central-element-monoid-Prop M
+
+ center-Monoid : Submonoid l M
+ pr1 center-Monoid = subtype-center-Monoid
+ pr1 (pr2 center-Monoid) = is-central-element-unit-Monoid M
+ pr2 (pr2 center-Monoid) = is-central-element-mul-Monoid M
+
+ monoid-center-Monoid : Monoid l
+ monoid-center-Monoid = monoid-Submonoid M center-Monoid
+
+ type-center-Monoid : UU l
+ type-center-Monoid =
+ type-Submonoid M center-Monoid
+
+ mul-center-Monoid :
+ (x y : type-center-Monoid) → type-center-Monoid
+ mul-center-Monoid = mul-Submonoid M center-Monoid
+
+ associative-mul-center-Monoid :
+ (x y z : type-center-Monoid) →
+ mul-center-Monoid (mul-center-Monoid x y) z ＝
+ mul-center-Monoid x (mul-center-Monoid y z)
+ associative-mul-center-Monoid =
+ associative-mul-Submonoid M center-Monoid
+
+ inclusion-center-Monoid :
+ type-center-Monoid → type-Monoid M
+ inclusion-center-Monoid =
+ inclusion-Submonoid M center-Monoid
+
+ preserves-mul-inclusion-center-Monoid :
+ (x y : type-center-Monoid) →
+ inclusion-center-Monoid (mul-center-Monoid x y) ＝
+ mul-Monoid M
+ ( inclusion-center-Monoid x)
+ ( inclusion-center-Monoid y)
+ preserves-mul-inclusion-center-Monoid =
+ preserves-mul-inclusion-Submonoid M center-Monoid
+
+ hom-inclusion-center-Monoid :
+ type-hom-Monoid monoid-center-Monoid M
+ hom-inclusion-center-Monoid =
+ hom-inclusion-Submonoid M center-Monoid
+```
diff --git a/src/group-theory/centers-semigroups.lagda.md b/src/group-theory/centers-semigroups.lagda.md
new file mode 100644
index 0000000000..9efb43e127
--- /dev/null
+++ b/src/group-theory/centers-semigroups.lagda.md
@@ -0,0 +1,77 @@
+# Center of a semigroup
+
+```agda
+module group-theory.centers-semigroups where
+```
+
+Imports
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import group-theory.central-elements-semigroups
+open import group-theory.homomorphisms-semigroups
+open import group-theory.semigroups
+open import group-theory.subsemigroups
+```
+
+
+
+## Idea
+
+The center of a semigroup consists of those elements that are central.
+
+## Definition
+
+```agda
+module _
+ {l : Level} (G : Semigroup l)
+ where
+
+ subtype-center-Semigroup : type-Semigroup G → Prop l
+ subtype-center-Semigroup = is-central-element-semigroup-Prop G
+
+ center-Semigroup : Subsemigroup l G
+ pr1 center-Semigroup = subtype-center-Semigroup
+ pr2 center-Semigroup = is-central-element-mul-Semigroup G
+
+ semigroup-center-Semigroup : Semigroup l
+ semigroup-center-Semigroup = semigroup-Subsemigroup G center-Semigroup
+
+ type-center-Semigroup : UU l
+ type-center-Semigroup =
+ type-Subsemigroup G center-Semigroup
+
+ mul-center-Semigroup :
+ (x y : type-center-Semigroup) → type-center-Semigroup
+ mul-center-Semigroup = mul-Subsemigroup G center-Semigroup
+
+ associative-mul-center-Semigroup :
+ (x y z : type-center-Semigroup) →
+ mul-center-Semigroup (mul-center-Semigroup x y) z ＝
+ mul-center-Semigroup x (mul-center-Semigroup y z)
+ associative-mul-center-Semigroup =
+ associative-mul-Subsemigroup G center-Semigroup
+
+ inclusion-center-Semigroup :
+ type-center-Semigroup → type-Semigroup G
+ inclusion-center-Semigroup =
+ inclusion-Subsemigroup G center-Semigroup
+
+ preserves-mul-inclusion-center-Semigroup :
+ (x y : type-center-Semigroup) →
+ inclusion-center-Semigroup (mul-center-Semigroup x y) ＝
+ mul-Semigroup G
+ ( inclusion-center-Semigroup x)
+ ( inclusion-center-Semigroup y)
+ preserves-mul-inclusion-center-Semigroup =
+ preserves-mul-inclusion-Subsemigroup G center-Semigroup
+
+ hom-inclusion-center-Semigroup :
+ type-hom-Semigroup semigroup-center-Semigroup G
+ hom-inclusion-center-Semigroup =
+ hom-inclusion-Subsemigroup G center-Semigroup
+```
diff --git a/src/group-theory/central-elements-groups.lagda.md b/src/group-theory/central-elements-groups.lagda.md
new file mode 100644
index 0000000000..ee85d300e4
--- /dev/null
+++ b/src/group-theory/central-elements-groups.lagda.md
@@ -0,0 +1,115 @@
+# Central elements of groups
+
+```agda
+module group-theory.central-elements-groups where
+```
+
+Imports
+
+```agda
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import group-theory.central-elements-monoids
+open import group-theory.conjugation
+open import group-theory.groups
+```
+
+
+
+## Idea
+
+An element `x` of a group `G` is said to be central if `xy ＝ yx` for every
+`y : G`.
+
+## Definition
+
+```agda
+module _
+ {l : Level} (G : Group l)
+ where
+
+ is-central-element-group-Prop : type-Group G → Prop l
+ is-central-element-group-Prop =
+ is-central-element-monoid-Prop (monoid-Group G)
+
+ is-central-element-Group : type-Group G → UU l
+ is-central-element-Group = is-central-element-Monoid (monoid-Group G)
+
+ is-prop-is-central-element-Group :
+ (x : type-Group G) → is-prop (is-central-element-Group x)
+ is-prop-is-central-element-Group =
+ is-prop-is-central-element-Monoid (monoid-Group G)
+```
+
+## Properties
+
+### The unit element is central
+
+```agda
+module _
+ {l : Level} (G : Group l)
+ where
+
+ is-central-element-unit-Group : is-central-element-Group G (unit-Group G)
+ is-central-element-unit-Group =
+ is-central-element-unit-Monoid (monoid-Group G)
+```
+
+### The product of two central elements is central
+
+```agda
+module _
+ {l : Level} (G : Group l)
+ where
+
+ is-central-element-mul-Group :
+ (x y : type-Group G) →
+ is-central-element-Group G x → is-central-element-Group G y →
+ is-central-element-Group G (mul-Group G x y)
+ is-central-element-mul-Group =
+ is-central-element-mul-Monoid (monoid-Group G)
+```
+
+### The inverse of a central element is central
+
+```agda
+module _
+ {l : Level} (G : Group l)
+ where
+
+ is-central-element-inv-Group :
+ (x : type-Group G) → is-central-element-Group G x →
+ is-central-element-Group G (inv-Group G x)
+ is-central-element-inv-Group x H y =
+ ( inv (inv-left-div-Group G y x)) ∙
+ ( ( ap (inv-Group G) (inv (H (inv-Group G y)))) ∙
+ ( inv-right-div-Group G x y))
+```
+
+### The central elements are closed under conjugation
+
+```agda
+module _
+ {l : Level} (G : Group l)
+ where
+
+ is-fixed-point-conjugation-is-central-element-Group :
+ (x y : type-Group G) → is-central-element-Group G x →
+ conjugation-Group G y x ＝ x
+ is-fixed-point-conjugation-is-central-element-Group x y H =
+ ( ap (mul-Group' G (inv-Group G y)) (inv (H y))) ∙
+ ( isretr-mul-inv-Group' G y x)
+
+ is-central-element-conjugation-Group :
+ (x y : type-Group G) → is-central-element-Group G x →
+ is-central-element-Group G (conjugation-Group G y x)
+ is-central-element-conjugation-Group x y H =
+ is-closed-under-eq-subtype'
+ ( is-central-element-group-Prop G)
+ ( H)
+ ( is-fixed-point-conjugation-is-central-element-Group x y H)
+```
diff --git a/src/group-theory/central-elements-monoids.lagda.md b/src/group-theory/central-elements-monoids.lagda.md
new file mode 100644
index 0000000000..849e6fff79
--- /dev/null
+++ b/src/group-theory/central-elements-monoids.lagda.md
@@ -0,0 +1,74 @@
+# Central elements of monoids
+
+```agda
+module group-theory.central-elements-monoids where
+```
+
+Imports
+
+```agda
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.central-elements-semigroups
+open import group-theory.monoids
+```
+
+
+
+## Idea
+
+An element `x` of a monoid `M` is said to be central if `xy ＝ yx` for every
+`y : M`.
+
+## Definition
+
+```agda
+module _
+ {l : Level} (M : Monoid l)
+ where
+
+ is-central-element-monoid-Prop : type-Monoid M → Prop l
+ is-central-element-monoid-Prop =
+ is-central-element-semigroup-Prop (semigroup-Monoid M)
+
+ is-central-element-Monoid : type-Monoid M → UU l
+ is-central-element-Monoid =
+ is-central-element-Semigroup (semigroup-Monoid M)
+
+ is-prop-is-central-element-Monoid :
+ (x : type-Monoid M) → is-prop (is-central-element-Monoid x)
+ is-prop-is-central-element-Monoid =
+ is-prop-is-central-element-Semigroup (semigroup-Monoid M)
+```
+
+## Properties
+
+### The unit element is central
+
+```agda
+module _
+ {l : Level} (M : Monoid l)
+ where
+
+ is-central-element-unit-Monoid : is-central-element-Monoid M (unit-Monoid M)
+ is-central-element-unit-Monoid y =
+ left-unit-law-mul-Monoid M y ∙ inv (right-unit-law-mul-Monoid M y)
+```
+
+### The product of two central elements is central
+
+```agda
+module _
+ {l : Level} (M : Monoid l)
+ where
+
+ is-central-element-mul-Monoid :
+ (x y : type-Monoid M) →
+ is-central-element-Monoid M x → is-central-element-Monoid M y →
+ is-central-element-Monoid M (mul-Monoid M x y)
+ is-central-element-mul-Monoid =
+ is-central-element-mul-Semigroup (semigroup-Monoid M)
+```
diff --git a/src/group-theory/central-elements-semigroups.lagda.md b/src/group-theory/central-elements-semigroups.lagda.md
new file mode 100644
index 0000000000..1cb9dc6fc7
--- /dev/null
+++ b/src/group-theory/central-elements-semigroups.lagda.md
@@ -0,0 +1,71 @@
+# Central elements of semirings
+
+```agda
+module group-theory.central-elements-semigroups where
+```
+
+Imports
+
+```agda
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.semigroups
+```
+
+
+
+## Idea
+
+An element `x` of a semigroup `G` is said to be central if `xy ＝ yx` for every
+`y : G`.
+
+## Definition
+
+```agda
+module _
+ {l : Level} (G : Semigroup l)
+ where
+
+ is-central-element-semigroup-Prop : type-Semigroup G → Prop l
+ is-central-element-semigroup-Prop x =
+ Π-Prop
+ ( type-Semigroup G)
+ ( λ y →
+ Id-Prop
+ ( set-Semigroup G)
+ ( mul-Semigroup G x y)
+ ( mul-Semigroup G y x))
+
+ is-central-element-Semigroup : type-Semigroup G → UU l
+ is-central-element-Semigroup x =
+ type-Prop (is-central-element-semigroup-Prop x)
+
+ is-prop-is-central-element-Semigroup :
+ (x : type-Semigroup G) → is-prop (is-central-element-Semigroup x)
+ is-prop-is-central-element-Semigroup x =
+ is-prop-type-Prop (is-central-element-semigroup-Prop x)
+```
+
+## Properties
+
+### The product of two central elements is central
+
+```agda
+module _
+ {l : Level} (G : Semigroup l)
+ where
+
+ is-central-element-mul-Semigroup :
+ (x y : type-Semigroup G) →
+ is-central-element-Semigroup G x → is-central-element-Semigroup G y →
+ is-central-element-Semigroup G (mul-Semigroup G x y)
+ is-central-element-mul-Semigroup x y H K z =
+ ( associative-mul-Semigroup G x y z) ∙
+ ( ( ap (mul-Semigroup G x) (K z)) ∙
+ ( ( inv (associative-mul-Semigroup G x z y)) ∙
+ ( ( ap (mul-Semigroup' G y) (H z)) ∙
+ ( associative-mul-Semigroup G z x y))))
+```
diff --git a/src/group-theory/decidable-subgroups.lagda.md b/src/group-theory/decidable-subgroups.lagda.md
index 8dcea4fce0..15857ac6e9 100644
--- a/src/group-theory/decidable-subgroups.lagda.md
+++ b/src/group-theory/decidable-subgroups.lagda.md
@@ -214,20 +214,15 @@ module _
type-group-Decidable-Subgroup =
type-group-Subgroup G (subgroup-Decidable-Subgroup G H)
- map-inclusion-group-Decidable-Subgroup :
+ map-inclusion-Decidable-Subgroup :
type-group-Decidable-Subgroup → type-Group G
- map-inclusion-group-Decidable-Subgroup =
- map-inclusion-group-Subgroup G (subgroup-Decidable-Subgroup G H)
-
- is-emb-inclusion-group-Decidable-Subgroup :
- is-emb map-inclusion-group-Decidable-Subgroup
- is-emb-inclusion-group-Decidable-Subgroup =
- is-emb-inclusion-group-Subgroup G (subgroup-Decidable-Subgroup G H)
+ map-inclusion-Decidable-Subgroup =
+ map-inclusion-Subgroup G (subgroup-Decidable-Subgroup G H)
eq-decidable-subgroup-eq-group :
{x y : type-group-Decidable-Subgroup} →
- ( map-inclusion-group-Decidable-Subgroup x ＝
- map-inclusion-group-Decidable-Subgroup y) →
+ ( map-inclusion-Decidable-Subgroup x ＝
+ map-inclusion-Decidable-Subgroup y) →
x ＝ y
eq-decidable-subgroup-eq-group =
eq-subgroup-eq-group G (subgroup-Decidable-Subgroup G H)
@@ -295,35 +290,35 @@ module _
{l1 l2 : Level} (G : Group l1) (H : Decidable-Subgroup l2 G)
where
- preserves-mul-inclusion-group-Decidable-Subgroup :
+ preserves-mul-inclusion-Decidable-Subgroup :
preserves-mul-Group
( group-Decidable-Subgroup G H)
( G)
- ( map-inclusion-group-Decidable-Subgroup G H)
- preserves-mul-inclusion-group-Decidable-Subgroup =
- preserves-mul-inclusion-group-Subgroup G (subgroup-Decidable-Subgroup G H)
+ ( map-inclusion-Decidable-Subgroup G H)
+ preserves-mul-inclusion-Decidable-Subgroup =
+ preserves-mul-inclusion-Subgroup G (subgroup-Decidable-Subgroup G H)
- preserves-unit-inclusion-group-Decidable-Subgroup :
+ preserves-unit-inclusion-Decidable-Subgroup :
preserves-unit-Group
( group-Decidable-Subgroup G H)
( G)
- ( map-inclusion-group-Decidable-Subgroup G H)
- preserves-unit-inclusion-group-Decidable-Subgroup =
- preserves-unit-inclusion-group-Subgroup G (subgroup-Decidable-Subgroup G H)
+ ( map-inclusion-Decidable-Subgroup G H)
+ preserves-unit-inclusion-Decidable-Subgroup =
+ preserves-unit-inclusion-Subgroup G (subgroup-Decidable-Subgroup G H)
- preserves-inverses-inclusion-group-Decidable-Subgroup :
+ preserves-inverses-inclusion-Decidable-Subgroup :
preserves-inverses-Group
( group-Decidable-Subgroup G H)
( G)
- ( map-inclusion-group-Decidable-Subgroup G H)
- preserves-inverses-inclusion-group-Decidable-Subgroup =
- preserves-inverses-inclusion-group-Subgroup G
+ ( map-inclusion-Decidable-Subgroup G H)
+ preserves-inverses-inclusion-Decidable-Subgroup =
+ preserves-inverses-inclusion-Subgroup G
( subgroup-Decidable-Subgroup G H)
- inclusion-group-Decidable-Subgroup :
+ hom-inclusion-Decidable-Subgroup :
type-hom-Group (group-Decidable-Subgroup G H) G
- inclusion-group-Decidable-Subgroup =
- inclusion-group-Subgroup G (subgroup-Decidable-Subgroup G H)
+ hom-inclusion-Decidable-Subgroup =
+ hom-inclusion-Subgroup G (subgroup-Decidable-Subgroup G H)
```
## Properties
diff --git a/src/group-theory/embeddings-groups.lagda.md b/src/group-theory/embeddings-groups.lagda.md
index 1daee280b5..c9c7df3f79 100644
--- a/src/group-theory/embeddings-groups.lagda.md
+++ b/src/group-theory/embeddings-groups.lagda.md
@@ -59,7 +59,7 @@ emb-group-slice-Subgroup :
{ l1 l2 : Level} (G : Group l1) →
Subgroup l2 G → emb-Group-Slice (l1 ⊔ l2) G
pr1 (emb-group-slice-Subgroup G P) = group-Subgroup G P
-pr1 (pr2 (emb-group-slice-Subgroup G P)) = inclusion-group-Subgroup G P
+pr1 (pr2 (emb-group-slice-Subgroup G P)) = hom-inclusion-Subgroup G P
pr2 (pr2 (emb-group-slice-Subgroup G P)) =
- is-emb-inclusion-group-Subgroup G P
+ is-emb-inclusion-Subgroup G P
```
diff --git a/src/group-theory/full-subgroups.lagda.md b/src/group-theory/full-subgroups.lagda.md
index 38f1abc3fe..a5d664f4ca 100644
--- a/src/group-theory/full-subgroups.lagda.md
+++ b/src/group-theory/full-subgroups.lagda.md
@@ -85,23 +85,23 @@ module _
group-full-Subgroup : Group (l1 ⊔ l2)
group-full-Subgroup = group-Subgroup G (full-Subgroup l2 G)
- inclusion-group-full-Subgroup : type-hom-Group group-full-Subgroup G
- inclusion-group-full-Subgroup =
- inclusion-group-Subgroup G (full-Subgroup l2 G)
+ hom-inclusion-full-Subgroup : type-hom-Group group-full-Subgroup G
+ hom-inclusion-full-Subgroup =
+ hom-inclusion-Subgroup G (full-Subgroup l2 G)
- preserves-mul-inclusion-group-full-Subgroup :
+ preserves-mul-inclusion-full-Subgroup :
preserves-mul-Group group-full-Subgroup G inclusion-full-Subgroup
- preserves-mul-inclusion-group-full-Subgroup =
- preserves-mul-inclusion-group-Subgroup G (full-Subgroup l2 G)
+ preserves-mul-inclusion-full-Subgroup =
+ preserves-mul-inclusion-Subgroup G (full-Subgroup l2 G)
- equiv-inclusion-group-full-Subgroup : equiv-Group group-full-Subgroup G
- pr1 equiv-inclusion-group-full-Subgroup = equiv-inclusion-full-Subgroup
- pr2 equiv-inclusion-group-full-Subgroup =
- preserves-mul-inclusion-group-full-Subgroup
+ equiv-group-inclusion-full-Subgroup : equiv-Group group-full-Subgroup G
+ pr1 equiv-group-inclusion-full-Subgroup = equiv-inclusion-full-Subgroup
+ pr2 equiv-group-inclusion-full-Subgroup =
+ preserves-mul-inclusion-full-Subgroup
iso-full-Subgroup : type-iso-Group group-full-Subgroup G
iso-full-Subgroup =
- iso-equiv-Group group-full-Subgroup G equiv-inclusion-group-full-Subgroup
+ iso-equiv-Group group-full-Subgroup G equiv-group-inclusion-full-Subgroup
inv-iso-full-Subgroup :
type-iso-Group G group-full-Subgroup
@@ -120,21 +120,21 @@ module _
is-iso-inclusion-is-full-Subgroup :
is-full-Subgroup G H →
- is-iso-hom-Group (group-Subgroup G H) G (inclusion-group-Subgroup G H)
+ is-iso-hom-Group (group-Subgroup G H) G (hom-inclusion-Subgroup G H)
is-iso-inclusion-is-full-Subgroup K =
is-iso-is-equiv-hom-Group
( group-Subgroup G H)
( G)
- ( inclusion-group-Subgroup G H)
+ ( hom-inclusion-Subgroup G H)
( is-equiv-inclusion-is-full-subtype (subset-Subgroup G H) K)
iso-inclusion-is-full-Subgroup :
is-full-Subgroup G H → type-iso-Group (group-Subgroup G H) G
- pr1 (iso-inclusion-is-full-Subgroup K) = inclusion-group-Subgroup G H
+ pr1 (iso-inclusion-is-full-Subgroup K) = hom-inclusion-Subgroup G H
pr2 (iso-inclusion-is-full-Subgroup K) = is-iso-inclusion-is-full-Subgroup K
is-full-is-iso-inclusion-Subgroup :
- is-iso-hom-Group (group-Subgroup G H) G (inclusion-group-Subgroup G H) →
+ is-iso-hom-Group (group-Subgroup G H) G (hom-inclusion-Subgroup G H) →
is-full-Subgroup G H
is-full-is-iso-inclusion-Subgroup K =
is-full-is-equiv-inclusion-subtype
@@ -142,6 +142,6 @@ module _
( is-equiv-is-iso-hom-Group
( group-Subgroup G H)
( G)
- ( inclusion-group-Subgroup G H)
+ ( hom-inclusion-Subgroup G H)
( K))
```
diff --git a/src/group-theory/homomorphisms-monoids.lagda.md b/src/group-theory/homomorphisms-monoids.lagda.md
index 39454e1365..39e170ce34 100644
--- a/src/group-theory/homomorphisms-monoids.lagda.md
+++ b/src/group-theory/homomorphisms-monoids.lagda.md
@@ -9,6 +9,9 @@ module group-theory.homomorphisms-monoids where
```agda
open import foundation.dependent-pair-types
open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
open import foundation.universe-levels
open import group-theory.homomorphisms-semigroups
@@ -27,25 +30,38 @@ semigroups that preserve the unit element.
### Homomorphisms of monoids
```agda
-preserves-unit-hom-Semigroup :
- { l1 l2 : Level} (M1 : Monoid l1) (M2 : Monoid l2) →
- ( type-hom-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2)) → UU l2
-preserves-unit-hom-Semigroup M1 M2 f =
- Id ( map-hom-Semigroup
- ( semigroup-Monoid M1)
- ( semigroup-Monoid M2)
- ( f)
- ( unit-Monoid M1))
- ( unit-Monoid M2)
-
-hom-Monoid :
- { l1 l2 : Level} (M1 : Monoid l1) (M2 : Monoid l2) → UU (l1 ⊔ l2)
-hom-Monoid M1 M2 =
- Σ ( type-hom-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2))
- ( preserves-unit-hom-Semigroup M1 M2)
+module _
+ {l1 l2 : Level} (M1 : Monoid l1) (M2 : Monoid l2)
+ where
+
+ preserves-unit-hom-semigroup-Prop :
+ type-hom-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2) → Prop l2
+ preserves-unit-hom-semigroup-Prop f =
+ Id-Prop
+ ( set-Monoid M2)
+ ( map-hom-Semigroup
+ ( semigroup-Monoid M1)
+ ( semigroup-Monoid M2)
+ ( f)
+ ( unit-Monoid M1))
+ ( unit-Monoid M2)
+
+ preserves-unit-hom-Semigroup :
+ type-hom-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2) → UU l2
+ preserves-unit-hom-Semigroup f =
+ type-Prop (preserves-unit-hom-semigroup-Prop f)
+
+ hom-Monoid : Set (l1 ⊔ l2)
+ hom-Monoid =
+ set-subset
+ ( hom-Semigroup (semigroup-Monoid M1) (semigroup-Monoid M2))
+ ( preserves-unit-hom-semigroup-Prop)
+
+ type-hom-Monoid : UU (l1 ⊔ l2)
+ type-hom-Monoid = type-Set hom-Monoid
module _
- {l1 l2 : Level} (M : Monoid l1) (N : Monoid l2) (f : hom-Monoid M N)
+ {l1 l2 : Level} (M : Monoid l1) (N : Monoid l2) (f : type-hom-Monoid M N)
where
hom-semigroup-hom-Monoid :
@@ -84,7 +100,7 @@ preserves-unit-id-hom-Monoid :
preserves-unit-id-hom-Monoid M = refl
id-hom-Monoid :
- {l : Level} (M : Monoid l) → hom-Monoid M M
+ {l : Level} (M : Monoid l) → type-hom-Monoid M M
pr1 (id-hom-Monoid M) = id-hom-Semigroup (semigroup-Monoid M)
pr2 (id-hom-Monoid M) = preserves-unit-id-hom-Monoid M
```
diff --git a/src/group-theory/kernels.lagda.md b/src/group-theory/kernels.lagda.md
index 078824521d..ae8d8e7f29 100644
--- a/src/group-theory/kernels.lagda.md
+++ b/src/group-theory/kernels.lagda.md
@@ -79,12 +79,12 @@ module _
inclusion-kernel-hom-Group : type-hom-Group group-kernel-hom-Group G
inclusion-kernel-hom-Group =
- inclusion-group-Subgroup G subgroup-kernel-hom-Group
+ hom-inclusion-Subgroup G subgroup-kernel-hom-Group
is-emb-inclusion-kernel-hom-Group :
is-emb-hom-Group group-kernel-hom-Group G inclusion-kernel-hom-Group
is-emb-inclusion-kernel-hom-Group =
- is-emb-inclusion-group-Subgroup G subgroup-kernel-hom-Group
+ is-emb-inclusion-Subgroup G subgroup-kernel-hom-Group
emb-inclusion-kernel-hom-Group : emb-Group group-kernel-hom-Group G
pr1 emb-inclusion-kernel-hom-Group =
diff --git a/src/group-theory/monoid-actions.lagda.md b/src/group-theory/monoid-actions.lagda.md
index 84b1b080e9..c12bab7fe4 100644
--- a/src/group-theory/monoid-actions.lagda.md
+++ b/src/group-theory/monoid-actions.lagda.md
@@ -30,7 +30,7 @@ A monoid `M` can act on a type `A` by a monoid homomorphism `hom M (A → A)`.
```agda
Monoid-Action : {l1 : Level} (l : Level) (M : Monoid l1) → UU (l1 ⊔ lsuc l)
-Monoid-Action l M = Σ (Set l) (λ X → hom-Monoid M (endo-Monoid X))
+Monoid-Action l M = Σ (Set l) (λ X → type-hom-Monoid M (endo-Monoid X))
module _
{l1 l2 : Level} (M : Monoid l1) (X : Monoid-Action l2 M)
diff --git a/src/group-theory/normal-submonoids.lagda.md b/src/group-theory/normal-submonoids.lagda.md
new file mode 100644
index 0000000000..9d6489bb45
--- /dev/null
+++ b/src/group-theory/normal-submonoids.lagda.md
@@ -0,0 +1,195 @@
+# Normal submonoids
+
+```agda
+module group-theory.normal-submonoids where
+```
+
+Imports
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.functions
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtype-identity-principle
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import group-theory.monoids
+open import group-theory.semigroups
+open import group-theory.submonoids
+```
+
+## Idea
+
+A normal submonoid `N` of `M` is a monoid that corresponds uniquely to a
+congruence relation ~ on `M` consisting of the elements congruent to `1`. This
+is the case if and only if for all `x y : M` and `u : N` we have
+
+```md
+ xuy ∈ N ⇔ xy ∈ N
+```
+
+## Definition
+
+```agda
+module _
+ {l1 l2 : Level} (M : Monoid l1) (N : Submonoid l2 M)
+ where
+
+ is-normal-submonoid-Prop : Prop (l1 ⊔ l2)
+ is-normal-submonoid-Prop =
+ Π-Prop
+ ( type-Monoid M)
+ ( λ x →
+ Π-Prop
+ ( type-Monoid M)
+ ( λ y →
+ Π-Prop
+ ( type-Monoid M)
+ ( λ u →
+ function-Prop
+ ( is-in-Submonoid M N u)
+ ( iff-Prop
+ ( subset-Submonoid M N (mul-Monoid M (mul-Monoid M x u) y))
+ ( subset-Submonoid M N (mul-Monoid M x y))))))
+
+ is-normal-Submonoid : UU (l1 ⊔ l2)
+ is-normal-Submonoid = type-Prop is-normal-submonoid-Prop
+
+ is-prop-is-normal-Submonoid : is-prop is-normal-Submonoid
+ is-prop-is-normal-Submonoid = is-prop-type-Prop is-normal-submonoid-Prop
+
+Normal-Submonoid :
+ {l1 : Level} (l2 : Level) → Monoid l1 → UU (l1 ⊔ lsuc l2)
+Normal-Submonoid l2 M = Σ (Submonoid l2 M) (is-normal-Submonoid M)
+
+module _
+ {l1 l2 : Level} (M : Monoid l1) (N : Normal-Submonoid l2 M)
+ where
+
+ submonoid-Normal-Submonoid : Submonoid l2 M
+ submonoid-Normal-Submonoid = pr1 N
+
+ is-normal-Normal-Submonoid : is-normal-Submonoid M submonoid-Normal-Submonoid
+ is-normal-Normal-Submonoid = pr2 N
+
+ subset-Normal-Submonoid : subtype l2 (type-Monoid M)
+ subset-Normal-Submonoid =
+ subset-Submonoid M submonoid-Normal-Submonoid
+
+ is-submonoid-Normal-Submonoid : is-submonoid-Monoid M subset-Normal-Submonoid
+ is-submonoid-Normal-Submonoid =
+ is-submonoid-Submonoid M submonoid-Normal-Submonoid
+
+ is-in-Normal-Submonoid : type-Monoid M → UU l2
+ is-in-Normal-Submonoid =
+ is-in-Submonoid M submonoid-Normal-Submonoid
+
+ is-prop-is-in-Normal-Submonoid :
+ (x : type-Monoid M) → is-prop (is-in-Normal-Submonoid x)
+ is-prop-is-in-Normal-Submonoid =
+ is-prop-is-in-Submonoid M submonoid-Normal-Submonoid
+
+ type-Normal-Submonoid : UU (l1 ⊔ l2)
+ type-Normal-Submonoid = type-Submonoid M submonoid-Normal-Submonoid
+
+ is-set-type-Normal-Submonoid : is-set type-Normal-Submonoid
+ is-set-type-Normal-Submonoid =
+ is-set-type-Submonoid M submonoid-Normal-Submonoid
+
+ set-Normal-Submonoid : Set (l1 ⊔ l2)
+ set-Normal-Submonoid = set-Submonoid M submonoid-Normal-Submonoid
+
+ inclusion-Normal-Submonoid : type-Normal-Submonoid → type-Monoid M
+ inclusion-Normal-Submonoid = inclusion-Submonoid M submonoid-Normal-Submonoid
+
+ ap-inclusion-Normal-Submonoid :
+ (x y : type-Normal-Submonoid) → x ＝ y →
+ inclusion-Normal-Submonoid x ＝ inclusion-Normal-Submonoid y
+ ap-inclusion-Normal-Submonoid =
+ ap-inclusion-Submonoid M submonoid-Normal-Submonoid
+
+ is-in-submonoid-inclusion-Normal-Submonoid :
+ (x : type-Normal-Submonoid) →
+ is-in-Normal-Submonoid (inclusion-Normal-Submonoid x)
+ is-in-submonoid-inclusion-Normal-Submonoid =
+ is-in-submonoid-inclusion-Submonoid M submonoid-Normal-Submonoid
+
+ contains-unit-Normal-Submonoid : is-in-Normal-Submonoid (unit-Monoid M)
+ contains-unit-Normal-Submonoid =
+ contains-unit-Submonoid M submonoid-Normal-Submonoid
+
+ unit-Normal-Submonoid : type-Normal-Submonoid
+ unit-Normal-Submonoid = unit-Submonoid M submonoid-Normal-Submonoid
+
+ is-closed-under-mul-Normal-Submonoid :
+ {x y : type-Monoid M} →
+ is-in-Normal-Submonoid x → is-in-Normal-Submonoid y →
+ is-in-Normal-Submonoid (mul-Monoid M x y)
+ is-closed-under-mul-Normal-Submonoid =
+ is-closed-under-mul-Submonoid M submonoid-Normal-Submonoid
+
+ mul-Normal-Submonoid : (x y : type-Normal-Submonoid) → type-Normal-Submonoid
+ mul-Normal-Submonoid = mul-Submonoid M submonoid-Normal-Submonoid
+
+ associative-mul-Normal-Submonoid :
+ (x y z : type-Normal-Submonoid) →
+ (mul-Normal-Submonoid (mul-Normal-Submonoid x y) z) ＝
+ (mul-Normal-Submonoid x (mul-Normal-Submonoid y z))
+ associative-mul-Normal-Submonoid =
+ associative-mul-Submonoid M submonoid-Normal-Submonoid
+
+ semigroup-Normal-Submonoid : Semigroup (l1 ⊔ l2)
+ semigroup-Normal-Submonoid =
+ semigroup-Submonoid M submonoid-Normal-Submonoid
+
+ left-unit-law-mul-Normal-Submonoid :
+ (x : type-Normal-Submonoid) →
+ mul-Normal-Submonoid unit-Normal-Submonoid x ＝ x
+ left-unit-law-mul-Normal-Submonoid =
+ left-unit-law-mul-Submonoid M submonoid-Normal-Submonoid
+
+ right-unit-law-mul-Normal-Submonoid :
+ (x : type-Normal-Submonoid) →
+ mul-Normal-Submonoid x unit-Normal-Submonoid ＝ x
+ right-unit-law-mul-Normal-Submonoid =
+ right-unit-law-mul-Submonoid M submonoid-Normal-Submonoid
+
+ monoid-Normal-Submonoid : Monoid (l1 ⊔ l2)
+ monoid-Normal-Submonoid = monoid-Submonoid M submonoid-Normal-Submonoid
+```
+
+## Properties
+
+### Extensionality of the type of all submonoids
+
+```agda
+module _
+ {l1 l2 : Level} (M : Monoid l1) (N : Normal-Submonoid l2 M)
+ where
+
+ has-same-elements-Normal-Submonoid : Normal-Submonoid l2 M → UU (l1 ⊔ l2)
+ has-same-elements-Normal-Submonoid K =
+ has-same-elements-Submonoid M
+ ( submonoid-Normal-Submonoid M N)
+ ( submonoid-Normal-Submonoid M K)
+
+ extensionality-Normal-Submonoid :
+ (K : Normal-Submonoid l2 M) →
+ (N ＝ K) ≃ has-same-elements-Normal-Submonoid K
+ extensionality-Normal-Submonoid =
+ extensionality-type-subtype
+ ( is-normal-submonoid-Prop M)
+ ( is-normal-Normal-Submonoid M N)
+ ( λ x → (id , id))
+ ( extensionality-Submonoid M (submonoid-Normal-Submonoid M N))
+```
+
+## References
+
+[1] S. Margolis and J.-É. Pin, Inverse semigroups and extensions of groups by
+semilattices, J. of Algebra 110 (1987), 277-297.
diff --git a/src/group-theory/representations-monoids.lagda.md b/src/group-theory/representations-monoids.lagda.md
index 7f0fbfd1ad..0716b7fabc 100644
--- a/src/group-theory/representations-monoids.lagda.md
+++ b/src/group-theory/representations-monoids.lagda.md
@@ -32,7 +32,7 @@ on `V`.
categorical-representation-Monoid :
{l1 l2 l3 : Level} (C : Cat l1 l2) (M : Monoid l3) → UU (l1 ⊔ l2 ⊔ l3)
categorical-representation-Monoid C M =
- Σ (obj-Cat C) (λ V → hom-Monoid M (monoid-endo-Cat C V))
+ Σ (obj-Cat C) (λ V → type-hom-Monoid M (monoid-endo-Cat C V))
module _
{l1 l2 l3 : Level} (C : Cat l1 l2) (M : Monoid l3)
@@ -43,7 +43,7 @@ module _
obj-categorical-representation-Monoid = pr1 ρ
hom-action-categorical-representation-Monoid :
- hom-Monoid M (monoid-endo-Cat C obj-categorical-representation-Monoid)
+ type-hom-Monoid M (monoid-endo-Cat C obj-categorical-representation-Monoid)
hom-action-categorical-representation-Monoid = pr2 ρ
action-categorical-representation-Monoid :
diff --git a/src/group-theory/subgroups-abelian-groups.lagda.md b/src/group-theory/subgroups-abelian-groups.lagda.md
index a8f5e5846a..0fb84f72c9 100644
--- a/src/group-theory/subgroups-abelian-groups.lagda.md
+++ b/src/group-theory/subgroups-abelian-groups.lagda.md
@@ -187,15 +187,15 @@ module _
type-ab-Subgroup-Ab : UU (l1 ⊔ l2)
type-ab-Subgroup-Ab = type-group-Subgroup (group-Ab A) B
- map-inclusion-ab-Subgroup-Ab : type-ab-Subgroup-Ab → type-Ab A
- map-inclusion-ab-Subgroup-Ab = map-inclusion-group-Subgroup (group-Ab A) B
+ map-inclusion-Subgroup-Ab : type-ab-Subgroup-Ab → type-Ab A
+ map-inclusion-Subgroup-Ab = map-inclusion-Subgroup (group-Ab A) B
- is-emb-incl-ab-Subgroup-Ab : is-emb map-inclusion-ab-Subgroup-Ab
- is-emb-incl-ab-Subgroup-Ab = is-emb-inclusion-group-Subgroup (group-Ab A) B
+ is-emb-incl-ab-Subgroup-Ab : is-emb map-inclusion-Subgroup-Ab
+ is-emb-incl-ab-Subgroup-Ab = is-emb-inclusion-Subgroup (group-Ab A) B
eq-subgroup-ab-eq-ab :
{x y : type-ab-Subgroup-Ab} →
- Id (map-inclusion-ab-Subgroup-Ab x) (map-inclusion-ab-Subgroup-Ab y) →
+ Id (map-inclusion-Subgroup-Ab x) (map-inclusion-Subgroup-Ab y) →
Id x y
eq-subgroup-ab-eq-ab = eq-subgroup-eq-group (group-Ab A) B
@@ -268,26 +268,26 @@ module _
{l1 l2 : Level} (A : Ab l1) (B : Subgroup-Ab l2 A)
where
- preserves-add-inclusion-ab-Subgroup-Ab :
- preserves-add-Ab (ab-Subgroup-Ab A B) A (map-inclusion-ab-Subgroup-Ab A B)
- preserves-add-inclusion-ab-Subgroup-Ab =
- preserves-mul-inclusion-group-Subgroup (group-Ab A) B
+ preserves-add-inclusion-Subgroup-Ab :
+ preserves-add-Ab (ab-Subgroup-Ab A B) A (map-inclusion-Subgroup-Ab A B)
+ preserves-add-inclusion-Subgroup-Ab =
+ preserves-mul-inclusion-Subgroup (group-Ab A) B
- preserves-zero-inclusion-ab-Subgroup-Ab :
- preserves-zero-Ab (ab-Subgroup-Ab A B) A (map-inclusion-ab-Subgroup-Ab A B)
- preserves-zero-inclusion-ab-Subgroup-Ab =
- preserves-unit-inclusion-group-Subgroup (group-Ab A) B
+ preserves-zero-inclusion-Subgroup-Ab :
+ preserves-zero-Ab (ab-Subgroup-Ab A B) A (map-inclusion-Subgroup-Ab A B)
+ preserves-zero-inclusion-Subgroup-Ab =
+ preserves-unit-inclusion-Subgroup (group-Ab A) B
- preserves-negatives-inclusion-ab-Subgroup-Ab :
+ preserves-negatives-inclusion-Subgroup-Ab :
preserves-negatives-Ab
( ab-Subgroup-Ab A B)
( A)
- ( map-inclusion-ab-Subgroup-Ab A B)
- preserves-negatives-inclusion-ab-Subgroup-Ab =
- preserves-inverses-inclusion-group-Subgroup (group-Ab A) B
+ ( map-inclusion-Subgroup-Ab A B)
+ preserves-negatives-inclusion-Subgroup-Ab =
+ preserves-inverses-inclusion-Subgroup (group-Ab A) B
- inclusion-ab-Subgroup-Ab : type-hom-Ab (ab-Subgroup-Ab A B) A
- inclusion-ab-Subgroup-Ab = inclusion-group-Subgroup (group-Ab A) B
+ hom-inclusion-Subgroup-Ab : type-hom-Ab (ab-Subgroup-Ab A B) A
+ hom-inclusion-Subgroup-Ab = hom-inclusion-Subgroup (group-Ab A) B
```
### Normal subgroups of an abelian group
diff --git a/src/group-theory/subgroups.lagda.md b/src/group-theory/subgroups.lagda.md
index f3ebd6e8f0..6584d4a789 100644
--- a/src/group-theory/subgroups.lagda.md
+++ b/src/group-theory/subgroups.lagda.md
@@ -234,18 +234,13 @@ module _
type-group-Subgroup : UU (l1 ⊔ l2)
type-group-Subgroup = type-subtype (subset-Subgroup G H)
- map-inclusion-group-Subgroup : type-group-Subgroup → type-Group G
- map-inclusion-group-Subgroup =
+ map-inclusion-Subgroup : type-group-Subgroup → type-Group G
+ map-inclusion-Subgroup =
inclusion-subtype (subset-Subgroup G H)
- is-emb-inclusion-group-Subgroup :
- is-emb map-inclusion-group-Subgroup
- is-emb-inclusion-group-Subgroup =
- is-emb-inclusion-subtype (subset-Subgroup G H)
-
- eq-subgroup-eq-group : is-injective map-inclusion-group-Subgroup
+ eq-subgroup-eq-group : is-injective map-inclusion-Subgroup
eq-subgroup-eq-group {x} {y} =
- map-inv-is-equiv (is-emb-inclusion-group-Subgroup x y)
+ map-inv-is-equiv (is-emb-inclusion-Subgroup G H x y)
set-group-Subgroup : Set (l1 ⊔ l2)
pr1 set-group-Subgroup = type-group-Subgroup
@@ -321,31 +316,31 @@ module _
{l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G)
where
- preserves-mul-inclusion-group-Subgroup :
+ preserves-mul-inclusion-Subgroup :
preserves-mul-Group
( group-Subgroup G H)
( G)
- ( map-inclusion-group-Subgroup G H)
- preserves-mul-inclusion-group-Subgroup x y = refl
+ ( map-inclusion-Subgroup G H)
+ preserves-mul-inclusion-Subgroup x y = refl
- preserves-unit-inclusion-group-Subgroup :
+ preserves-unit-inclusion-Subgroup :
preserves-unit-Group
( group-Subgroup G H)
( G)
- ( map-inclusion-group-Subgroup G H)
- preserves-unit-inclusion-group-Subgroup = refl
+ ( map-inclusion-Subgroup G H)
+ preserves-unit-inclusion-Subgroup = refl
- preserves-inverses-inclusion-group-Subgroup :
+ preserves-inverses-inclusion-Subgroup :
preserves-inverses-Group
( group-Subgroup G H)
( G)
- ( map-inclusion-group-Subgroup G H)
- preserves-inverses-inclusion-group-Subgroup x = refl
+ ( map-inclusion-Subgroup G H)
+ preserves-inverses-inclusion-Subgroup x = refl
- inclusion-group-Subgroup : type-hom-Group (group-Subgroup G H) G
- pr1 inclusion-group-Subgroup = map-inclusion-group-Subgroup G H
- pr2 inclusion-group-Subgroup =
- preserves-mul-inclusion-group-Subgroup
+ hom-inclusion-Subgroup :
+ type-hom-Group (group-Subgroup G H) G
+ pr1 hom-inclusion-Subgroup = inclusion-Subgroup G H
+ pr2 hom-inclusion-Subgroup = preserves-mul-inclusion-Subgroup
```
## Properties
diff --git a/src/group-theory/submonoids.lagda.md b/src/group-theory/submonoids.lagda.md
index 53eff2d15c..df35f74d80 100644
--- a/src/group-theory/submonoids.lagda.md
+++ b/src/group-theory/submonoids.lagda.md
@@ -17,6 +17,7 @@ open import foundation.subtype-identity-principle
open import foundation.subtypes
open import foundation.universe-levels
+open import group-theory.homomorphisms-monoids
open import group-theory.monoids
open import group-theory.semigroups
```
@@ -76,10 +77,10 @@ module _
### Submonoids
```agda
-is-submonoid-subset-Monoid-Prop :
+is-submonoid-monoid-Prop :
{l1 l2 : Level} (M : Monoid l1) (P : subset-Monoid l2 M) →
Prop (l1 ⊔ l2)
-is-submonoid-subset-Monoid-Prop M P =
+is-submonoid-monoid-Prop M P =
prod-Prop
( P (unit-Monoid M))
( Π-Prop
@@ -89,15 +90,15 @@ is-submonoid-subset-Monoid-Prop M P =
( type-Monoid M)
( λ y → hom-Prop (P x) (hom-Prop (P y) (P (mul-Monoid M x y))))))
-is-submonoid-subset-Monoid :
+is-submonoid-Monoid :
{l1 l2 : Level} (M : Monoid l1) (P : subset-Monoid l2 M) → UU (l1 ⊔ l2)
-is-submonoid-subset-Monoid M P =
- type-Prop (is-submonoid-subset-Monoid-Prop M P)
+is-submonoid-Monoid M P =
+ type-Prop (is-submonoid-monoid-Prop M P)
Submonoid :
{l1 : Level} (l2 : Level) (M : Monoid l1) → UU (l1 ⊔ lsuc l2)
Submonoid l2 M =
- type-subtype (is-submonoid-subset-Monoid-Prop {l2 = l2} M)
+ type-subtype (is-submonoid-monoid-Prop {l2 = l2} M)
module _
{l1 l2 : Level} (M : Monoid l1) (P : Submonoid l2 M)
@@ -105,9 +106,9 @@ module _
subset-Submonoid : subtype l2 (type-Monoid M)
subset-Submonoid =
- inclusion-subtype (is-submonoid-subset-Monoid-Prop M) P
+ inclusion-subtype (is-submonoid-monoid-Prop M) P
- is-submonoid-Submonoid : is-submonoid-subset-Monoid M subset-Submonoid
+ is-submonoid-Submonoid : is-submonoid-Monoid M subset-Submonoid
is-submonoid-Submonoid = pr2 P
is-in-Submonoid : type-Monoid M → UU l2
@@ -203,6 +204,22 @@ module _
pr1 (pr2 monoid-Submonoid) = unit-Submonoid
pr1 (pr2 (pr2 monoid-Submonoid)) = left-unit-law-mul-Submonoid
pr2 (pr2 (pr2 monoid-Submonoid)) = right-unit-law-mul-Submonoid
+
+ preserves-unit-inclusion-Submonoid :
+ inclusion-Submonoid unit-Submonoid ＝ unit-Monoid M
+ preserves-unit-inclusion-Submonoid = refl
+
+ preserves-mul-inclusion-Submonoid :
+ (x y : type-Submonoid) →
+ inclusion-Submonoid (mul-Submonoid x y) ＝
+ mul-Monoid M (inclusion-Submonoid x) (inclusion-Submonoid y)
+ preserves-mul-inclusion-Submonoid x y = refl
+
+ hom-inclusion-Submonoid :
+ type-hom-Monoid monoid-Submonoid M
+ pr1 (pr1 hom-inclusion-Submonoid) = inclusion-Submonoid
+ pr2 (pr1 hom-inclusion-Submonoid) = preserves-mul-inclusion-Submonoid
+ pr2 hom-inclusion-Submonoid = preserves-unit-inclusion-Submonoid
```
## Properties
@@ -222,7 +239,7 @@ module _
(K : Submonoid l2 M) → (N ＝ K) ≃ has-same-elements-Submonoid K
extensionality-Submonoid =
extensionality-type-subtype
- ( is-submonoid-subset-Monoid-Prop M)
+ ( is-submonoid-monoid-Prop M)
( is-submonoid-Submonoid M N)
( λ x → pair id id)
( extensionality-subtype (subset-Submonoid M N))
diff --git a/src/group-theory/subsemigroups.lagda.md b/src/group-theory/subsemigroups.lagda.md
index ba019cadcf..93ecd65a35 100644
--- a/src/group-theory/subsemigroups.lagda.md
+++ b/src/group-theory/subsemigroups.lagda.md
@@ -17,6 +17,7 @@ open import foundation.subtype-identity-principle
open import foundation.subtypes
open import foundation.universe-levels
+open import group-theory.homomorphisms-semigroups
open import group-theory.semigroups
```
@@ -177,6 +178,17 @@ module _
pr1 semigroup-Subsemigroup = set-Subsemigroup
pr1 (pr2 semigroup-Subsemigroup) = mul-Subsemigroup
pr2 (pr2 semigroup-Subsemigroup) = associative-mul-Subsemigroup
+
+ preserves-mul-inclusion-Subsemigroup :
+ (x y : type-Subsemigroup) →
+ inclusion-Subsemigroup (mul-Subsemigroup x y) ＝
+ mul-Semigroup G (inclusion-Subsemigroup x) (inclusion-Subsemigroup y)
+ preserves-mul-inclusion-Subsemigroup x y = refl
+
+ hom-inclusion-Subsemigroup :
+ type-hom-Semigroup semigroup-Subsemigroup G
+ pr1 hom-inclusion-Subsemigroup = inclusion-Subsemigroup
+ pr2 hom-inclusion-Subsemigroup = preserves-mul-inclusion-Subsemigroup
```
## Properties
diff --git a/src/ring-theory.lagda.md b/src/ring-theory.lagda.md
index 8475f7bc4f..749552f256 100644
--- a/src/ring-theory.lagda.md
+++ b/src/ring-theory.lagda.md
@@ -6,6 +6,8 @@ module ring-theory where
open import ring-theory.algebras-rings public
open import ring-theory.binomial-theorem-rings public
open import ring-theory.binomial-theorem-semirings public
+open import ring-theory.central-elements-rings public
+open import ring-theory.central-elements-semirings public
open import ring-theory.congruence-relations-rings public
open import ring-theory.congruence-relations-semirings public
open import ring-theory.dependent-products-rings public
@@ -16,6 +18,7 @@ open import ring-theory.function-semirings public
open import ring-theory.homomorphisms-rings public
open import ring-theory.ideals-generated-by-subsets-rings public
open import ring-theory.ideals-rings public
+open import ring-theory.ideals-semirings public
open import ring-theory.idempotent-elements-rings public
open import ring-theory.invariant-basis-property-rings public
open import ring-theory.invertible-elements-rings public
@@ -26,6 +29,7 @@ open import ring-theory.maximal-ideals-rings public
open import ring-theory.modules-rings public
open import ring-theory.nil-ideals-rings public
open import ring-theory.nilpotent-elements-rings public
+open import ring-theory.nilpotent-elements-semirings public
open import ring-theory.nontrivial-rings public
open import ring-theory.opposite-rings public
open import ring-theory.powers-of-elements-rings public
@@ -36,6 +40,7 @@ open import ring-theory.radical-ideals-rings 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.sums-rings public
open import ring-theory.sums-semirings public
```
diff --git a/src/ring-theory/central-elements-rings.lagda.md b/src/ring-theory/central-elements-rings.lagda.md
new file mode 100644
index 0000000000..47d1fb435a
--- /dev/null
+++ b/src/ring-theory/central-elements-rings.lagda.md
@@ -0,0 +1,127 @@
+# Central elements of rings
+
+```agda
+module ring-theory.central-elements-rings where
+```
+
+Imports
+
+```agda
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.universe-levels
+
+open import ring-theory.central-elements-semirings
+open import ring-theory.rings
+```
+
+
+
+## Idea
+
+An element `x` of a ring `R` is said to be central if `xy ＝ yx` for every
+`y : R`.
+
+## Definition
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ is-central-element-ring-Prop : type-Ring R → Prop l
+ is-central-element-ring-Prop =
+ is-central-element-semiring-Prop (semiring-Ring R)
+
+ is-central-element-Ring : type-Ring R → UU l
+ is-central-element-Ring = is-central-element-Semiring (semiring-Ring R)
+
+ is-prop-is-central-element-Ring :
+ (x : type-Ring R) → is-prop (is-central-element-Ring x)
+ is-prop-is-central-element-Ring =
+ is-prop-is-central-element-Semiring (semiring-Ring R)
+```
+
+## Properties
+
+### The zero element is central
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ is-central-element-zero-Ring : is-central-element-Ring R (zero-Ring R)
+ is-central-element-zero-Ring =
+ is-central-element-zero-Semiring (semiring-Ring R)
+```
+
+### The unit element is central
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ is-central-element-one-Ring : is-central-element-Ring R (one-Ring R)
+ is-central-element-one-Ring =
+ is-central-element-one-Semiring (semiring-Ring R)
+```
+
+### The sum of two central elements is central
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ is-central-element-add-Ring :
+ (x y : type-Ring R) → is-central-element-Ring R x →
+ is-central-element-Ring R y → is-central-element-Ring R (add-Ring R x y)
+ is-central-element-add-Ring =
+ is-central-element-add-Semiring (semiring-Ring R)
+```
+
+### The negative of a central element is central
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ is-central-element-neg-Ring :
+ (x : type-Ring R) → is-central-element-Ring R x →
+ is-central-element-Ring R (neg-Ring R x)
+ is-central-element-neg-Ring x H y =
+ ( left-negative-law-mul-Ring R x y) ∙
+ ( ( ap (neg-Ring R) (H y)) ∙
+ ( inv (right-negative-law-mul-Ring R y x)))
+```
+
+### `-1` is a central element
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ is-central-element-neg-one-Ring :
+ is-central-element-Ring R (neg-one-Ring R)
+ is-central-element-neg-one-Ring =
+ is-central-element-neg-Ring R (one-Ring R) (is-central-element-one-Ring R)
+```
+
+### The product of two central elements is central
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ is-central-element-mul-Ring :
+ (x y : type-Ring R) → is-central-element-Ring R x →
+ is-central-element-Ring R y → is-central-element-Ring R (mul-Ring R x y)
+ is-central-element-mul-Ring =
+ is-central-element-mul-Semiring (semiring-Ring R)
+```
diff --git a/src/ring-theory/central-elements-semirings.lagda.md b/src/ring-theory/central-elements-semirings.lagda.md
new file mode 100644
index 0000000000..01977c08d3
--- /dev/null
+++ b/src/ring-theory/central-elements-semirings.lagda.md
@@ -0,0 +1,107 @@
+# Central elements of semirings
+
+```agda
+module ring-theory.central-elements-semirings where
+```
+
+Imports
+
+```agda
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.central-elements-monoids
+
+open import ring-theory.semirings
+```
+
+
+
+## Idea
+
+An element `x` of a semiring `R` is said to be central if `xy ＝ yx` for every
+`y : R`.
+
+## Definition
+
+```agda
+module _
+ {l : Level} (R : Semiring l)
+ where
+
+ is-central-element-semiring-Prop : type-Semiring R → Prop l
+ is-central-element-semiring-Prop =
+ is-central-element-monoid-Prop
+ ( multiplicative-monoid-Semiring R)
+
+ is-central-element-Semiring : type-Semiring R → UU l
+ is-central-element-Semiring =
+ is-central-element-Monoid (multiplicative-monoid-Semiring R)
+
+ is-prop-is-central-element-Semiring :
+ (x : type-Semiring R) → is-prop (is-central-element-Semiring x)
+ is-prop-is-central-element-Semiring =
+ is-prop-is-central-element-Monoid (multiplicative-monoid-Semiring R)
+```
+
+## Properties
+
+### The zero element is central
+
+```agda
+module _
+ {l : Level} (R : Semiring l)
+ where
+
+ is-central-element-zero-Semiring :
+ is-central-element-Semiring R (zero-Semiring R)
+ is-central-element-zero-Semiring x =
+ left-zero-law-mul-Semiring R x ∙ inv (right-zero-law-mul-Semiring R x)
+```
+
+### The unit element is central
+
+```agda
+module _
+ {l : Level} (R : Semiring l)
+ where
+
+ is-central-element-one-Semiring :
+ is-central-element-Semiring R (one-Semiring R)
+ is-central-element-one-Semiring =
+ is-central-element-unit-Monoid (multiplicative-monoid-Semiring R)
+```
+
+### The sum of two central elements is central
+
+```agda
+module _
+ {l : Level} (R : Semiring l)
+ where
+
+ is-central-element-add-Semiring :
+ (x y : type-Semiring R) → is-central-element-Semiring R x →
+ is-central-element-Semiring R y →
+ is-central-element-Semiring R (add-Semiring R x y)
+ is-central-element-add-Semiring x y H K z =
+ ( right-distributive-mul-add-Semiring R x y z) ∙
+ ( ( ap-add-Semiring R (H z) (K z)) ∙
+ ( inv (left-distributive-mul-add-Semiring R z x y)))
+```
+
+### The product of two central elements is central
+
+```agda
+module _
+ {l : Level} (R : Semiring l)
+ where
+
+ is-central-element-mul-Semiring :
+ (x y : type-Semiring R) →
+ is-central-element-Semiring R x → is-central-element-Semiring R y →
+ is-central-element-Semiring R (mul-Semiring R x y)
+ is-central-element-mul-Semiring =
+ is-central-element-mul-Monoid (multiplicative-monoid-Semiring R)
+```
diff --git a/src/ring-theory/ideals-rings.lagda.md b/src/ring-theory/ideals-rings.lagda.md
index ae0122dfe9..2b03bb9c5c 100644
--- a/src/ring-theory/ideals-rings.lagda.md
+++ b/src/ring-theory/ideals-rings.lagda.md
@@ -242,8 +242,10 @@ module _
subgroup-two-sided-ideal-Ring : Subgroup l2 (group-Ring R)
pr1 subgroup-two-sided-ideal-Ring = subset-two-sided-ideal-Ring
pr1 (pr2 subgroup-two-sided-ideal-Ring) = contains-zero-two-sided-ideal-Ring
- pr1 (pr2 (pr2 subgroup-two-sided-ideal-Ring)) x y = is-closed-under-add-two-sided-ideal-Ring
- pr2 (pr2 (pr2 subgroup-two-sided-ideal-Ring)) x = is-closed-under-neg-two-sided-ideal-Ring
+ pr1 (pr2 (pr2 subgroup-two-sided-ideal-Ring)) x y =
+ is-closed-under-add-two-sided-ideal-Ring
+ pr2 (pr2 (pr2 subgroup-two-sided-ideal-Ring)) x =
+ is-closed-under-neg-two-sided-ideal-Ring
normal-subgroup-two-sided-ideal-Ring : Normal-Subgroup l2 (group-Ring R)
pr1 normal-subgroup-two-sided-ideal-Ring = subgroup-two-sided-ideal-Ring
@@ -252,9 +254,17 @@ module _
( is-in-two-sided-ideal-Ring)
( equational-reasoning
y
- ＝ add-Ring R y (zero-Ring R) by inv (right-unit-law-add-Ring R y)
- ＝ add-Ring R y (add-Ring R x (neg-Ring R x)) by inv (ap (add-Ring R y) (right-inverse-law-add-Ring R x))
- ＝ add-Ring R (add-Ring R y x) (neg-Ring R x) by inv (associative-add-Ring R y x (neg-Ring R x))
- ＝ add-Ring R (add-Ring R x y) (neg-Ring R x) by ap (add-Ring' R (neg-Ring R x)) (commutative-add-Ring R y x))
+ ＝ add-Ring R y (zero-Ring R)
+ by
+ inv (right-unit-law-add-Ring R y)
+ ＝ add-Ring R y (add-Ring R x (neg-Ring R x))
+ by
+ inv (ap (add-Ring R y) (right-inverse-law-add-Ring R x))
+ ＝ add-Ring R (add-Ring R y x) (neg-Ring R x)
+ by
+ inv (associative-add-Ring R y x (neg-Ring R x))
+ ＝ add-Ring R (add-Ring R x y) (neg-Ring R x)
+ by
+ ap (add-Ring' R (neg-Ring R x)) (commutative-add-Ring R y x))
( H)
```
diff --git a/src/ring-theory/ideals-semirings.lagda.md b/src/ring-theory/ideals-semirings.lagda.md
new file mode 100644
index 0000000000..fd527f1b91
--- /dev/null
+++ b/src/ring-theory/ideals-semirings.lagda.md
@@ -0,0 +1,254 @@
+# Ideals in semirings
+
+```agda
+module ring-theory.ideals-semirings where
+```
+
+Imports
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.equational-reasoning
+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
+```
+
+
@@ -28,16 +33,80 @@ number `n` such that `x^n = 0`.
## Definition
```agda
-is-nilpotent-element-ring-Prop :
- {l : Level} (R : Ring l) → type-Ring R → Prop l
-is-nilpotent-element-ring-Prop R x = ∃-Prop ℕ (λ n → Id (power-Ring R n x) (zero-Ring R))
-
-is-nilpotent-element-Ring : {l : Level} (R : Ring l) → type-Ring R → UU l
-is-nilpotent-element-Ring R x = type-Prop (is-nilpotent-element-ring-Prop R x)
-
-is-prop-is-nilpotent-element-Ring :
- {l : Level} (R : Ring l) (x : type-Ring R) →
- is-prop (is-nilpotent-element-Ring R x)
-is-prop-is-nilpotent-element-Ring R x =
- is-prop-type-Prop (is-nilpotent-element-ring-Prop R x)
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ is-nilpotent-element-ring-Prop : type-Ring R → Prop l
+ is-nilpotent-element-ring-Prop =
+ is-nilpotent-element-semiring-Prop (semiring-Ring R)
+
+ is-nilpotent-element-Ring : type-Ring R → UU l
+ is-nilpotent-element-Ring = is-nilpotent-element-Semiring (semiring-Ring R)
+
+ is-prop-is-nilpotent-element-Ring :
+ (x : type-Ring R) → is-prop (is-nilpotent-element-Ring x)
+ is-prop-is-nilpotent-element-Ring =
+ is-prop-is-nilpotent-element-Semiring (semiring-Ring R)
+```
+
+## Properties
+
+### Zero is nilpotent
+
+```agda
+is-nilpotent-zero-Ring :
+ {l : Level} (R : Ring l) → is-nilpotent-element-Ring R (zero-Ring R)
+is-nilpotent-zero-Ring R = is-nilpotent-zero-Semiring (semiring-Ring R)
+```
+
+### If `x` and `y` commute and are both nilpotent, then `x + y` is nilpotent
+
+```agda
+is-nilpotent-add-Ring :
+ {l : Level} (R : Ring l) →
+ (x y : type-Ring R) → (mul-Ring R x y ＝ mul-Ring R y x) →
+ is-nilpotent-element-Ring R x → is-nilpotent-element-Ring R y →
+ is-nilpotent-element-Ring R (add-Ring R x y)
+is-nilpotent-add-Ring R = is-nilpotent-add-Semiring (semiring-Ring R)
+```
+
+### If `x` is nilpotent, then so is `-x`
+
+```agda
+is-nilpotent-element-neg-Ring :
+ {l : Level} (R : Ring l) →
+ is-closed-under-negatives-subset-Ring R (is-nilpotent-element-ring-Prop R)
+is-nilpotent-element-neg-Ring R x H =
+ apply-universal-property-trunc-Prop H
+ ( is-nilpotent-element-ring-Prop R (neg-Ring R x))
+ ( λ (n , p) →
+ intro-∃ n
+ ( ( power-neg-Ring R n x) ∙
+ ( ( ap (mul-Ring R (power-Ring R n (neg-one-Ring R))) p) ∙
+ ( right-zero-law-mul-Ring R (power-Ring R n (neg-one-Ring R))))))
+```
+
+### If `x` is nilpotent and `y` commutes with `x`, then `xy` is also nilpotent
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ is-nilpotent-element-mul-Ring :
+ (x y : type-Ring R) →
+ mul-Ring R x y ＝ mul-Ring R y x →
+ is-nilpotent-element-Ring R x →
+ is-nilpotent-element-Ring R (mul-Ring R x y)
+ is-nilpotent-element-mul-Ring =
+ is-nilpotent-element-mul-Semiring (semiring-Ring R)
+
+ is-nilpotent-element-mul-Ring' :
+ (x y : type-Ring R) →
+ mul-Ring R x y ＝ mul-Ring R y x →
+ is-nilpotent-element-Ring R x →
+ is-nilpotent-element-Ring R (mul-Ring R y x)
+ is-nilpotent-element-mul-Ring' =
+ is-nilpotent-element-mul-Semiring' (semiring-Ring R)
```
diff --git a/src/ring-theory/nilpotent-elements-semirings.lagda.md b/src/ring-theory/nilpotent-elements-semirings.lagda.md
new file mode 100644
index 0000000000..a2c34f576e
--- /dev/null
+++ b/src/ring-theory/nilpotent-elements-semirings.lagda.md
@@ -0,0 +1,240 @@
+# Nilpotent elements in semirings
+
+```agda
+module ring-theory.nilpotent-elements-semirings where
+```
+
+Imports
+
+```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.binomial-coefficients
+open import elementary-number-theory.distance-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import ring-theory.binomial-theorem-semirings
+open import ring-theory.powers-of-elements-semirings
+open import ring-theory.semirings
+open import ring-theory.subsets-semirings
+open import ring-theory.sums-semirings
+
+open import univalent-combinatorics.coproduct-types
+open import univalent-combinatorics.standard-finite-types
+```
+
+Imports
```agda
+open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.parity-natural-numbers
+open import foundation.empty-types
+open import foundation.functions
open import foundation.identity-types
open import foundation.universe-levels
+open import ring-theory.central-elements-rings
open import ring-theory.powers-of-elements-semirings
open import ring-theory.rings
```
@@ -45,6 +50,20 @@ module _
power-succ-Ring = power-succ-Semiring (semiring-Ring R)
```
+### Powers by sums of natural numbers are products of powers
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ power-add-Ring :
+ (m n : ℕ) {x : type-Ring R} →
+ power-Ring R (add-ℕ m n) x ＝
+ mul-Ring R (power-Ring R m x) (power-Ring R n x)
+ power-add-Ring = power-add-Semiring (semiring-Ring R)
+```
+
### If `x` commutes with `y` then so do their powers
```agda
@@ -65,3 +84,86 @@ module _
( mul-Ring R (power-Ring R n y) (power-Ring R m x))
commute-powers-Ring = commute-powers-Semiring (semiring-Ring R)
```
+
+### If `x` commutes with `y`, then powers distribute over the product of `x` and `y`.
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ distributive-power-mul-Ring :
+ (n : ℕ) {x y : type-Ring R} → mul-Ring R x y ＝ mul-Ring R y x →
+ power-Ring R n (mul-Ring R x y) ＝
+ mul-Ring R (power-Ring R n x) (power-Ring R n y)
+ distributive-power-mul-Ring =
+ distributive-power-mul-Semiring (semiring-Ring R)
+```
+
+### `(-x)ⁿ = (-1)ⁿxⁿ`
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ power-neg-Ring :
+ (n : ℕ) (x : type-Ring R) →
+ power-Ring R n (neg-Ring R x) ＝
+ mul-Ring R (power-Ring R n (neg-one-Ring R)) (power-Ring R n x)
+ power-neg-Ring n x =
+ ( ap (power-Ring R n) (inv (mul-neg-one-Ring R x))) ∙
+ ( distributive-power-mul-Ring R n (is-central-element-neg-one-Ring R x))
+
+ even-power-neg-Ring :
+ (n : ℕ) (x : type-Ring R) →
+ is-even-ℕ n → power-Ring R n (neg-Ring R x) ＝ power-Ring R n x
+ even-power-neg-Ring zero-ℕ x H = refl
+ even-power-neg-Ring (succ-ℕ zero-ℕ) x H = ex-falso (is-odd-one-ℕ H)
+ even-power-neg-Ring (succ-ℕ (succ-ℕ n)) x H =
+ ( right-negative-law-mul-Ring R
+ ( power-Ring R (succ-ℕ n) (neg-Ring R x))
+ ( x)) ∙
+ ( ( ap
+ ( neg-Ring R)
+ ( ( ap
+ ( mul-Ring' R x)
+ ( ( power-succ-Ring R n (neg-Ring R x)) ∙
+ ( ( right-negative-law-mul-Ring R
+ ( power-Ring R n (neg-Ring R x))
+ ( x)) ∙
+ ( ap
+ ( neg-Ring R)
+ ( ( ap
+ ( mul-Ring' R x)
+ ( even-power-neg-Ring n x
+ ( is-even-is-even-succ-succ-ℕ n H))) ∙
+ ( inv (power-succ-Ring R n x))))))) ∙
+ ( left-negative-law-mul-Ring R (power-Ring R (succ-ℕ n) x) x))) ∙
+ ( neg-neg-Ring R (power-Ring R (succ-ℕ (succ-ℕ n)) x)))
+
+ odd-power-neg-Ring :
+ (n : ℕ) (x : type-Ring R) →
+ is-odd-ℕ n → power-Ring R n (neg-Ring R x) ＝ neg-Ring R (power-Ring R n x)
+ odd-power-neg-Ring zero-ℕ x H = ex-falso (H is-even-zero-ℕ)
+ odd-power-neg-Ring (succ-ℕ zero-ℕ) x H = refl
+ odd-power-neg-Ring (succ-ℕ (succ-ℕ n)) x H =
+ ( right-negative-law-mul-Ring R
+ ( power-Ring R (succ-ℕ n) (neg-Ring R x))
+ ( x)) ∙
+ ( ap
+ ( neg-Ring R ∘ mul-Ring' R x)
+ ( ( power-succ-Ring R n (neg-Ring R x)) ∙
+ ( ( right-negative-law-mul-Ring R
+ ( power-Ring R n (neg-Ring R x))
+ ( x)) ∙
+ ( ( ap
+ ( neg-Ring R)
+ ( ( ap
+ ( mul-Ring' R x)
+ ( odd-power-neg-Ring n x
+ ( is-odd-is-odd-succ-succ-ℕ n H))) ∙
+ ( ( left-negative-law-mul-Ring R (power-Ring R n x) x) ∙
+ ( ap (neg-Ring R) (inv (power-succ-Ring R n x)))))) ∙
+ ( neg-neg-Ring R (power-Ring R (succ-ℕ n) x))))))
+```
diff --git a/src/ring-theory/powers-of-elements-semirings.lagda.md b/src/ring-theory/powers-of-elements-semirings.lagda.md
index e1d6e5d077..4cfed7e2ba 100644
--- a/src/ring-theory/powers-of-elements-semirings.lagda.md
+++ b/src/ring-theory/powers-of-elements-semirings.lagda.md
@@ -7,6 +7,7 @@ module ring-theory.powers-of-elements-semirings where
Imports
```agda
+open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers
open import foundation.identity-types
@@ -49,6 +50,33 @@ module _
power-succ-Semiring (succ-ℕ n) x = refl
```
+### Powers by sums of natural numbers are products of powers
+
+```agda
+module _
+ {l : Level} (R : Semiring l)
+ where
+
+ power-add-Semiring :
+ (m n : ℕ) {x : type-Semiring R} →
+ power-Semiring R (add-ℕ m n) x ＝
+ mul-Semiring R (power-Semiring R m x) (power-Semiring R n x)
+ power-add-Semiring m zero-ℕ {x} =
+ inv
+ ( right-unit-law-mul-Semiring R
+ ( power-Semiring R m x))
+ power-add-Semiring m (succ-ℕ n) {x} =
+ ( power-succ-Semiring R (add-ℕ m n) x) ∙
+ ( ( ap (mul-Semiring' R x) (power-add-Semiring m n)) ∙
+ ( ( associative-mul-Semiring R
+ ( power-Semiring R m x)
+ ( power-Semiring R n x)
+ ( x)) ∙
+ ( ap
+ ( mul-Semiring R (power-Semiring R m x))
+ ( inv (power-succ-Semiring R n x)))))
+```
+
### If `x` commutes with `y` then so do their powers
```agda
@@ -147,3 +175,50 @@ module _
( mul-Semiring R (power-Semiring R (succ-ℕ n) y))
( inv (power-succ-Semiring R m x))))))))
```
+
+### If `x` commutes with `y`, then powers distribute over the product of `x` and `y`.
+
+```agda
+module _
+ {l : Level} (R : Semiring l)
+ where
+
+ distributive-power-mul-Semiring :
+ (n : ℕ) {x y : type-Semiring R} →
+ (H : mul-Semiring R x y ＝ mul-Semiring R y x) →
+ power-Semiring R n (mul-Semiring R x y) ＝
+ mul-Semiring R (power-Semiring R n x) (power-Semiring R n y)
+ distributive-power-mul-Semiring zero-ℕ H =
+ inv (left-unit-law-mul-Semiring R (one-Semiring R))
+ distributive-power-mul-Semiring (succ-ℕ n) {x} {y} H =
+ ( power-succ-Semiring R n (mul-Semiring R x y)) ∙
+ ( ( ap
+ ( mul-Semiring' R (mul-Semiring R x y))
+ ( distributive-power-mul-Semiring n H)) ∙
+ ( ( inv
+ ( associative-mul-Semiring R
+ ( mul-Semiring R (power-Semiring R n x) (power-Semiring R n y))
+ ( x)
+ ( y))) ∙
+ ( ( ap
+ ( mul-Semiring' R y)
+ ( ( associative-mul-Semiring R
+ ( power-Semiring R n x)
+ ( power-Semiring R n y)
+ ( x)) ∙
+ ( ( ap
+ ( mul-Semiring R (power-Semiring R n x))
+ ( commute-powers-Semiring' R n (inv H))) ∙
+ ( inv
+ ( associative-mul-Semiring R
+ ( power-Semiring R n x)
+ ( x)
+ ( power-Semiring R n y)))))) ∙
+ ( ( associative-mul-Semiring R
+ ( mul-Semiring R (power-Semiring R n x) x)
+ ( power-Semiring R n y)
+ ( y)) ∙
+ ( ap-mul-Semiring R
+ ( inv (power-succ-Semiring R n x))
+ ( inv (power-succ-Semiring R n y)))))))
+```
diff --git a/src/ring-theory/rings.lagda.md b/src/ring-theory/rings.lagda.md
index f7db511c15..3ada9ebdbc 100644
--- a/src/ring-theory/rings.lagda.md
+++ b/src/ring-theory/rings.lagda.md
@@ -18,6 +18,7 @@ open import foundation.embeddings
open import foundation.equivalences
open import foundation.identity-types
open import foundation.injective-maps
+open import foundation.involutions
open import foundation.negation
open import foundation.propositions
open import foundation.sets
@@ -209,6 +210,14 @@ module _
right-inverse-law-add-Ring :
(x : type-Ring R) → Id (add-Ring R x (neg-Ring x)) (zero-Ring R)
right-inverse-law-add-Ring = right-inverse-law-add-Ab (ab-Ring R)
+
+ neg-neg-Ring : (x : type-Ring R) → neg-Ring (neg-Ring x) ＝ x
+ neg-neg-Ring = neg-neg-Ab (ab-Ring R)
+
+ distributive-neg-add-Ring :
+ (x y : type-Ring R) →
+ neg-Ring (add-Ring R x y) ＝ add-Ring R (neg-Ring x) (neg-Ring y)
+ distributive-neg-add-Ring = distributive-neg-add-Ab (ab-Ring R)
```
### Multiplication in a ring
@@ -342,17 +351,81 @@ module _
neg-one-Ring = neg-Ring R (one-Ring R)
mul-neg-one-Ring :
- (x : type-Ring R) → Id (mul-Ring R neg-one-Ring x) (neg-Ring R x)
+ (x : type-Ring R) → mul-Ring R neg-one-Ring x ＝ neg-Ring R x
mul-neg-one-Ring x =
+ is-injective-add-Ring R x
+ ( ( ( ap
+ ( add-Ring' R (mul-Ring R neg-one-Ring x))
+ ( inv (left-unit-law-mul-Ring R x))) ∙
+ ( ( inv
+ ( right-distributive-mul-add-Ring R
+ ( one-Ring R)
+ ( neg-one-Ring)
+ ( x))) ∙
+ ( ( ap
+ ( mul-Ring' R x)
+ ( right-inverse-law-add-Ring R (one-Ring R))) ∙
+ ( left-zero-law-mul-Ring R x)))) ∙
+ ( inv (right-inverse-law-add-Ring R x)))
+
+ mul-neg-one-Ring' :
+ (x : type-Ring R) → mul-Ring R x neg-one-Ring ＝ neg-Ring R x
+ mul-neg-one-Ring' x =
is-injective-add-Ring R x
( ( ap
- ( add-Ring' R (mul-Ring R neg-one-Ring x))
- ( inv (left-unit-law-mul-Ring R x)) ∙
+ ( add-Ring' R (mul-Ring R x neg-one-Ring))
+ ( inv (right-unit-law-mul-Ring R x))) ∙
( ( inv
- ( right-distributive-mul-add-Ring R (one-Ring R) neg-one-Ring x)) ∙
- ( ( ap (mul-Ring' R x) (right-inverse-law-add-Ring R (one-Ring R))) ∙
- ( left-zero-law-mul-Ring R x)))) ∙
- ( inv (right-inverse-law-add-Ring R x)))
+ ( left-distributive-mul-add-Ring R x (one-Ring R) neg-one-Ring)) ∙
+ ( ( ap (mul-Ring R x) (right-inverse-law-add-Ring R (one-Ring R))) ∙
+ ( ( right-zero-law-mul-Ring R x) ∙
+ ( inv (right-inverse-law-add-Ring R x))))))
+
+ is-involution-mul-neg-one-Ring :
+ is-involution (mul-Ring R neg-one-Ring)
+ is-involution-mul-neg-one-Ring x =
+ ( mul-neg-one-Ring (mul-Ring R neg-one-Ring x)) ∙
+ ( ( ap (neg-Ring R) (mul-neg-one-Ring x)) ∙
+ ( neg-neg-Ring R x))
+
+ is-involution-mul-neg-one-Ring' :
+ is-involution (mul-Ring' R neg-one-Ring)
+ is-involution-mul-neg-one-Ring' x =
+ ( mul-neg-one-Ring' (mul-Ring R x neg-one-Ring)) ∙
+ ( ( ap (neg-Ring R) (mul-neg-one-Ring' x)) ∙
+ ( neg-neg-Ring R x))
+```
+
+### Left and right negative laws for multiplication
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ left-negative-law-mul-Ring :
+ (x y : type-Ring R) →
+ mul-Ring R (neg-Ring R x) y ＝ neg-Ring R (mul-Ring R x y)
+ left-negative-law-mul-Ring x y =
+ ( ap (mul-Ring' R y) (inv (mul-neg-one-Ring R x))) ∙
+ ( ( associative-mul-Ring R (neg-one-Ring R) x y) ∙
+ ( mul-neg-one-Ring R (mul-Ring R x y)))
+
+ right-negative-law-mul-Ring :
+ (x y : type-Ring R) →
+ mul-Ring R x (neg-Ring R y) ＝ neg-Ring R (mul-Ring R x y)
+ right-negative-law-mul-Ring x y =
+ ( ap (mul-Ring R x) (inv (mul-neg-one-Ring' R y))) ∙
+ ( ( inv (associative-mul-Ring R x y (neg-one-Ring R))) ∙
+ ( mul-neg-one-Ring' R (mul-Ring R x y)))
+
+ mul-neg-Ring :
+ (x y : type-Ring R) →
+ mul-Ring R (neg-Ring R x) (neg-Ring R y) ＝ mul-Ring R x y
+ mul-neg-Ring x y =
+ ( left-negative-law-mul-Ring x (neg-Ring R y)) ∙
+ ( ( ap (neg-Ring R) (right-negative-law-mul-Ring x y)) ∙
+ ( neg-neg-Ring R (mul-Ring R x y)))
```
### Scalar multiplication of ring elements by a natural number
@@ -370,6 +443,16 @@ module _
(m ＝ n) → (x ＝ y) → mul-nat-scalar-Ring m x ＝ mul-nat-scalar-Ring n y
ap-mul-nat-scalar-Ring = ap-mul-nat-scalar-Semiring (semiring-Ring R)
+ left-zero-law-mul-nat-scalar-Ring :
+ (x : type-Ring R) → mul-nat-scalar-Ring 0 x ＝ zero-Ring R
+ left-zero-law-mul-nat-scalar-Ring =
+ left-zero-law-mul-nat-scalar-Semiring (semiring-Ring R)
+
+ right-zero-law-mul-nat-scalar-Ring :
+ (n : ℕ) → mul-nat-scalar-Ring n (zero-Ring R) ＝ zero-Ring R
+ right-zero-law-mul-nat-scalar-Ring =
+ right-zero-law-mul-nat-scalar-Semiring (semiring-Ring R)
+
left-unit-law-mul-nat-scalar-Ring :
(x : type-Ring R) → mul-nat-scalar-Ring 1 x ＝ x
left-unit-law-mul-nat-scalar-Ring =
diff --git a/src/ring-theory/semirings.lagda.md b/src/ring-theory/semirings.lagda.md
index 131ab04687..158eb70c1f 100644
--- a/src/ring-theory/semirings.lagda.md
+++ b/src/ring-theory/semirings.lagda.md
@@ -294,6 +294,17 @@ module _
mul-nat-scalar-Semiring m x ＝ mul-nat-scalar-Semiring n y
ap-mul-nat-scalar-Semiring p q = ap-binary mul-nat-scalar-Semiring p q
+ left-zero-law-mul-nat-scalar-Semiring :
+ (x : type-Semiring R) → mul-nat-scalar-Semiring 0 x ＝ zero-Semiring R
+ left-zero-law-mul-nat-scalar-Semiring x = refl
+
+ right-zero-law-mul-nat-scalar-Semiring :
+ (n : ℕ) → mul-nat-scalar-Semiring n (zero-Semiring R) ＝ zero-Semiring R
+ right-zero-law-mul-nat-scalar-Semiring zero-ℕ = refl
+ right-zero-law-mul-nat-scalar-Semiring (succ-ℕ n) =
+ ( right-unit-law-add-Semiring R _) ∙
+ ( right-zero-law-mul-nat-scalar-Semiring n)
+
left-unit-law-mul-nat-scalar-Semiring :
(x : type-Semiring R) → mul-nat-scalar-Semiring 1 x ＝ x
left-unit-law-mul-nat-scalar-Semiring x = left-unit-law-add-Semiring R x
diff --git a/src/ring-theory/subsets-rings.lagda.md b/src/ring-theory/subsets-rings.lagda.md
index 1dbe02e02d..1198cbec35 100644
--- a/src/ring-theory/subsets-rings.lagda.md
+++ b/src/ring-theory/subsets-rings.lagda.md
@@ -24,6 +24,8 @@ A subset of a ring is a subtype of the underlying type of a ring
## Definition
+### Subsets of rings
+
```agda
subset-Ring :
(l : Level) {l1 : Level} (R : Ring l1) → UU ((lsuc l) ⊔ l1)
@@ -44,3 +46,66 @@ module _
inclusion-subset-Ring : type-subset-Ring → type-Ring R
inclusion-subset-Ring = pr1
```
+
+### The condition that a subset contains zero
+
+```agda
+module _
+ {l1 l2 : Level} (R : Ring l1) (S : subset-Ring l2 R)
+ where
+
+ contains-zero-subset-Ring : UU l2
+ contains-zero-subset-Ring = is-in-subtype S (zero-Ring R)
+```
+
+### The condition that a subset contains one
+
+```agda
+ contains-one-subset-Ring : UU l2
+ contains-one-subset-Ring = is-in-subtype S (one-Ring R)
+```
+
+### The condition that a subset is closed under addition
+
+```agda
+ is-closed-under-addition-subset-Ring : UU (l1 ⊔ l2)
+ is-closed-under-addition-subset-Ring =
+ (x y : type-Ring R) →
+ is-in-subtype S x → is-in-subtype S y →
+ is-in-subtype S (add-Ring R x y)
+```
+
+### The condition that a subset is closed under negatives
+
+```agda
+ is-closed-under-negatives-subset-Ring : UU (l1 ⊔ l2)
+ is-closed-under-negatives-subset-Ring =
+ (x : type-Ring R) → is-in-subtype S x → is-in-subtype S (neg-Ring R x)
+```
+
+### The condition that a subset is closed under multiplication
+
+```agda
+ is-closed-under-multiplication-subset-Ring : UU (l1 ⊔ l2)
+ is-closed-under-multiplication-subset-Ring =
+ (x y : type-Ring R) → is-in-subtype S x → is-in-subtype S y →
+ is-in-subtype S (mul-Ring R x y)
+```
+
+### The condition that a subset is closed under multiplication from the left by an arbitrary element
+
+```agda
+ is-closed-under-left-multiplication-subset-Ring : UU (l1 ⊔ l2)
+ is-closed-under-left-multiplication-subset-Ring =
+ (x y : type-Ring R) → is-in-subtype S y →
+ is-in-subtype S (mul-Ring R x y)
+```
+
+### The condition that a subset is closed-under-multiplication from the right by an arbitrary element
+
+```agda
+ is-closed-under-right-multiplication-subset-Ring : UU (l1 ⊔ l2)
+ is-closed-under-right-multiplication-subset-Ring =
+ (x y : type-Ring R) → is-in-subtype S x →
+ is-in-subtype S (mul-Ring R x y)
+```
diff --git a/src/ring-theory/subsets-semirings.lagda.md b/src/ring-theory/subsets-semirings.lagda.md
new file mode 100644
index 0000000000..830589e302
--- /dev/null
+++ b/src/ring-theory/subsets-semirings.lagda.md
@@ -0,0 +1,103 @@
+# Subsets of semirings
+
+```agda
+module ring-theory.subsets-semirings where
+```
+
+Imports
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.propositional-extensionality
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import ring-theory.semirings
+```
+
+Imports
```agda
+open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers
open import foundation.functions
@@ -20,6 +21,7 @@ open import linear-algebra.vectors-on-rings
open import ring-theory.rings
open import ring-theory.sums-semirings
+open import univalent-combinatorics.coproduct-types
open import univalent-combinatorics.standard-finite-types
```
@@ -167,3 +169,28 @@ module _
sum-Ring R n f
shift-sum-Ring = shift-sum-Semiring (semiring-Ring R)
```
+
+### A sum of zeroes is zero
+
+```agda
+module _
+ {l : Level} (R : Ring l)
+ where
+
+ sum-zero-Ring :
+ (n : ℕ) → sum-Ring R n (zero-functional-vec-Ring R n) ＝ zero-Ring R
+ sum-zero-Ring = sum-zero-Semiring (semiring-Ring R)
+```
+
+### Splitting Sums
+
+```agda
+split-sum-Ring :
+ {l : Level} (R : Ring l)
+ (n m : ℕ) (f : functional-vec-Ring R (add-ℕ n m)) →
+ sum-Ring R (add-ℕ n m) f ＝
+ add-Ring R
+ ( sum-Ring R n (f ∘ inl-coprod-Fin n m))
+ ( sum-Ring R m (f ∘ inr-coprod-Fin n m))
+split-sum-Ring R = split-sum-Semiring (semiring-Ring R)
+```
diff --git a/src/ring-theory/sums-semirings.lagda.md b/src/ring-theory/sums-semirings.lagda.md
index cb64d58791..1657d6938d 100644
--- a/src/ring-theory/sums-semirings.lagda.md
+++ b/src/ring-theory/sums-semirings.lagda.md
@@ -7,6 +7,7 @@ module ring-theory.sums-semirings where
Imports
```agda
+open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers
open import foundation.coproduct-types
@@ -21,6 +22,7 @@ open import linear-algebra.vectors-on-semirings
open import ring-theory.semirings
+open import univalent-combinatorics.coproduct-types
open import univalent-combinatorics.standard-finite-types
```
@@ -229,3 +231,37 @@ module _
( shift-sum-Semiring n
( tail-functional-vec-Semiring R n f))
```
+
+### A sum of zeroes is zero
+
+```agda
+module _
+ {l : Level} (R : Semiring l)
+ where
+
+ sum-zero-Semiring :
+ (n : ℕ) →
+ sum-Semiring R n (zero-functional-vec-Semiring R n) ＝ zero-Semiring R
+ sum-zero-Semiring zero-ℕ = refl
+ sum-zero-Semiring (succ-ℕ n) =
+ right-unit-law-add-Semiring R _ ∙ sum-zero-Semiring n
+```
+
+### Splitting Sums
+
+```agda
+split-sum-Semiring :
+ {l : Level} (R : Semiring l)
+ (n m : ℕ) (f : functional-vec-Semiring R (add-ℕ n m)) →
+ sum-Semiring R (add-ℕ n m) f ＝
+ add-Semiring R
+ ( sum-Semiring R n (f ∘ inl-coprod-Fin n m))
+ ( sum-Semiring R m (f ∘ inr-coprod-Fin n m))
+split-sum-Semiring R n zero-ℕ f =
+ inv (right-unit-law-add-Semiring R (sum-Semiring R n f))
+split-sum-Semiring R n (succ-ℕ m) f =
+ ( ap
+ ( add-Semiring' R (f(inr star)))
+ ( split-sum-Semiring R n m (f ∘ inl))) ∙
+ ( associative-add-Semiring R _ _ _ )
+```
diff --git a/src/univalent-combinatorics/coproduct-types.lagda.md b/src/univalent-combinatorics/coproduct-types.lagda.md
index 726f5abd2f..0757fa620d 100644
--- a/src/univalent-combinatorics/coproduct-types.lagda.md
+++ b/src/univalent-combinatorics/coproduct-types.lagda.md
@@ -16,11 +16,13 @@ open import foundation.equivalences
open import foundation.functions
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-propositional-truncation
+open import foundation.homotopies
open import foundation.identity-types
open import foundation.mere-equivalences
open import foundation.propositional-truncations
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-empty-type
+open import foundation.unit-type
open import foundation.universe-levels
open import univalent-combinatorics.counting
@@ -48,9 +50,48 @@ coprod-Fin k zero-ℕ = right-unit-law-coprod (Fin k)
coprod-Fin k (succ-ℕ l) =
(equiv-coprod (coprod-Fin k l) id-equiv) ∘e inv-assoc-coprod
+map-coprod-Fin :
+ (k l : ℕ) → (Fin k + Fin l) → Fin (add-ℕ k l)
+map-coprod-Fin k l = map-equiv (coprod-Fin k l)
+
Fin-add-ℕ :
(k l : ℕ) → Fin (add-ℕ k l) ≃ (Fin k + Fin l)
Fin-add-ℕ k l = inv-equiv (coprod-Fin k l)
+
+inl-coprod-Fin :
+ (k l : ℕ) → Fin k → Fin (add-ℕ k l)
+inl-coprod-Fin k l = map-coprod-Fin k l ∘ inl
+
+inr-coprod-Fin :
+ (k l : ℕ) → Fin l → Fin (add-ℕ k l)
+inr-coprod-Fin k l = map-coprod-Fin k l ∘ inr
+
+compute-inl-coprod-Fin :
+ (k : ℕ) → inl-coprod-Fin k 0 ~ id
+compute-inl-coprod-Fin k x = refl
+```
+
+### Inclusion of `coprod-Fin` into the natural numbers
+
+```agda
+nat-coprod-Fin :
+ (n m : ℕ) → (x : Fin n + Fin m) →
+ nat-Fin (add-ℕ n m) (map-coprod-Fin n m x) ＝
+ ind-coprod _ (nat-Fin n) (λ i → add-ℕ n (nat-Fin m i)) x
+nat-coprod-Fin n zero-ℕ (inl x) = refl
+nat-coprod-Fin n (succ-ℕ m) (inl x) = nat-coprod-Fin n m (inl x)
+nat-coprod-Fin n (succ-ℕ m) (inr (inl x)) = nat-coprod-Fin n m (inr x)
+nat-coprod-Fin n (succ-ℕ m) (inr (inr star)) = refl
+
+nat-inl-coprod-Fin :
+ (n m : ℕ) (i : Fin n) →
+ nat-Fin (add-ℕ n m) (inl-coprod-Fin n m i) ＝ nat-Fin n i
+nat-inl-coprod-Fin n m i = nat-coprod-Fin n m (inl i)
+
+nat-inr-coprod-Fin :
+ (n m : ℕ) (i : Fin m) →
+ nat-Fin (add-ℕ n m) (inr-coprod-Fin n m i) ＝ add-ℕ n (nat-Fin m i)
+nat-inr-coprod-Fin n m i = nat-coprod-Fin n m (inr i)
```
### Types equipped with a count are closed under coproducts
diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md
index 6419281722..a267d18322 100644
--- a/src/univalent-combinatorics/standard-finite-types.lagda.md
+++ b/src/univalent-combinatorics/standard-finite-types.lagda.md
@@ -183,6 +183,11 @@ upper-bound-nat-Fin (succ-ℕ k) (inl x) =
preserves-leq-succ-ℕ (nat-Fin (succ-ℕ k) x) k (upper-bound-nat-Fin k x)
upper-bound-nat-Fin (succ-ℕ k) (inr star) = refl-leq-ℕ (succ-ℕ k)
+upper-bound-nat-Fin' :
+ (k : ℕ) (x : Fin k) → leq-ℕ (nat-Fin k x) k
+upper-bound-nat-Fin' k x =
+ leq-le-ℕ {nat-Fin k x} {k} (strict-upper-bound-nat-Fin k x)
+
is-injective-nat-Fin : (k : ℕ) → is-injective (nat-Fin k)
is-injective-nat-Fin (succ-ℕ k) {inl x} {inl y} p =
ap inl (is-injective-nat-Fin k p)