diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 843af39e47..065549cb7c 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -53,7 +53,6 @@ open import elementary-number-theory.goldbach-conjecture public open import elementary-number-theory.greatest-common-divisor-integers public open import elementary-number-theory.greatest-common-divisor-natural-numbers public open import elementary-number-theory.group-of-integers public -open import elementary-number-theory.groups-of-modular-arithmetic public open import elementary-number-theory.half-integers public open import elementary-number-theory.inequality-integer-fractions public open import elementary-number-theory.inequality-integers public @@ -85,7 +84,7 @@ open import elementary-number-theory.multiplication-natural-numbers public open import elementary-number-theory.multiplication-rational-numbers public open import elementary-number-theory.multiplicative-monoid-of-natural-numbers public open import elementary-number-theory.multiplicative-units-integers public -open import elementary-number-theory.multiplicative-units-modular-arithmetic public +open import elementary-number-theory.multiplicative-units-standard-cyclic-rings public open import elementary-number-theory.multiset-coefficients public open import elementary-number-theory.natural-numbers public open import elementary-number-theory.nonzero-integers public @@ -107,12 +106,13 @@ open import elementary-number-theory.relatively-prime-natural-numbers public open import elementary-number-theory.repeating-element-standard-finite-type public open import elementary-number-theory.retracts-of-natural-numbers public open import elementary-number-theory.ring-of-integers public -open import elementary-number-theory.rings-of-modular-arithmetic public open import elementary-number-theory.sieve-of-eratosthenes public open import elementary-number-theory.square-free-natural-numbers public open import elementary-number-theory.squares-integers public open import elementary-number-theory.squares-modular-arithmetic public open import elementary-number-theory.squares-natural-numbers public +open import elementary-number-theory.standard-cyclic-groups public +open import elementary-number-theory.standard-cyclic-rings public open import elementary-number-theory.stirling-numbers-of-the-second-kind public open import elementary-number-theory.strict-inequality-natural-numbers public open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public diff --git a/src/elementary-number-theory/eulers-totient-function.lagda.md b/src/elementary-number-theory/eulers-totient-function.lagda.md index 70f1a51592..13a8305760 100644 --- a/src/elementary-number-theory/eulers-totient-function.lagda.md +++ b/src/elementary-number-theory/eulers-totient-function.lagda.md @@ -29,7 +29,7 @@ open import univalent-combinatorics.standard-finite-types **Euler's totient function** `φ : ℕ → ℕ` is the function that maps a [natural number](elementary-number-theory.natural-numbers.md) `n` to the number of -[multiplicative units modulo `n`](elementary-number-theory.multiplicative-units-modular-arithmetic.md). +[multiplicative units modulo `n`](elementary-number-theory.multiplicative-units-standard-cyclic-rings.md). In other words, the number `φ n` is the cardinality of the [group of units](ring-theory.groups-of-units-rings.md) of the [ring](ring-theory.rings.md) `ℤ-Mod n`. @@ -58,3 +58,9 @@ eulers-totient-function-relatively-prime n = ( Fin-𝔽 n) ( λ x → is-relatively-prime-ℕ-Decidable-Prop (nat-Fin n x) n) ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/elementary-number-theory/finitely-cyclic-maps.lagda.md b/src/elementary-number-theory/finitely-cyclic-maps.lagda.md index ca1087b887..d5cbb43992 100644 --- a/src/elementary-number-theory/finitely-cyclic-maps.lagda.md +++ b/src/elementary-number-theory/finitely-cyclic-maps.lagda.md @@ -118,3 +118,9 @@ pr2 (is-finitely-cyclic-succ-Fin {succ-ℕ k} x y) = ( ( ap (add-Fin (succ-ℕ k) y) (left-inverse-law-add-Fin k x)) ∙ ( right-unit-law-add-Fin k y))))) ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/elementary-number-theory/modular-arithmetic.lagda.md b/src/elementary-number-theory/modular-arithmetic.lagda.md index decefd45fc..94b2defa16 100644 --- a/src/elementary-number-theory/modular-arithmetic.lagda.md +++ b/src/elementary-number-theory/modular-arithmetic.lagda.md @@ -62,6 +62,10 @@ Some modular arithmetic was already defined in more convenient format that also includes the integers modulo `0`, i.e., the integers. +The fact that `ℤ-Mod n` is a [ring](ring-theory.rings.md) for every `n : ℕ` is +recorded in +[`elementary-number-theory.standard-cyclic-rings`](elementary-number-theory.standard-cyclic-rings.md). + ```agda ℤ-Mod : ℕ → UU lzero ℤ-Mod zero-ℕ = ℤ diff --git a/src/elementary-number-theory/multiplicative-units-modular-arithmetic.lagda.md b/src/elementary-number-theory/multiplicative-units-modular-arithmetic.lagda.md deleted file mode 100644 index 72b9781fe0..0000000000 --- a/src/elementary-number-theory/multiplicative-units-modular-arithmetic.lagda.md +++ /dev/null @@ -1,13 +0,0 @@ -# Multiplicative units in modular arithmetic - -```agda -module elementary-number-theory.multiplicative-units-modular-arithmetic where -``` - -
Imports - -```agda - -``` - -
diff --git a/src/elementary-number-theory/multiplicative-units-standard-cyclic-rings.lagda.md b/src/elementary-number-theory/multiplicative-units-standard-cyclic-rings.lagda.md new file mode 100644 index 0000000000..6c65138a35 --- /dev/null +++ b/src/elementary-number-theory/multiplicative-units-standard-cyclic-rings.lagda.md @@ -0,0 +1,19 @@ +# Multiplicative units in modular arithmetic + +```agda +module elementary-number-theory.multiplicative-units-standard-cyclic-rings where +``` + +
Imports + +```agda + +``` + +
+ +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/elementary-number-theory/relatively-prime-natural-numbers.lagda.md b/src/elementary-number-theory/relatively-prime-natural-numbers.lagda.md index 1f7808e778..6a6e2ee402 100644 --- a/src/elementary-number-theory/relatively-prime-natural-numbers.lagda.md +++ b/src/elementary-number-theory/relatively-prime-natural-numbers.lagda.md @@ -17,7 +17,7 @@ open import elementary-number-theory.modular-arithmetic open import elementary-number-theory.multiplication-integers open import elementary-number-theory.natural-numbers open import elementary-number-theory.prime-numbers -open import elementary-number-theory.rings-of-modular-arithmetic +open import elementary-number-theory.standard-cyclic-rings open import foundation.decidable-propositions open import foundation.decidable-types diff --git a/src/elementary-number-theory/ring-of-integers.lagda.md b/src/elementary-number-theory/ring-of-integers.lagda.md index a334e5c1cb..d54a1644e3 100644 --- a/src/elementary-number-theory/ring-of-integers.lagda.md +++ b/src/elementary-number-theory/ring-of-integers.lagda.md @@ -159,3 +159,34 @@ is-initial-ℤ-Ring : is-initial-Ring ℤ-Ring pr1 (is-initial-ℤ-Ring S) = initial-hom-Ring S pr2 (is-initial-ℤ-Ring S) f = contraction-initial-hom-Ring S f ``` + +### Integer multiplication in the ring of integers coincides with multiplication of integers + +```agda +integer-multiple-one-ℤ-Ring : + (k : ℤ) → integer-multiple-Ring ℤ-Ring k one-ℤ ＝ k +integer-multiple-one-ℤ-Ring (inl zero-ℕ) = refl +integer-multiple-one-ℤ-Ring (inl (succ-ℕ n)) = + ap pred-ℤ (integer-multiple-one-ℤ-Ring (inl n)) +integer-multiple-one-ℤ-Ring (inr (inl star)) = refl +integer-multiple-one-ℤ-Ring (inr (inr zero-ℕ)) = refl +integer-multiple-one-ℤ-Ring (inr (inr (succ-ℕ n))) = + ap succ-ℤ (integer-multiple-one-ℤ-Ring (inr (inr n))) + +compute-integer-multiple-ℤ-Ring : + (k l : ℤ) → integer-multiple-Ring ℤ-Ring k l ＝ mul-ℤ k l +compute-integer-multiple-ℤ-Ring k l = + equational-reasoning + integer-multiple-Ring ℤ-Ring k l + ＝ integer-multiple-Ring ℤ-Ring k (integer-multiple-Ring ℤ-Ring l one-ℤ) + by + ap + ( integer-multiple-Ring ℤ-Ring k) + ( inv (integer-multiple-one-ℤ-Ring l)) + ＝ integer-multiple-Ring ℤ-Ring (mul-ℤ k l) one-ℤ + by + inv (integer-multiple-mul-Ring ℤ-Ring k l one-ℤ) + ＝ mul-ℤ k l + by + integer-multiple-one-ℤ-Ring _ +``` diff --git a/src/elementary-number-theory/groups-of-modular-arithmetic.lagda.md b/src/elementary-number-theory/standard-cyclic-groups.lagda.md similarity index 60% rename from src/elementary-number-theory/groups-of-modular-arithmetic.lagda.md rename to src/elementary-number-theory/standard-cyclic-groups.lagda.md index cd021def78..dc65ddde36 100644 --- a/src/elementary-number-theory/groups-of-modular-arithmetic.lagda.md +++ b/src/elementary-number-theory/standard-cyclic-groups.lagda.md @@ -1,7 +1,7 @@ -# The groups `ℤ/kℤ` +# The standard cyclic groups ```agda -module elementary-number-theory.groups-of-modular-arithmetic where +module elementary-number-theory.standard-cyclic-groups where ```
Imports @@ -22,17 +22,29 @@ open import group-theory.semigroups ## Idea -The integers modulo k, equipped with the zero-element, addition, and negatives, -form groups. +The **standard cyclic groups** are the [groups](group-theory.groups.md) of +[integers](elementary-number-theory.integers.md) +[modulo `k`](elementary-number-theory.modular-arithmetic.md). The standard +cyclic groups are [abelian groups](group-theory.abelian-groups.md). -## Definition +The fact that the standard cyclic groups are +[cyclic groups](group-theory.cyclic-groups.md) is shown in +[`elementary-number-theory.standard-cyclic-rings`](elementary-number-theory.standard-cyclic-rings.md). + +## Definitions + +### The semigroup `ℤ/k` ```agda ℤ-Mod-Semigroup : (k : ℕ) → Semigroup lzero pr1 (ℤ-Mod-Semigroup k) = ℤ-Mod-Set k pr1 (pr2 (ℤ-Mod-Semigroup k)) = add-ℤ-Mod k pr2 (pr2 (ℤ-Mod-Semigroup k)) = associative-add-ℤ-Mod k +``` +### The group `ℤ/k` + +```agda ℤ-Mod-Group : (k : ℕ) → Group lzero pr1 (ℤ-Mod-Group k) = ℤ-Mod-Semigroup k pr1 (pr1 (pr2 (ℤ-Mod-Group k))) = zero-ℤ-Mod k @@ -41,8 +53,18 @@ pr2 (pr2 (pr1 (pr2 (ℤ-Mod-Group k)))) = right-unit-law-add-ℤ-Mod k pr1 (pr2 (pr2 (ℤ-Mod-Group k))) = neg-ℤ-Mod k pr1 (pr2 (pr2 (pr2 (ℤ-Mod-Group k)))) = left-inverse-law-add-ℤ-Mod k pr2 (pr2 (pr2 (pr2 (ℤ-Mod-Group k)))) = right-inverse-law-add-ℤ-Mod k +``` +### The abelian group `ℤ/k` + +```agda ℤ-Mod-Ab : (k : ℕ) → Ab lzero pr1 (ℤ-Mod-Ab k) = ℤ-Mod-Group k pr2 (ℤ-Mod-Ab k) = commutative-add-ℤ-Mod k ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/elementary-number-theory/rings-of-modular-arithmetic.lagda.md b/src/elementary-number-theory/standard-cyclic-rings.lagda.md similarity index 69% rename from src/elementary-number-theory/rings-of-modular-arithmetic.lagda.md rename to src/elementary-number-theory/standard-cyclic-rings.lagda.md index 57d913dea9..7114e64292 100644 --- a/src/elementary-number-theory/rings-of-modular-arithmetic.lagda.md +++ b/src/elementary-number-theory/standard-cyclic-rings.lagda.md @@ -1,7 +1,7 @@ -# Rings of modular arithmetic +# The standard cyclic rings ```agda -module elementary-number-theory.rings-of-modular-arithmetic where +module elementary-number-theory.standard-cyclic-rings where ```
Imports @@ -10,12 +10,12 @@ module elementary-number-theory.rings-of-modular-arithmetic where open import commutative-algebra.commutative-rings open import elementary-number-theory.addition-integers -open import elementary-number-theory.groups-of-modular-arithmetic open import elementary-number-theory.integers open import elementary-number-theory.modular-arithmetic open import elementary-number-theory.modular-arithmetic-standard-finite-types open import elementary-number-theory.natural-numbers open import elementary-number-theory.ring-of-integers +open import elementary-number-theory.standard-cyclic-groups open import foundation.action-on-identifications-functions open import foundation.coproduct-types @@ -29,6 +29,7 @@ open import foundation.universe-levels open import foundation-core.function-types +open import group-theory.cyclic-groups open import group-theory.generating-elements-groups open import ring-theory.cyclic-rings @@ -43,13 +44,13 @@ open import univalent-combinatorics.standard-finite-types ## Idea The **standard cyclic rings** `ℤ/n` are the [rings](ring-theory.rings.md) of -[modular arithmetic](elementary-number-theory.modular-arithmetic.md). - -The fact that the rings `ℤ/n` are [cyclic](ring-theory.cyclic-rings.md) remains -to be shown. +[integers](elementary-number-theory.integers.md) +[modulo `n`](elementary-number-theory.modular-arithmetic.md). ## Definitions +### The standard cyclic rings + ```agda ℤ-Mod-Ring : ℕ → Ring lzero pr1 (ℤ-Mod-Ring n) = ℤ-Mod-Ab n @@ -66,32 +67,32 @@ pr1 (ℤ-Mod-Commutative-Ring n) = ℤ-Mod-Ring n pr2 (ℤ-Mod-Commutative-Ring n) = commutative-mul-ℤ-Mod n ``` +### Integer multiplication in the standard cyclic rings + +```agda +integer-multiple-ℤ-Mod : + (n : ℕ) → ℤ → ℤ-Mod n → ℤ-Mod n +integer-multiple-ℤ-Mod n k x = integer-multiple-Ring (ℤ-Mod-Ring n) k x +``` + ## Properties -### Rings of modular arithmetic are cyclic +### The negative-one element of the ring `ℤ/n` coincides with the element `neg-one-ℤ-Mod n` ```agda -integer-multiple-one-ℤ-Ring : - (k : ℤ) → - ( integer-multiple-Ring (ℤ-Mod-Ring zero-ℕ) k (one-ℤ-Mod zero-ℕ)) ＝ - ( k) -integer-multiple-one-ℤ-Ring (inl zero-ℕ) = refl -integer-multiple-one-ℤ-Ring (inl (succ-ℕ n)) = - ap pred-ℤ (integer-multiple-one-ℤ-Ring (inl n)) -integer-multiple-one-ℤ-Ring (inr (inl star)) = refl -integer-multiple-one-ℤ-Ring (inr (inr zero-ℕ)) = refl -integer-multiple-one-ℤ-Ring (inr (inr (succ-ℕ n))) = - ap succ-ℤ (integer-multiple-one-ℤ-Ring (inr (inr n))) - is-neg-one-neg-one-ℤ-Mod : - ( n : ℕ) → (neg-one-Ring (ℤ-Mod-Ring n)) ＝ (neg-one-ℤ-Mod n) + ( n : ℕ) → neg-one-Ring (ℤ-Mod-Ring n) ＝ neg-one-ℤ-Mod n is-neg-one-neg-one-ℤ-Mod zero-ℕ = refl is-neg-one-neg-one-ℤ-Mod (succ-ℕ n) = is-neg-one-neg-one-Fin n +``` + +### The integer multiple `k · 1` is equal to `[k] : ℤ-Mod n` +```agda integer-multiplication-by-one-preserves-succ-ℤ : (n : ℕ) (x : ℤ) → - integer-multiple-Ring (ℤ-Mod-Ring n) (succ-ℤ x) (one-ℤ-Mod n) ＝ - succ-ℤ-Mod n (integer-multiple-Ring (ℤ-Mod-Ring n) x (one-ℤ-Mod n)) + integer-multiple-ℤ-Mod n (succ-ℤ x) (one-ℤ-Mod n) ＝ + succ-ℤ-Mod n (integer-multiple-ℤ-Mod n x (one-ℤ-Mod n)) integer-multiplication-by-one-preserves-succ-ℤ n x = ( integer-multiple-succ-Ring (ℤ-Mod-Ring n) x (one-ℤ-Mod n)) ∙ ( inv @@ -101,11 +102,11 @@ integer-multiplication-by-one-preserves-succ-ℤ n x = integer-multiplication-by-one-preserves-pred-ℤ : (n : ℕ) (x : ℤ) → - integer-multiple-Ring (ℤ-Mod-Ring n) (pred-ℤ x) (one-ℤ-Mod n) ＝ - pred-ℤ-Mod n (integer-multiple-Ring (ℤ-Mod-Ring n) x (one-ℤ-Mod n)) + integer-multiple-ℤ-Mod n (pred-ℤ x) (one-ℤ-Mod n) ＝ + pred-ℤ-Mod n (integer-multiple-ℤ-Mod n x (one-ℤ-Mod n)) integer-multiplication-by-one-preserves-pred-ℤ n x = ( ap - ( λ k → integer-multiple-Ring (ℤ-Mod-Ring n) k (one-ℤ-Mod n)) + ( λ k → integer-multiple-ℤ-Mod n k (one-ℤ-Mod n)) ( is-right-add-neg-one-pred-ℤ x)) ∙ ( distributive-integer-multiple-add-Ring ( ℤ-Mod-Ring n) @@ -115,24 +116,22 @@ integer-multiplication-by-one-preserves-pred-ℤ n x = ( ap ( λ k → add-ℤ-Mod n - ( integer-multiple-Ring (ℤ-Mod-Ring n) x (one-ℤ-Mod n)) + ( integer-multiple-ℤ-Mod n x (one-ℤ-Mod n)) ( k)) ( integer-multiple-neg-one-Ring (ℤ-Mod-Ring n) (one-ℤ-Mod n))) ∙ ( ap ( λ k → add-ℤ-Mod n - ( integer-multiple-Ring (ℤ-Mod-Ring n) x (one-ℤ-Mod n)) + ( integer-multiple-ℤ-Mod n x (one-ℤ-Mod n)) ( k)) ( is-neg-one-neg-one-ℤ-Mod n)) ∙ ( inv ( is-left-add-neg-one-pred-ℤ-Mod' ( n) - ( integer-multiple-Ring (ℤ-Mod-Ring n) x (one-ℤ-Mod n)))) + ( integer-multiple-ℤ-Mod n x (one-ℤ-Mod n)))) compute-integer-multiple-one-ℤ-Mod : - ( n : ℕ) → - ( λ k → integer-multiple-Ring (ℤ-Mod-Ring n) k (one-ℤ-Mod n)) ~ - ( mod-ℤ n) + ( n : ℕ) → (λ k → integer-multiple-ℤ-Mod n k (one-ℤ-Mod n)) ~ mod-ℤ n compute-integer-multiple-one-ℤ-Mod zero-ℕ x = integer-multiple-one-ℤ-Ring x compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inl zero-ℕ) = ( integer-multiple-neg-one-Ring @@ -147,7 +146,7 @@ compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inl (succ-ℕ x)) = ( ap ( pred-ℤ-Mod (succ-ℕ n)) ( compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inl x))) ∙ - (inv (preserves-predecessor-mod-ℤ (succ-ℕ n) (inl x))) + ( inv (preserves-predecessor-mod-ℤ (succ-ℕ n) (inl x))) compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inr (inl star)) = refl compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inr (inr zero-ℕ)) = ( integer-multiple-one-Ring @@ -161,27 +160,42 @@ compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inr (inr (succ-ℕ x))) = ( ap ( succ-ℤ-Mod (succ-ℕ n)) ( compute-integer-multiple-one-ℤ-Mod (succ-ℕ n) (inr (inr x)))) ∙ - (inv (preserves-successor-mod-ℤ (succ-ℕ n) (inr (inr x)))) + ( inv (preserves-successor-mod-ℤ (succ-ℕ n) (inr (inr x)))) +``` -is-surjective-hom-element-one-ℤ-Mod-Ring : +### The standard cyclic rings are cyclic + +```agda +is-surjective-hom-element-one-ℤ-Mod : ( n : ℕ) → is-surjective-hom-element-Group (ℤ-Mod-Group n) (one-ℤ-Mod n) -is-surjective-hom-element-one-ℤ-Mod-Ring n = +is-surjective-hom-element-one-ℤ-Mod n = is-surjective-htpy ( compute-integer-multiple-one-ℤ-Mod n) ( is-surjective-mod-ℤ n) -is-generating-element-one-ℤ-Mod-Ring : +is-generating-element-one-ℤ-Mod : ( n : ℕ) → is-generating-element-Group (ℤ-Mod-Group n) (one-ℤ-Mod n) -is-generating-element-one-ℤ-Mod-Ring n = +is-generating-element-one-ℤ-Mod n = is-generating-element-is-surjective-hom-element-Group ( ℤ-Mod-Group n) ( one-ℤ-Mod n) - ( is-surjective-hom-element-one-ℤ-Mod-Ring n) + ( is-surjective-hom-element-one-ℤ-Mod n) -is-cyclic-ℤ-Mod-Ring : - ( n : ℕ) → is-cyclic-Ring (ℤ-Mod-Ring n) -is-cyclic-ℤ-Mod-Ring n = +is-cyclic-ℤ-Mod-Group : + ( n : ℕ) → is-cyclic-Group (ℤ-Mod-Group n) +is-cyclic-ℤ-Mod-Group n = intro-∃ ( one-ℤ-Mod n) - ( is-generating-element-one-ℤ-Mod-Ring n) + ( is-generating-element-one-ℤ-Mod n) + +is-cyclic-ℤ-Mod-Ring : + ( n : ℕ) → is-cyclic-Ring (ℤ-Mod-Ring n) +is-cyclic-ℤ-Mod-Ring = + is-cyclic-ℤ-Mod-Group ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/finite-group-theory/groups-of-order-2.lagda.md b/src/finite-group-theory/groups-of-order-2.lagda.md index 6e561b3744..6d766f606e 100644 --- a/src/finite-group-theory/groups-of-order-2.lagda.md +++ b/src/finite-group-theory/groups-of-order-2.lagda.md @@ -9,7 +9,7 @@ module finite-group-theory.groups-of-order-2 where
Imports ```agda -open import elementary-number-theory.groups-of-modular-arithmetic +open import elementary-number-theory.standard-cyclic-groups open import finite-group-theory.finite-groups diff --git a/src/finite-group-theory/tetrahedra-in-3-space.lagda.md b/src/finite-group-theory/tetrahedra-in-3-space.lagda.md index 13679635fa..67a80de24a 100644 --- a/src/finite-group-theory/tetrahedra-in-3-space.lagda.md +++ b/src/finite-group-theory/tetrahedra-in-3-space.lagda.md @@ -12,7 +12,7 @@ open import foundation.empty-types open import foundation.universe-levels open import univalent-combinatorics.2-element-decidable-subtypes -open import univalent-combinatorics.cyclic-types +open import univalent-combinatorics.cyclic-finite-types open import univalent-combinatorics.finite-types ``` diff --git a/src/graph-theory/acyclic-undirected-graphs.lagda.md b/src/graph-theory/acyclic-undirected-graphs.lagda.md index 53f4567da9..caca26aa95 100644 --- a/src/graph-theory/acyclic-undirected-graphs.lagda.md +++ b/src/graph-theory/acyclic-undirected-graphs.lagda.md @@ -51,3 +51,9 @@ is-acyclic-Undirected-Graph l G = is-geometric-realization-reflecting-map-Undirected-Graph l G ( terminal-reflecting-map-Undirected-Graph G) ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/graph-theory/polygons.lagda.md b/src/graph-theory/polygons.lagda.md index fe9665a9ce..9cd2058e1d 100644 --- a/src/graph-theory/polygons.lagda.md +++ b/src/graph-theory/polygons.lagda.md @@ -170,3 +170,9 @@ pr1 (is-simple-standard-polygon-Undirected-Graph k H) p (pair x (pair y α)) = pr2 (is-simple-standard-polygon-Undirected-Graph k H) p = {!!} -} ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/group-theory/cyclic-groups.lagda.md b/src/group-theory/cyclic-groups.lagda.md index 18d82a0b7a..b51af13775 100644 --- a/src/group-theory/cyclic-groups.lagda.md +++ b/src/group-theory/cyclic-groups.lagda.md @@ -153,3 +153,7 @@ module _ endomorphism rings. Furthermore, the multiplicative structure of these rings is commutative, so that groups equipped with a generating element are also equipped with the structure of a commutative ring. + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/group-theory/dihedral-groups.lagda.md b/src/group-theory/dihedral-groups.lagda.md index 2015e7d0db..526451b1ce 100644 --- a/src/group-theory/dihedral-groups.lagda.md +++ b/src/group-theory/dihedral-groups.lagda.md @@ -7,8 +7,8 @@ module group-theory.dihedral-groups where
Imports ```agda -open import elementary-number-theory.groups-of-modular-arithmetic open import elementary-number-theory.natural-numbers +open import elementary-number-theory.standard-cyclic-groups open import foundation.universe-levels diff --git a/src/group-theory/generating-elements-groups.lagda.md b/src/group-theory/generating-elements-groups.lagda.md index 2692b16491..a2ed29ade4 100644 --- a/src/group-theory/generating-elements-groups.lagda.md +++ b/src/group-theory/generating-elements-groups.lagda.md @@ -673,3 +673,9 @@ module _ pr2 commutative-ring-Group-With-Generating-Element = commutative-mul-Group-With-Generating-Element ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/higher-group-theory/cyclic-higher-groups.lagda.md b/src/higher-group-theory/cyclic-higher-groups.lagda.md index a0228231ba..d0c2493c1c 100644 --- a/src/higher-group-theory/cyclic-higher-groups.lagda.md +++ b/src/higher-group-theory/cyclic-higher-groups.lagda.md @@ -71,6 +71,12 @@ module _ is-prop-is-cyclic-∞-Group = is-prop-type-Prop is-cyclic-prop-∞-Group ``` +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} + ## References 1. Haynes Miller. _The Sullivan Conjecture on Maps from Classifying Spaces_. diff --git a/src/ring-theory/category-of-cyclic-rings.lagda.md b/src/ring-theory/category-of-cyclic-rings.lagda.md index 8f0f1a3155..b85650094e 100644 --- a/src/ring-theory/category-of-cyclic-rings.lagda.md +++ b/src/ring-theory/category-of-cyclic-rings.lagda.md @@ -109,3 +109,9 @@ is-large-poset-Cyclic-Ring-Large-Category : is-large-poset-Cyclic-Ring-Large-Category = is-prop-hom-Cyclic-Ring ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/ring-theory/cyclic-rings.lagda.md b/src/ring-theory/cyclic-rings.lagda.md index c91b2430af..00456a2c8a 100644 --- a/src/ring-theory/cyclic-rings.lagda.md +++ b/src/ring-theory/cyclic-rings.lagda.md @@ -490,6 +490,12 @@ module _ pr2 commutative-ring-Cyclic-Ring = commutative-mul-Cyclic-Ring ``` +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} + ## References - \[1\] Maria Balintne-Szendrei, Gabor Czedli, and Agnes Szendrei. _Absztrakt diff --git a/src/ring-theory/homomorphisms-cyclic-rings.lagda.md b/src/ring-theory/homomorphisms-cyclic-rings.lagda.md index 9896912b0a..a8dd816577 100644 --- a/src/ring-theory/homomorphisms-cyclic-rings.lagda.md +++ b/src/ring-theory/homomorphisms-cyclic-rings.lagda.md @@ -205,3 +205,9 @@ module _ ( ring-Cyclic-Ring T) ( ring-Cyclic-Ring U) ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/ring-theory/poset-of-cyclic-rings.lagda.md b/src/ring-theory/poset-of-cyclic-rings.lagda.md index d776d605b5..0ec90ccaeb 100644 --- a/src/ring-theory/poset-of-cyclic-rings.lagda.md +++ b/src/ring-theory/poset-of-cyclic-rings.lagda.md @@ -37,3 +37,9 @@ Cyclic-Ring-Large-Poset = ( Cyclic-Ring-Large-Category) ( is-large-poset-Cyclic-Ring-Large-Category) ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/species/cycle-index-series-species-of-types.lagda.md b/src/species/cycle-index-series-species-of-types.lagda.md index 7eff2d1988..c09e10d146 100644 --- a/src/species/cycle-index-series-species-of-types.lagda.md +++ b/src/species/cycle-index-series-species-of-types.lagda.md @@ -12,7 +12,7 @@ open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types open import foundation.universe-levels -open import univalent-combinatorics.cyclic-types +open import univalent-combinatorics.cyclic-finite-types ```
diff --git a/src/structured-types/cyclic-types.lagda.md b/src/structured-types/cyclic-types.lagda.md index 7e731ac2dd..e37ac82b8c 100644 --- a/src/structured-types/cyclic-types.lagda.md +++ b/src/structured-types/cyclic-types.lagda.md @@ -110,3 +110,9 @@ module _ map-Cyclic-Set : type-Cyclic-Set → type-Cyclic-Set map-Cyclic-Set = map-Set-With-Automorphism set-with-automorphism-Cyclic-Set ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md index 263da4159c..dbaef401e0 100644 --- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md @@ -36,3 +36,9 @@ module _ is-prop-is-acyclic-map : (f : A → B) → is-prop (is-acyclic-map f) is-prop-is-acyclic-map f = is-prop-type-Prop (is-acyclic-map-Prop f) ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/synthetic-homotopy-theory/acyclic-types.lagda.md b/src/synthetic-homotopy-theory/acyclic-types.lagda.md index 9dc557c5b3..d138ed4669 100644 --- a/src/synthetic-homotopy-theory/acyclic-types.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-types.lagda.md @@ -32,3 +32,9 @@ is-acyclic A = type-Prop (is-acyclic-Prop A) is-prop-is-acyclic : {l : Level} (A : UU l) → is-prop (is-acyclic A) is-prop-is-acyclic A = is-prop-type-Prop (is-acyclic-Prop A) ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/synthetic-homotopy-theory/circle.lagda.md b/src/synthetic-homotopy-theory/circle.lagda.md index 8c5d707856..2f6a8a2dc8 100644 --- a/src/synthetic-homotopy-theory/circle.lagda.md +++ b/src/synthetic-homotopy-theory/circle.lagda.md @@ -573,3 +573,9 @@ equiv-sphere-1-circle : 𝕊¹ ≃ sphere 1 pr1 equiv-sphere-1-circle = sphere-1-circle pr2 equiv-sphere-1-circle = is-equiv-sphere-1-circle ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/synthetic-homotopy-theory/connected-set-bundles-circle.lagda.md b/src/synthetic-homotopy-theory/connected-set-bundles-circle.lagda.md index c08e5f073b..995d4b249a 100644 --- a/src/synthetic-homotopy-theory/connected-set-bundles-circle.lagda.md +++ b/src/synthetic-homotopy-theory/connected-set-bundles-circle.lagda.md @@ -162,3 +162,9 @@ module _ #### The set equipped with an automorphism obtained from a connected set bundle over the circle is a cyclic set This remains to be shown. + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md index d320dba8d0..5305f96985 100644 --- a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md +++ b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md @@ -245,3 +245,9 @@ module _ ( interchange-concat-Ω² a b a b))))))))) ( is-contr-total-path refl) ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md b/src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md index afe1393edf..e4a0b42f52 100644 --- a/src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md +++ b/src/synthetic-homotopy-theory/infinite-cyclic-types.lagda.md @@ -38,7 +38,7 @@ open import structured-types.types-equipped-with-endomorphisms open import synthetic-homotopy-theory.loop-spaces -open import univalent-combinatorics.cyclic-types +open import univalent-combinatorics.cyclic-finite-types ```
@@ -210,3 +210,9 @@ module _ -- pr2 (pr1 (Infinite-Cyclic-Type-𝕊¹ x)) = {!!} -- pr2 (Infinite-Cyclic-Type-𝕊¹ x) = {!!} ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/univalent-combinatorics.lagda.md b/src/univalent-combinatorics.lagda.md index 008ad5b3b2..0cbecf9212 100644 --- a/src/univalent-combinatorics.lagda.md +++ b/src/univalent-combinatorics.lagda.md @@ -37,7 +37,7 @@ open import univalent-combinatorics.counting-maybe public open import univalent-combinatorics.cubes public open import univalent-combinatorics.cycle-partitions public open import univalent-combinatorics.cycle-prime-decomposition-natural-numbers public -open import univalent-combinatorics.cyclic-types public +open import univalent-combinatorics.cyclic-finite-types public open import univalent-combinatorics.decidable-dependent-function-types public open import univalent-combinatorics.decidable-dependent-pair-types public open import univalent-combinatorics.decidable-equivalence-relations public diff --git a/src/univalent-combinatorics/bracelets.lagda.md b/src/univalent-combinatorics/bracelets.lagda.md index 90bebceefc..f2e65151d7 100644 --- a/src/univalent-combinatorics/bracelets.lagda.md +++ b/src/univalent-combinatorics/bracelets.lagda.md @@ -27,3 +27,9 @@ open import univalent-combinatorics.standard-finite-types bracelet : ℕ → ℕ → UU (lsuc lzero) bracelet m n = Σ (Polygon m) (λ X → vertex-Polygon m X → Fin n) ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/univalent-combinatorics/cycle-partitions.lagda.md b/src/univalent-combinatorics/cycle-partitions.lagda.md index 377d3ee776..177fd2d745 100644 --- a/src/univalent-combinatorics/cycle-partitions.lagda.md +++ b/src/univalent-combinatorics/cycle-partitions.lagda.md @@ -13,7 +13,7 @@ open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.universe-levels -open import univalent-combinatorics.cyclic-types +open import univalent-combinatorics.cyclic-finite-types open import univalent-combinatorics.finite-types ``` diff --git a/src/univalent-combinatorics/cycle-prime-decomposition-natural-numbers.lagda.md b/src/univalent-combinatorics/cycle-prime-decomposition-natural-numbers.lagda.md index a93706de19..f1c5ab49c3 100644 --- a/src/univalent-combinatorics/cycle-prime-decomposition-natural-numbers.lagda.md +++ b/src/univalent-combinatorics/cycle-prime-decomposition-natural-numbers.lagda.md @@ -35,7 +35,7 @@ open import lists.functoriality-lists open import lists.permutation-lists open import lists.sort-by-insertion-lists -open import univalent-combinatorics.cyclic-types +open import univalent-combinatorics.cyclic-finite-types ```
diff --git a/src/univalent-combinatorics/cyclic-types.lagda.md b/src/univalent-combinatorics/cyclic-finite-types.lagda.md similarity index 98% rename from src/univalent-combinatorics/cyclic-types.lagda.md rename to src/univalent-combinatorics/cyclic-finite-types.lagda.md index a543df9eea..75437b8a59 100644 --- a/src/univalent-combinatorics/cyclic-types.lagda.md +++ b/src/univalent-combinatorics/cyclic-finite-types.lagda.md @@ -1,18 +1,18 @@ -# Cyclic types +# Cyclic finite types ```agda -module univalent-combinatorics.cyclic-types where +module univalent-combinatorics.cyclic-finite-types where ```
Imports ```agda open import elementary-number-theory.addition-integers -open import elementary-number-theory.groups-of-modular-arithmetic open import elementary-number-theory.integers open import elementary-number-theory.modular-arithmetic open import elementary-number-theory.modular-arithmetic-standard-finite-types open import elementary-number-theory.natural-numbers +open import elementary-number-theory.standard-cyclic-groups open import foundation.0-connected-types open import foundation.action-on-identifications-functions @@ -615,3 +615,9 @@ iso-Ω-Cyclic-Type-Group k = ( ℤ-Mod-Group k) ( equiv-Ω-Cyclic-Type-Group k) ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/src/univalent-combinatorics/necklaces.lagda.md b/src/univalent-combinatorics/necklaces.lagda.md index 0ad9f87fbb..a92a72fabe 100644 --- a/src/univalent-combinatorics/necklaces.lagda.md +++ b/src/univalent-combinatorics/necklaces.lagda.md @@ -18,9 +18,10 @@ open import foundation.identity-types open import foundation.structure-identity-principle open import foundation.universe-levels +open import structured-types.cyclic-types open import structured-types.types-equipped-with-endomorphisms -open import univalent-combinatorics.cyclic-types +open import univalent-combinatorics.cyclic-finite-types open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types ``` @@ -29,8 +30,10 @@ open import univalent-combinatorics.standard-finite-types ## Idea -A necklace is an arrangement of coloured beads. Two necklaces are considered the -same if one can be obtained from the other by rotating. +A **necklace** is an arrangement of coloured beads, i.e., it consists of a +[cyclic finite type](univalent-combinatorics.cyclic-finite-types.md) equipped +with a coloring of the elements. Two necklaces are considered the same if one +can be obtained from the other by rotating. ## Definition @@ -123,3 +126,9 @@ module _ Id (map-equiv (extensionality-necklace N N) refl) (id-equiv-necklace m n N) refl-extensionality-necklace N = refl ``` + +## See also + +### Table of files related to cyclic types, groups, and rings + +{{#include tables/cyclic-types.md}} diff --git a/tables/cyclic-types.md b/tables/cyclic-types.md new file mode 100644 index 0000000000..dda8b45bec --- /dev/null +++ b/tables/cyclic-types.md @@ -0,0 +1,26 @@ +| Concept | File | +| ------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------- | +| Acyclic maps | [`synthetic-homotopy-theory.acyclic-maps`](synthetic-homotopy-theory.acyclic-maps.md) | +| Acyclic types | [`synthetic-homotopy-theory.acyclic-types`](synthetic-homotopy-theory.acyclic-types.md) | +| Acyclic undirected graphs | [`graph-theory.acyclic-undirected-graphs`](graph-theory.acyclic-undirected-graphs.md) | +| Bracelets | [`univalent-combinatorics.bracelets`](univalent-combinatorics.bracelets.md) | +| The category of cyclic rings | [`ring-theory.category-of-cyclic-rings`](ring-theory.category-of-cyclic-rings.md) | +| The circle | [`synthetic-homotopy-theory.circle`](synthetic-homotopy-theory.circle.md) | +| Connected set bundles over the circle | [`synthetic-homotopy-theory.connected-set-bundles-circle`](synthetic-homotopy-theory.connected-set-bundles-circle.md) | +| Cyclic finite types | [`univalent-combinatorics.cyclic-finite-types`](univalent-combinatorics.cyclic-finite-types.md) | +| Cyclic groups | [`group-theory.cyclic-groups`](group-theory.cyclic-groups.md) | +| Cyclic higher groups | [`higher-group-theory.cyclic-higher-groups`](higher-group-theory.cyclic-higher-groups.md) | +| Cyclic rings | [`ring-theory.cyclic-rings`](ring-theory.cyclic-rings.md) | +| Cyclic types | [`structured-types.cyclic-types`](structured-types.cyclic-types.md) | +| Euler's totient function | [`elementary-number-theory.eulers-totient-function`](elementary-number-theory.eulers-totient-function.md) | +| Finitely cyclic maps | [`elementary-number-theory.finitely-cyclic-maps`](elementary-number-theory.finitely-cyclic-maps.md) | +| Generating elements of groups | [`group-theory.generating-elements-groups`](group-theory.generating-elements-groups.md) | +| Hatcher's acyclic type | [`synthetic-homotopy-theory.hatchers-acyclic-type`](synthetic-homotopy-theory.hatchers-acyclic-type.md) | +| Homomorphisms of cyclic rings | [`ring-theory.homomorphisms-cyclic-rings`](ring-theory.homomorphisms-cyclic-rings.md) | +| Infinite cyclic types | [`synthetic-homotopy-theory.infinite-cyclic-types`](synthetic-homotopy-theory.infinite-cyclic-types.md) | +| Multiplicative units in the standard cyclic rings | [`elementary-number-theory.multiplicative-units-standard-cyclic-rings`](elementary-number-theory.multiplicative-units-standard-cyclic-rings.md) | +| Necklaces | [`univalent-combinatorics.necklaces`](univalent-combinatorics.necklaces.md) | +| Polygons | [`graph-theory.polygons`](graph-theory.polygons.md) | +| The poset of cyclic rings | [`ring-theory.poset-of-cyclic-rings`](ring-theory.poset-of-cyclic-rings.md) | +| Standard cyclic groups (ℤ/k) | [`elementary-number-theory.standard-cyclic-groups`](elementary-number-theory.standard-cyclic-groups.md) | +| Standard cyclic rings (ℤ/k) | [`elementary-number-theory.standard-cyclic-rings`](elementary-number-theory.standard-cyclic-rings.md) |