From 85481cca853e5ebd5c402b71cc2dd37ea8c58d69 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Na=C3=AFm=20Favier?= Date: Sat, 24 Aug 2024 16:58:43 +0200 Subject: [PATCH 1/9] chore: misc --- src/Algebra/Monoid/Category.lagda.md | 2 +- src/Cat/Diagram/Initial.lagda.md | 16 ++++++++-------- src/Cat/Diagram/Terminal.lagda.md | 2 +- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/Algebra/Monoid/Category.lagda.md b/src/Algebra/Monoid/Category.lagda.md index a4d7a58cf..20958c37d 100644 --- a/src/Algebra/Monoid/Category.lagda.md +++ b/src/Algebra/Monoid/Category.lagda.md @@ -107,7 +107,7 @@ Mon↪Sets : ∀ {ℓ} → Functor (Monoids ℓ) (Sets ℓ) Mon↪Sets = Forget-structure (Monoid-structure _) ``` -## Free objects {defines=free-monoid} +## Free monoids {defines=free-monoid} We piece together some properties of `lists`{.Agda ident=List} to show that, if $A$ is a set, then $\rm{List}(A)$ is an object of diff --git a/src/Cat/Diagram/Initial.lagda.md b/src/Cat/Diagram/Initial.lagda.md index 7916c4ce9..12256894d 100644 --- a/src/Cat/Diagram/Initial.lagda.md +++ b/src/Cat/Diagram/Initial.lagda.md @@ -17,7 +17,7 @@ module _ {o h} (C : Precategory o h) where ``` --> -# Initial objects {defines="initial-object"} +# Initial objects {defines="initial-object initial"} An object $\bot$ of a category $\mathcal{C}$ is said to be **initial** if there exists a _unique_ map to any other object: @@ -25,7 +25,7 @@ if there exists a _unique_ map to any other object: ```agda is-initial : Ob → Type _ is-initial ob = ∀ x → is-contr (Hom ob x) - + record Initial : Type (o ⊔ h) where field bot : Ob @@ -38,13 +38,13 @@ contractible type, it is unique. ```agda ¡ : ∀ {x} → Hom bot x ¡ = has⊥ _ .centre - + ¡-unique : ∀ {x} (h : Hom bot x) → ¡ ≡ h ¡-unique = has⊥ _ .paths - + ¡-unique₂ : ∀ {x} (f g : Hom bot x) → f ≡ g ¡-unique₂ = is-contr→is-prop (has⊥ _) - + open Initial ``` @@ -85,7 +85,7 @@ a proposition: ⊥-is-prop : is-category C → is-prop Initial ⊥-is-prop ccat x1 x2 i .bot = Univalent.iso→path ccat (⊥-unique x1 x2) i - + ⊥-is-prop ccat x1 x2 i .has⊥ ob = is-prop→pathp (λ i → is-contr-is-prop @@ -107,7 +107,7 @@ This is an instance of the more general notion of [van Kampen colimits]. ```agda is-strict-initial : Initial → Type _ is-strict-initial i = ∀ x → (f : Hom x (i .bot)) → is-invertible f - + record Strict-initial : Type (o ⊔ h) where field initial : Initial @@ -125,7 +125,7 @@ Strictness is a property of, not structure on, an initial object. ```agda module _ {o h} {C : Precategory o h} where open Cat.Morphism C - private unquoteDecl eqv = declare-record-iso eqv (quote Initial) + private unquoteDecl eqv = declare-record-iso eqv (quote Initial) instance Extensional-Initial diff --git a/src/Cat/Diagram/Terminal.lagda.md b/src/Cat/Diagram/Terminal.lagda.md index c3438ac2d..ba9a405ab 100644 --- a/src/Cat/Diagram/Terminal.lagda.md +++ b/src/Cat/Diagram/Terminal.lagda.md @@ -20,7 +20,7 @@ module _ {o h} (C : Precategory o h) where ``` --> -# Terminal objects {defines=terminal-object} +# Terminal objects {defines="terminal-object terminal"} An object $\top$ of a category $\mathcal{C}$ is said to be **terminal** if it admits a _unique_ map from any other object: From e451e01937f4e1b93db717f5a6cc29a3119b9ed8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Na=C3=AFm=20Favier?= Date: Fri, 2 Aug 2024 16:24:35 +0200 Subject: [PATCH 2/9] def: (amalgamated) free products of groups --- src/Algebra/Group.lagda.md | 2 +- .../Group/Cat/FinitelyComplete.lagda.md | 2 +- src/Algebra/Group/Free/Product.lagda.md | 188 ++++++++++++++++++ 3 files changed, 190 insertions(+), 2 deletions(-) create mode 100644 src/Algebra/Group/Free/Product.lagda.md diff --git a/src/Algebra/Group.lagda.md b/src/Algebra/Group.lagda.md index 7b99944d9..3cec489d5 100644 --- a/src/Algebra/Group.lagda.md +++ b/src/Algebra/Group.lagda.md @@ -151,7 +151,7 @@ instance H-Level-is-group = prop-instance is-group-is-prop ``` -# Group homomorphisms +# Group homomorphisms {defines="group-homomorphism"} In contrast with monoid homomorphisms, for group homomorphisms, it is not necessary for the underlying map to explicitly preserve the unit diff --git a/src/Algebra/Group/Cat/FinitelyComplete.lagda.md b/src/Algebra/Group/Cat/FinitelyComplete.lagda.md index a107d50d4..3a89e8ed9 100644 --- a/src/Algebra/Group/Cat/FinitelyComplete.lagda.md +++ b/src/Algebra/Group/Cat/FinitelyComplete.lagda.md @@ -86,7 +86,7 @@ Zero-group-is-zero = record ∅ᴳ .Zero.has-is-zero = Zero-group-is-zero ``` -## Direct products +## Direct products {defines="direct-product-of-groups"} We compute the product of two groups $G \times H$ as the product of their underlying sets, equipped with the operation of "pointwise diff --git a/src/Algebra/Group/Free/Product.lagda.md b/src/Algebra/Group/Free/Product.lagda.md new file mode 100644 index 000000000..f31e942f3 --- /dev/null +++ b/src/Algebra/Group/Free/Product.lagda.md @@ -0,0 +1,188 @@ + + +```agda +module Algebra.Group.Free.Product {ℓ} where +``` + +# Free products of groups {defines="free-product amalgamated-free-product"} + +Given two [[groups]] $A$ and $B$, their **free product** is the [[coproduct]] +$A + B$ in the [[category of groups]] (not to be confused with the +[[*direct* product|direct product of groups]] $A \times B$, which is the +categorical [[product]]). + +As the name suggests, we can describe the free product $A + B$ as the +free group equipped with inclusions $A \hookrightarrow A + B$ and +$B \hookrightarrow A + B$. In fact, we define a more general construction: +the **amalgamated free product** of a span of groups +$A \overset{f}{\ot} C \overset{g}{\to} B$, which realises the +[[pushout]] of this span. + + + +We start by freely adding the group operations and enforcing the group +axioms, just like for [[free groups|free group construction]]... + +```agda + data Amalgamated : Type ℓ where + _◆_ : Amalgamated → Amalgamated → Amalgamated + inv : Amalgamated → Amalgamated + nil : Amalgamated + + f-assoc : ∀ x y z → x ◆ (y ◆ z) ≡ (x ◆ y) ◆ z + f-invl : ∀ x → inv x ◆ x ≡ nil + f-idl : ∀ x → nil ◆ x ≡ x +``` + +...we then throw in the inclusions of $A$ and $B$, which are required to +be [[group homomorphisms]] and to make the pushout square commute... + +```agda + inl : ⌞ A ⌟ → Amalgamated + inl-hom : ∀ a a' → inl (a A.⋆ a') ≡ inl a ◆ inl a' + + inr : ⌞ B ⌟ → Amalgamated + inr-hom : ∀ b b' → inr (b B.⋆ b') ≡ inr b ◆ inr b' + + glue : (c : ⌞ C ⌟) → inl (f # c) ≡ inr (g # c) +``` + +...finally, we truncate the resulting type to a set. + +```agda + squash : is-set Amalgamated +``` + + + +
+ +As expected, this data perfectly assembles into a group $A +_C B$ +together with homomorphisms $A \to A +_C B$ and $B \to A +_C B$ +fitting into a square with $f$ and $g$. + +~~~{.quiver} +\[\begin{tikzcd} + & C \\ + A && B \\ + & {A +_C B} + \arrow["f"', from=1-2, to=2-1] + \arrow["g", from=1-2, to=2-3] + \arrow["{\mathrm{inl}}"', from=2-1, to=3-2] + \arrow["{\mathrm{inr}}", from=2-3, to=3-2] +\end{tikzcd}\] +~~~ + +```agda + Amalgamated-free-product : Group ℓ + inlᴳ : Groups.Hom A Amalgamated-free-product + inrᴳ : Groups.Hom B Amalgamated-free-product + glueᴳ : inlᴳ Groups.∘ f ≡ inrᴳ Groups.∘ g +``` + + +```agda + Amalgamated-free-product = to-group fp where + fp : make-group Amalgamated + fp .make-group.group-is-set = squash + fp .make-group.unit = nil + fp .make-group.mul = _◆_ + fp .make-group.inv = inv + fp .make-group.assoc = f-assoc + fp .make-group.invl = f-invl + fp .make-group.idl = f-idl + + inlᴳ .hom = inl + inlᴳ .preserves .pres-⋆ = inl-hom + + inrᴳ .hom = inr + inrᴳ .preserves .pres-⋆ = inr-hom + + glueᴳ = ext glue +``` +
+ +The universal property of the pushout is easy to verify. + +```agda + Groups-pushout : is-pushout (Groups ℓ) f inlᴳ g inrᴳ + Groups-pushout .square = glueᴳ + Groups-pushout .universal {Q} {p} {q} comm .hom = go where + module Q = Group-on (Q .snd) + go : Amalgamated → ⌞ Q ⌟ + go (x ◆ y) = go x Q.⋆ go y + go (inv x) = go x Q.⁻¹ + go nil = Q.unit + go (f-assoc x y z i) = Q.associative {go x} {go y} {go z} i + go (f-invl x i) = Q.inversel {go x} i + go (f-idl x i) = Q.idl {go x} i + go (inl a) = p # a + go (inl-hom a a' i) = p .preserves .pres-⋆ a a' i + go (inr b) = q # b + go (inr-hom b b' i) = q .preserves .pres-⋆ b b' i + go (glue c i) = unext comm c i + go (squash x y α β i j) = + Q.has-is-set (go x) (go y) (λ i → go (α i)) (λ i → go (β i)) i j + Groups-pushout .universal comm .preserves .pres-⋆ _ _ = refl + Groups-pushout .universal∘i₁ = trivial! + Groups-pushout .universal∘i₂ = trivial! + Groups-pushout .unique {Q = Q} {colim' = u} comm₁ comm₂ = ext $ + Amalgamated-elim-prop (λ _ → hlevel 1) + (λ x p y q → u .preserves .pres-⋆ x y ∙ ap₂ Q._⋆_ p q) + (λ x p → pres-inv (u .preserves) ∙ ap Q._⁻¹ p) + (pres-id (u .preserves)) + (unext comm₁) (unext comm₂) + where module Q = Group-on (Q .snd) + + Groups-Pushout : Pushout (Groups ℓ) f g + Groups-Pushout .coapex = Amalgamated-free-product + Groups-Pushout .i₁ = inlᴳ + Groups-Pushout .i₂ = inrᴳ + Groups-Pushout .has-is-po = Groups-pushout +``` + +Since the [[zero group]] is also an [[initial object]], this shows that the +category of groups is [[finitely cocomplete]]. + +```agda +Groups-finitely-cocomplete : Finitely-cocomplete (Groups ℓ) +Groups-finitely-cocomplete = with-pushouts (Groups _) + (Zero.initial ∅ᴳ) Groups-Pushout +``` + +We thus get the free product of $A$ and $B$ by abstract nonsense, as the +pushout of the span $A \overset{¡}{\ot} 0 \overset{¡}{\to} B$. + +```agda +Free-product : Group ℓ → Group ℓ → Group ℓ +Free-product A B = Groups-finitely-cocomplete .coproducts A B .coapex +``` From 755d602f488b6154564dfbbf2a594a18f1ef3dcf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Na=C3=AFm=20Favier?= Date: Sat, 3 Aug 2024 18:29:42 +0200 Subject: [PATCH 3/9] def: semidirect product of groups --- src/1Lab/Underlying.agda | 7 + src/Algebra/Group.lagda.md | 2 +- src/Algebra/Group/Action.lagda.md | 65 +++++- src/Algebra/Group/Cayley.lagda.md | 4 +- .../Group/Concrete/Semidirect.lagda.md | 207 ++++++++++++++++++ src/Algebra/Group/Semidirect.lagda.md | 133 +++++++++++ src/Cat/Displayed/Univalence/Thin.lagda.md | 32 ++- src/Cat/Morphism/Instances.agda | 33 +-- src/Cat/Univalent.lagda.md | 5 + src/Homotopy/Connectedness.lagda.md | 17 +- .../Connectedness/Automation.lagda.md | 12 +- src/Homotopy/Truncation.lagda.md | 27 ++- 12 files changed, 505 insertions(+), 39 deletions(-) create mode 100644 src/Algebra/Group/Concrete/Semidirect.lagda.md create mode 100644 src/Algebra/Group/Semidirect.lagda.md diff --git a/src/1Lab/Underlying.agda b/src/1Lab/Underlying.agda index 068c8ed12..187ff6261 100644 --- a/src/1Lab/Underlying.agda +++ b/src/1Lab/Underlying.agda @@ -114,6 +114,13 @@ instance → Funlike (f ≡ g) A (λ x → f x ≡ g x) Funlike-Homotopy = record { _#_ = happly } + Funlike-Σ + : ∀ {ℓ ℓ' ℓx ℓp} {A : Type ℓ} {B : A → Type ℓ'} {X : Type ℓx} {P : X → Type ℓp} + → ⦃ Funlike X A B ⦄ + → Funlike (Σ X P) A B + Funlike-Σ = record { _#_ = λ (f , _) → f #_ } + {-# OVERLAPPABLE Funlike-Σ #-} + -- Generalised "sections" (e.g. of a presheaf) notation. _ʻ_ : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {F : Type ℓ''} diff --git a/src/Algebra/Group.lagda.md b/src/Algebra/Group.lagda.md index 3cec489d5..68940d96b 100644 --- a/src/Algebra/Group.lagda.md +++ b/src/Algebra/Group.lagda.md @@ -193,7 +193,7 @@ record ``` A tedious calculation shows that this is sufficient to preserve the -identity: +identity and inverses: ```agda private diff --git a/src/Algebra/Group/Action.lagda.md b/src/Algebra/Group/Action.lagda.md index 983121d93..81b35b825 100644 --- a/src/Algebra/Group/Action.lagda.md +++ b/src/Algebra/Group/Action.lagda.md @@ -1,10 +1,13 @@ -# Group actions +# Group actions {defines="group-action"} A useful way to think about [groups] is to think of their elements as encoding "symmetries" of a particular object. For a concrete example, @@ -64,7 +68,7 @@ we want a group $G$ to act on an object $X$ of a more general [group of symmetries]: Algebra.Group.html#symmetric-groups [category]: Cat.Base.html -## Automorphism groups +## Automorphism groups {defines="automorphism-group"} The answer is that, for an object $X$ of some category $\cC$, the collection of all [isomorphisms] $X \cong X$ forms a group under @@ -83,7 +87,7 @@ module _ {o ℓ} (C : Precategory o ℓ) where mg : make-group (X C.≅ X) mg .make-group.group-is-set = hlevel 2 mg .make-group.unit = C.id-iso - mg .make-group.mul g f = g C.∘Iso f + mg .make-group.mul f g = f C.∘Iso g mg .make-group.inv = C._Iso⁻¹ mg .make-group.assoc x y z = ext (sym (C.assoc _ _ _)) mg .make-group.invl x = ext (x .C.invl) @@ -99,6 +103,14 @@ $G$; A **$G$-action on $X$** is a group homomorphism $G \to Action G X = Groups.Hom G (Aut X) ``` +::: note +Since we've defined $f \star g = g \circ f$ in the automorphism group, +our definition corresponds to *right* actions. If we had defined +$f \star g = f \circ g$ instead, we would get *left* actions. +Of course, the two definitions are formally dual, so it does not +really matter. +::: + # As functors Recall that we defined the [delooping] of a [monoid] $M$ into a category @@ -153,3 +165,50 @@ applying the right helpers for pushing paths inwards, we're left with (is-prop→pathp (λ i → is-group-hom-is-prop) _ _) .is-iso.linv x → Functor-path (λ _ → refl) λ _ → refl ``` + +# Examples of actions + +:::{.definition #trivial-action} +For any group $G$, category $\cC$ and object $X : \cC$, we have the +**trivial action** of $G$ on $X$ which maps every element to the +identity automorphism. It can be defined simply as the [[zero morphism]] +$G \to \rm{Aut}(X)$. +::: + +```agda +module _ {o ℓ} {C : Precategory o ℓ} (G : Group ℓ) where + trivial-action : ∀ X → Action C G X + trivial-action X = Zero.zero→ ∅ᴳ +``` + +:::{.definition #principal-action} +Any group $G$ acts on itself on the right in two ways: first, $G$ acts on its +underlying set by multiplication on the right. This is sometimes called +the **principal action** or the **(right-)regular action**, and is the +basis for [[Cayley's theorem]]. +::: + + + +```agda + principal-action : Action (Sets ℓ) G (G .fst) + principal-action .hom x = equiv→iso ((G._⋆ x) , G.⋆-equivr x) + principal-action .preserves .pres-⋆ x y = ext λ z → G.associative +``` + +$G$ also acts on itself *as a group* by **conjugation**. An automorphism +of $G$ that arises from conjugation with an element of $G$ is called an +**inner automorphism**. + +```agda + conjugation-action : Action (Groups ℓ) G G + conjugation-action .hom x = total-iso Groups-equational + ((λ y → x G.⁻¹ G.⋆ y G.⋆ x) , ∙-is-equiv (G.⋆-equivr x) (G.⋆-equivl (x G.⁻¹))) + (record { pres-⋆ = λ y z → group! G }) + conjugation-action .preserves .pres-⋆ x y = ext λ z → group! G +``` diff --git a/src/Algebra/Group/Cayley.lagda.md b/src/Algebra/Group/Cayley.lagda.md index 0022b457a..f05fcb55f 100644 --- a/src/Algebra/Group/Cayley.lagda.md +++ b/src/Algebra/Group/Cayley.lagda.md @@ -13,7 +13,7 @@ module Algebra.Group.Cayley {ℓ} (G : Group ℓ) where open Group-on (G .snd) renaming (underlying-set to G-set) ``` -# Cayley's theorem +# Cayley's theorem {defines="cayleys-theorem"} Cayley's theorem says that any group $G$ admits a representation as a subgroup of a [symmetric group], specifically the symmetric group acting @@ -22,7 +22,7 @@ on the underlying set of $G$. [symmetric group]: Algebra.Group.html#symmetric-groups First, recall that we get a family of equivalences $G \simeq G$ by multiplication -on the left: +on the left, the [[principal action]] of $G$ on itself: ```agda Cayley : ⌞ G ⌟ → ⌞ G ⌟ ≃ ⌞ G ⌟ diff --git a/src/Algebra/Group/Concrete/Semidirect.lagda.md b/src/Algebra/Group/Concrete/Semidirect.lagda.md new file mode 100644 index 000000000..6821058b5 --- /dev/null +++ b/src/Algebra/Group/Concrete/Semidirect.lagda.md @@ -0,0 +1,207 @@ + + +```agda +module Algebra.Group.Concrete.Semidirect {ℓ} where +``` + +# Semidirect products of concrete groups {defines="semidirect-product-of-concrete-groups"} + +The construction of the [[semidirect product]] for [[concrete groups]] +is quite natural: given a concrete group $G$ and an action $\varphi : +\B G \to \rm{ConcreteGroups}$ of $G$ on $H = \varphi(\point{G})$, we +simply define $\B(G \ltimes H)$ as the $\Sigma$-type + +$$ +\sum_{g : \B G} \B \varphi(g) +$$ + +pointed at $(\point{G}, \point{H})$. + + + +```agda + H : ConcreteGroup ℓ + H = φ (pt G) + + Semidirect-concrete : ConcreteGroup ℓ + Semidirect-concrete .B .fst = Σ ⌞ B G ⌟ λ g → ⌞ B (φ g) ⌟ + Semidirect-concrete .B .snd = pt G , pt H +``` + +That this is a connected groupoid follows from standard results. + +```agda + Semidirect-concrete .has-is-connected = is-connected→is-connected∙ $ + Σ-is-n-connected 2 + (is-connected∙→is-connected (G .has-is-connected)) + (λ a → is-connected∙→is-connected (φ a .has-is-connected)) + Semidirect-concrete .has-is-groupoid = Σ-is-hlevel 3 + (G .has-is-groupoid) + (λ a → φ a .has-is-groupoid) +``` + +In order to relate this with the definition of [[semidirect products]] +for abstract groups, we show that the [[fundamental group]] +$\pi_1\B(G \ltimes H)$ is the semidirect product $\pi_1\B G \ltimes +\pi_1\B H$. + +To that end, we start by defining the action of $\pi_1\B G$ on +$\pi_1\B H$ induced by $\varphi$. +Given a loop $p : \point{G} \equiv \point{G}$, we can apply the function +$x \mapsto \pi_1 \B \varphi(x)$ to it to get a loop $\pi_1 \B H \equiv +\pi_1 \B H$, which we then turn into an automorphism. + + + +```agda + π₁-φ : Action (Groups ℓ) (π₁B G) (π₁B H) + π₁-φ .hom p = path→iso (ap (π₁B ⊙ φ) p) + π₁-φ .preserves .pres-⋆ p q = + path→iso (ap (π₁B ⊙ φ) (p ∙ q)) ≡⟨ ap path→iso (ap-∙ (π₁B ⊙ φ) p q) ⟩ + path→iso (ap (π₁B ⊙ φ) p ∙ ap (π₁B ⊙ φ) q) ≡⟨ path→iso-∙ (Groups ℓ) _ _ ⟩ + path→iso (ap (π₁B ⊙ φ) p) ∘Iso path→iso (ap (π₁B ⊙ φ) q) ∎ + + π₁BG⋉π₁BH : Group ℓ + π₁BG⋉π₁BH = Semidirect-product (π₁B G) (π₁B H) π₁-φ + + private module ⋉ = Group-on (π₁BG⋉π₁BH .snd) +``` + +::: source +The following proof is adapted from Symmetry [-@Symmetry, §4.14]. +::: + +The first step is to construct an equivalence between the underlying +sets of $\pi_1\B(G \ltimes H)$ and $\pi_1\B G \ltimes \pi_1\B H$. +Since $\B(G \ltimes H)$ is a $\Sigma$-type, its loops consist of pairs +$(p : \point{G} \is \point{G}, q : \point{H} \is_p \point{H})$, where +the second component is a [[dependent path]] over $p$ in the total space +of $\varphi$. What we actually want is a pair of non-dependent loops, +so we need to "realign" the second component by transporting one of +its endpoints along $p$; we do this by generalising on the endpoints +and using [[path induction]]. + +Note that we have a type $A = \B G$, a type family $B(a) = \B\varphi(a)$, +and a function $f : (a : A) \to B(a)$ given by $a \mapsto \point{\varphi(a)}$. +The following constructions work in this general setting. + + + +```agda + align + : ∀ {a a' : A} (p : a ≡ a') + → PathP (λ i → B (p i)) (f a) (f a') ≃ (f a' ≡ f a') + align {a} = + J (λ a' p → PathP (λ i → B (p i)) (f a) (f a') ≃ (f a' ≡ f a')) id≃ + + align-refl + : ∀ {a : A} (q : f a ≡ f a) + → align (λ _ → a) # q ≡ q + align-refl {a} = unext $ + J-refl (λ a' p → PathP (λ i → B (p i)) (f a) (f a') ≃ (f a' ≡ f a')) id≃ + + Σ-align + : ∀ {a a' : A} + → ((a , f a) ≡ (a' , f a')) ≃ ((a ≡ a') × (f a' ≡ f a')) + Σ-align = Iso→Equiv Σ-pathp-iso e⁻¹ ∙e Σ-ap-snd align +``` + +It remains to show that this equivalence is a [[group homomorphism]] +--- or rather a group*oid* homomorphism, since we've generalised the +endpoints. +First, note that we can describe the action of $\varphi$ on paths using +a kind of dependent [[conjugation]] operation. + +```agda + conjP : ∀ {a a' : A} → (p : a ≡ a') → f a ≡ f a → f a' ≡ f a' + conjP {a} p = transport (λ i → f a ≡ f a → f (p i) ≡ f (p i)) λ q → q + + conjP-refl : ∀ {a : A} → (q : f a ≡ f a) → conjP refl q ≡ q + conjP-refl {a} = unext $ transport-refl {A = f a ≡ f a → _} λ q → q +``` + +Thus we have a composition operation on pairs of paths that generalises +the multiplication in $\pi_1\B G \ltimes \pi_1\B H$. + +```agda + _∙⋉_ + : ∀ {a₀ a₁ a₂ : A} + → (a₀ ≡ a₁) × (f a₁ ≡ f a₁) + → (a₁ ≡ a₂) × (f a₂ ≡ f a₂) + → (a₀ ≡ a₂) × (f a₂ ≡ f a₂) + (p , q) ∙⋉ (p' , q') = p ∙ p' , conjP p' q ∙ q' +``` + +
+ +We can then show that `Σ-align`{.Agda} preserves the group(oid) +operations by double path induction. + +```agda + Σ-align-∙ + : ∀ {a₀ a₁ a₂ : A} + → (p : (a₀ , f a₀) ≡ (a₁ , f a₁)) + → (p' : (a₁ , f a₁) ≡ (a₂ , f a₂)) + → Σ-align # (p ∙ p') + ≡ Σ-align # p ∙⋉ Σ-align # p' +``` + + +```agda + Σ-align-∙ {a₀} {a₁} {a₂} p p' = J₂ + (λ a₀ a₂ p⁻¹ p' → + ∀ (q : PathP (λ i → B (p⁻¹ (~ i))) (f a₀) (f a₁)) + → (q' : PathP (λ i → B (p' i)) (f a₁) (f a₂)) + → Σ-align # ((sym p⁻¹ ,ₚ q) ∙ (p' ,ₚ q')) + ≡ Σ-align # (sym p⁻¹ ,ₚ q) ∙⋉ Σ-align # (p' ,ₚ q')) + (λ q q' → + Σ-align # ((refl ,ₚ q) ∙ (refl ,ₚ q')) ≡˘⟨ ap# Σ-align (ap-∙ (a₁ ,_) q q') ⟩ + Σ-align # (refl ,ₚ q ∙ q') ≡⟨⟩ + refl , align refl # (q ∙ q') ≡⟨ refl ,ₚ align-refl (q ∙ q') ⟩ + refl , q ∙ q' ≡˘⟨ refl ,ₚ ap₂ _∙_ (align-refl q) (align-refl q') ⟩ + refl , align refl # q ∙ align refl # q' ≡˘⟨ ∙-idl _ ,ₚ ap (_∙ align refl # q') (conjP-refl (align refl # q)) ⟩ + refl ∙ refl , conjP refl (align refl # q) ∙ align refl # q' ∎) + (ap fst (sym p)) (ap fst p') (ap snd p) (ap snd p') +``` +
+ +This concludes the proof that the constructions of the semidirect +product of abstract and concrete groups agree over the equivalence +between abstract and concrete groups. + +```agda + Semidirect-concrete-abstract : π₁B Semidirect-concrete ≡ π₁BG⋉π₁BH + Semidirect-concrete-abstract = ∫-Path + (total-hom (Σ-align (pt ⊙ φ) .fst) + (record { pres-⋆ = Σ-align-∙ (pt ⊙ φ) })) + (Σ-align (pt ⊙ φ) .snd) +``` diff --git a/src/Algebra/Group/Semidirect.lagda.md b/src/Algebra/Group/Semidirect.lagda.md new file mode 100644 index 000000000..6c0d43f62 --- /dev/null +++ b/src/Algebra/Group/Semidirect.lagda.md @@ -0,0 +1,133 @@ + + +```agda +module Algebra.Group.Semidirect {ℓ} where +``` + +# Semidirect products of groups {defines="semidirect-product"} + +Given a [[group]] $A$ [[acting|group action]] on another group $B$ (that is, +equipped with a [[group homomorphism]] $\varphi : A \to \rm{Aut}(B)$ from $A$ to +the [[automorphism group]] of $B$), we define the **semidirect product** +$A \ltimes B$ as a variant of the [[direct product|direct product of groups]] $A \times B$ in which +the $A$ component influences the multiplication of the $B$ component. + +To motivate the concept, let's consider some examples: + +- The [[dihedral group]] of order $2n$, $D_n$, which is the group of +symmetries of a regular $n$-gon, can be defined as the semidirect product +$\ZZ/2\ZZ \ltimes \ZZ/n\ZZ$, where the action of $\ZZ/2\ZZ$ sends $1$ +to the "negation" automorphism of $\ZZ/n\ZZ$. Intuitively, a symmetry +of the regular $n$-gon has two components: a reflection (captured by the +cyclic group $\ZZ/2\ZZ$) and a rotation (captured by the cyclic group $\ZZ/n\ZZ$); +but when combining two symmetries, a reflection will swap the direction +of further rotations. This is exactly captured by the semidirect product. +- The group of isometries of the square lattice $\ZZ^2$ (considered +as a subspace of $\RR^2$), which we will refer to by its IUC notation +$p4m$, consists of reflections, rotations and translations. It can thus +be defined as a further semidirect product of the [[dihedral group]] +$D_4$ acting on the group of translations $\ZZ^2$ in the obvious way. +- Leaving the discrete world, the group of all isometries of the plane +$\RR^2$ can be seen analogously as the semidirect product of the +orthogonal group $O(2)$ acting on the translation group $\RR^2$, where +$O(2)$ is itself the semidirect product of $\ZZ/2\ZZ$ acting on the +*special* orthogonal group $SO(2)$, also known as the circle group. + + + +We are now ready to define $A \ltimes B$. The underlying set is the +cartesian product $A \times B$; the unit is the pair of units +$(1_A, 1_B)$. The interesting part of the definition is the multiplication: +we set $(a, b) \star (a', b') = (a \star_A a', \varphi_{a'}(b) \star_B b')$. + +::: note +Since our [[group actions]] are *right* actions, what we define here +is the *right* semidirect product. The version that works with *left* +actions instead would be $(a \star_A a', b \star_B \varphi_{a}(b'))$. +::: + +```agda + Semidirect-product : Group ℓ + Semidirect-product = to-group A⋉B where + A⋉B : make-group (⌞ A ⌟ × ⌞ B ⌟) + A⋉B .group-is-set = hlevel 2 + A⋉B .unit = A.unit , B.unit + A⋉B .mul (a , b) (a' , b') = a A.⋆ a' , (φ # a' # b) B.⋆ b' +``` + +The definition of the inverses is then forced, and we easily check that +the group axioms are verified. + +```agda + A⋉B .inv (a , b) = a A.⁻¹ , (φ # (a A.⁻¹) # b) B.⁻¹ + A⋉B .assoc (ax , bx) (ay , by) (az , bz) = Σ-pathp A.associative $ + ⌜ φ # (ay A.⋆ az) # bx ⌝ B.⋆ φ # az # by B.⋆ bz ≡⟨ ap! (unext (φ .preserves .pres-⋆ _ _) _) ⟩ + φ # az # (φ # ay # bx) B.⋆ φ # az # by B.⋆ bz ≡⟨ B.associative ⟩ + (φ # az # (φ # ay # bx) B.⋆ φ # az # by) B.⋆ bz ≡˘⟨ ap (B._⋆ bz) ((φ # az) .Groups.to .preserves .pres-⋆ _ _) ⟩ + φ # az # (φ # ay # bx B.⋆ by) B.⋆ bz ∎ + A⋉B .invl (a , b) = Σ-pathp A.inversel $ + φ # a # ⌜ (φ # (a A.⁻¹) # b) B.⁻¹ ⌝ B.⋆ b ≡˘⟨ ap¡ (pres-inv ((φ # _) .Groups.to .preserves)) ⟩ + φ # a # (φ # (a A.⁻¹) # (b B.⁻¹)) B.⋆ b ≡˘⟨ ap (B._⋆ b) (unext (pres-⋆ (φ .preserves) _ _) _) ⟩ + φ # ⌜ a A.⁻¹ A.⋆ a ⌝ # (b B.⁻¹) B.⋆ b ≡⟨ ap! A.inversel ⟩ + φ # A.unit # (b B.⁻¹) B.⋆ b ≡⟨ ap (B._⋆ b) (unext (pres-id (φ .preserves)) _) ⟩ + b B.⁻¹ B.⋆ b ≡⟨ B.inversel ⟩ + B.unit ∎ + A⋉B .idl (a , b) = Σ-pathp A.idl $ + φ # a # B.unit B.⋆ b ≡⟨ ap (B._⋆ b) (pres-id ((φ # a) .Groups.to .preserves)) ⟩ + B.unit B.⋆ b ≡⟨ B.idl ⟩ + b ∎ +``` + +The natural projection from $A \ltimes B$ to the first component $A$ is +a [[group homomorphism]], but the same cannot be said about the second +component (can you see why?). + +```agda + ⋉-proj : Groups.Hom Semidirect-product A + ⋉-proj .hom = fst + ⋉-proj .preserves .pres-⋆ _ _ = refl +``` + +When the action of $A$ on $B$ is [[trivial|trivial action]], i.e. $\varphi_a$ is the +identity automorphism for all $a : A$, it's easy to see that the +semidirect product $A \ltimes B$ agrees with the direct product +$A \times B$. + + + +```agda + Semidirect-trivial + : Semidirect-product A B (trivial-action A B) ≡ Direct-product A B + Semidirect-trivial = ∫-Path Groups-equational + (total-hom (λ x → x) (record { pres-⋆ = λ _ _ → refl })) + id-equiv +``` + +Another way to understand the semidirect product is to look at its +definition [[for concrete groups|semidirect product of concrete groups]], +which is remarkably simple. diff --git a/src/Cat/Displayed/Univalence/Thin.lagda.md b/src/Cat/Displayed/Univalence/Thin.lagda.md index bfa44ca44..296d07c10 100644 --- a/src/Cat/Displayed/Univalence/Thin.lagda.md +++ b/src/Cat/Displayed/Univalence/Thin.lagda.md @@ -148,27 +148,35 @@ record is-equational {ℓ o' ℓ'} {S : Type ℓ → Type o'} (spec : Thin-struc module So = Precategory (Structured-objects spec) module Som = Cat.Morphism (Structured-objects spec) - equiv-hom→inverse-hom + abstract + equiv-hom→inverse-hom + : ∀ {a b : So.Ob} + → (f : ⌞ a ⌟ ≃ ⌞ b ⌟) + → ∣ spec .is-hom (Equiv.to f) (a .snd) (b .snd) ∣ + → ∣ spec .is-hom (Equiv.from f) (b .snd) (a .snd) ∣ + equiv-hom→inverse-hom {a = a} {b = b} f e = + EquivJ (λ B e → ∀ st → ∣ spec .is-hom (e .fst) (a .snd) st ∣ → ∣ spec .is-hom (Equiv.from e) st (a .snd) ∣) + (λ _ → invert-id-hom) f (b .snd) e + + total-iso : ∀ {a b : So.Ob} → (f : ⌞ a ⌟ ≃ ⌞ b ⌟) → ∣ spec .is-hom (Equiv.to f) (a .snd) (b .snd) ∣ - → ∣ spec .is-hom (Equiv.from f) (b .snd) (a .snd) ∣ - equiv-hom→inverse-hom {a = a} {b = b} f e = - EquivJ (λ B e → ∀ st → ∣ spec .is-hom (e .fst) (a .snd) st ∣ → ∣ spec .is-hom (Equiv.from e) st (a .snd) ∣) - (λ _ → invert-id-hom) f (b .snd) e + → a Som.≅ b + total-iso f e = Som.make-iso + (total-hom (Equiv.to f) e) + (total-hom (Equiv.from f) (equiv-hom→inverse-hom f e)) + (ext (Equiv.ε f)) + (ext (Equiv.η f)) ∫-Path : ∀ {a b : So.Ob} → (f : So.Hom a b) → is-equiv (f #_) → a ≡ b - ∫-Path {a = a} {b = b} f eqv = - Σ-pathp (n-ua (f .hom , eqv)) $ - EquivJ (λ B e → ∀ st → ∣ spec .is-hom (e .fst) (a .snd) st ∣ → PathP (λ i → S (ua e i)) (a .snd) st) - (λ st pres → to-pathp (ap (λ e → subst S e (a .snd)) ua-id-equiv - ·· transport-refl _ - ·· spec .id-hom-unique pres (invert-id-hom pres))) - (f .hom , eqv) (b .snd) (f .preserves) + ∫-Path {a = a} {b = b} f eqv = Univalent.iso→path + (Structured-objects-is-category spec) + (total-iso ((f #_) , eqv) (f .preserves)) open is-equational public ``` diff --git a/src/Cat/Morphism/Instances.agda b/src/Cat/Morphism/Instances.agda index 940afe8aa..0d234b73d 100644 --- a/src/Cat/Morphism/Instances.agda +++ b/src/Cat/Morphism/Instances.agda @@ -7,19 +7,20 @@ open Precategory module Cat.Morphism.Instances where -instance - H-Level-is-invertible - : ∀ {o ℓ} {C : Precategory o ℓ} {a b} {f : C .Hom a b} {n} → H-Level (is-invertible C f) (suc n) - H-Level-is-invertible {C = C} = prop-instance (is-invertible-is-prop C) - -unquoteDecl H-Level-↪ = declare-record-hlevel 2 H-Level-↪ (quote _↪_) -unquoteDecl H-Level-↠ = declare-record-hlevel 2 H-Level-↠ (quote _↠_) -unquoteDecl H-Level-Inverses = declare-record-hlevel 2 H-Level-Inverses (quote Inverses) -unquoteDecl H-Level-≅ = declare-record-hlevel 2 H-Level-≅ (quote _≅_) -unquoteDecl - H-Level-has-section = declare-record-hlevel 2 H-Level-has-section (quote has-section) -unquoteDecl - H-Level-has-retract = declare-record-hlevel 2 H-Level-has-retract (quote has-retract) +abstract + instance + H-Level-is-invertible + : ∀ {o ℓ} {C : Precategory o ℓ} {a b} {f : C .Hom a b} {n} → H-Level (is-invertible C f) (suc n) + H-Level-is-invertible {C = C} = prop-instance (is-invertible-is-prop C) + + unquoteDecl H-Level-↪ = declare-record-hlevel 2 H-Level-↪ (quote _↪_) + unquoteDecl H-Level-↠ = declare-record-hlevel 2 H-Level-↠ (quote _↠_) + unquoteDecl H-Level-Inverses = declare-record-hlevel 2 H-Level-Inverses (quote Inverses) + unquoteDecl H-Level-≅ = declare-record-hlevel 2 H-Level-≅ (quote _≅_) + unquoteDecl + H-Level-has-section = declare-record-hlevel 2 H-Level-has-section (quote has-section) + unquoteDecl + H-Level-has-retract = declare-record-hlevel 2 H-Level-has-retract (quote has-retract) module _ {o ℓ} {C : Precategory o ℓ} where instance Extensional-↪ : ∀ {a b ℓr} ⦃ _ : Extensional (C .Hom a b) ℓr ⦄ → Extensional (_↪_ C a b) ℓr @@ -30,3 +31,9 @@ module _ {o ℓ} {C : Precategory o ℓ} where instance Extensional-≅ : ∀ {a b ℓr} ⦃ _ : Extensional (C .Hom a b) ℓr ⦄ → Extensional (_≅_ C a b) ℓr Extensional-≅ ⦃ sa ⦄ = injection→extensional! (≅-pathp C refl refl) sa + + Funlike-≅ + : ∀ {ℓ' ℓ''} {A : Type ℓ'} {B : A → Type ℓ''} + → ∀ {a b} ⦃ i : Funlike (Hom C a b) A B ⦄ + → Funlike (_≅_ C a b) A B + Funlike-≅ .Funlike._#_ f x = f .to # x diff --git a/src/Cat/Univalent.lagda.md b/src/Cat/Univalent.lagda.md index 3cddaea93..0a6358d82 100644 --- a/src/Cat/Univalent.lagda.md +++ b/src/Cat/Univalent.lagda.md @@ -176,6 +176,11 @@ paths in `Hom`{.Agda}-sets. ) p q + path→iso-∙ + : ∀ {A B C} (p : A ≡ B) (q : B ≡ C) + → path→iso (p ∙ q) ≡ path→iso p ∘Iso path→iso q + path→iso-∙ p q = ext (path→to-∙ p q) + path→to-sym : ∀ {A B} (p : A ≡ B) → path→iso p .from ≡ path→iso (sym p) .to path→to-sym = J (λ B p → path→iso p .from ≡ path→iso (sym p) .to) refl diff --git a/src/Homotopy/Connectedness.lagda.md b/src/Homotopy/Connectedness.lagda.md index 14223e02a..04eaf9a14 100644 --- a/src/Homotopy/Connectedness.lagda.md +++ b/src/Homotopy/Connectedness.lagda.md @@ -18,6 +18,7 @@ module Homotopy.Connectedness where private variable ℓ ℓ' ℓ'' : Level A B : Type ℓ + P : A → Type ℓ x y : A ``` --> @@ -216,7 +217,7 @@ retract→is-n-connected (suc (suc n)) f g h a-conn = Since the truncation operator $\| - \|_n$ also preserves products, a remarkably similar argument shows that if $A$ and $B$ are $n$-connected, -then so is $A \times B$ is. +then so is $A \times B$. ```agda ×-is-n-connected @@ -226,6 +227,20 @@ then so is $A \times B$ is. n-Tr-product (×-is-hlevel 0 (n-connected.to n a-conn) (n-connected.to n b-conn)) ``` +We can generalise this to $\Sigma$-types: if $A$ is $n$-connected and +$B$ is an $A$-indexed family of $n$-connected types, then we have +$\|\Sigma_{a : A} B(a)\|_n \simeq \|\Sigma_{a : A} \|B(a)\|_n\|_n +\simeq \|A\|_n \simeq 1$. + +```agda +Σ-is-n-connected + : ∀ n → is-n-connected A n → (∀ a → is-n-connected (P a) n) → is-n-connected (Σ A P) n +Σ-is-n-connected 0 = _ +Σ-is-n-connected (suc n) a-conn b-conn = n-connected.from n $ Equiv→is-hlevel 0 + (n-Tr-Σ ∙e n-Tr-≃ (Σ-contract λ _ → n-connected.to n (b-conn _))) + (n-connected.to n a-conn) +``` + Finally, we show the dual of two properties of truncations: if $A$ is $(1+n)$-connected, then each path space $x \equiv_A y$ is $n$-connected; And if $A$ is $(2+n)$-connected, then it is also $(1+n$) connected. This diff --git a/src/Homotopy/Connectedness/Automation.lagda.md b/src/Homotopy/Connectedness/Automation.lagda.md index 569b7959a..94fe06700 100644 --- a/src/Homotopy/Connectedness/Automation.lagda.md +++ b/src/Homotopy/Connectedness/Automation.lagda.md @@ -64,12 +64,12 @@ instance Connected-⊤ {n} = conn-instance (n-connected-∥-∥.from n (is-contr→is-connected (hlevel 0))) - Connected-× - : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {n} - → ⦃ Connected A n ⦄ → ⦃ Connected B n ⦄ - → Connected (A × B) n - Connected-× {n = n} ⦃ conn-instance ac ⦄ ⦃ conn-instance bc ⦄ = conn-instance - (×-is-n-connected n ac bc) + Connected-Σ + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {n} + → ⦃ Connected A n ⦄ → ⦃ ∀ {a} → Connected (B a) n ⦄ + → Connected (Σ A B) n + Connected-Σ {n = n} ⦃ conn-instance ac ⦄ ⦃ bc ⦄ = conn-instance + (Σ-is-n-connected n ac λ _ → Connected.has-n-connected bc) Connected-Path : ∀ {ℓ} {A : Type ℓ} {x y : A} {n} diff --git a/src/Homotopy/Truncation.lagda.md b/src/Homotopy/Truncation.lagda.md index 3b15b1e74..60deeb849 100644 --- a/src/Homotopy/Truncation.lagda.md +++ b/src/Homotopy/Truncation.lagda.md @@ -183,6 +183,11 @@ n-Tr-rec! → ⦃ hl : H-Level B (suc n) ⦄ → (A → B) → n-Tr A (suc n) → B n-Tr-rec! = n-Tr-elim (λ _ → _) (λ _ → hlevel _) + +n-Tr-map + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {n} + → (A → B) → n-Tr A (suc n) → n-Tr B (suc n) +n-Tr-map f = n-Tr-rec! (inc ∘ f) ``` --> @@ -267,7 +272,7 @@ n-Tr-univ n b-hl = Iso→Equiv λ where n-Tr-product : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {n} → n-Tr (A × B) (suc n) ≃ (n-Tr A (suc n) × n-Tr B (suc n)) -n-Tr-product {A = A} {B} {n} = distrib , distrib-is-equiv module n-Tr-product where +n-Tr-product {A = A} {B} {n} = distrib , distrib-is-equiv where distrib : n-Tr (A × B) (suc n) → n-Tr A (suc n) × n-Tr B (suc n) distrib (inc (x , y)) = inc x , inc y distrib (hub r) .fst = hub λ s → distrib (r s) .fst @@ -291,4 +296,24 @@ n-Tr-product {A = A} {B} {n} = distrib , distrib-is-equiv module n-Tr-product wh distrib-is-iso .linv = n-Tr-elim! _ λ x → refl distrib-is-equiv = is-iso→is-equiv distrib-is-iso + +n-Tr-Σ + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {n} + → n-Tr (Σ A B) (suc n) ≃ n-Tr (Σ A λ a → n-Tr (B a) (suc n)) (suc n) +n-Tr-Σ {A = A} {B} {n} = Iso→Equiv is where + is : Iso _ _ + is .fst = n-Tr-map (Σ-map id inc) + is .snd .is-iso.inv = n-Tr-rec! λ (a , b) → n-Tr-map (a ,_) b + is .snd .is-iso.rinv = n-Tr-elim! _ λ (a , b) → n-Tr-elim! (λ b → n-Tr-map (Σ-map id inc) (n-Tr-map (a ,_) b) ≡ inc (a , b)) (λ _ → refl) b + is .snd .is-iso.linv = n-Tr-elim! _ λ _ → refl + +n-Tr-≃ + : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {n} + → (e : A ≃ B) → n-Tr A (suc n) ≃ n-Tr B (suc n) +n-Tr-≃ e = Iso→Equiv is where + is : Iso _ _ + is .fst = n-Tr-map (e .fst) + is .snd .is-iso.inv = n-Tr-map (Equiv.from e) + is .snd .is-iso.rinv = elim! λ _ → ap inc (Equiv.ε e _) + is .snd .is-iso.linv = elim! λ _ → ap inc (Equiv.η e _) ``` From e0e97307983e40c89c3c3e286d341dfbceb106ac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Na=C3=AFm=20Favier?= Date: Mon, 5 Aug 2024 23:40:28 +0200 Subject: [PATCH 4/9] def: cyclic groups --- src/1Lab/Equiv.lagda.md | 2 + src/1Lab/Type.lagda.md | 5 + src/1Lab/Type/Pi.lagda.md | 7 + src/Algebra/Group.lagda.md | 51 +--- src/Algebra/Group/Ab.lagda.md | 56 +++-- src/Algebra/Group/Action.lagda.md | 12 +- src/Algebra/Group/Cat/Monadic.lagda.md | 2 +- src/Algebra/Group/Cayley.lagda.md | 5 +- src/Algebra/Group/Concrete/Abelian.lagda.md | 1 + src/Algebra/Group/Homotopy.lagda.md | 2 +- src/Algebra/Group/Homotopy/BAut.lagda.md | 7 +- src/Algebra/Group/Instances/Cyclic.lagda.md | 235 ++++++++++++++++++ src/Algebra/Group/Instances/Integers.lagda.md | 164 ++++++++++++ .../Group/Instances/Symmetric.lagda.md | 66 +++++ src/Algebra/Group/Semidirect.lagda.md | 4 +- src/Algebra/Group/Subgroup.lagda.md | 3 + src/Algebra/Magma/Unital.lagda.md | 2 +- src/Algebra/Ring.lagda.md | 2 +- src/Cat/Abelian/Endo.lagda.md | 2 +- src/Cat/Displayed/Univalence/Thin.lagda.md | 2 +- src/Data/Fin/Base.lagda.md | 20 +- src/Data/Fin/Closure.lagda.md | 50 +++- src/Data/Fin/Finite.lagda.md | 6 +- src/Data/Fin/Properties.lagda.md | 32 +++ src/Data/Int/Base.lagda.md | 11 +- src/Data/Int/DivMod.lagda.md | 231 +++++++++++++++++ src/Data/Int/Divisible.lagda.md | 69 +++++ src/Data/Int/Properties.lagda.md | 131 +++++++++- src/Data/Int/Universal.lagda.md | 2 +- src/Data/Nat/DivMod.lagda.md | 4 +- src/Data/Nat/Divisible.lagda.md | 4 +- src/Data/Nat/Properties.lagda.md | 5 + src/Data/Set/Coequaliser.lagda.md | 4 + src/Homotopy/Space/Circle.lagda.md | 6 +- src/Homotopy/Space/Delooping.lagda.md | 2 +- 35 files changed, 1079 insertions(+), 128 deletions(-) create mode 100644 src/Algebra/Group/Instances/Cyclic.lagda.md create mode 100644 src/Algebra/Group/Instances/Integers.lagda.md create mode 100644 src/Algebra/Group/Instances/Symmetric.lagda.md create mode 100644 src/Data/Int/DivMod.lagda.md create mode 100644 src/Data/Int/Divisible.lagda.md diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md index 520346896..89bff45ec 100644 --- a/src/1Lab/Equiv.lagda.md +++ b/src/1Lab/Equiv.lagda.md @@ -960,10 +960,12 @@ is-involutive→is-equiv inv = is-iso→is-equiv (iso _ inv inv) ## Closure properties +:::{.definition #two-out-of-three} We will now show a rather fundamental property of equivalences: they are closed under *two-out-of-three*. This means that, considering $f : A \to B$, $g : B \to C$, and $(g \circ f) : A \to C$ as a set of three things, if any two are an equivalence, then so is the third: +::: diff --git a/src/1Lab/Type/Pi.lagda.md b/src/1Lab/Type/Pi.lagda.md index 11030a05e..0fc2340c3 100644 --- a/src/1Lab/Type/Pi.lagda.md +++ b/src/1Lab/Type/Pi.lagda.md @@ -1,6 +1,7 @@ @@ -56,6 +52,13 @@ record is-abelian-group (_*_ : G → G → G) : Type (level-of G) where open is-group has-is-group renaming (unit to 1g) public ``` + + -The fundamental example of abelian group is the integers, $\ZZ$, under -addition. A type-theoretic interjection is necessary: the integers live -on the zeroth universe, so to have an $\ell$-sized group of integers, we -must lift it. - -```agda -ℤ-ab : ∀ {ℓ} → Abelian-group ℓ -ℤ-ab = to-ab mk-ℤ where - open make-abelian-group - mk-ℤ : make-abelian-group (Lift _ Int) - mk-ℤ .ab-is-set = hlevel 2 - mk-ℤ .mul (lift x) (lift y) = lift (x +ℤ y) - mk-ℤ .inv (lift x) = lift (negℤ x) - mk-ℤ .1g = lift 0 - mk-ℤ .idl (lift x) = ap lift (+ℤ-zerol x) - mk-ℤ .assoc (lift x) (lift y) (lift z) = ap lift (+ℤ-assoc x y z) - mk-ℤ .invl (lift x) = ap lift (+ℤ-invl x) - mk-ℤ .comm (lift x) (lift y) = ap lift (+ℤ-commutative x y) - -ℤ : ∀ {ℓ} → Group ℓ -ℤ = Abelian→Group ℤ-ab -``` +The fundamental example of an abelian group is the [[group of integers]]. diff --git a/src/Algebra/Group/Action.lagda.md b/src/Algebra/Group/Action.lagda.md index 81b35b825..6efe86bc9 100644 --- a/src/Algebra/Group/Action.lagda.md +++ b/src/Algebra/Group/Action.lagda.md @@ -54,19 +54,15 @@ $\bb{C} \to \bb{C}$ in a way _compatible_ with the group structure: Additive inverses "translate to" inverse maps, addition translates to function composition, and the additive identity is mapped to the identity function. Note that since $\bb{C}$ is a set, this is -equivalently a [group homomorphism] +equivalently a [[group homomorphism]] $$ \bb{R} \to \rm{Sym}(\bb{C}) $$, -where the codomain is the [group of symmetries] of $\bb{C}$. But what if +where the codomain is the [[group of symmetries|symmetric group]] of $\bb{C}$. But what if we want a group $G$ to act on an object $X$ of a more general -[category], rather than an object of $\Sets$? - -[group homomorphism]: Algebra.Group.html#group-homomorphisms -[group of symmetries]: Algebra.Group.html#symmetric-groups -[category]: Cat.Base.html +[[category]], rather than an object of $\Sets$? ## Automorphism groups {defines="automorphism-group"} @@ -207,7 +203,7 @@ of $G$ that arises from conjugation with an element of $G$ is called an ```agda conjugation-action : Action (Groups ℓ) G G - conjugation-action .hom x = total-iso Groups-equational + conjugation-action .hom x = total-iso ((λ y → x G.⁻¹ G.⋆ y G.⋆ x) , ∙-is-equiv (G.⋆-equivr x) (G.⋆-equivl (x G.⁻¹))) (record { pres-⋆ = λ y z → group! G }) conjugation-action .preserves .pres-⋆ x y = ext λ z → group! G diff --git a/src/Algebra/Group/Cat/Monadic.lagda.md b/src/Algebra/Group/Cat/Monadic.lagda.md index c5dc14bfe..6c0df60e4 100644 --- a/src/Algebra/Group/Cat/Monadic.lagda.md +++ b/src/Algebra/Group/Cat/Monadic.lagda.md @@ -163,7 +163,7 @@ but the other direction is by induction on "words". ```agda isom : is-iso K.₀ isom .is-iso.inv (A , alg) = A , Algebra-on→group-on alg - isom .is-iso.linv x = ∫-Path Groups-equational + isom .is-iso.linv x = ∫-Path (total-hom (λ x → x) (record { pres-⋆ = λ x y → refl })) id-equiv isom .is-iso.rinv x = Σ-pathp refl (Algebra-on-pathp _ _ go) where diff --git a/src/Algebra/Group/Cayley.lagda.md b/src/Algebra/Group/Cayley.lagda.md index f05fcb55f..24db969e3 100644 --- a/src/Algebra/Group/Cayley.lagda.md +++ b/src/Algebra/Group/Cayley.lagda.md @@ -2,6 +2,7 @@ ``` open import 1Lab.Prelude +open import Algebra.Group.Instances.Symmetric open import Algebra.Group.Cat.Base open import Algebra.Group ``` @@ -16,11 +17,9 @@ open Group-on (G .snd) renaming (underlying-set to G-set) # Cayley's theorem {defines="cayleys-theorem"} Cayley's theorem says that any group $G$ admits a representation as a -subgroup of a [symmetric group], specifically the symmetric group acting +subgroup of a [[symmetric group]], specifically the symmetric group acting on the underlying set of $G$. -[symmetric group]: Algebra.Group.html#symmetric-groups - First, recall that we get a family of equivalences $G \simeq G$ by multiplication on the left, the [[principal action]] of $G$ on itself: diff --git a/src/Algebra/Group/Concrete/Abelian.lagda.md b/src/Algebra/Group/Concrete/Abelian.lagda.md index af05780df..28ded9d8c 100644 --- a/src/Algebra/Group/Concrete/Abelian.lagda.md +++ b/src/Algebra/Group/Concrete/Abelian.lagda.md @@ -3,6 +3,7 @@ open import 1Lab.Path.Reasoning open import 1Lab.Prelude +open import Algebra.Group.Instances.Integers open import Algebra.Group.Cat.Base open import Algebra.Group.Concrete open import Algebra.Group.Ab diff --git a/src/Algebra/Group/Homotopy.lagda.md b/src/Algebra/Group/Homotopy.lagda.md index d461ea914..1266e7d06 100644 --- a/src/Algebra/Group/Homotopy.lagda.md +++ b/src/Algebra/Group/Homotopy.lagda.md @@ -162,7 +162,7 @@ module π₁Groupoid {ℓ} ((T , t) : Type∙ ℓ) (grpd : is-groupoid T) where π₁ = to-group mk π₁≡π₀₊₁ : π₁ ≡ πₙ₊₁ 0 (T , t) - π₁≡π₀₊₁ = ∫-Path Groups-equational + π₁≡π₀₊₁ = ∫-Path (total-hom inc (record { pres-⋆ = λ _ _ → refl })) (∥-∥₀-idempotent (grpd _ _)) ``` diff --git a/src/Algebra/Group/Homotopy/BAut.lagda.md b/src/Algebra/Group/Homotopy/BAut.lagda.md index 5e57f6be3..ee0ed874f 100644 --- a/src/Algebra/Group/Homotopy/BAut.lagda.md +++ b/src/Algebra/Group/Homotopy/BAut.lagda.md @@ -10,17 +10,14 @@ module Algebra.Group.Homotopy.BAut where # Deloopings of automorphism groups -Recall that any set $X$ generates a group [$\rm{Sym}(X)$][symg], given +Recall that any set $X$ generates a group [[$\rm{Sym}(X)$|symmetric group]] given by the automorphisms $X \simeq X$. We also have a generic construction of [[deloopings]]: special spaces $K(G,1)$ (for a group $G$), where the -[fundamental group] $\pi_1(K(G,1))$ recovers $G$. For the specific case +[[fundamental group]] $\pi_1(K(G,1))$ recovers $G$. For the specific case of deloping automorphism groups, we can give an alternative construction: The type of small types [[merely]] equivalent to $X$ has a fundamental group of $\rm{Sym}(X)$. -[symg]: Algebra.Group.html#symmetric-groups -[fundamental group]: Algebra.Group.Homotopy.html#homotopy-groups - ```agda module _ {ℓ} (T : Type ℓ) where BAut : Type (lsuc ℓ) diff --git a/src/Algebra/Group/Instances/Cyclic.lagda.md b/src/Algebra/Group/Instances/Cyclic.lagda.md new file mode 100644 index 000000000..455649920 --- /dev/null +++ b/src/Algebra/Group/Instances/Cyclic.lagda.md @@ -0,0 +1,235 @@ + + +```agda +module Algebra.Group.Instances.Cyclic where +``` + + + +# Cyclic groups {defines="cyclic-group"} + +We say that a [[group]] is **cyclic** if it is generated by a single +element $g$: that is, every element of the group can be written as some +integer power of $g$^[Some authors (namely, Bourbaki) call such groups +*monogeneous*, and reserve "cyclic" for the *finite* cyclic groups.]. + +```agda +_is-generated-by_ : ∀ {ℓ} (G : Group ℓ) (g : ⌞ G ⌟) → Type ℓ +G is-generated-by g = ∀ x → ∃[ n ∈ Int ] x ≡ pow G g n + +is-cyclic : ∀ {ℓ} (G : Group ℓ) → Type ℓ +is-cyclic G = ∃[ g ∈ G ] G is-generated-by g +``` + +::: note +Generators are not unique, so we must use $\exists$ to get a [[proposition]]. +In fact, if $g$ generates $G$, then so does $g^{-1}$, hence a non-trivial +cyclic group has at least two generators! + +```agda +module _ {ℓ} (G : Group ℓ) (open Group-on (G .snd)) where + inverse-generates + : ∀ g → G is-generated-by g → G is-generated-by g ⁻¹ + inverse-generates g gen x = gen x <&> λ (n , p) → negℤ n , ( + x ≡⟨ p ⟩ + pow G g n ≡˘⟨ inv-inv ⟩ + pow G g n ⁻¹ ⁻¹ ≡˘⟨ ap _⁻¹ (pres-inv (pow-hom G g .preserves) {lift n}) ⟩ + pow G g (negℤ n) ⁻¹ ≡˘⟨ pow-inverse G g (negℤ n) ⟩ + pow G (g ⁻¹) (negℤ n) ∎) +``` +::: + +The obvious example is the **infinite cyclic group** $\ZZ$ of the (additive) +integers generated by $1$, but there is also a **finite cyclic group** of order +$n$ for every $n \geq 1$. As it turns out, we can construct *all* the cyclic +groups using the same machine: the quotient group $\ZZ/n\ZZ$, where $n\ZZ$ +is the [[normal subgroup]] of multiples of $n$, is the cyclic group of order +$n$ when $n \geq 1$, and is the infinite cyclic group when $n = 0$. + +```agda +infix 30 _·ℤ +_·ℤ : ∀ (n : Nat) {ℓ} → normal-subgroup (ℤ {ℓ}) λ (lift i) → el (n ∣ℤ i) (∣ℤ-is-prop n i) +(n ·ℤ) .has-rep .has-unit = ∣ℤ-zero +(n ·ℤ) .has-rep .has-⋆ = ∣ℤ-+ +(n ·ℤ) .has-rep .has-inv = ∣ℤ-negℤ +(n ·ℤ) {ℓ} .has-conjugate {lift x} {lift y} = subst (n ∣ℤ_) x≡y+x-y + where + x≡y+x-y : x ≡ y +ℤ (x -ℤ y) + x≡y+x-y = + x ≡⟨ ap lower (ℤ.insertl {h = lift {ℓ = ℓ} y} (ℤ.inverser {x = lift y})) ⟩ + y +ℤ (negℤ y +ℤ x) ≡⟨ ap (y +ℤ_) (+ℤ-commutative (negℤ y) x) ⟩ + y +ℤ (x -ℤ y) ∎ + +infix 25 ℤ/_ +ℤ/_ : Nat → ∀ {ℓ} → Group ℓ +ℤ/ n = ℤ /ᴳ n ·ℤ +``` + +$\ZZ/n\ZZ$ is an [[abelian group]], since the commutativity of +addition descends to the quotient. + +```agda +ℤ/n-commutative : ∀ n {ℓ} → is-commutative-group {ℓ} (ℤ/ n) +ℤ/n-commutative n = elim! λ x y → ap (inc ⊙ lift) (+ℤ-commutative x y) + +infix 25 ℤ-ab/_ +ℤ-ab/_ : Nat → ∀ {ℓ} → Abelian-group ℓ +ℤ-ab/_ n = from-commutative-group (ℤ/ n) (ℤ/n-commutative n) +``` + +Furthermore, $\ZZ/n\ZZ$ is, by construction, cyclic, and is generated +by $1$. + + + +```agda + ℤ/n-cyclic : is-cyclic ℤ/n + ℤ/n-cyclic = inc (1 , gen) where + gen : ℤ/n is-generated-by 1 + gen = elim! λ x → inc (x , Integers.induction Int-integers + {P = λ x → inc (lift x) ≡ pow ℤ/n 1 x} + refl + (λ x → + inc (lift x) ≡ pow ℤ/n 1 x ≃⟨ _ , equiv→cancellable (⋆-equivr 1) ⟩ + inc (lift x) ⋆ 1 ≡ pow ℤ/n 1 x ⋆ 1 ≃⟨ ∙-pre-equiv (sym (ap (inc ⊙ lift) (+ℤ-oner x))) ⟩ + inc (lift (sucℤ x)) ≡ pow ℤ/n 1 x ⋆ 1 ≃⟨ ∙-post-equiv (sym (pow-sucr ℤ/n 1 x)) ⟩ + inc (lift (sucℤ x)) ≡ pow ℤ/n 1 (sucℤ x) ≃∎) + x) +``` + +We prove the following mapping-out property for $\ZZ/n\ZZ$: a [[group +homomorphism]] $\ZZ/n\ZZ \to G$ is uniquely determined by an element +$x : G$ of *order* $n$, i.e. such that $x^n = 1$. Note that this +condition is trivially satisfied if $n = 0$, so we don't need a +special case. + +This follows from the fact that a group homomorphism $\ZZ \to G$ out of +the [[group of integers]] is uniquely determined by an element of $G$, +and some basic algebra. + +```agda +module _ + (n : Nat) + {ℓ} {G : Group ℓ} (open Group-on (G .snd)) + (x : ⌞ G ⌟) (open pow G x renaming (pow to infixr 30 x^_; pow-hom to x^-)) + (wraps : x^ pos n ≡ unit) + where + + ℤ/-out : Groups.Hom (ℤ/ n) G + ℤ/-out .hom = Coeq-rec (apply x^-) λ (lift a , lift b , n∣a-b) → zero-diff $ + let k , k*n≡a-b = ∣ℤ→fibre n∣a-b in + x^ a — x^ b ≡˘⟨ pres-diff (x^- .preserves) {lift a} {lift b} ⟩ + x^ (a -ℤ b) ≡˘⟨ ap x^_ k*n≡a-b ⟩ + x^ (k *ℤ pos n) ≡⟨ ap x^_ (*ℤ-commutative k (pos n)) ⟩ + x^ (pos n *ℤ k) ≡⟨ pow-* G x (pos n) k ⟩ + pow G ⌜ x^ pos n ⌝ k ≡⟨ ap! wraps ⟩ + pow G unit k ≡⟨ pow-unit G k ⟩ + unit ∎ + ℤ/-out .preserves .pres-⋆ = elim! λ x y → + x^- .preserves .pres-⋆ (lift x) (lift y) +``` + +We can check that $\ZZ/0\ZZ \is \ZZ$: + +```agda +ℤ-ab/0≡ℤ-ab : ∀ {ℓ} → ℤ-ab/ 0 ≡ ℤ-ab {ℓ} +ℤ-ab/0≡ℤ-ab = ∫-Path + (total-hom + (Coeq-rec (λ z → z) (λ (_ , _ , p) → ℤ.zero-diff (ap lift p))) + (record { pres-⋆ = elim! λ _ _ → refl })) + (is-iso→is-equiv (iso inc (λ _ → refl) (elim! λ _ → refl))) + +ℤ/0≡ℤ : ∀ {ℓ} → ℤ/ 0 ≡ ℤ {ℓ} +ℤ/0≡ℤ = Grp→Ab→Grp (ℤ/ 0) (ℤ/n-commutative 0) ∙ ap Abelian→Group ℤ-ab/0≡ℤ-ab +``` + +For positive $n$, we show that $\ZZ/n\ZZ$ is finite; more precisely, +we construct an equivalence $\ZZ/n\ZZ \simeq \NN^{ + +```agda +module Algebra.Group.Instances.Integers where +``` + + + +# The group of integers {defines="integer-group group-of-integers"} + +The fundamental example of an [[abelian group]] is the group of [[**integers**]], $\ZZ$, under +addition. A type-theoretic interjection is necessary: the integers live +on the zeroth universe, so to have an $\ell$-sized group of integers, we +must lift it. + +```agda +ℤ-ab : ∀ {ℓ} → Abelian-group ℓ +ℤ-ab = to-ab mk-ℤ where + open make-abelian-group + mk-ℤ : make-abelian-group (Lift _ Int) + mk-ℤ .ab-is-set = hlevel 2 + mk-ℤ .mul (lift x) (lift y) = lift (x +ℤ y) + mk-ℤ .inv (lift x) = lift (negℤ x) + mk-ℤ .1g = 0 + mk-ℤ .idl (lift x) = ap lift (+ℤ-zerol x) + mk-ℤ .assoc (lift x) (lift y) (lift z) = ap lift (+ℤ-assoc x y z) + mk-ℤ .invl (lift x) = ap lift (+ℤ-invl x) + mk-ℤ .comm (lift x) (lift y) = ap lift (+ℤ-commutative x y) + +ℤ : ∀ {ℓ} → Group ℓ +ℤ = Abelian→Group ℤ-ab +``` + +We show that $\ZZ$ is the [[free group]] on one generator, i.e. the +[[free object]] on $\top$ relative to the forgetful functor from groups +to sets, `Grp↪Sets`{.Agda}. + +We start by defining the [[group homomorphism]] $\ZZ \to G$ that sends +$n$ to $x^n$ (or, in additive notation, $n \cdot x$), where $G$ is a group +and $x$ is an element of $G$, using the [[universal property of the integers]]. + + + +```agda + module pow (x : ⌞ G ⌟) where + pow : Int → ⌞ G ⌟ + pow = ℤ.map-out unit ((_⋆ x) , ⋆-equivr x) + + pow-sucr : ∀ a → pow (sucℤ a) ≡ pow a ⋆ x + pow-sucr = ℤ.map-out-rotate _ _ + + pow-+ : ∀ a b → pow (a +ℤ b) ≡ pow a ⋆ pow b + pow-+ a = ℤ.induction + (ap pow (+ℤ-zeror a) ∙ sym idr) + λ b → + pow (a +ℤ b) ≡ pow a ⋆ pow b ≃⟨ ap (_⋆ x) , equiv→cancellable (⋆-equivr x) ⟩ + pow (a +ℤ b) ⋆ x ≡ (pow a ⋆ pow b) ⋆ x ≃⟨ ∙-post-equiv (sym associative) ⟩ + pow (a +ℤ b) ⋆ x ≡ pow a ⋆ pow b ⋆ x ≃⟨ ∙-post-equiv (ap (pow a ⋆_) (sym (pow-sucr b))) ⟩ + pow (a +ℤ b) ⋆ x ≡ pow a ⋆ pow (sucℤ b) ≃⟨ ∙-pre-equiv (pow-sucr (a +ℤ b)) ⟩ + pow (sucℤ (a +ℤ b)) ≡ pow a ⋆ pow (sucℤ b) ≃⟨ ∙-pre-equiv (ap pow (+ℤ-sucr a b)) ⟩ + pow (a +ℤ sucℤ b) ≡ pow a ⋆ pow (sucℤ b) ≃∎ + + pow-hom : Groups.Hom ℤ G + pow-hom .hom (lift i) = pow i + pow-hom .preserves .pres-⋆ (lift a) (lift b) = pow-+ a b +``` + +This is the unique group homomorphism $\ZZ \to G$ that sends $1$ to $x$. + +```agda + pow-unique : (g : Groups.Hom ℤ G) → g # 1 ≡ x → g ≡ pow-hom + pow-unique g g1≡x = ext $ ℤ.map-out-unique (λ i → g # lift i) + (pres-id (g .preserves)) + λ y → + g # lift ⌜ sucℤ y ⌝ ≡⟨ ap! (sym (+ℤ-oner y)) ⟩ + g # lift (y +ℤ 1) ≡⟨ g .preserves .pres-⋆ (lift y) 1 ⟩ + g # lift y ⋆ g # 1 ≡⟨ ap (g # lift y ⋆_) g1≡x ⟩ + g # lift y ⋆ x ∎ + + open pow public +``` + +
+ +We prove some other useful basic properties of exponentiation. +^[Pedantically, these properties say that `pow`{.Agda} is the unique +*near-ring* homomorphism from $\ZZ$, the [[initial near-ring|initial +ring]], to the near-ring of (pointed) endofunctions of $G$, a generalisation +of [[endomorphism rings]] to non-abelian groups.] + +```agda + pow-sucl : ∀ x a → pow x (sucℤ a) ≡ x ⋆ pow x a + pow-0 : ∀ x → pow x 0 ≡ unit + pow-1 : ∀ x → pow x 1 ≡ x + pow-* : ∀ x a b → pow x (a *ℤ b) ≡ pow (pow x a) b + pow-unit : ∀ n → pow unit n ≡ unit + pow-inverse : ∀ x n → pow (x ⁻¹) n ≡ pow x n ⁻¹ +``` + + +```agda + pow-sucl x a = + pow x (sucℤ a) ≡˘⟨ ap (pow x) (+ℤ-onel a) ⟩ + pow x (1 +ℤ a) ≡⟨ pow-+ x 1 a ⟩ + pow x 1 ⋆ pow x a ≡⟨ ap (_⋆ pow x a) (pow-1 x) ⟩ + x ⋆ pow x a ∎ + + pow-0 x = refl + + pow-1 x = idl + + pow-* x a = ℤ.induction (ap (pow x) (*ℤ-zeror a)) λ b → + pow x (a *ℤ b) ≡ pow (pow x a) b ≃⟨ _ , equiv→cancellable (⋆-equivr _) ⟩ + pow x (a *ℤ b) ⋆ pow x a ≡ pow (pow x a) b ⋆ pow x a ≃⟨ ∙-pre-equiv (pow-+ x (a *ℤ b) a) ⟩ + pow x (a *ℤ b +ℤ a) ≡ pow (pow x a) b ⋆ pow x a ≃⟨ ∙-pre-equiv (ap (pow x) (*ℤ-sucr a b)) ⟩ + pow x (a *ℤ sucℤ b) ≡ pow (pow x a) b ⋆ pow x a ≃⟨ ∙-post-equiv (sym (pow-sucr (pow x a) b)) ⟩ + pow x (a *ℤ sucℤ b) ≡ pow (pow x a) (sucℤ b) ≃∎ + + pow-unit = ℤ.induction refl (λ x → ∙-pre-equiv (pow-sucr unit x ∙ idr)) + + pow-inverse x = ℤ.induction (sym inv-unit) λ n → + pow (x ⁻¹) n ≡ pow x n ⁻¹ ≃⟨ _ , equiv→cancellable (⋆-equivr (x ⁻¹)) ⟩ + pow (x ⁻¹) n ⋆ x ⁻¹ ≡ pow x n ⁻¹ ⋆ x ⁻¹ ≃⟨ ∙-pre-equiv (pow-sucr (x ⁻¹) n) ⟩ + pow (x ⁻¹) (sucℤ n) ≡ pow x n ⁻¹ ⋆ x ⁻¹ ≃⟨ ∙-post-equiv (sym inv-comm) ⟩ + pow (x ⁻¹) (sucℤ n) ≡ (x ⋆ pow x n) ⁻¹ ≃⟨ ∙-post-equiv (ap _⁻¹ (sym (pow-sucl x n))) ⟩ + pow (x ⁻¹) (sucℤ n) ≡ pow x (sucℤ n) ⁻¹ ≃∎ +``` +
+ +Finally, the properties above imply that $\ZZ$ is the free group on +one generator. + +```agda +ℤ-free : Free-object Grp↪Sets (el! ⊤) +ℤ-free .Free-object.free = ℤ +ℤ-free .Free-object.unit _ = 1 +ℤ-free .Free-object.fold {G} x = pow-hom G (x _) +ℤ-free .Free-object.commute {G} {x} = ext λ _ → pow-1 G (x _) +ℤ-free .Free-object.unique {G} {x} g comm = + pow-unique G (x _) g (unext comm _) +``` diff --git a/src/Algebra/Group/Instances/Symmetric.lagda.md b/src/Algebra/Group/Instances/Symmetric.lagda.md new file mode 100644 index 000000000..a3282da7d --- /dev/null +++ b/src/Algebra/Group/Instances/Symmetric.lagda.md @@ -0,0 +1,66 @@ + + +```agda +module Algebra.Group.Instances.Symmetric where +``` + +# Symmetric groups {defines="symmetric-group"} + +If $X$ is a set, then the type of all bijections $X \simeq X$ is also a +set, and it forms the carrier for a [[group]]: The _symmetric group_ on $X$. + +```agda +Sym : ∀ {ℓ} (X : Set ℓ) → Group-on (∣ X ∣ ≃ ∣ X ∣) +Sym X = to-group-on group-str where + open make-group + group-str : make-group (∣ X ∣ ≃ ∣ X ∣) + group-str .mul g f = f ∙e g +``` + +The group operation is `composition of equivalences`{.Agda ident=∙e}; +The identity element is `the identity equivalence`{.Agda ident=id-equiv}. + +```agda + group-str .unit = id , id-equiv +``` + +This type is a set because $X \to X$ is a set (because $X$ is a set by +assumption), and `being an equivalence is a proposition`{.Agdaa +ident=is-equiv-is-prop}. + +```agda + group-str .group-is-set = hlevel 2 +``` + +The associativity and identity laws hold definitionally. + +```agda + group-str .assoc _ _ _ = trivial! + group-str .idl _ = trivial! +``` + +The inverse is given by `the inverse equivalence`{.Agda ident=_e⁻¹}, and +the inverse equations hold by the fact that the inverse of an +equivalence is both a section and a retraction. + +```agda + group-str .inv = _e⁻¹ + group-str .invl (f , eqv) = ext (equiv→unit eqv) +``` + +We write $S_n$ for the symmetric group on the [[standard finite set]] +with $n$ elements. + +```agda +S : Nat → Group lzero +S n = el! (Fin n ≃ Fin n) , Sym (el! (Fin n)) +``` diff --git a/src/Algebra/Group/Semidirect.lagda.md b/src/Algebra/Group/Semidirect.lagda.md index 6c0d43f62..97e1c7e2d 100644 --- a/src/Algebra/Group/Semidirect.lagda.md +++ b/src/Algebra/Group/Semidirect.lagda.md @@ -28,7 +28,7 @@ To motivate the concept, let's consider some examples: - The [[dihedral group]] of order $2n$, $D_n$, which is the group of symmetries of a regular $n$-gon, can be defined as the semidirect product $\ZZ/2\ZZ \ltimes \ZZ/n\ZZ$, where the action of $\ZZ/2\ZZ$ sends $1$ -to the "negation" automorphism of $\ZZ/n\ZZ$. Intuitively, a symmetry +to the [[negation automorphism]] of $\ZZ/n\ZZ$. Intuitively, a symmetry of the regular $n$-gon has two components: a reflection (captured by the cyclic group $\ZZ/2\ZZ$) and a rotation (captured by the cyclic group $\ZZ/n\ZZ$); but when combining two symmetries, a reflection will swap the direction @@ -123,7 +123,7 @@ module _ (A : Group ℓ) (B : Group ℓ) where ```agda Semidirect-trivial : Semidirect-product A B (trivial-action A B) ≡ Direct-product A B - Semidirect-trivial = ∫-Path Groups-equational + Semidirect-trivial = ∫-Path (total-hom (λ x → x) (record { pres-⋆ = λ _ _ → refl })) id-equiv ``` diff --git a/src/Algebra/Group/Subgroup.lagda.md b/src/Algebra/Group/Subgroup.lagda.md index 4138277d9..06d14ac30 100644 --- a/src/Algebra/Group/Subgroup.lagda.md +++ b/src/Algebra/Group/Subgroup.lagda.md @@ -387,6 +387,7 @@ f(yy\inv) = f(1) = 1$$. B.unit ∎ ``` +:::{.definition #normal-subgroup} It turns out that this last property is enough to pick out exactly the kernels amongst the representations of subgroups: If $H$ is closed under conjugation, then $H$ generates an equivalence relation on the set @@ -395,6 +396,7 @@ this equivalence relation with a group structure. The kernel of the quotient map $G \to G/H$ is then $H$. We call a predicate representing a kernel a **normal subgroup**, and we denote this in shorthand by $H \unlhd G$. +::: ```agda record normal-subgroup (G : Group ℓ) (H : ℙ ⌞ G ⌟) : Type ℓ where @@ -495,6 +497,7 @@ rather directly: Group-on-G/H .make-group.invl = elim! λ x → ap Coeq.inc inversel Group-on-G/H .make-group.idl = elim! λ x → ap Coeq.inc idl + infix 25 _/ᴳ_ _/ᴳ_ : Group _ _/ᴳ_ = to-group Group-on-G/H diff --git a/src/Algebra/Magma/Unital.lagda.md b/src/Algebra/Magma/Unital.lagda.md index a291c02aa..758b39ae3 100644 --- a/src/Algebra/Magma/Unital.lagda.md +++ b/src/Algebra/Magma/Unital.lagda.md @@ -142,7 +142,7 @@ record open Unital-magma≃ ``` -* One-sided identities +## One-sided identities Dropping either of the paths involved in a unital magma results in a right identity or a left identity. diff --git a/src/Algebra/Ring.lagda.md b/src/Algebra/Ring.lagda.md index 5221dd515..d3ebbfe8d 100644 --- a/src/Algebra/Ring.lagda.md +++ b/src/Algebra/Ring.lagda.md @@ -2,7 +2,7 @@ ```agda open import Algebra.Group.Cat.Base open import Algebra.Semigroup -open import Algebra.Group.Ab hiding (ℤ) +open import Algebra.Group.Ab open import Algebra.Prelude open import Algebra.Monoid open import Algebra.Group diff --git a/src/Cat/Abelian/Endo.lagda.md b/src/Cat/Abelian/Endo.lagda.md index 758e0ed4d..836d9e33d 100644 --- a/src/Cat/Abelian/Endo.lagda.md +++ b/src/Cat/Abelian/Endo.lagda.md @@ -17,7 +17,7 @@ private module A = Ab-category A ``` --> -# Endomorphism rings +# Endomorphism rings {defines="endomorphism-ring"} Fix an [$\Ab$-category] $\cA$: It can be the category of [[abelian groups]] $\Ab$ itself, for example, or $R$-Mod for your favourite diff --git a/src/Cat/Displayed/Univalence/Thin.lagda.md b/src/Cat/Displayed/Univalence/Thin.lagda.md index 296d07c10..836d8603b 100644 --- a/src/Cat/Displayed/Univalence/Thin.lagda.md +++ b/src/Cat/Displayed/Univalence/Thin.lagda.md @@ -178,7 +178,7 @@ record is-equational {ℓ o' ℓ'} {S : Type ℓ → Type o'} (spec : Thin-struc (Structured-objects-is-category spec) (total-iso ((f #_) , eqv) (f .preserves)) -open is-equational public +open is-equational ⦃ ... ⦄ public ``` diff --git a/src/Data/Fin/Closure.lagda.md b/src/Data/Fin/Closure.lagda.md index 86945a535..126de3e2f 100644 --- a/src/Data/Fin/Closure.lagda.md +++ b/src/Data/Fin/Closure.lagda.md @@ -4,6 +4,7 @@ open import 1Lab.Prelude open import Data.Set.Coequaliser open import Data.Fin.Properties +open import Data.Nat.Prime open import Data.Fin.Base open import Data.Dec open import Data.Sum @@ -135,7 +136,7 @@ Finite-multiply {n} {m} = sum≡* (suc n) m = ap (m +_) (sum≡* n m) ``` -## Products +### Products Similarly to the case for sums, the cardinality of a dependent *product* of finite sets is the `product`{.Agda} of the cardinalities: @@ -158,6 +159,53 @@ Finite-product {suc n} B = Fin (B fzero * product n (B ∘ fsuc)) ≃∎ ``` +## Permutations + +We show that the set of permutations $[n] \simeq [n]$ is finite with +cardinality $n!$ (the `factorial`{.Agda} of $n$). + +We start by showing that $([n+1] \simeq [n+1]) \simeq [n+1] \times +([n] \simeq [n])$: a permutation of $[n+1]$ is determined by what happens +to $0$ and by the remaining permutation of $[n]$. + +```agda +Fin-permutations-suc + : ∀ n → (Fin (suc n) ≃ Fin (suc n)) ≃ (Fin (suc n) × (Fin n ≃ Fin n)) +Fin-permutations-suc n = to , is-iso→is-equiv is where + to : (Fin (suc n) ≃ Fin (suc n)) → Fin (suc n) × (Fin n ≃ Fin n) + to e .fst = e # 0 + to e .snd .fst i = avoid (e # 0) (e # (fsuc i)) λ p → + fzero≠fsuc (Equiv.injective e p) + to e .snd .snd = Fin-injection→equiv _ λ p → + fsuc-inj (Equiv.injective e (avoid-injective (e # 0) p)) + + is : is-iso to + is .is-iso.inv (n , e) .fst fzero = n + is .is-iso.inv (n , e) .fst (fsuc x) = skip n (e # x) + is .is-iso.inv (n , e) .snd = Fin-injection→equiv _ λ where + {fzero} {fzero} p → refl + {fzero} {fsuc y} p → absurd (skip-skips n _ (sym p)) + {fsuc x} {fzero} p → absurd (skip-skips n _ p) + {fsuc x} {fsuc y} p → ap fsuc (Equiv.injective e (skip-injective n _ _ p)) + is .is-iso.rinv (n , e) = Σ-pathp refl (ext λ i → avoid-skip n (e # i)) + is .is-iso.linv e = ext λ where + fzero → refl + (fsuc i) → skip-avoid (e # 0) (e # (fsuc i)) +``` + +We can now show that $([n] \simeq [n]) \simeq [n!]$ by induction. + +```agda +Fin-permutations : ∀ n → (Fin n ≃ Fin n) ≃ Fin (factorial n) +Fin-permutations zero = is-contr→≃ + (contr id≃ λ _ → ext λ ()) Finite-one-is-contr +Fin-permutations (suc n) = + Fin (suc n) ≃ Fin (suc n) ≃⟨ Fin-permutations-suc n ⟩ + Fin (suc n) × (Fin n ≃ Fin n) ≃⟨ Σ-ap-snd (λ _ → Fin-permutations n) ⟩ + Fin (suc n) × Fin (factorial n) ≃⟨ Finite-multiply ⟩ + Fin (factorial (suc n)) ≃∎ +``` + ## Decidable subsets Given a [[decidable]] predicate on $[n]$, we can compute $s$ such that diff --git a/src/Data/Fin/Finite.lagda.md b/src/Data/Fin/Finite.lagda.md index 3b296c199..ad90bcc1d 100644 --- a/src/Data/Fin/Finite.lagda.md +++ b/src/Data/Fin/Finite.lagda.md @@ -242,7 +242,9 @@ Finite-Σ {A = A} {P = P} ⦃ afin ⦄ ⦃ pfin ⦄ = ∥-∥-out! do Finite-⊥ = fin (inc (Finite-zero-is-initial e⁻¹)) Finite-⊤ = fin (inc (is-contr→≃⊤ Finite-one-is-contr e⁻¹)) -Finite-Bool = fin (inc (Iso→Equiv enum)) where + +Bool≃Fin2 : Bool ≃ Fin 2 +Bool≃Fin2 = Iso→Equiv enum where enum : Iso Bool (Fin 2) enum .fst false = 0 enum .fst true = 1 @@ -253,6 +255,8 @@ Finite-Bool = fin (inc (Iso→Equiv enum)) where enum .snd .is-iso.linv true = refl enum .snd .is-iso.linv false = refl +Finite-Bool = fin (inc Bool≃Fin2) + Finite-PathP = subst Finite (sym (PathP≡Path _ _ _)) (Discrete→Finite≡ Finite→Discrete) Finite-Lift = Finite-≃ (Lift-≃ e⁻¹) diff --git a/src/Data/Fin/Properties.lagda.md b/src/Data/Fin/Properties.lagda.md index e9e37fed9..fbdc8a807 100644 --- a/src/Data/Fin/Properties.lagda.md +++ b/src/Data/Fin/Properties.lagda.md @@ -178,6 +178,38 @@ avoid-injective {suc n} (fsuc i) {fzero} {fsuc k} p = absurd (fzero≠fsuc p) avoid-injective {suc n} (fsuc i) {fsuc j} {fzero} p = absurd (fzero≠fsuc (sym p)) avoid-injective {suc n} (fsuc i) {fsuc j} {fsuc k} p = ap fsuc (avoid-injective {n} i {j} {k} (fsuc-inj p)) + +skip-injective + : ∀ {n} (i : Fin (suc n)) (j k : Fin n) + → skip i j ≡ skip i k → j ≡ k +skip-injective fzero j k p = fsuc-inj p +skip-injective (fsuc i) fzero fzero p = refl +skip-injective (fsuc i) fzero (fsuc k) p = absurd (fzero≠fsuc p) +skip-injective (fsuc i) (fsuc j) fzero p = absurd (fzero≠fsuc (sym p)) +skip-injective (fsuc i) (fsuc j) (fsuc k) p = ap fsuc (skip-injective i j k (fsuc-inj p)) + +skip-skips + : ∀ {n} (i : Fin (suc n)) (j : Fin n) + → skip i j ≠ i +skip-skips fzero j p = fzero≠fsuc (sym p) +skip-skips (fsuc i) fzero p = fzero≠fsuc p +skip-skips (fsuc i) (fsuc j) p = skip-skips i j (fsuc-inj p) + +avoid-skip + : ∀ {n} (i : Fin (suc n)) (j : Fin n) {neq : i ≠ skip i j} + → avoid i (skip i j) neq ≡ j +avoid-skip fzero fzero = refl +avoid-skip fzero (fsuc j) = refl +avoid-skip (fsuc i) fzero = refl +avoid-skip (fsuc i) (fsuc j) = ap fsuc (avoid-skip i j) + +skip-avoid + : ∀ {n} (i : Fin (suc n)) (j : Fin (suc n)) {i≠j : i ≠ j} + → skip i (avoid i j i≠j) ≡ j +skip-avoid fzero fzero {i≠j} = absurd (i≠j refl) +skip-avoid {suc n} fzero (fsuc j) = refl +skip-avoid {suc n} (fsuc i) fzero = refl +skip-avoid {suc n} (fsuc i) (fsuc j) = ap fsuc (skip-avoid i j) ``` ## Iterated products and sums {defines="iterated-products"} diff --git a/src/Data/Int/Base.lagda.md b/src/Data/Int/Base.lagda.md index 183856700..157aa2073 100644 --- a/src/Data/Int/Base.lagda.md +++ b/src/Data/Int/Base.lagda.md @@ -15,14 +15,14 @@ open import Data.Nat.Base module Data.Int.Base where ``` -# The integers {defines=integers} +# The integers {defines=integer} The familiar [[set]] of integers, in addition to its intuitive characterisation in terms of positive and negative numbers, can be specified by a wide variety of universal properties: - The set of integers, with the operation of addition, is the [[free -group]] on one generator. +group]] on one generator (see the [[group of integers]]). - The set of integers, with the operations of addition and multiplication, is the [[initial ring]]. @@ -255,6 +255,13 @@ natural numbers. If the numbers have mismatched sign, then the addition function is actually computing a difference, and we already know how to compute differences. + + ```agda _+ℤ_ : Int → Int → Int pos x +ℤ pos y = pos (x + y) diff --git a/src/Data/Int/DivMod.lagda.md b/src/Data/Int/DivMod.lagda.md new file mode 100644 index 000000000..779c248d6 --- /dev/null +++ b/src/Data/Int/DivMod.lagda.md @@ -0,0 +1,231 @@ + + +```agda +module Data.Int.DivMod where +``` + + + +# Integer division {defines="integer-division"} + +We define the division $a/b$ where $a$ is an [[integer]] and $b$ is +a positive [[natural number]]. + +```agda +record DivModℤ (a : Int) (b : Nat) : Type where + constructor divmodℤ + + field + quotℤ : Int + remℤ : Nat + .quotient : a ≡ quotℤ *ℤ pos b +ℤ pos remℤ + .smaller : remℤ < b + +open DivModℤ +``` + +In order to compute integer division, we reuse [[natural division]]. +We proceed by cases: if $a$ is positive, we can simply compute the +division $a/b$ as natural numbers. + +```agda +divide-posℤ : ∀ a b → .⦃ _ : Positive b ⦄ → DivModℤ a b +divide-posℤ (pos a) b using divmod q r p s ← divide-pos a b + = divmodℤ (pos q) r (ap pos p ∙ sym (ap (_+ℤ pos r) (assign-pos _))) s +``` + +If $a$ is negative, we can compute $(-a)/b$ as natural numbers and +distinguish two cases: if the remainder is $0$, then $b$ divides $a$, +so we simply negate the quotient and set the remainder to $0$. + +```agda +divide-posℤ (negsuc a) b@(suc b') with divide-pos (suc a) b +... | divmod q zero p s = divmodℤ (assign neg q) 0 + (ap (assign neg) p ∙ assign-+ (q * b) 0 ∙ ap (_+ℤ 0) (assign-*l q b)) + (s≤s 0≤x) +``` + +If the remainder is non-zero, we have to correct for the fact that +integer division as we've defined it rounds towards $-\infty$, while +natural division rounds towards $0$ (hence towards $+\infty$, for +negative numbers), so we take $-((-a)/b) - 1$ as the quotient and +$b - (-a)\%b$ as the remainder. + +```agda +... | divmod q (suc r) p s = divmodℤ (negsuc q) (b - suc r) + (ap (assign neg) p ∙ lemma) + (s≤s (monus-≤ b' r)) +``` + +
+One annoying lemma later, we are done. + +```agda + where + lemma : assign neg (q * b + suc r) ≡ pos (b' - r) +ℤ negsuc (b' + q * b) + lemma = + assign neg (q * b + suc r) ≡⟨ ap (assign neg) (+-commutative (q * b) _) ⟩ + negsuc (r + q * b) ≡˘⟨ negℤ-+ℤ-negsuc r (q * b) ⟩ + negℤ (pos r) +ℤ negsuc (q * b) ≡⟨ ap (_+ℤ negsuc (q * b)) (ap Lift.lower (ℤ.insertl {h = lift (negℤ (pos b'))} (ap lift (+ℤ-invl (pos b'))) {f = lift (negℤ (pos r))})) ⟩ + ⌜ negℤ (pos b') ⌝ +ℤ (pos b' -ℤ pos r) +ℤ negsuc (q * b) ≡˘⟨ ap¡ (assign-neg b') ⟩ + assign neg b' +ℤ (pos b' -ℤ pos r) +ℤ negsuc (q * b) ≡⟨ ap (_+ℤ negsuc (q * b)) (+ℤ-commutative (assign neg b') (pos b' -ℤ pos r)) ⟩ + (pos b' -ℤ pos r) +ℤ assign neg b' +ℤ negsuc (q * b) ≡˘⟨ +ℤ-assoc (pos b' -ℤ pos r) _ _ ⟩ + (pos b' -ℤ pos r) +ℤ (assign neg b' +ℤ negsuc (q * b)) ≡⟨ ap₂ _+ℤ_ (pos-pos b' r) (ap (_+ℤ negsuc (q * b)) (assign-neg b')) ⟩ + (b' ℕ- r) +ℤ (negℤ (pos b') +ℤ negsuc (q * b)) ≡⟨ ap ((b' ℕ- r) +ℤ_) (negℤ-+ℤ-negsuc b' (q * b)) ⟩ + (b' ℕ- r) +ℤ negsuc (b' + q * b) ≡⟨ ap₂ _+ℤ_ (nat-diff-monus b' r (≤-peel (<-weaken (recover s)))) refl ⟩ + pos (b' - r) +ℤ negsuc (b' + q * b) ∎ +``` +
+ +```agda +_/ℤ_ : Int → (b : Nat) → .⦃ _ : Positive b ⦄ → Int +a /ℤ b = divide-posℤ a b .quotℤ + +_%ℤ_ : Int → (b : Nat) → .⦃ _ : Positive b ⦄ → Nat +a %ℤ b = divide-posℤ a b .remℤ + +is-divmodℤ : ∀ x y → .⦃ _ : Positive y ⦄ → x ≡ (x /ℤ y) *ℤ pos y +ℤ pos (x %ℤ y) +is-divmodℤ x (suc y) with divide-posℤ x (suc y) +... | divmodℤ q r α β = recover α + +x%ℤy + +```agda +module Data.Int.Divisible where +``` + +# Divisibility of integers {defines="divisibility-of-integers"} + +We define what it means for an [[integer]] to be [[divisible]] by a +natural number, as a straightforward generalisation of the case for +natural numbers. + +```agda +_∣ℤ_ : Nat → Int → Type +zero ∣ℤ y = y ≡ 0 +suc x ∣ℤ y = fibre (_*ℤ possuc x) y + +infix 7 _∣ℤ_ + +∣ℤ-is-prop : ∀ x y → is-prop (x ∣ℤ y) +∣ℤ-is-prop zero y n k = prop! +∣ℤ-is-prop (suc x) y (n , p) (n' , q) = Σ-prop-path! (*ℤ-injectiver-possuc x n n' (p ∙ sym q)) + +∣ℤ-is-truncation : ∀ {x y} → (x ∣ℤ y) ≃ ∥ fibre (_*ℤ pos x) y ∥ +∣ℤ-is-truncation {zero} {y} = + prop-ext! + (λ p → inc (y , *ℤ-zeror y ∙ sym p)) + (rec! λ x p → sym p ∙ *ℤ-zeror x ) +∣ℤ-is-truncation {suc x} {y} = Equiv.to is-prop≃equiv∥-∥ (∣ℤ-is-prop (suc x) y) + +∣ℤ→fibre : ∀ {x y} → x ∣ℤ y → fibre (_*ℤ pos x) y +∣ℤ→fibre {zero} wit = 0 , sym wit +∣ℤ→fibre {suc x} wit = wit + +fibre→∣ℤ : ∀ {x y} → fibre (_*ℤ pos x) y → x ∣ℤ y +fibre→∣ℤ f = Equiv.from ∣ℤ-is-truncation (inc f) + +dividesℤ : ∀ {x y} (q : Int) → q *ℤ pos x ≡ y → x ∣ℤ y +dividesℤ x p = fibre→∣ℤ (x , p) + +∣ℤ-zero : ∀ {x} → x ∣ℤ 0 +∣ℤ-zero = dividesℤ 0 refl + +∣ℤ-one : ∀ {x} → 1 ∣ℤ x +∣ℤ-one {x} = dividesℤ x (*ℤ-oner x) + +m∣ℤsn→m≤sn : ∀ {x y} → ¬ (y ≡ 0) → x ∣ℤ y → x Nat.≤ abs y +m∣ℤsn→m≤sn {x} {y} nz p with ∣ℤ→fibre p +... | posz , p = absurd (nz (sym p)) +... | possuc k , p = difference→≤ (k * x) + (ap abs (sym (assign-pos (x + k * x))) ∙ ap abs p) +... | negsuc k , p = difference→≤ (k * x) + (sym (abs-negℤ (pos (x + k * x))) ∙ ap abs (sym (assign-neg (x + k * x))) ∙ ap abs p) + +∣ℤ-+ : ∀ {k n m} → k ∣ℤ n → k ∣ℤ m → k ∣ℤ (n +ℤ m) +∣ℤ-+ {zero} {n} {m} p q = ap₂ _+ℤ_ p q +∣ℤ-+ {suc k} (x , p) (y , q) = x +ℤ y , *ℤ-distribr (possuc k) x y ∙ ap₂ _+ℤ_ p q + +∣ℤ-negℤ : ∀ {k n} → k ∣ℤ n → k ∣ℤ negℤ n +∣ℤ-negℤ {zero} d = ap negℤ d +∣ℤ-negℤ {suc k} (x , p) = negℤ x , *ℤ-negl x _ ∙ ap negℤ p +``` diff --git a/src/Data/Int/Properties.lagda.md b/src/Data/Int/Properties.lagda.md index 07ce298fb..81b827501 100644 --- a/src/Data/Int/Properties.lagda.md +++ b/src/Data/Int/Properties.lagda.md @@ -4,6 +4,7 @@ open import 1Lab.Prelude open import Data.Nat.Properties open import Data.Nat.Solver +open import Data.Nat.Order open import Data.Int.Base open import Data.Nat.Base ``` @@ -32,6 +33,11 @@ no further comments. nat-diff-zero zero = refl nat-diff-zero (suc x) = nat-diff-zero x + nat-diff-positive : ∀ a b → a ℕ- b ≡ 0 → a ≡ b + nat-diff-positive a zero p = pos-injective p + nat-diff-positive zero (suc b) p = absurd (negsuc≠pos p) + nat-diff-positive (suc a) (suc b) p = ap suc (nat-diff-positive a b p) + sucℤ-nat-diff : ∀ x y → sucℤ (x ℕ- y) ≡ suc x ℕ- y sucℤ-nat-diff zero zero = refl sucℤ-nat-diff zero (suc zero) = refl @@ -44,6 +50,16 @@ no further comments. predℤ-nat-diff zero (suc y) = refl predℤ-nat-diff (suc x) zero = refl predℤ-nat-diff (suc x) (suc y) = predℤ-nat-diff x y + + nat-diff-monus : ∀ x y → y ≤ x → x ℕ- y ≡ pos (x - y) + nat-diff-monus x y 0≤x = refl + nat-diff-monus (suc x) (suc zero) (s≤s y≤x) = refl + nat-diff-monus (suc x) (suc (suc y)) (s≤s y≤x) = nat-diff-monus x (suc y) y≤x + + nat-diff-bounded : ∀ a b c → a ≤ c → b ≤ c → abs (a ℕ- b) ≤ c + nat-diff-bounded a zero c ac bc = ac + nat-diff-bounded zero (suc b) c ac bc = bc + nat-diff-bounded (suc a) (suc b) c ac bc = nat-diff-bounded a b c (<-weaken ac) (<-weaken bc) ``` ## Negations @@ -92,6 +108,19 @@ no further comments. negℤ-distrib-min (negsuc x) (negsuc y) = refl ``` +## Absolute value + +```agda + abs-positive : ∀ x → abs x ≡ 0 → x ≡ 0 + abs-positive (pos x) p = ap pos p + abs-positive (negsuc x) p = absurd (suc≠zero p) + + abs-negℤ : ∀ z → abs (negℤ z) ≡ abs z + abs-negℤ (posz) = refl + abs-negℤ (possuc _) = refl + abs-negℤ (negsuc _) = refl +``` + ## Rotations ```agda @@ -201,6 +230,12 @@ no further comments. +ℤ-predr : ∀ x y → x +ℤ predℤ y ≡ predℤ (x +ℤ y) +ℤ-predr x y = +ℤ-commutative x (predℤ y) ·· +ℤ-predl y x ·· ap predℤ (+ℤ-commutative y x) + +ℤ-onel : ∀ x → 1 +ℤ x ≡ sucℤ x + +ℤ-onel x = +ℤ-sucl 0 x ∙ ap sucℤ (+ℤ-zerol x) + + +ℤ-oner : ∀ x → x +ℤ 1 ≡ sucℤ x + +ℤ-oner x = +ℤ-sucr x 0 ∙ ap sucℤ (+ℤ-zeror x) + +ℤ-injectiver : ∀ k x y → k +ℤ x ≡ k +ℤ y → x ≡ y +ℤ-injectiver k x y p = sym (+ℤ-zerol x) @@ -220,6 +255,39 @@ no further comments. ap negℤ (rot-is-add x y) ·· negℤ-distrib-rot x y ·· sym (rot-is-add (negℤ x) (negℤ y)) + + negℤ-+ℤ-negsuc : ∀ a b → negℤ (pos a) +ℤ negsuc b ≡ negsuc (a + b) + negℤ-+ℤ-negsuc a b = + +ℤ-commutative (negℤ (pos a)) (negsuc b) + ·· sym (negℤ-distrib (possuc b) (pos a)) + ·· ap negsuc (+-commutative b a) + + pos-pos : ∀ a b → pos a -ℤ pos b ≡ a ℕ- b + pos-pos a zero = +ℤ-zeror _ + pos-pos a (suc b) = refl + + -ℤ-swapl : ∀ a b c → a +ℤ b ≡ c → a ≡ c -ℤ b + -ℤ-swapl a b c p = + sym (+ℤ-zeror _) + ∙ ap (a +ℤ_) (sym (+ℤ-invr b)) + ·· +ℤ-assoc a _ _ + ·· ap (_+ℤ negℤ b) p + + private + distrib-lemma + : ∀ x y z w → (x +ℤ y) +ℤ (z +ℤ w) ≡ (x +ℤ z) +ℤ (y +ℤ w) + distrib-lemma x y z w = + +ℤ-assoc (x +ℤ y) z w + ·· ap (_+ℤ w) (sym (+ℤ-assoc x y z) ·· ap (x +ℤ_) (+ℤ-commutative y z) ·· +ℤ-assoc x z y) + ·· sym (+ℤ-assoc (x +ℤ z) y w) + + -ℤ-cancelr : ∀ k x y → (x +ℤ k) -ℤ (y +ℤ k) ≡ x -ℤ y + -ℤ-cancelr k x y = + (x +ℤ k) -ℤ (y +ℤ k) ≡⟨ ap ((x +ℤ k) +ℤ_) (negℤ-distrib y k) ⟩ + (x +ℤ k) +ℤ (negℤ y -ℤ k) ≡⟨ distrib-lemma x k (negℤ y) (negℤ k) ⟩ + (x -ℤ y) +ℤ (k -ℤ k) ≡⟨ ap ((x -ℤ y) +ℤ_) (+ℤ-invr k) ⟩ + (x -ℤ y) +ℤ 0 ≡⟨ +ℤ-zeror (x -ℤ y) ⟩ + x -ℤ y ∎ ``` ## Multiplication @@ -229,6 +297,28 @@ no further comments. assign-pos zero = refl assign-pos (suc x) = refl + assign-neg : ∀ x → assign neg x ≡ negℤ (pos x) + assign-neg zero = refl + assign-neg (suc x) = refl + + neg-sign : Sign → Sign + neg-sign pos = neg + neg-sign neg = pos + + neg-assign : ∀ {s} x → assign (neg-sign s) x ≡ negℤ (assign s x) + neg-assign {pos} zero = refl + neg-assign {pos} (suc x) = refl + neg-assign {neg} zero = refl + neg-assign {neg} (suc x) = refl + + assign-+ : ∀ {s} x y → assign s (x + y) ≡ assign s x +ℤ assign s y + assign-+ {pos} zero y = sym (+ℤ-zerol _) + assign-+ {pos} (suc x) zero = refl + assign-+ {pos} (suc x) (suc y) = refl + assign-+ {neg} zero y = sym (+ℤ-zerol _) + assign-+ {neg} (suc x) zero = ap negsuc (+-zeror _) + assign-+ {neg} (suc x) (suc y) = ap negsuc (+-sucr _ _) + *ℤ-onel : ∀ x → 1 *ℤ x ≡ x *ℤ-onel (pos x) = ap (assign pos) (+-zeror x) ∙ assign-pos x *ℤ-onel (negsuc x) = ap negsuc (+-zeror x) @@ -245,6 +335,21 @@ no further comments. *ℤ-zeror (pos x) = ap (assign pos) (*-zeror x) *ℤ-zeror (negsuc x) = ap (assign neg) (*-zeror x) + assign-*l : ∀ {s} x y → assign s (x * y) ≡ assign s x *ℤ pos y + assign-*l {pos} zero y = sym (*ℤ-zerol (pos y)) + assign-*l {pos} (suc x) y = refl + assign-*l {neg} zero y = refl + assign-*l {neg} (suc x) y = refl + + *ℤ-negl : ∀ x y → negℤ x *ℤ y ≡ negℤ (x *ℤ y) + *ℤ-negl posz y = refl + *ℤ-negl (possuc x) y with sign y + ... | pos = neg-assign (suc x * abs y) + ... | neg = neg-assign (suc x * abs y) + *ℤ-negl (negsuc x) y with sign y + ... | pos = neg-assign (suc x * abs y) + ... | neg = neg-assign (suc x * abs y) + private lemma : ∀ x y z → z + y * suc z + x * suc (z + y * suc z) ≡ z + (y + x * suc y) * suc z lemma x y z = nat! @@ -307,14 +412,6 @@ no further comments. dot-is-mul (negsuc zero) (negsuc x) = ap possuc (sym (+-zeror x)) dot-is-mul (negsuc (suc x)) y = sym (*ℤ-negsucl x y ∙ ap (negℤ y +ℤ_) (sym (dot-is-mul (negsuc x) y))) - private - distrib-lemma - : ∀ x y z w → (x +ℤ y) +ℤ (z +ℤ w) ≡ (x +ℤ z) +ℤ (y +ℤ w) - distrib-lemma x y z w = - +ℤ-assoc (x +ℤ y) z w - ·· ap (_+ℤ w) (sym (+ℤ-assoc x y z) ·· ap (x +ℤ_) (+ℤ-commutative y z) ·· +ℤ-assoc x z y) - ·· sym (+ℤ-assoc (x +ℤ z) y w) - dot-distribr : ∀ x y z → dotℤ z (x +ℤ y) ≡ (dotℤ z x) +ℤ (dotℤ z y) dot-distribr x y posz = refl dot-distribr x y (possuc z) = @@ -336,4 +433,22 @@ no further comments. *ℤ-commutative (y +ℤ z) x ·· *ℤ-distribl x y z ·· ap₂ _+ℤ_ (*ℤ-commutative x y) (*ℤ-commutative x z) + + *ℤ-distribr-minus : ∀ x y z → (y -ℤ z) *ℤ x ≡ (y *ℤ x) -ℤ (z *ℤ x) + *ℤ-distribr-minus x y z = *ℤ-distribr x y (negℤ z) ∙ ap (y *ℤ x +ℤ_) (*ℤ-negl z x) + + *ℤ-sucr : ∀ x y → x *ℤ sucℤ y ≡ x *ℤ y +ℤ x + *ℤ-sucr x y = + x *ℤ sucℤ y ≡˘⟨ ap (x *ℤ_) (+ℤ-oner y) ⟩ + x *ℤ (y +ℤ 1) ≡⟨ *ℤ-distribl x y 1 ⟩ + x *ℤ y +ℤ x *ℤ 1 ≡⟨ ap (x *ℤ y +ℤ_) (*ℤ-oner x) ⟩ + x *ℤ y +ℤ x ∎ + + *ℤ-injectiver-possuc : ∀ k x y → x *ℤ possuc k ≡ y *ℤ possuc k → x ≡ y + *ℤ-injectiver-possuc k (pos x) (pos y) p = + ap pos (*-suc-inj k x y (pos-injective (sym (assign-pos _) ·· p ·· assign-pos _))) + *ℤ-injectiver-possuc k (pos x) (negsuc y) p = absurd (pos≠negsuc (sym (assign-pos (x * suc k)) ∙ p)) + *ℤ-injectiver-possuc k (negsuc x) (pos y) p = absurd (negsuc≠pos (p ∙ assign-pos (y * suc k))) + *ℤ-injectiver-possuc k (negsuc x) (negsuc y) p = + ap (assign neg) (*-suc-inj k (suc x) (suc y) (ap suc (negsuc-injective p))) ``` diff --git a/src/Data/Int/Universal.lagda.md b/src/Data/Int/Universal.lagda.md index 101e542a7..c5526e175 100644 --- a/src/Data/Int/Universal.lagda.md +++ b/src/Data/Int/Universal.lagda.md @@ -13,7 +13,7 @@ import Data.Int.HIT as HIT module Data.Int.Universal where ``` -# Universal property of the integers +# Universal property of the integers {defines="universal-property-of-the-integers"} We define and prove a type-theoretic universal property of the integers, which characterises them as the initial pointed set equipped with an diff --git a/src/Data/Nat/DivMod.lagda.md b/src/Data/Nat/DivMod.lagda.md index 6009ce464..8f3e67959 100644 --- a/src/Data/Nat/DivMod.lagda.md +++ b/src/Data/Nat/DivMod.lagda.md @@ -16,7 +16,7 @@ open import Data.Sum.Base module Data.Nat.DivMod where ``` -# Natural division +# Natural division {defines="natural-division"} This module implements the basics of the theory of **division** (not [divisibility], see there) for the natural numbers. In particular, we @@ -160,6 +160,8 @@ d1 /ₙ suc d2 = div-helper 0 d2 d1 d2 _%_ : (d1 d2 : Nat) .⦃ _ : Positive d2 ⦄ → Nat d1 % suc d2 = mod-helper 0 d2 d1 d2 +infixl 9 _/ₙ_ _%_ + abstract private div-mod-lemma : ∀ am ad d n → am + ad * suc (am + n) + d ≡ mod-helper am (am + n) d n + div-helper ad (am + n) d n * suc (am + n) diff --git a/src/Data/Nat/Divisible.lagda.md b/src/Data/Nat/Divisible.lagda.md index b6fefa833..266ae70b5 100644 --- a/src/Data/Nat/Divisible.lagda.md +++ b/src/Data/Nat/Divisible.lagda.md @@ -14,7 +14,7 @@ open import Data.Sum.Base module Data.Nat.Divisible where ``` -# Divisibility {defines="divisibility"} +# Divisibility of natural numbers {defines="divisibility divisible"} In the natural numbers, **divisibility**[^divide] is the property expressing that a given number can be expressed as a multiple of @@ -176,7 +176,7 @@ The only number that divides 1 is 1 itself: ∣-1 {suc (suc n)} (k , p) = *-is-oner k (2 + n) p ``` -## Even and odd numbers +## Even and odd natural numbers A number is **even** if it is divisible by 2, and **odd** otherwise. Note that a number is odd if and only if its successor is even; we take this diff --git a/src/Data/Nat/Properties.lagda.md b/src/Data/Nat/Properties.lagda.md index 71a2563d0..a4b941330 100644 --- a/src/Data/Nat/Properties.lagda.md +++ b/src/Data/Nat/Properties.lagda.md @@ -198,6 +198,11 @@ arithmetic operators: +-≤r x zero = 0≤x +-≤r x (suc y) = subst (λ p → suc y ≤ p) (sym (+-sucr x y)) (s≤s (+-≤r x y)) +monus-≤ : (x y : Nat) → x - y ≤ x +monus-≤ x zero = x≤x +monus-≤ zero (suc y) = 0≤x +monus-≤ (suc x) (suc y) = ≤-sucr (monus-≤ x y) + +-preserves-≤l : (x y z : Nat) → x ≤ y → (z + x) ≤ (z + y) +-preserves-≤l .0 y zero 0≤x = 0≤x +-preserves-≤l .0 y (suc z) 0≤x = diff --git a/src/Data/Set/Coequaliser.lagda.md b/src/Data/Set/Coequaliser.lagda.md index 2e20a318f..c50a763da 100644 --- a/src/Data/Set/Coequaliser.lagda.md +++ b/src/Data/Set/Coequaliser.lagda.md @@ -132,6 +132,10 @@ instance elim! (happly (sf .idsᵉ .to-path h)) Extensional-coeq-map ⦃ sf ⦄ .idsᵉ .to-path-over p = is-prop→pathp (λ i → Pathᵉ-is-hlevel 1 sf (hlevel 2)) _ _ + + Number-Coeq : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → ⦃ Number B ⦄ → {f g : A → B} → Number (Coeq f g) + Number-Coeq {ℓ = ℓ} ⦃ b ⦄ .Number.Constraint n = Lift ℓ (b .Number.Constraint n) + Number-Coeq ⦃ b ⦄ .Number.fromNat n ⦃ lift c ⦄ = inc (b .Number.fromNat n ⦃ c ⦄) ``` --> diff --git a/src/Homotopy/Space/Circle.lagda.md b/src/Homotopy/Space/Circle.lagda.md index b8d22cdc6..a582f8134 100644 --- a/src/Homotopy/Space/Circle.lagda.md +++ b/src/Homotopy/Space/Circle.lagda.md @@ -4,9 +4,9 @@ open import 1Lab.Path.Reasoning open import 1Lab.Prelude open import Algebra.Group.Cat.FinitelyComplete +open import Algebra.Group.Instances.Integers open import Algebra.Group.Cat.Base open import Algebra.Group.Homotopy -open import Algebra.Group.Ab open import Algebra.Group open import Data.Set.Truncation @@ -299,7 +299,7 @@ loopⁿ-+ a = Integers.induction Int-integers loopⁿ (a +ℤ sucℤ b) ≡ loopⁿ a ∙ loopⁿ (sucℤ b) ≃∎ π₁S¹≡ℤ : π₁Groupoid.π₁ S¹∙ S¹-is-groupoid ≡ ℤ -π₁S¹≡ℤ = sym $ ∫-Path Groups-equational +π₁S¹≡ℤ = sym $ ∫-Path (total-hom (Equiv.from ΩS¹≃integers ∘ Lift.lower) (record { pres-⋆ = λ (lift a) (lift b) → loopⁿ-+ a b })) (∙-is-equiv (Lift-≃ .snd) ((ΩS¹≃integers e⁻¹) .snd)) @@ -314,7 +314,7 @@ get that all of its higher homotopy groups are trivial. Ωⁿ⁺²S¹-is-contr (suc n) = Path-is-hlevel 0 (Ωⁿ⁺²S¹-is-contr n) πₙ₊₂S¹≡0 : ∀ n → πₙ₊₁ (suc n) S¹∙ ≡ Zero-group {lzero} -πₙ₊₂S¹≡0 n = ∫-Path Groups-equational +πₙ₊₂S¹≡0 n = ∫-Path (Zero-group-is-terminal _ .centre) (is-contr→≃ (is-contr→∥-∥₀-is-contr (Ωⁿ⁺²S¹-is-contr n)) (hlevel 0) .snd) ``` diff --git a/src/Homotopy/Space/Delooping.lagda.md b/src/Homotopy/Space/Delooping.lagda.md index 6a7314322..fc218d3e1 100644 --- a/src/Homotopy/Space/Delooping.lagda.md +++ b/src/Homotopy/Space/Delooping.lagda.md @@ -284,7 +284,7 @@ group of `Deloop`{.Agda} is `G`, which is what we wanted. G≃ΩB = Iso→Equiv (decode base , iso (encode base) encode→decode (decode→encode base)) G≡π₁B : G ≡ πₙ₊₁ 0 (Deloop , base) - G≡π₁B = ∫-Path Groups-equational + G≡π₁B = ∫-Path (total-hom (λ x → inc (path x)) record { pres-⋆ = λ x y → ap ∥_∥₀.inc (path-∙ _ _) }) (∙-is-equiv (G≃ΩB .snd) (∥-∥₀-idempotent (squash base base))) From 59e14d562018a3ed5b3da2dd9cd6a197d71505d3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Na=C3=AFm=20Favier?= Date: Fri, 23 Aug 2024 23:51:39 +0200 Subject: [PATCH 5/9] def: dihedral groups --- src/Algebra/Group/Ab.lagda.md | 21 ++++ src/Algebra/Group/Instances/Dihedral.lagda.md | 105 ++++++++++++++++++ 2 files changed, 126 insertions(+) create mode 100644 src/Algebra/Group/Instances/Dihedral.lagda.md diff --git a/src/Algebra/Group/Ab.lagda.md b/src/Algebra/Group/Ab.lagda.md index 5dae93045..e0c3af059 100644 --- a/src/Algebra/Group/Ab.lagda.md +++ b/src/Algebra/Group/Ab.lagda.md @@ -216,3 +216,24 @@ Ab↪Sets = Grp↪Sets F∘ Ab↪Grp --> The fundamental example of an abelian group is the [[group of integers]]. + +:::{.definition #negation-automorphism} +Given an abelian group $G$, we can define the **negation automorphism** +$G \cong G$ which inverts every element: since the group operation is +commutative, we have $(x \star y)^{-1} = y^{-1} \star x^{-1} = x^{-1} +\star y^{-1}$, so this is a homomorphism. +::: + + + +```agda + negation : G Ab.≅ G + negation = total-iso + (_⁻¹ , is-involutive→is-equiv (λ _ → inv-inv)) + (record { pres-⋆ = λ x y → inv-comm ∙ commutes }) +``` diff --git a/src/Algebra/Group/Instances/Dihedral.lagda.md b/src/Algebra/Group/Instances/Dihedral.lagda.md new file mode 100644 index 000000000..d37bb3c6a --- /dev/null +++ b/src/Algebra/Group/Instances/Dihedral.lagda.md @@ -0,0 +1,105 @@ + + +```agda +module Algebra.Group.Instances.Dihedral where +``` + +# Dihedral groups {defines="dihedral-group generalised-dihedral-group"} + +The [[group]] of symmetries of a regular $n$-gon, comprising rotations +around the center and reflections, is called the **dihedral group** +of order $2n$: there are $n$ rotations and $n$ reflections, where +each reflection can be obtained by composing a rotation with a chosen +reflection. + +::: terminology +There are two notational conventions for the dihedral group associated +with the regular $n$-gon: the *geometric* convention is to write $D_n$, +while the *algebraic* convention is to write $D_{2n}$, alluding to the +order of the group. We will use the geometric convention here. +::: + +Given any [[abelian group]] $G$, we define the **generalised dihedral +group** $\mathrm{Dih}(G)$ as the [[semidirect product]]^[See +[[there|semidirect product]] for some intuition.] group $\ZZ/2\ZZ \ltimes +G$, where the [[cyclic group]] $\ZZ/2\ZZ$ [[acts|group action]] on $G$ +by `negation`{.Agda}. + +```agda +Dih : ∀ {ℓ} → Abelian-group ℓ → Group ℓ +Dih G = Semidirect-product (ℤ/ 2) (Abelian→Group G) $ + ℤ/-out 2 (F-map-iso Ab↪Grp (negation G)) (ext λ _ → inv-inv) + where open Abelian-group-on (G .snd) +``` + +We can then define the dihedral group $D_n$ as the generalised dihedral +group of $\ZZ/n\ZZ$, the group of *rotations* of the regular $n$-gon. + +```agda +D : Nat → Group lzero +D n = Dih (ℤ-ab/ n) +``` + +We also define the **infinite dihedral group** $D_\infty$ as the +generalised dihedral group of the [[group of integers]], +$\mathrm{Dih}(\ZZ)$. + +```agda +D∞ : Group lzero +D∞ = Dih ℤ-ab +``` + +Geometrically, $D_\infty$ is the symmetry group of the following +infinitely repeating frieze pattern, also known as $p1m1$: there is +a horizontal translation for every integer, as well as a reflection +across the vertical axis that flips all the translations. + +~~~{.quiver} +\begin{tikzpicture} + \node (-3) at (-3, 0) {}; + \node (-2) at (-2, 0) {}; + \node (-1) at (-1, 0) {}; + \node (0) at (0, 0) {}; + \node (1) at (1, 0) {}; + \node (2) at (2, 0) {}; + \node (3) at (3, 0) {}; + \draw (-3.center) to (-2.center); + \draw (-2.center) to (-1.center); + \draw (-1.center) to (0.center); + \draw (0.center) to (1.center); + \draw (1.center) to (2.center); + \draw (2.center) to (3.center); + + \node[left,at=(-3)] {$\cdots$}; + \node[right,at=(3)] {$\cdots$}; + + \node (-2') at (-2, 1) {}; + \draw (-2.center) to (-2'.center); + \node (-1') at (-1, 1) {}; + \draw (-1.center) to (-1'.center); + \node (0') at (0, 1) {}; + \draw (0.center) to (0'.center); + \node (1') at (1, 1) {}; + \draw (1.center) to (1'.center); + \node (2') at (2, 1) {}; + \draw (2.center) to (2'.center); +\end{tikzpicture} +~~~ + +Note that our construction of $D_n$ makes $D_0$ equal to $D_\infty$, +since $\ZZ/0\ZZ$ is $\ZZ$. + +```agda +D₀≡D∞ : D 0 ≡ D∞ +D₀≡D∞ = ap Dih ℤ-ab/0≡ℤ-ab +``` From 2d49ac7f1f057391e744a61f422a23407639f83e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Na=C3=AFm=20Favier?= Date: Sun, 25 Aug 2024 15:17:40 +0200 Subject: [PATCH 6/9] def: finite limits of concrete groups --- src/1Lab/Type/Pointed.lagda.md | 17 ++++ .../Group/Concrete/FinitelyComplete.lagda.md | 84 +++++++++++++++++++ src/Cat/Functor/Equivalence/Path.lagda.md | 32 ++++--- src/Homotopy/Connectedness.lagda.md | 9 ++ .../Connectedness/Automation.lagda.md | 7 ++ 5 files changed, 131 insertions(+), 18 deletions(-) create mode 100644 src/Algebra/Group/Concrete/FinitelyComplete.lagda.md diff --git a/src/1Lab/Type/Pointed.lagda.md b/src/1Lab/Type/Pointed.lagda.md index 8c80dcd67..4ba6a90c0 100644 --- a/src/1Lab/Type/Pointed.lagda.md +++ b/src/1Lab/Type/Pointed.lagda.md @@ -35,6 +35,8 @@ Those are called **pointed maps**. ```agda _→∙_ : Type∙ ℓ → Type∙ ℓ' → Type _ (A , a) →∙ (B , b) = Σ[ f ∈ (A → B) ] (f a ≡ b) + +infixr 0 _→∙_ ``` Pointed maps compose in a straightforward way. @@ -58,3 +60,18 @@ funext∙ : {f g : A →∙ B} → f ≡ g funext∙ h pth i = funext h i , pth i ``` + +The product of two pointed types is again a pointed type. + +```agda +_×∙_ : Type∙ ℓ → Type∙ ℓ' → Type∙ (ℓ ⊔ ℓ') +(A , a) ×∙ (B , b) = A × B , a , b + +infixr 5 _×∙_ + +fst∙ : A ×∙ B →∙ A +fst∙ = fst , refl + +snd∙ : A ×∙ B →∙ B +snd∙ = snd , refl +``` diff --git a/src/Algebra/Group/Concrete/FinitelyComplete.lagda.md b/src/Algebra/Group/Concrete/FinitelyComplete.lagda.md new file mode 100644 index 000000000..e90691af5 --- /dev/null +++ b/src/Algebra/Group/Concrete/FinitelyComplete.lagda.md @@ -0,0 +1,84 @@ + + +```agda +module Algebra.Group.Concrete.FinitelyComplete {ℓ} where +``` + +# Finite limits of concrete groups + +Since the category of [[concrete groups]] is equivalent to the +[[category of groups]], and the latter is [[finitely complete]], then +so is the former. + +```agda +ConcreteGroups-finitely-complete : Finitely-complete (ConcreteGroups ℓ) +ConcreteGroups-finitely-complete = subst Finitely-complete + (sym (eqv→path ConcreteGroups-is-category Groups-is-category _ π₁F-is-equivalence)) + Groups-finitely-complete +``` + +However, the construction of binary [[products]] of concrete groups +(corresponding to the [[direct product of groups]]) is natural enough to +spell out explicitly: one can simply take the product of the underlying +groupoids! + +```agda +Direct-product-concrete : ConcreteGroup ℓ → ConcreteGroup ℓ → ConcreteGroup ℓ +Direct-product-concrete G H .B = B G ×∙ B H +Direct-product-concrete G H .has-is-connected = is-connected→is-connected∙ $ + ×-is-n-connected 2 + (is-connected∙→is-connected (G .has-is-connected)) + (is-connected∙→is-connected (H .has-is-connected)) +Direct-product-concrete G H .has-is-groupoid = ×-is-hlevel 3 + (G .has-is-groupoid) + (H .has-is-groupoid) + +ConcreteGroups-products + : (X Y : ConcreteGroup ℓ) → Product (ConcreteGroups ℓ) X Y +ConcreteGroups-products X Y = prod where + prod : Product (ConcreteGroups ℓ) X Y + prod .apex = Direct-product-concrete X Y + prod .π₁ = fst∙ + prod .π₂ = snd∙ + prod .has-is-product .⟨_,_⟩ f g .fst x = f # x , g # x + prod .has-is-product .⟨_,_⟩ f g .snd = f .snd ,ₚ g .snd + prod .has-is-product .π₁∘⟨⟩ = funext∙ (λ _ → refl) (∙-idr _) + prod .has-is-product .π₂∘⟨⟩ = funext∙ (λ _ → refl) (∙-idr _) + prod .has-is-product .unique {Q} {f} {g} {u} p1 p2 = + funext∙ (λ x → p1 #ₚ x ,ₚ p2 #ₚ x) (fix ◁ square) + where + square : Square + (p1 #ₚ pt Q ,ₚ p2 #ₚ pt Q) ((fst∙ ∘∙ u) .snd ,ₚ (snd∙ ∘∙ u) .snd) + (f .snd ,ₚ g .snd) refl + square i = p1 i .snd ,ₚ p2 i .snd + + fix : u .snd ≡ ((fst∙ ∘∙ u) .snd ,ₚ (snd∙ ∘∙ u) .snd) + fix i = ∙-idr (ap fst (u .snd)) (~ i) ,ₚ ∙-idr (ap snd (u .snd)) (~ i) +``` + +Similarly, the [[terminal]] concrete group is just the unit type. + +```agda +Terminal-concrete : ConcreteGroup ℓ +Terminal-concrete .B = Lift _ ⊤ , _ +Terminal-concrete .has-is-connected = is-connected→is-connected∙ (n-connected 2) +Terminal-concrete .has-is-groupoid = hlevel 3 +``` diff --git a/src/Cat/Functor/Equivalence/Path.lagda.md b/src/Cat/Functor/Equivalence/Path.lagda.md index a99a8f2c0..a4f530062 100644 --- a/src/Cat/Functor/Equivalence/Path.lagda.md +++ b/src/Cat/Functor/Equivalence/Path.lagda.md @@ -246,24 +246,6 @@ Category-identity-system-pre = (fst , (Subset-proj-embedding (λ x → is-identity-system-is-prop))) ``` - - Then, since the spaces of equivalences $\cC \cong \cD$ and isomorphisms $\cC \to \cD$ are both defined as the total space of a predicate on the same types, it suffices to show that the predicates @@ -317,3 +299,17 @@ the necessary paths for showing that $F_0$ is an equivalence of types. .is-iso.rinv x → dcat .to-path $ isoⁿ→iso (F∘F⁻¹≅Id eqv) _ .is-iso.linv x → sym $ ccat .to-path $ isoⁿ→iso (Id≅F⁻¹∘F eqv) _ ``` + + diff --git a/src/Homotopy/Connectedness.lagda.md b/src/Homotopy/Connectedness.lagda.md index 04eaf9a14..d2da6921a 100644 --- a/src/Homotopy/Connectedness.lagda.md +++ b/src/Homotopy/Connectedness.lagda.md @@ -215,6 +215,15 @@ retract→is-n-connected (suc (suc n)) f g h a-conn = (is-n-connected-Tr (suc n) a-conn) ``` + + Since the truncation operator $\| - \|_n$ also preserves products, a remarkably similar argument shows that if $A$ and $B$ are $n$-connected, then so is $A \times B$. diff --git a/src/Homotopy/Connectedness/Automation.lagda.md b/src/Homotopy/Connectedness/Automation.lagda.md index 94fe06700..a0c2ecdc3 100644 --- a/src/Homotopy/Connectedness/Automation.lagda.md +++ b/src/Homotopy/Connectedness/Automation.lagda.md @@ -77,4 +77,11 @@ instance → Connected (Path A x y) n Connected-Path {n = n} ⦃ conn-instance ac ⦄ = conn-instance (Path-is-connected n ac) + + Connected-Lift + : ∀ {ℓ ℓ'} {A : Type ℓ} {n} + → ⦃ Connected A n ⦄ + → Connected (Lift ℓ' A) n + Connected-Lift {n = n} ⦃ conn-instance ac ⦄ = conn-instance + (is-n-connected-≃ n (Lift-≃ e⁻¹) ac) ``` From 131224b382964275d685ea7b13ee8798e2070184 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Na=C3=AFm=20Favier?= Date: Sun, 25 Aug 2024 17:27:23 +0200 Subject: [PATCH 7/9] =?UTF-8?q?chore:=20flip=20`=E2=88=98Iso`=20and=20`?= =?UTF-8?q?=E2=88=98ni`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We try to stick to the convention that `∘` means the classical composition order while `∙` means diagrammatic order. --- src/Algebra/Group/Action.lagda.md | 2 +- .../Group/Concrete/Semidirect.lagda.md | 2 +- src/Cat/Bi/Instances/Relations.lagda.md | 2 +- src/Cat/Displayed/Bifibration.lagda.md | 4 +- .../Functor/Adjoint/Representable.lagda.md | 12 +++--- src/Cat/Functor/Equivalence.lagda.md | 2 +- src/Cat/Functor/Hom/Duality.lagda.md | 8 ++-- src/Cat/Functor/Hom/Representable.lagda.md | 4 +- src/Cat/Functor/Naturality.lagda.md | 7 +++- src/Cat/Monoidal/Base.lagda.md | 16 ++++---- src/Cat/Monoidal/Braided.lagda.md | 4 +- src/Cat/Morphism.lagda.md | 37 ++++++++++--------- src/Cat/Reasoning.lagda.md | 18 ++++----- src/Cat/Univalent.lagda.md | 2 +- src/Cat/Univalent/Rezk/Universal.lagda.md | 10 ++--- 15 files changed, 68 insertions(+), 62 deletions(-) diff --git a/src/Algebra/Group/Action.lagda.md b/src/Algebra/Group/Action.lagda.md index 6efe86bc9..62e949ddb 100644 --- a/src/Algebra/Group/Action.lagda.md +++ b/src/Algebra/Group/Action.lagda.md @@ -83,7 +83,7 @@ module _ {o ℓ} (C : Precategory o ℓ) where mg : make-group (X C.≅ X) mg .make-group.group-is-set = hlevel 2 mg .make-group.unit = C.id-iso - mg .make-group.mul f g = f C.∘Iso g + mg .make-group.mul f g = g C.∘Iso f mg .make-group.inv = C._Iso⁻¹ mg .make-group.assoc x y z = ext (sym (C.assoc _ _ _)) mg .make-group.invl x = ext (x .C.invl) diff --git a/src/Algebra/Group/Concrete/Semidirect.lagda.md b/src/Algebra/Group/Concrete/Semidirect.lagda.md index 6821058b5..c0d3e7787 100644 --- a/src/Algebra/Group/Concrete/Semidirect.lagda.md +++ b/src/Algebra/Group/Concrete/Semidirect.lagda.md @@ -84,7 +84,7 @@ involve a `sym` to align them up. π₁-φ .preserves .pres-⋆ p q = path→iso (ap (π₁B ⊙ φ) (p ∙ q)) ≡⟨ ap path→iso (ap-∙ (π₁B ⊙ φ) p q) ⟩ path→iso (ap (π₁B ⊙ φ) p ∙ ap (π₁B ⊙ φ) q) ≡⟨ path→iso-∙ (Groups ℓ) _ _ ⟩ - path→iso (ap (π₁B ⊙ φ) p) ∘Iso path→iso (ap (π₁B ⊙ φ) q) ∎ + path→iso (ap (π₁B ⊙ φ) p) ∙Iso path→iso (ap (π₁B ⊙ φ) q) ∎ π₁BG⋉π₁BH : Group ℓ π₁BG⋉π₁BH = Semidirect-product (π₁B G) (π₁B H) π₁-φ diff --git a/src/Cat/Bi/Instances/Relations.lagda.md b/src/Cat/Bi/Instances/Relations.lagda.md index f597e5e09..faaf13fd9 100644 --- a/src/Cat/Bi/Instances/Relations.lagda.md +++ b/src/Cat/Bi/Instances/Relations.lagda.md @@ -443,7 +443,7 @@ want to look at the formalisation. (image-pre-cover r[st].it _ β-cover) done : Im r[st].it Sub.≅ Im [rs]t.it - done = r[st]≅i Sub.∘Iso ([rs]t≅i Sub.Iso⁻¹) + done = [rs]t≅i Sub.Iso⁻¹ Sub.∘Iso r[st]≅i ``` --> diff --git a/src/Cat/Displayed/Bifibration.lagda.md b/src/Cat/Displayed/Bifibration.lagda.md index 7383866fa..14e74c64b 100644 --- a/src/Cat/Displayed/Bifibration.lagda.md +++ b/src/Cat/Displayed/Bifibration.lagda.md @@ -96,7 +96,7 @@ module _ (bifib : is-bifibration) where → cobase-change f ⊣ base-change f cobase-change⊣base-change {x} {y} f = hom-natural-iso→adjoints $ - (opfibration→hom-iso opfibration f ni⁻¹) ∘ni fibration→hom-iso fibration f + fibration→hom-iso fibration f ∘ni opfibration→hom-iso opfibration f ni⁻¹ ``` In fact, if $\cE \liesover \cB$ is a cartesian fibration where every @@ -127,7 +127,7 @@ module _ (fib : Cartesian-fibration) where left-adjoint-base-change→opfibration L adj = cartesian+weak-opfibration→opfibration fib $ hom-iso→weak-opfibration L λ u → - fibration→hom-iso-from fib u ∘ni (adjunct-hom-iso-from (adj u) _ ni⁻¹) + adjunct-hom-iso-from (adj u) _ ni⁻¹ ∘ni fibration→hom-iso-from fib u ``` @@ -301,24 +301,24 @@ desired equation since $1 \otimes -$ is an equivalence. triangle-λ← {A} {B} = push-eqⁿ (unitor-l ni⁻¹) $ ▶.F-∘ _ _ ∙ ap to (Iso-prism base sq1 sq2 sq3) where - base : ◀.F-map-iso (α≅ Iso⁻¹) ∘Iso ◀.F-map-iso (◀.F-map-iso (ρ≅ Iso⁻¹)) + base : ◀.F-map-iso (α≅ Iso⁻¹) ∙Iso ◀.F-map-iso (◀.F-map-iso (ρ≅ Iso⁻¹)) ≡ ◀.F-map-iso (▶.F-map-iso (λ≅ Iso⁻¹)) base = ≅-path (◀.collapse triangle) - sq1 : ◀.F-map-iso (α≅ Iso⁻¹) ∘Iso α≅ ∘Iso α≅ ≡ α≅ ∘Iso ▶.F-map-iso α≅ + sq1 : ◀.F-map-iso (α≅ Iso⁻¹) ∙Iso α≅ ∙Iso α≅ ≡ α≅ ∙Iso ▶.F-map-iso α≅ sq1 = ≅-path (rswizzle (sym pentagon-α→ ∙ assoc _ _ _) (◀.annihilate (α≅ .invl))) - sq2 : ◀.F-map-iso (◀.F-map-iso (ρ≅ Iso⁻¹)) ∘Iso α≅ - ≡ (α≅ ∘Iso α≅) ∘Iso ▶.F-map-iso (λ≅ Iso⁻¹) + sq2 : ◀.F-map-iso (◀.F-map-iso (ρ≅ Iso⁻¹)) ∙Iso α≅ + ≡ (α≅ ∙Iso α≅) ∙Iso ▶.F-map-iso (λ≅ Iso⁻¹) sq2 = ≅-path $ α→ _ _ _ ∘ ((ρ← ⊗₁ id) ⊗₁ id) ≡⟨ associator .Isoⁿ.to .is-natural _ _ _ ⟩ (ρ← ⊗₁ ⌜ id ⊗₁ id ⌝) ∘ α→ _ _ _ ≡⟨ ap! ⊗.F-id ⟩ (ρ← ⊗₁ id) ∘ α→ _ _ _ ≡˘⟨ pulll triangle-α→ ⟩ (id ⊗₁ λ←) ∘ α→ _ _ _ ∘ α→ _ _ _ ∎ - sq3 : ◀.F-map-iso (▶.F-map-iso (λ≅ Iso⁻¹)) ∘Iso α≅ - ≡ α≅ ∘Iso ▶.F-map-iso (◀.F-map-iso (λ≅ Iso⁻¹)) + sq3 : ◀.F-map-iso (▶.F-map-iso (λ≅ Iso⁻¹)) ∙Iso α≅ + ≡ α≅ ∙Iso ▶.F-map-iso (◀.F-map-iso (λ≅ Iso⁻¹)) sq3 = ≅-path (associator .Isoⁿ.to .is-natural _ _ _) ``` diff --git a/src/Cat/Monoidal/Braided.lagda.md b/src/Cat/Monoidal/Braided.lagda.md index c86e1ccfe..1e71a3dd7 100644 --- a/src/Cat/Monoidal/Braided.lagda.md +++ b/src/Cat/Monoidal/Braided.lagda.md @@ -121,8 +121,8 @@ braiding. β←-α← : ∀ {A B C} → (β← ⊗₁ id) ∘ α← B A C ∘ (id ⊗₁ β←) ≡ α← A B C ∘ β← ∘ α← B C A β←-α← = inverse-unique refl refl - (◀.F-map-iso β≅ ∘Iso α≅ ∘Iso ▶.F-map-iso β≅) - (α≅ ∘Iso β≅ ∘Iso α≅) + (◀.F-map-iso β≅ ∙Iso α≅ ∙Iso ▶.F-map-iso β≅) + (α≅ ∙Iso β≅ ∙Iso α≅) (sym (assoc _ _ _) ·· braiding-α→ ·· assoc _ _ _) ``` --> diff --git a/src/Cat/Morphism.lagda.md b/src/Cat/Morphism.lagda.md index 492df4d99..d810b510a 100644 --- a/src/Cat/Morphism.lagda.md +++ b/src/Cat/Morphism.lagda.md @@ -420,33 +420,36 @@ id-iso .inverses .invr = idl id Isomorphism = _≅_ -Inverses-∘ : {f : Hom a b} {f⁻¹ : Hom b a} {g : Hom b c} {g⁻¹ : Hom c b} - → Inverses f f⁻¹ → Inverses g g⁻¹ → Inverses (g ∘ f) (f⁻¹ ∘ g⁻¹) +Inverses-∘ : {a b c : Ob} {f : Hom b c} {f⁻¹ : Hom c b} {g : Hom a b} {g⁻¹ : Hom b a} + → Inverses f f⁻¹ → Inverses g g⁻¹ → Inverses (f ∘ g) (g⁻¹ ∘ f⁻¹) Inverses-∘ {f = f} {f⁻¹} {g} {g⁻¹} finv ginv = record { invl = l ; invr = r } where module finv = Inverses finv module ginv = Inverses ginv abstract - l : (g ∘ f) ∘ f⁻¹ ∘ g⁻¹ ≡ id - l = (g ∘ f) ∘ f⁻¹ ∘ g⁻¹ ≡⟨ cat! C ⟩ - g ∘ (f ∘ f⁻¹) ∘ g⁻¹ ≡⟨ (λ i → g ∘ finv.invl i ∘ g⁻¹) ⟩ - g ∘ id ∘ g⁻¹ ≡⟨ cat! C ⟩ - g ∘ g⁻¹ ≡⟨ ginv.invl ⟩ + l : (f ∘ g) ∘ g⁻¹ ∘ f⁻¹ ≡ id + l = (f ∘ g) ∘ g⁻¹ ∘ f⁻¹ ≡⟨ cat! C ⟩ + f ∘ (g ∘ g⁻¹) ∘ f⁻¹ ≡⟨ (λ i → f ∘ ginv.invl i ∘ f⁻¹) ⟩ + f ∘ id ∘ f⁻¹ ≡⟨ cat! C ⟩ + f ∘ f⁻¹ ≡⟨ finv.invl ⟩ id ∎ - r : (f⁻¹ ∘ g⁻¹) ∘ g ∘ f ≡ id - r = (f⁻¹ ∘ g⁻¹) ∘ g ∘ f ≡⟨ cat! C ⟩ - f⁻¹ ∘ (g⁻¹ ∘ g) ∘ f ≡⟨ (λ i → f⁻¹ ∘ ginv.invr i ∘ f) ⟩ - f⁻¹ ∘ id ∘ f ≡⟨ cat! C ⟩ - f⁻¹ ∘ f ≡⟨ finv.invr ⟩ + r : (g⁻¹ ∘ f⁻¹) ∘ f ∘ g ≡ id + r = (g⁻¹ ∘ f⁻¹) ∘ f ∘ g ≡⟨ cat! C ⟩ + g⁻¹ ∘ (f⁻¹ ∘ f) ∘ g ≡⟨ (λ i → g⁻¹ ∘ finv.invr i ∘ g) ⟩ + g⁻¹ ∘ id ∘ g ≡⟨ cat! C ⟩ + g⁻¹ ∘ g ≡⟨ ginv.invr ⟩ id ∎ -_∘Iso_ : a ≅ b → b ≅ c → a ≅ c -(f ∘Iso g) .to = g .to ∘ f .to -(f ∘Iso g) .from = f .from ∘ g .from +_∘Iso_ : ∀ {a b c : Ob} → b ≅ c → a ≅ b → a ≅ c +(f ∘Iso g) .to = f .to ∘ g .to +(f ∘Iso g) .from = g .from ∘ f .from (f ∘Iso g) .inverses = Inverses-∘ (f .inverses) (g .inverses) -infixr 40 _∘Iso_ +_∙Iso_ : ∀ {a b c : Ob} → a ≅ b → b ≅ c → a ≅ c +f ∙Iso g = g ∘Iso f + +infixr 40 _∘Iso_ _∙Iso_ infixr 41 _Iso⁻¹ invertible-∘ @@ -455,7 +458,7 @@ invertible-∘ → is-invertible (f ∘ g) invertible-∘ f-inv g-inv = record { inv = g-inv.inv ∘ f-inv.inv - ; inverses = Inverses-∘ g-inv.inverses f-inv.inverses + ; inverses = Inverses-∘ f-inv.inverses g-inv.inverses } where module f-inv = is-invertible f-inv diff --git a/src/Cat/Reasoning.lagda.md b/src/Cat/Reasoning.lagda.md index b87406fe8..ab8391208 100644 --- a/src/Cat/Reasoning.lagda.md +++ b/src/Cat/Reasoning.lagda.md @@ -340,8 +340,8 @@ of isomorphisms. ```agda Iso-swapr : ∀ {a : x ≅ y} {b : y ≅ z} {c : x ≅ z} - → a ∘Iso b ≡ c - → a ≡ c ∘Iso (b Iso⁻¹) + → b ∘Iso a ≡ c + → a ≡ b Iso⁻¹ ∘Iso c Iso-swapr {a = a} {b = b} {c = c} p = ≅-path $ a .to ≡⟨ introl (b .invr) ⟩ (b .from ∘ b .to) ∘ a .to ≡⟨ pullr (ap to p) ⟩ @@ -349,8 +349,8 @@ Iso-swapr {a = a} {b = b} {c = c} p = ≅-path $ Iso-swapl : ∀ {a : x ≅ y} {b : y ≅ z} {c : x ≅ z} - → a ∘Iso b ≡ c - → b ≡ (a Iso⁻¹) ∘Iso c + → b ∘Iso a ≡ c + → b ≡ c ∘Iso a Iso⁻¹ Iso-swapl {a = a} {b = b} {c = c} p = ≅-path $ b .to ≡⟨ intror (a .invl) ⟩ b .to ∘ a .to ∘ a .from ≡⟨ pulll (ap to p) ⟩ @@ -384,11 +384,11 @@ bottom face. Iso-prism : ∀ {a : u ≅ v} {b : v ≅ w} {c : u ≅ w} → {d : u ≅ x} {e : v ≅ y} {f : w ≅ z} → {g : x ≅ y} {h : y ≅ z} {i : x ≅ z} - → a ∘Iso b ≡ c - → a ∘Iso e ≡ d ∘Iso g - → b ∘Iso f ≡ e ∘Iso h - → c ∘Iso f ≡ d ∘Iso i - → g ∘Iso h ≡ i + → b ∘Iso a ≡ c + → e ∘Iso a ≡ g ∘Iso d + → f ∘Iso b ≡ h ∘Iso e + → f ∘Iso c ≡ i ∘Iso d + → h ∘Iso g ≡ i Iso-prism {a = a} {b} {c} {d} {e} {f} {g} {h} {i} top left right front = ≅-path $ h .to ∘ g .to ≡⟨ ap₂ _∘_ (ap to (Iso-swapl (sym right))) (ap to (Iso-swapl (sym left)) ∙ sym (assoc _ _ _)) ⟩ diff --git a/src/Cat/Univalent.lagda.md b/src/Cat/Univalent.lagda.md index 0a6358d82..2f383d07e 100644 --- a/src/Cat/Univalent.lagda.md +++ b/src/Cat/Univalent.lagda.md @@ -178,7 +178,7 @@ paths in `Hom`{.Agda}-sets. path→iso-∙ : ∀ {A B C} (p : A ≡ B) (q : B ≡ C) - → path→iso (p ∙ q) ≡ path→iso p ∘Iso path→iso q + → path→iso (p ∙ q) ≡ path→iso p ∙Iso path→iso q path→iso-∙ p q = ext (path→to-∙ p q) path→to-sym : ∀ {A B} (p : A ≡ B) → path→iso p .from ≡ path→iso (sym p) .to diff --git a/src/Cat/Univalent/Rezk/Universal.lagda.md b/src/Cat/Univalent/Rezk/Universal.lagda.md index 789084ec7..b0bfd7225 100644 --- a/src/Cat/Univalent/Rezk/Universal.lagda.md +++ b/src/Cat/Univalent/Rezk/Universal.lagda.md @@ -351,7 +351,7 @@ candidate over it. ```agda obj' : ∀ {b} → Essential-fibre H b → Obs b obj' (a₀ , h₀) .fst = F.₀ a₀ - obj' (a₀ , h₀) .snd .fst a h = F-map-iso F (H.iso.from (h B.∘Iso (h₀ B.Iso⁻¹))) + obj' (a₀ , h₀) .snd .fst a h = F-map-iso F (H.iso.from (h₀ B.Iso⁻¹ B.∘Iso h)) obj' (a₀ , h₀) .snd .snd (a , h) (a' , h') f p = F.collapse (H.ipushr p) Obs-is-prop : ∀ {b} (f : Essential-fibre H b) (c : Obs b) → obj' f ≡ c @@ -367,7 +367,7 @@ candidate over it. c = ckα .fst k = ckα .snd .fst α = ckα .snd .snd - c≅c' = (k a₀ h₀ C.Iso⁻¹) C.∘Iso k' a₀ h₀ + c≅c' = k' a₀ h₀ C.∘Iso k a₀ h₀ C.Iso⁻¹ ``` @@ -162,3 +165,82 @@ one generator. ℤ-free .Free-object.unique {G} {x} g comm = pow-unique G (x _) g (unext comm _) ``` + +::: note +While the notation $x^n$ for `pow`{.Agda} makes sense in +multiplicative notation, we would instead write $n \cdot x$ in additive +notation. In fact, we can show that $n \cdot x$ coincides with the +multiplication $n \times x$ in the group of integers itself. + +```agda +pow-ℤ : ∀ {ℓ} a b → Lift.lower (pow (ℤ {ℓ}) (lift a) b) ≡ a *ℤ b +pow-ℤ {ℓ} a = ℤ.induction (sym (*ℤ-zeror a)) λ b → + lower (pow ℤ (lift a) b) ≡ a *ℤ b ≃⟨ ap (_+ℤ a) , equiv→cancellable (equiv≃ Lift-≃ Lift-≃ .fst (_ , Group-on.⋆-equivr (ℤ {ℓ} .snd) (lift a)) .snd) ⟩ + lower (pow ℤ (lift a) b) +ℤ a ≡ a *ℤ b +ℤ a ≃⟨ ∙-pre-equiv (ap lower (pow-sucr ℤ (lift a) b)) ⟩ + lower (pow ℤ (lift a) (sucℤ b)) ≡ a *ℤ b +ℤ a ≃⟨ ∙-post-equiv (sym (*ℤ-sucr a b)) ⟩ + lower (pow ℤ (lift a) (sucℤ b)) ≡ a *ℤ sucℤ b ≃∎ +``` +::: + +# Order of an element {defines="order-of-an-element"} + + + +We define the **order** of an element $x : G$ of a group $G$ as the +minimal *positive*^[Without this requirement, every element would +trivially have order $0$!] integer $n$ such that $x^n = 1$, if it exists. + +In particular, if $x^n = 1$, then we have that the order of $x$ divides +$n$. We define this notion first in the code, then use it to define the +order of $x$. + +```agda + order-divides : ⌞ G ⌟ → Nat → Type ℓ + order-divides x n = pow G x (pos n) ≡ unit + + has-finite-order : ⌞ G ⌟ → Type ℓ + has-finite-order x = minimal-solution λ n → + Positive n × order-divides x n + + order : (x : ⌞ G ⌟) → has-finite-order x → Nat + order x (n , _) = n +``` + +::: {.definition #torsion} +An element $x$ with finite order is also called a **torsion element**. +A group all of whose elements are torsion is called a **torsion group**, +while a group whose only torsion element is the unit is called +**torsion-free**. +::: + +```agda + is-torsion-group : Type ℓ + is-torsion-group = ∀ g → has-finite-order g + + is-torsion-free : Type ℓ + is-torsion-free = ∀ g → has-finite-order g → g ≡ unit +``` + +::: note +Our definition of torsion groups requires being able to compute +the order of every element of the group. There is a weaker definition +that only requires every element $x$ to have *some* $n$ such that +$x^n = 1$; the two definitions are equivalent if the group is +[[discrete]], since [[$\NN$ is well-ordered|N is well-ordered]]. +::: + +We quickly note that $\ZZ$ is torsion-free, since multiplication by +a nonzero integer is injective. + +```agda +ℤ-torsion-free : ∀ {ℓ} → is-torsion-free (ℤ {ℓ}) +ℤ-torsion-free (lift n) (k , (k>0 , nk≡0) , _) = ap lift $ + *ℤ-injectiver (pos k) n 0 + (λ p → <-not-equal k>0 (pos-injective (sym p))) + (sym (pow-ℤ n (pos k)) ∙ ap Lift.lower nk≡0) +``` diff --git a/src/Data/Int/Properties.lagda.md b/src/Data/Int/Properties.lagda.md index 81b827501..ced6cc3c2 100644 --- a/src/Data/Int/Properties.lagda.md +++ b/src/Data/Int/Properties.lagda.md @@ -319,6 +319,10 @@ no further comments. assign-+ {neg} (suc x) zero = ap negsuc (+-zeror _) assign-+ {neg} (suc x) (suc y) = ap negsuc (+-sucr _ _) + possuc≠assign-neg : ∀ {x y} → possuc x ≠ assign neg y + possuc≠assign-neg {x} {zero} p = suc≠zero (pos-injective p) + possuc≠assign-neg {x} {suc y} p = pos≠negsuc p + *ℤ-onel : ∀ x → 1 *ℤ x ≡ x *ℤ-onel (pos x) = ap (assign pos) (+-zeror x) ∙ assign-pos x *ℤ-onel (negsuc x) = ap negsuc (+-zeror x) @@ -451,4 +455,17 @@ no further comments. *ℤ-injectiver-possuc k (negsuc x) (pos y) p = absurd (negsuc≠pos (p ∙ assign-pos (y * suc k))) *ℤ-injectiver-possuc k (negsuc x) (negsuc y) p = ap (assign neg) (*-suc-inj k (suc x) (suc y) (ap suc (negsuc-injective p))) + + *ℤ-injectiver-negsuc : ∀ k x y → x *ℤ negsuc k ≡ y *ℤ negsuc k → x ≡ y + *ℤ-injectiver-negsuc k (pos x) (pos y) p = ap pos (*-suc-inj k x y (pos-injective (negℤ-injective _ _ (sym (assign-neg _) ·· p ·· assign-neg _)))) + *ℤ-injectiver-negsuc k posz (negsuc y) p = absurd (zero≠suc (pos-injective p)) + *ℤ-injectiver-negsuc k (possuc x) (negsuc y) p = absurd (negsuc≠pos p) + *ℤ-injectiver-negsuc k (negsuc x) posz p = absurd (suc≠zero (pos-injective p)) + *ℤ-injectiver-negsuc k (negsuc x) (possuc y) p = absurd (pos≠negsuc p) + *ℤ-injectiver-negsuc k (negsuc x) (negsuc y) p = ap (assign neg) (*-suc-inj k (suc x) (suc y) (ap suc (suc-inj (pos-injective p)))) + + *ℤ-injectiver : ∀ k x y → k ≠ 0 → x *ℤ k ≡ y *ℤ k → x ≡ y + *ℤ-injectiver posz x y k≠0 p = absurd (k≠0 refl) + *ℤ-injectiver (possuc k) x y k≠0 p = *ℤ-injectiver-possuc k x y p + *ℤ-injectiver (negsuc k) x y k≠0 p = *ℤ-injectiver-negsuc k x y p ``` diff --git a/src/Data/Nat/Order.lagda.md b/src/Data/Nat/Order.lagda.md index 5d4186564..108334fc3 100644 --- a/src/Data/Nat/Order.lagda.md +++ b/src/Data/Nat/Order.lagda.md @@ -235,7 +235,7 @@ that here (it is a more general fact about from {suc x} {suc y} p = s≤s (from (suc-inj p)) ``` -## Well-ordering +## Well-ordering {defines="N-is-well-ordered"} In classical mathematics, the well-ordering principle states that every nonempty subset of the natural numbers has a minimal element. In @@ -256,14 +256,14 @@ implicitly appealing to path induction to reduce this to the case where $p, q : P(n)$] automatically have that $p = q$. ```agda -module _ {ℓ} {P : Nat → Prop ℓ} where - private - minimal-solution : ∀ {ℓ} (P : Nat → Type ℓ) → Type _ - minimal-solution P = Σ[ n ∈ Nat ] (P n × (∀ k → P k → n ≤ k)) - - minimal-solution-unique : is-prop (minimal-solution λ x → ∣ P x ∣) - minimal-solution-unique (n , pn , n-min) (k , pk , k-min) = - Σ-prop-path! (≤-antisym (n-min _ pk) (k-min _ pn)) +minimal-solution : ∀ {ℓ} (P : Nat → Type ℓ) → Type _ +minimal-solution P = Σ[ n ∈ Nat ] (P n × (∀ k → P k → n ≤ k)) + +minimal-solution-unique + : ∀ {ℓ} {P : Nat → Prop ℓ} + → is-prop (minimal-solution λ x → ∣ P x ∣) +minimal-solution-unique (n , pn , n-min) (k , pk , k-min) = + Σ-prop-path! (≤-antisym (n-min _ pk) (k-min _ pn)) ``` The step of the code that actually finds a minimal solution does not @@ -271,30 +271,32 @@ need $P$ to be a predicate: we only need that for actually searching for an inhabited subset. ```agda - min-suc - : ∀ {P : Nat → Type ℓ} → ∀ n → ¬ P 0 - → (∀ k → P (suc k) → n ≤ k) - → ∀ k → P k → suc n ≤ k - min-suc n ¬p0 nmins zero pk = absurd (¬p0 pk) - min-suc zero ¬p0 nmins (suc k) psk = s≤s 0≤x - min-suc (suc n) ¬p0 nmins (suc k) psk = s≤s (nmins k psk) - - ℕ-minimal-solution - : ∀ (P : Nat → Type ℓ) - → (∀ n → Dec (P n)) - → (n : Nat) → P n - → minimal-solution P - ℕ-minimal-solution P decp zero p = 0 , p , λ k _ → 0≤x - ℕ-minimal-solution P decp (suc n) p = case decp zero of λ where - (yes p0) → 0 , p0 , λ k _ → 0≤x - (no ¬p0) → - let (a , pa , x) = ℕ-minimal-solution (P ∘ suc) (decp ∘ suc) n p - in suc a , pa , min-suc {P} a ¬p0 x - - ℕ-well-ordered - : (∀ n → Dec ∣ P n ∣) - → ∃[ n ∈ Nat ] ∣ P n ∣ - → Σ[ n ∈ Nat ] (∣ P n ∣ × (∀ k → ∣ P k ∣ → n ≤ k)) - ℕ-well-ordered P-dec wit = ∥-∥-rec minimal-solution-unique - (λ { (n , p) → ℕ-minimal-solution _ P-dec n p }) wit +min-suc + : ∀ {ℓ} {P : Nat → Type ℓ} + → ∀ n → ¬ P 0 + → (∀ k → P (suc k) → n ≤ k) + → ∀ k → P k → suc n ≤ k +min-suc n ¬p0 nmins zero pk = absurd (¬p0 pk) +min-suc zero ¬p0 nmins (suc k) psk = s≤s 0≤x +min-suc (suc n) ¬p0 nmins (suc k) psk = s≤s (nmins k psk) + +ℕ-minimal-solution + : ∀ {ℓ} (P : Nat → Type ℓ) + → (∀ n → Dec (P n)) + → (n : Nat) → P n + → minimal-solution P +ℕ-minimal-solution P decp zero p = 0 , p , λ k _ → 0≤x +ℕ-minimal-solution P decp (suc n) p = case decp zero of λ where + (yes p0) → 0 , p0 , λ k _ → 0≤x + (no ¬p0) → + let (a , pa , x) = ℕ-minimal-solution (P ∘ suc) (decp ∘ suc) n p + in suc a , pa , min-suc {P = P} a ¬p0 x + +ℕ-well-ordered + : ∀ {ℓ} {P : Nat → Prop ℓ} + → (∀ n → Dec ∣ P n ∣) + → ∃[ n ∈ Nat ] ∣ P n ∣ + → Σ[ n ∈ Nat ] (∣ P n ∣ × (∀ k → ∣ P k ∣ → n ≤ k)) +ℕ-well-ordered {P = P} P-dec wit = ∥-∥-rec (minimal-solution-unique {P = P}) + (λ { (n , p) → ℕ-minimal-solution _ P-dec n p }) wit ``` From 210881667d7f04ead89cf23fe69fe9e5827beecd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Na=C3=AFm=20Favier?= Date: Tue, 27 Aug 2024 13:12:37 +0200 Subject: [PATCH 9/9] =?UTF-8?q?chore:=20only=20lift=20=E2=84=A4=20and=20?= =?UTF-8?q?=E2=84=A4/n=20as=20needed?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Having ℤ unlifted means that we can use the category reasoning combinators to prove identities of the integers without having to sprinkle lifts and lowers everywhere. --- src/Algebra/Group/Cat/Base.lagda.md | 31 ++++++++++ src/Algebra/Group/Instances/Cyclic.lagda.md | 60 +++++++++---------- src/Algebra/Group/Instances/Dihedral.lagda.md | 2 +- src/Algebra/Group/Instances/Integers.lagda.md | 58 +++++++++--------- src/Data/Int/DivMod.lagda.md | 8 +-- src/Homotopy/Space/Circle.lagda.md | 6 +- 6 files changed, 99 insertions(+), 66 deletions(-) diff --git a/src/Algebra/Group/Cat/Base.lagda.md b/src/Algebra/Group/Cat/Base.lagda.md index a71952259..2943014ab 100644 --- a/src/Algebra/Group/Cat/Base.lagda.md +++ b/src/Algebra/Group/Cat/Base.lagda.md @@ -1,7 +1,10 @@ + ## The underlying set The category of groups admits a `faithful`{.Agda ident=is-faithful} diff --git a/src/Algebra/Group/Instances/Cyclic.lagda.md b/src/Algebra/Group/Instances/Cyclic.lagda.md index 455649920..e45f16113 100644 --- a/src/Algebra/Group/Instances/Cyclic.lagda.md +++ b/src/Algebra/Group/Instances/Cyclic.lagda.md @@ -19,7 +19,6 @@ open import Data.Nat open represents-subgroup open normal-subgroup open is-group-hom -open Lift ``` --> @@ -29,7 +28,7 @@ module Algebra.Group.Instances.Cyclic where @@ -75,20 +74,20 @@ $n$ when $n \geq 1$, and is the infinite cyclic group when $n = 0$. ```agda infix 30 _·ℤ -_·ℤ : ∀ (n : Nat) {ℓ} → normal-subgroup (ℤ {ℓ}) λ (lift i) → el (n ∣ℤ i) (∣ℤ-is-prop n i) +_·ℤ : ∀ (n : Nat) → normal-subgroup ℤ λ i → el (n ∣ℤ i) (∣ℤ-is-prop n i) (n ·ℤ) .has-rep .has-unit = ∣ℤ-zero (n ·ℤ) .has-rep .has-⋆ = ∣ℤ-+ (n ·ℤ) .has-rep .has-inv = ∣ℤ-negℤ -(n ·ℤ) {ℓ} .has-conjugate {lift x} {lift y} = subst (n ∣ℤ_) x≡y+x-y +(n ·ℤ) .has-conjugate {x} {y} = subst (n ∣ℤ_) x≡y+x-y where x≡y+x-y : x ≡ y +ℤ (x -ℤ y) x≡y+x-y = - x ≡⟨ ap lower (ℤ.insertl {h = lift {ℓ = ℓ} y} (ℤ.inverser {x = lift y})) ⟩ + x ≡⟨ ℤ.insertl {h = y} (ℤ.inverser {x = y}) ⟩ y +ℤ (negℤ y +ℤ x) ≡⟨ ap (y +ℤ_) (+ℤ-commutative (negℤ y) x) ⟩ y +ℤ (x -ℤ y) ∎ infix 25 ℤ/_ -ℤ/_ : Nat → ∀ {ℓ} → Group ℓ +ℤ/_ : Nat → Group lzero ℤ/ n = ℤ /ᴳ n ·ℤ ``` @@ -96,11 +95,11 @@ $\ZZ/n\ZZ$ is an [[abelian group]], since the commutativity of addition descends to the quotient. ```agda -ℤ/n-commutative : ∀ n {ℓ} → is-commutative-group {ℓ} (ℤ/ n) -ℤ/n-commutative n = elim! λ x y → ap (inc ⊙ lift) (+ℤ-commutative x y) +ℤ/n-commutative : ∀ n → is-commutative-group (ℤ/ n) +ℤ/n-commutative n = elim! λ x y → ap inc (+ℤ-commutative x y) infix 25 ℤ-ab/_ -ℤ-ab/_ : Nat → ∀ {ℓ} → Abelian-group ℓ +ℤ-ab/_ : Nat → Abelian-group lzero ℤ-ab/_ n = from-commutative-group (ℤ/ n) (ℤ/n-commutative n) ``` @@ -109,24 +108,23 @@ by $1$. ```agda - ℤ/n-cyclic : is-cyclic ℤ/n + ℤ/n-cyclic : is-cyclic (ℤ/ n) ℤ/n-cyclic = inc (1 , gen) where - gen : ℤ/n is-generated-by 1 + gen : ℤ/ n is-generated-by 1 gen = elim! λ x → inc (x , Integers.induction Int-integers - {P = λ x → inc (lift x) ≡ pow ℤ/n 1 x} + {P = λ x → inc x ≡ pow (ℤ/ n) 1 x} refl (λ x → - inc (lift x) ≡ pow ℤ/n 1 x ≃⟨ _ , equiv→cancellable (⋆-equivr 1) ⟩ - inc (lift x) ⋆ 1 ≡ pow ℤ/n 1 x ⋆ 1 ≃⟨ ∙-pre-equiv (sym (ap (inc ⊙ lift) (+ℤ-oner x))) ⟩ - inc (lift (sucℤ x)) ≡ pow ℤ/n 1 x ⋆ 1 ≃⟨ ∙-post-equiv (sym (pow-sucr ℤ/n 1 x)) ⟩ - inc (lift (sucℤ x)) ≡ pow ℤ/n 1 (sucℤ x) ≃∎) + inc x ≡ pow (ℤ/ n) 1 x ≃⟨ _ , equiv→cancellable (⋆-equivr 1) ⟩ + inc x ⋆ 1 ≡ pow (ℤ/ n) 1 x ⋆ 1 ≃⟨ ∙-pre-equiv (sym (ap inc (+ℤ-oner x))) ⟩ + inc (sucℤ x) ≡ pow (ℤ/ n) 1 x ⋆ 1 ≃⟨ ∙-post-equiv (sym (pow-sucr (ℤ/ n) 1 x)) ⟩ + inc (sucℤ x) ≡ pow (ℤ/ n) 1 (sucℤ x) ≃∎) x) ``` @@ -148,8 +146,8 @@ module _ (wraps : x^ pos n ≡ unit) where - ℤ/-out : Groups.Hom (ℤ/ n) G - ℤ/-out .hom = Coeq-rec (apply x^-) λ (lift a , lift b , n∣a-b) → zero-diff $ + ℤ/-out : Groups.Hom (LiftGroup ℓ (ℤ/ n)) G + ℤ/-out .hom (lift i) = Coeq-rec (apply x^- ⊙ lift) (λ (a , b , n∣a-b) → zero-diff $ let k , k*n≡a-b = ∣ℤ→fibre n∣a-b in x^ a — x^ b ≡˘⟨ pres-diff (x^- .preserves) {lift a} {lift b} ⟩ x^ (a -ℤ b) ≡˘⟨ ap x^_ k*n≡a-b ⟩ @@ -157,7 +155,8 @@ module _ x^ (pos n *ℤ k) ≡⟨ pow-* G x (pos n) k ⟩ pow G ⌜ x^ pos n ⌝ k ≡⟨ ap! wraps ⟩ pow G unit k ≡⟨ pow-unit G k ⟩ - unit ∎ + unit ∎) + i ℤ/-out .preserves .pres-⋆ = elim! λ x y → x^- .preserves .pres-⋆ (lift x) (lift y) ``` @@ -165,14 +164,14 @@ module _ We can check that $\ZZ/0\ZZ \is \ZZ$: ```agda -ℤ-ab/0≡ℤ-ab : ∀ {ℓ} → ℤ-ab/ 0 ≡ ℤ-ab {ℓ} +ℤ-ab/0≡ℤ-ab : ℤ-ab/ 0 ≡ ℤ-ab ℤ-ab/0≡ℤ-ab = ∫-Path (total-hom - (Coeq-rec (λ z → z) (λ (_ , _ , p) → ℤ.zero-diff (ap lift p))) + (Coeq-rec (λ z → z) (λ (_ , _ , p) → ℤ.zero-diff p)) (record { pres-⋆ = elim! λ _ _ → refl })) (is-iso→is-equiv (iso inc (λ _ → refl) (elim! λ _ → refl))) -ℤ/0≡ℤ : ∀ {ℓ} → ℤ/ 0 ≡ ℤ {ℓ} +ℤ/0≡ℤ : ℤ/ 0 ≡ ℤ ℤ/0≡ℤ = Grp→Ab→Grp (ℤ/ 0) (ℤ/n-commutative 0) ∙ ap Abelian→Group ℤ-ab/0≡ℤ-ab ``` @@ -182,16 +181,16 @@ $x : \ZZ$ to the representative of its congruence class modulo $n$, $x \% n$. ```agda -ℤ/n≃ℕ @@ -29,26 +28,24 @@ private module ℤ = Integers Int-integers # The group of integers {defines="integer-group group-of-integers"} -The fundamental example of an [[abelian group]] is the group of [[**integers**]], $\ZZ$, under -addition. A type-theoretic interjection is necessary: the integers live -on the zeroth universe, so to have an $\ell$-sized group of integers, we -must lift it. +The fundamental example of an [[abelian group]] is the group of +[[**integers**]], $\ZZ$, under addition. ```agda -ℤ-ab : ∀ {ℓ} → Abelian-group ℓ +ℤ-ab : Abelian-group lzero ℤ-ab = to-ab mk-ℤ where open make-abelian-group - mk-ℤ : make-abelian-group (Lift _ Int) + mk-ℤ : make-abelian-group Int mk-ℤ .ab-is-set = hlevel 2 - mk-ℤ .mul (lift x) (lift y) = lift (x +ℤ y) - mk-ℤ .inv (lift x) = lift (negℤ x) + mk-ℤ .mul x y = x +ℤ y + mk-ℤ .inv x = negℤ x mk-ℤ .1g = 0 - mk-ℤ .idl (lift x) = ap lift (+ℤ-zerol x) - mk-ℤ .assoc (lift x) (lift y) (lift z) = ap lift (+ℤ-assoc x y z) - mk-ℤ .invl (lift x) = ap lift (+ℤ-invl x) - mk-ℤ .comm (lift x) (lift y) = ap lift (+ℤ-commutative x y) + mk-ℤ .idl x = +ℤ-zerol x + mk-ℤ .assoc x y z = +ℤ-assoc x y z + mk-ℤ .invl x = +ℤ-invl x + mk-ℤ .comm x y = +ℤ-commutative x y -ℤ : ∀ {ℓ} → Group ℓ +ℤ : Group lzero ℤ = Abelian→Group ℤ-ab ``` @@ -85,8 +82,14 @@ module _ {ℓ} (G : Group ℓ) where pow (a +ℤ b) ⋆ x ≡ pow a ⋆ pow (sucℤ b) ≃⟨ ∙-pre-equiv (pow-sucr (a +ℤ b)) ⟩ pow (sucℤ (a +ℤ b)) ≡ pow a ⋆ pow (sucℤ b) ≃⟨ ∙-pre-equiv (ap pow (+ℤ-sucr a b)) ⟩ pow (a +ℤ sucℤ b) ≡ pow a ⋆ pow (sucℤ b) ≃∎ +``` - pow-hom : Groups.Hom ℤ G +A type-theoretic interjection is necessary: the integers live on the +zeroth universe, so to have an $\ell$-sized group of integers, we +must lift it. + +```agda + pow-hom : Groups.Hom (LiftGroup ℓ ℤ) G pow-hom .hom (lift i) = pow i pow-hom .preserves .pres-⋆ (lift a) (lift b) = pow-+ a b ``` @@ -94,7 +97,7 @@ module _ {ℓ} (G : Group ℓ) where This is the unique group homomorphism $\ZZ \to G$ that sends $1$ to $x$. ```agda - pow-unique : (g : Groups.Hom ℤ G) → g # 1 ≡ x → g ≡ pow-hom + pow-unique : (g : Groups.Hom (LiftGroup ℓ ℤ) G) → g # 1 ≡ x → g ≡ pow-hom pow-unique g g1≡x = ext $ ℤ.map-out-unique (λ i → g # lift i) (pres-id (g .preserves)) λ y → @@ -158,7 +161,7 @@ one generator. ```agda ℤ-free : Free-object Grp↪Sets (el! ⊤) -ℤ-free .Free-object.free = ℤ +ℤ-free .Free-object.free = LiftGroup lzero ℤ ℤ-free .Free-object.unit _ = 1 ℤ-free .Free-object.fold {G} x = pow-hom G (x _) ℤ-free .Free-object.commute {G} {x} = ext λ _ → pow-1 G (x _) @@ -173,12 +176,12 @@ notation. In fact, we can show that $n \cdot x$ coincides with the multiplication $n \times x$ in the group of integers itself. ```agda -pow-ℤ : ∀ {ℓ} a b → Lift.lower (pow (ℤ {ℓ}) (lift a) b) ≡ a *ℤ b -pow-ℤ {ℓ} a = ℤ.induction (sym (*ℤ-zeror a)) λ b → - lower (pow ℤ (lift a) b) ≡ a *ℤ b ≃⟨ ap (_+ℤ a) , equiv→cancellable (equiv≃ Lift-≃ Lift-≃ .fst (_ , Group-on.⋆-equivr (ℤ {ℓ} .snd) (lift a)) .snd) ⟩ - lower (pow ℤ (lift a) b) +ℤ a ≡ a *ℤ b +ℤ a ≃⟨ ∙-pre-equiv (ap lower (pow-sucr ℤ (lift a) b)) ⟩ - lower (pow ℤ (lift a) (sucℤ b)) ≡ a *ℤ b +ℤ a ≃⟨ ∙-post-equiv (sym (*ℤ-sucr a b)) ⟩ - lower (pow ℤ (lift a) (sucℤ b)) ≡ a *ℤ sucℤ b ≃∎ +pow-ℤ : ∀ a b → pow ℤ a b ≡ a *ℤ b +pow-ℤ a = ℤ.induction (sym (*ℤ-zeror a)) λ b → + pow ℤ a b ≡ a *ℤ b ≃⟨ ap (_+ℤ a) , equiv→cancellable (Group-on.⋆-equivr (ℤ .snd) a) ⟩ + pow ℤ a b +ℤ a ≡ a *ℤ b +ℤ a ≃⟨ ∙-pre-equiv (pow-sucr ℤ a b) ⟩ + pow ℤ a (sucℤ b) ≡ a *ℤ b +ℤ a ≃⟨ ∙-post-equiv (sym (*ℤ-sucr a b)) ⟩ + pow ℤ a (sucℤ b) ≡ a *ℤ sucℤ b ≃∎ ``` ::: @@ -238,9 +241,8 @@ We quickly note that $\ZZ$ is torsion-free, since multiplication by a nonzero integer is injective. ```agda -ℤ-torsion-free : ∀ {ℓ} → is-torsion-free (ℤ {ℓ}) -ℤ-torsion-free (lift n) (k , (k>0 , nk≡0) , _) = ap lift $ - *ℤ-injectiver (pos k) n 0 - (λ p → <-not-equal k>0 (pos-injective (sym p))) - (sym (pow-ℤ n (pos k)) ∙ ap Lift.lower nk≡0) +ℤ-torsion-free : is-torsion-free ℤ +ℤ-torsion-free n (k , (k>0 , nk≡0) , _) = *ℤ-injectiver (pos k) n 0 + (λ p → <-not-equal k>0 (pos-injective (sym p))) + (sym (pow-ℤ n (pos k)) ∙ nk≡0) ``` diff --git a/src/Data/Int/DivMod.lagda.md b/src/Data/Int/DivMod.lagda.md index 779c248d6..a6fa2f9ff 100644 --- a/src/Data/Int/DivMod.lagda.md +++ b/src/Data/Int/DivMod.lagda.md @@ -21,7 +21,7 @@ module Data.Int.DivMod where @@ -85,7 +85,7 @@ $b - (-a)\%b$ as the remainder. lemma = assign neg (q * b + suc r) ≡⟨ ap (assign neg) (+-commutative (q * b) _) ⟩ negsuc (r + q * b) ≡˘⟨ negℤ-+ℤ-negsuc r (q * b) ⟩ - negℤ (pos r) +ℤ negsuc (q * b) ≡⟨ ap (_+ℤ negsuc (q * b)) (ap Lift.lower (ℤ.insertl {h = lift (negℤ (pos b'))} (ap lift (+ℤ-invl (pos b'))) {f = lift (negℤ (pos r))})) ⟩ + negℤ (pos r) +ℤ negsuc (q * b) ≡⟨ ap (_+ℤ negsuc (q * b)) (ℤ.insertl {h = negℤ (pos b')} (+ℤ-invl (pos b')) {f = negℤ (pos r)}) ⟩ ⌜ negℤ (pos b') ⌝ +ℤ (pos b' -ℤ pos r) +ℤ negsuc (q * b) ≡˘⟨ ap¡ (assign-neg b') ⟩ assign neg b' +ℤ (pos b' -ℤ pos r) +ℤ negsuc (q * b) ≡⟨ ap (_+ℤ negsuc (q * b)) (+ℤ-commutative (assign neg b') (pos b' -ℤ pos r)) ⟩ (pos b' -ℤ pos r) +ℤ assign neg b' +ℤ negsuc (q * b) ≡˘⟨ +ℤ-assoc (pos b' -ℤ pos r) _ _ ⟩ @@ -135,7 +135,7 @@ hence it must be zero. b∣r'-r .fst = q -ℤ q' b∣r'-r .snd = (q -ℤ q') *ℤ pos b ≡⟨ *ℤ-distribr-minus (pos b) q q' ⟩ - q *ℤ pos b -ℤ q' *ℤ pos b ≡⟨ ap Lift.lower (ℤ.equal-sum→equal-diff (lift (q *ℤ pos b)) (lift (pos r)) (lift (q' *ℤ pos b)) (lift (pos r')) (ap lift (sym (recover p) ∙ recover p'))) ⟩ + q *ℤ pos b -ℤ q' *ℤ pos b ≡⟨ ℤ.equal-sum→equal-diff (q *ℤ pos b) (pos r) (q' *ℤ pos b) (pos r') (sym (recover p) ∙ recover p') ⟩ pos r' -ℤ pos r ≡⟨ pos-pos r' r ⟩ r' ℕ- r ∎ @@ -186,7 +186,7 @@ divides-diff→same-rem n x y n∣x-y p' : y ≡ (q -ℤ k) *ℤ pos n +ℤ pos r p' = y ≡˘⟨ negℤ-negℤ y ⟩ - negℤ (negℤ y) ≡⟨ ap Lift.lower (ℤ.insertr (ℤ.inversel {lift x}) {f = lift (negℤ (negℤ y))}) ⟩ + negℤ (negℤ y) ≡⟨ ℤ.insertr (ℤ.inversel {x}) {f = negℤ (negℤ y)} ⟩ ⌜ negℤ (negℤ y) +ℤ negℤ x ⌝ +ℤ x ≡⟨ ap! (+ℤ-commutative (negℤ (negℤ y)) _) ⟩ ⌜ negℤ x -ℤ negℤ y ⌝ +ℤ x ≡˘⟨ ap¡ (negℤ-distrib x (negℤ y)) ⟩ negℤ ⌜ x -ℤ y ⌝ +ℤ x ≡˘⟨ ap¡ z ⟩ diff --git a/src/Homotopy/Space/Circle.lagda.md b/src/Homotopy/Space/Circle.lagda.md index a582f8134..ac74cc9a7 100644 --- a/src/Homotopy/Space/Circle.lagda.md +++ b/src/Homotopy/Space/Circle.lagda.md @@ -300,9 +300,9 @@ loopⁿ-+ a = Integers.induction Int-integers π₁S¹≡ℤ : π₁Groupoid.π₁ S¹∙ S¹-is-groupoid ≡ ℤ π₁S¹≡ℤ = sym $ ∫-Path - (total-hom (Equiv.from ΩS¹≃integers ∘ Lift.lower) - (record { pres-⋆ = λ (lift a) (lift b) → loopⁿ-+ a b })) - (∙-is-equiv (Lift-≃ .snd) ((ΩS¹≃integers e⁻¹) .snd)) + (total-hom (Equiv.from ΩS¹≃integers) + (record { pres-⋆ = loopⁿ-+ })) + ((ΩS¹≃integers e⁻¹) .snd) ``` Furthermore, since the loop space of the circle is a set, we automatically