Basic group theory

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:
+:::
 
 <!--
 ```agda

src/1Lab/Type.lagda.md

@@ -131,5 +131,10 @@ case x return P of f = f x
 
 {-# INLINE case_of_        #-}
 {-# INLINE case_return_of_ #-}
+
+instance
+  Number-Lift : ∀ {ℓ ℓ'} {A : Type ℓ} → ⦃ Number A ⦄ → Number (Lift ℓ' A)
+  Number-Lift {ℓ' = ℓ'} ⦃ a ⦄ .Number.Constraint n = Lift ℓ' (a .Number.Constraint n)
+  Number-Lift ⦃ a ⦄ .Number.fromNat n ⦃ lift c ⦄ = lift (a .Number.fromNat n ⦃ c ⦄)
 ```
 -->

src/1Lab/Type/Pi.lagda.md

@@ -1,6 +1,7 @@
 <!--
 ```
 open import 1Lab.Path.Cartesian
+open import 1Lab.Type.Sigma
 open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path
@@ -85,6 +86,12 @@ function≃ dom rng = Iso→Equiv the-iso where
   the-iso .snd .is-iso.linv f =
     funext λ x → rng-iso .is-iso.linv _
                ∙ ap f (dom-iso .is-iso.linv _)
+
+equiv≃ : (A ≃ B) → (C ≃ D) → (A ≃ C) ≃ (B ≃ D)
+equiv≃ x y = Σ-ap (function≃ x y) λ f → prop-ext
+  (is-equiv-is-prop _) (is-equiv-is-prop _)
+  (λ e → ∙-is-equiv (∙-is-equiv ((x e⁻¹) .snd) e) (y .snd))
+  λ e → equiv-cancelr ((x e⁻¹) .snd) (equiv-cancell (y .snd) e)
 ```
 
 

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
+```

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 ℓ''}

src/Algebra/Group.lagda.md

@@ -21,11 +21,11 @@ module Algebra.Group where
 # Groups {defines=group}
 
 A **group** is a [monoid] that has inverses for every element. The
-inverse for an element is [necessarily, unique]; Thus, to say that "$(G,
+inverse for an element is, [necessarily, unique]; thus, to say that "$(G,
 \star)$ is a group" is a statement about $(G, \star)$ having a certain
 _property_ (namely, being a group), not _structure_ on $(G, \star)$.
 
-Furthermore, since `group homomorphisms`{.Agda ident=is-group-hom}
+Furthermore, since [[group homomorphisms]]
 automatically preserve this structure, we are justified in calling this
 _property_ rather than _property-like structure_.
 
@@ -59,6 +59,7 @@ give the unit, both on the left and on the right:
 
 <!--
 ```agda
+  infixr 20 _—_
   _—_ : A → A → A
   x — y = x * inverse y
 
@@ -151,7 +152,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
@@ -193,7 +194,7 @@ record
 ```
 
 A tedious calculation shows that this is sufficient to preserve the
-identity:
+identity and inverses:
 
 ```agda
   private
@@ -252,7 +253,7 @@ Group[_⇒_] : ∀ {ℓ} (A B : Σ (Type ℓ) Group-on) → Type ℓ
 Group[ A ⇒ B ] = Σ (A .fst → B .fst) (is-group-hom (A .snd) (B .snd))
 ```
 
-## Making groups
+# Making groups
 
 Since the interface of `Group-on`{.Agda} is very deeply nested, we
 introduce a helper function for arranging the data of a group into a
@@ -303,47 +304,3 @@ record make-group {ℓ} (G : Type ℓ) : Type ℓ where
 
 open make-group using (to-group-on) public
 ```
-
-# Symmetric groups
-
-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)
-```

src/Algebra/Group/Ab.lagda.md

@@ -3,13 +3,9 @@
 open import Algebra.Group.Cat.Base
 open import Algebra.Group
 
-open import Cat.Displayed.Univalence.Thin
-open import Cat.Displayed.Total
+open import Cat.Functor.Properties
 open import Cat.Prelude hiding (_*_ ; _+_)
 
-open import Data.Int.Properties
-open import Data.Int.Base
-
 import Cat.Reasoning
 ```
 -->
@@ -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
 ```
 
+<!--
+```agda
+  equal-sum→equal-diff : ∀ a b c d → a * b ≡ c * d → a — c ≡ d — b
+  equal-sum→equal-diff a b c d p = commutes ∙ swizzle p inverser inversel
+```
+-->
+
 <!--
 ```agda
 private unquoteDecl eqv = declare-record-iso eqv (quote is-abelian-group)
@@ -113,6 +116,10 @@ Ab : ∀ ℓ → Precategory (lsuc ℓ) ℓ
 Ab ℓ = Structured-objects (Abelian-group-structure ℓ)
 
 module Ab {ℓ} = Cat.Reasoning (Ab ℓ)
+
+instance
+  Ab-equational : ∀ {ℓ} → is-equational (Abelian-group-structure ℓ)
+  Ab-equational .is-equational.invert-id-hom = Groups-equational .is-equational.invert-id-hom
 ```
 
 <!--
@@ -176,6 +183,14 @@ from-commutative-group G comm .snd .Abelian-group-on.has-is-ab .is-abelian-group
 from-commutative-group G comm .snd .Abelian-group-on.has-is-ab .is-abelian-group.commutes =
   comm _ _
 
+Grp→Ab→Grp
+  : ∀ {ℓ} (G : Group ℓ) (c : is-commutative-group G)
+  → Abelian→Group (from-commutative-group G c) ≡ G
+Grp→Ab→Grp G c = Σ-pathp refl go where
+  go : Abelian→Group-on (from-commutative-group G c .snd) ≡ G .snd
+  go i .Group-on._⋆_ = G .snd .Group-on._⋆_
+  go i .Group-on.has-is-group = G .snd .Group-on.has-is-group
+
 open make-abelian-group using (make-abelian-group→make-group ; to-group-on-ab ; to-abelian-group-on ; to-ab) public
 
 open Functor
@@ -187,30 +202,38 @@ Ab↪Grp .F₁ f .preserves = f .preserves
 Ab↪Grp .F-id = trivial!
 Ab↪Grp .F-∘ f g = trivial!
 
+Ab↪Grp-is-ff : ∀ {ℓ} → is-fully-faithful (Ab↪Grp {ℓ})
+Ab↪Grp-is-ff {x = A} {B} = is-iso→is-equiv $ iso
+  promote (λ _ → trivial!) (λ _ → trivial!)
+  where
+    promote : Groups.Hom (Abelian→Group A) (Abelian→Group B) → Ab.Hom A B
+    promote f .hom = f .hom
+    promote f .preserves = f .preserves
+
 Ab↪Sets : ∀ {ℓ} → Functor (Ab ℓ) (Sets ℓ)
 Ab↪Sets = Grp↪Sets F∘ Ab↪Grp
 ```
 -->
 
-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.
+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
+module _ {ℓ} (G : Abelian-group ℓ) where
+  open Abelian-group-on (G .snd)
+```
+-->
 
 ```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
+  negation : G Ab.≅ G
+  negation = total-iso
+    (_⁻¹ , is-involutive→is-equiv (λ _ → inv-inv))
+    (record { pres-⋆ = λ x y → inv-comm ∙ commutes })
 ```