defn: normal subgroups ≃ kernels

src/Algebra/Group.lagda.md

@@ -48,8 +48,8 @@ give the unit, both on the left and on the right:
   open is-monoid has-is-monoid public
 
   abstract
-    inv-unit≡unit : inverse unit ≡ unit
-    inv-unit≡unit = monoid-inverse-unique
+    inv-unit : inverse unit ≡ unit
+    inv-unit = monoid-inverse-unique
       has-is-monoid unit _ _ inversel (idl has-is-monoid)
 
     inv-inv : ∀ {x} → inverse (inverse x) ≡ x

src/Algebra/Group/Subgroup.lagda.md

@@ -334,3 +334,253 @@ will compute.
                           ∙ sym (happly (ap fst prf) f) })
             t
 ```
+
+## Representing kernels
+
+If an evil wizard kidnaps your significant others and demands that you
+find out whether a predicate $P : G \to \prop$ is a kernel, how would
+you go about doing it? Well, I should point out that no matter how evil
+the wizard is, they are still human: The predicate $P$ definitely
+represents a subgroup, in the sense introduced
+[above](#represents-subgroup) --- so there's definitely a group
+homomorphism $\Sigma G \mono G$. All we need to figure out is whether
+there exists a group $H$ and a map $f : G \to H$, such that $\Sigma G
+\cong \ker f$ as subgroups of $G$.
+
+We begin by assuming that we have a kernel and investigating some
+properties that the fibres of its inclusion have. Of course, the fibre
+over $0$ is inhabited, and they are closed under multiplication and
+inverses, though we shall not make note of that here).
+
+```agda
+module _ {ℓ} {A B : Group ℓ} (f : Groups.Hom A B) where private
+  module Ker[f] = Kernel (Ker f)
+  module f = Group-hom (f .snd)
+  module A = Group-on (A .snd)
+  module B = Group-on (B .snd)
+
+  kerf : Ker[f].ker .fst → A .fst
+  kerf = Ker[f].kernel .fst
+
+  has-zero : fibre kerf A.unit
+  has-zero = (A.unit , f.pres-id) , refl
+
+  has-⋆ : ∀ {x y} → fibre kerf x → fibre kerf y → fibre kerf (x A.⋆ y)
+  has-⋆ ((a , p) , q) ((b , r) , s) =
+    (a A.⋆ b , f.pres-⋆ _ _ ·· ap₂ B._⋆_ p r ·· B.idl) ,
+    ap₂ A._⋆_ q s
+```
+
+It turns out that $\ker f$ is also closed under _conjugation_ by
+elements of the enveloping group, in that if $f(x) = 1$ (quickly
+switching to "multiplicative" notation for the unit), then $f(yxy^{-1})$
+must be $1$ as well: for we have $$f(y)f(x)f(y^{-1}) = f(y)1f(y^{-1}) =
+f(yy^{-1}) = f(1) = 1$$.
+
+```agda
+  has-conjugate : ∀ {x y} → fibre kerf x → fibre kerf (y A.⋆ x A.⋆ y A.⁻¹)
+  has-conjugate {x} {y} ((a , p) , q) = (_ , path) , refl where
+    path =
+      f .fst (y A.⋆ x A.⋆ y A.⁻¹)                 ≡⟨ ap (f .fst) A.associative ⟩
+      f .fst ((y A.⋆ x) A.⋆ y A.⁻¹)               ≡⟨ f.pres-⋆ _ _ ⟩
+      f .fst (y A.⋆ x) B.⋆ f .fst (y A.⁻¹)        ≡⟨ ap (B._⋆ _) (f.pres-⋆ y x) ⟩
+      (f .fst y B.⋆ f .fst x) B.⋆ f .fst (y A.⁻¹) ≡⟨ ap (B._⋆ _) (ap (_ B.⋆_) (ap (f .fst) (sym q) ∙ p) ∙ B.idr) ⟩
+      f .fst y B.⋆ f .fst (y A.⁻¹)                ≡˘⟨ f.pres-⋆ _ _ ⟩
+      f .fst (y A.⋆ y A.⁻¹)                       ≡⟨ ap (f .fst) A.inverser ∙ f.pres-id ⟩
+      B.unit                                      ∎
+```
+
+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
+underlying $G$ (namely, $(x - y) \in H$), and equip the [quotient] of
+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$.
+
+[quotient]: Data.Set.Coequaliser.html
+
+```agda
+record normal-subgroup (G : Group ℓ) (H : ℙ (G .fst)) : Type ℓ where
+  open Group-on (G .snd)
+  field
+    has-rep : represents-subgroup G H
+    has-conjugate : ∀ {x y} → x ∈ H → (y ⋆ x ⋆ y ⁻¹) ∈ H
+
+  has-conjugatel : ∀ {x y} → y ∈ H → ((x ⋆ y) ⋆ x ⁻¹) ∈ H
+  has-conjugatel yin = subst (_∈ H) associative (has-conjugate yin)
+
+  has-comm : ∀ {x y} → (x ⋆ y) ∈ H → (y ⋆ x) ∈ H
+  has-comm {x = x} {y} ∈ = subst (_∈ H) p (has-conjugate ∈) where
+    p = x ⁻¹ ⋆ (x ⋆ y) ⋆ x ⁻¹ ⁻¹ ≡⟨ ap₂ _⋆_ refl (sym associative) ∙ (λ i → x ⁻¹ ⋆ x ⋆ y ⋆ inv-inv {x = x} i) ⟩
+        x ⁻¹ ⋆ x ⋆ y ⋆ x         ≡⟨ associative ⟩
+        (x ⁻¹ ⋆ x) ⋆ y ⋆ x       ≡⟨ ap₂ _⋆_ inversel refl ∙ idl ⟩
+        y ⋆ x                    ∎
+
+  open represents-subgroup has-rep public
+```
+
+So, suppose we have a normal subgroup $H \unlhd G$. We define the
+underlying type of the quotient $G/H$ to be the quotient of the relation
+$R(x, y) = (x - y) \in H$; It can be equipped with a group operation
+inherited from $G$, but this is _incredibly_ tedious to do.
+
+<!--
+```agda
+module _ (Grp : Group ℓ) {H : ℙ (Grp .fst)} (N : normal-subgroup Grp H) where
+  open normal-subgroup N
+  open Group-on (Grp .snd) renaming (inverse to inv)
+  private
+    G0 = Grp .fst
+    rel : G0 → G0 → Type _
+    rel x y = (x ⋆ y ⁻¹) ∈ H
+
+    rel-refl : ∀ x → rel x x
+    rel-refl _ = subst (_∈ H) (sym inverser) has-unit
+```
+-->
+
+```agda
+    G/H : Type _
+    G/H = G0 / rel
+
+    op : G/H → G/H → G/H
+    op = Quot-op₂ rel-refl rel-refl _⋆_ (λ w x y z a b → rem₃ y z w x b a) where
+```
+
+To prove that the group operation `_⋆_`{.Agda} descends to the quotient,
+we prove that it takes related inputs to related outputs — a
+characterisation of binary operations on quotients we can invoke since
+the relation we’re quotienting by is reflexive. It suffices to show that
+$(yw - zx) \in H$ whenever $w - x$ and $y - z$ are both in $H$, which is
+a tedious but straightforward calculation:
+
+```agda
+      module
+        _ (w x y z : G0)
+          (w-x∈ : (w ⋆ inv x) ∈ H)
+          (y-z∈ : (y ⋆ inv z) ∈ H) where abstract
+        rem₁ : ((w ⋆ inv x) ⋆ (inv z ⋆ y)) ∈ H
+        rem₁ = has-⋆ w-x∈ (has-comm y-z∈)
+
+        rem₂ : ((w ⋆ (inv x ⋆ inv z)) ⋆ y) ∈ H
+        rem₂ = subst (_∈ H) (associative ∙ ap (_⋆ y) (sym associative)) rem₁
+
+        rem₃ : ((y ⋆ w) ⋆ inv (z ⋆ x)) ∈ H
+        rem₃ = subst (_∈ H) (associative ∙ ap₂ _⋆_ refl (sym inv-comm))
+          (has-comm rem₂)
+```
+
+To define inverses on the quotient, it suffices to show that whenever
+$(x - y) \in H$, we also have $(x^{-1} - y) \in H$.
+
+```agda
+    inverse : G/H → G/H
+    inverse =
+      Coeq-rec squash (λ x → inc (inv x)) λ { (x , y , r) → quot (p x y r) }
+      where abstract
+        p : ∀ x y → (x ⋆ inv y) ∈ H → (inv x ⋆ inv (inv y)) ∈ H
+        p x y r = has-comm (subst (_∈ H) inv-comm (has-inv r))
+```
+
+Even after this tedious algebra, it still remains to show that the
+operation is associative and has inverses. Fortunately, since equality
+in a group is a proposition, these follow from the group axioms on $G$
+rather directly:
+
+```agda
+    Group-on-G/H : Group-on G/H
+    Group-on-G/H = make-group squash (inc unit) op inverse
+      (Coeq-elim-prop₃ (λ _ _ _ → squash _ _)
+        λ x y z i → inc (associative {x = x} {y} {z} (~ i)))
+      (Coeq-elim-prop (λ _ → squash _ _) λ x i → inc (inversel {x = x} i))
+      (Coeq-elim-prop (λ _ → squash _ _) λ x i → inc (inverser {x = x} i))
+      (Coeq-elim-prop (λ _ → squash _ _) λ x i → inc (idl {x = x} i))
+
+  _/ᴳ_ : Group _
+  _/ᴳ_ = G/H , Group-on-G/H
+
+  incl : Groups.Hom Grp _/ᴳ_
+  incl .fst = inc
+  incl .snd .Group-hom.pres-⋆ x y = refl
+```
+
+Before we show that the kernel of the quotient map is isomorphic to the
+subgroup we started with (and indeed, that this isomorphism commutes
+with the respective, so that they determine the same subobject of $G$),
+we must show that the relation $(x - y) \in H$ is an equivalence
+relation; We can then appeal to [effectivity of quotients] to conclude
+that, if $\id{inc}(x) = \id{inc}(y)$, then $(x - y) \in H$.
+
+[effectivity of quotients]: Data.Set.Coequaliser.html#effecitivity
+
+```agda
+  private
+    rel-sym : ∀ {x y} → rel x y → rel y x
+    rel-sym h = subst (_∈ H) (inv-comm ∙ ap (_⋆ _) inv-inv) (has-inv h)
+
+    rel-trans : ∀ {x y z} → rel x y → rel y z → rel x z
+    rel-trans {x} {y} {z} h g = subst (_∈ H) p (has-⋆ h g) where
+      p = (x ⋆ y ⁻¹) ⋆ (y ⋆ z ⁻¹) ≡˘⟨ associative ⟩
+          x ⋆ (y ⁻¹ ⋆ (y ⋆ z ⁻¹)) ≡⟨ ap (x ⋆_) associative ⟩
+          x ⋆ ((y ⁻¹ ⋆ y) ⋆ z ⁻¹) ≡⟨ ap (x ⋆_) (ap (_⋆ _) inversel ∙ idl) ⟩
+          x ⋆ z ⁻¹                ∎
+
+  /ᴳ-effective : ∀ {x y} → Path G/H (inc x) (inc y) → rel x y
+  /ᴳ-effective = equiv→inverse
+    (effective (λ _ _ → H _ .is-tr) (rel-refl _) rel-trans rel-sym)
+```
+
+<!--
+```agda
+  private
+    module Ker[incl] = Kernel (Ker incl)
+    Ker-sg = Ker-subgroup incl
+    H-sg = predicate→subgroup H has-rep
+    H-g = H-sg .object ./-Obj.domain
+```
+-->
+
+The two halves of the isomorphism are now very straightforward to
+define: If we have $\id{inc}(x) = \id{inc}(0)$, then $x - 0 \in H$ by
+effectivity, and $x \in H$ by the group laws. Conversely, if $x \in H$,
+then $x - 0 \in H$, thus they are identified in the quotient. Thus, the
+predicate $\id{inc}(x) = \id{inc}(0)$ recovers the subgroup $H$; And
+(the total space of) that predicate is exactly the kernel of $\id{inc}$!
+
+```agda
+  Ker[incl]≅H-group : Ker[incl].ker Groups.≅ H-g
+  Ker[incl]≅H-group = Groups.make-iso to from il ir where
+    to : Groups.Hom _ _
+    to .fst (x , p) = x , subst (_∈ H) (ap (_ ⋆_) inv-unit ∙ idr) x-0∈H where
+      x-0∈H = /ᴳ-effective p
+    to .snd .Group-hom.pres-⋆ _ _ = Σ-prop-path (λ _ → H _ .is-tr) refl
+
+    from : Groups.Hom _ _
+    from .fst (x , p) = x , quot (subst (_∈ H) (sym idr ∙ ap (_ ⋆_) (sym inv-unit)) p)
+    from .snd .Group-hom.pres-⋆ _ _ = Σ-prop-path (λ _ → squash _ _) refl
+
+    il = Forget-is-faithful $ funext λ x → Σ-prop-path (λ _ → H _ .is-tr) refl
+    ir = Forget-is-faithful $ funext λ x → Σ-prop-path (λ _ → squash _ _) refl
+```
+
+To show that these are equal as subgroups of $G$, we must show that the
+isomorphism above commutes with the inclusions; But this is immediate by
+computation, so we can conclude: Every normal subgroup is a kernel.
+
+```
+  Ker[incl]≡H↪G : Ker-sg ≡ H-sg
+  Ker[incl]≡H↪G = antisym ker≤H H≤ker where
+    SubG = Subobjects (Groups ℓ) Groups-is-category Grp
+    open Poset SubG
+    open Groups._≅_ Ker[incl]≅H-group
+
+    ker≤H : Ker-sg ≤ H-sg
+    ker≤H ./-Hom.map = to
+    ker≤H ./-Hom.commutes = Forget-is-faithful refl
+
+    H≤ker : H-sg ≤ Ker-sg
+    H≤ker ./-Hom.map = from
+    H≤ker ./-Hom.commutes = Forget-is-faithful refl
+```

src/Algebra/Prelude.agda

@@ -7,6 +7,7 @@ open import Cat.Instances.Slice public
 open import Cat.Functor.Base public
 open import Cat.Univalent public
 open import Cat.Prelude public
+open import Cat.Thin using (Poset ; Proset) public
 
 import Cat.Diagram.Coequaliser
 import Cat.Diagram.Coproduct