module Algebra.Group.Subgroup where

SubgroupsπŸ”—

A subgroup mm of a group GG is a monomorphism Hβ†’mGH \xrightarrow{m} G, that is, an object of the poset of subobjects Sub⁑(G)\operatorname*{Sub}(G). Since group homomorphisms are injective exactly when their underlying function is an embedding, we can alternatively describe this as a condition on a predicate Gβ†’PropG \to \mathrm{Prop}.

Subgroup : Group β„“ β†’ Type (lsuc β„“)
Subgroup {β„“ = β„“} G = Ξ£ (Group β„“) Ξ» H β†’ H Groups.β†ͺ G

A proposition H:Gβ†’PropH : G \to \mathrm{Prop} of a group (G,⋆)(G, \star) represents a subgroup if it contains the group unit, is closed under multiplication, and is closed under inverses.

record represents-subgroup (G : Group β„“) (H : β„™ ⌞ G ⌟) : Type β„“ where
  open Group-on (G .snd)

  field
    has-unit : unit ∈ H
    has-⋆    : βˆ€ {x y} β†’ x ∈ H β†’ y ∈ H β†’ (x ⋆ y) ∈ H
    has-inv  : βˆ€ {x} β†’ x ∈ H β†’ x ⁻¹ ∈ H

If HH represents a subgroup, then its total space ΣH\Sigma H inherits a group structure from GG, and the first projection ΣH→G\Sigma H \to G is a group homormophism.

rep-subgroup→group-on
  : (H : β„™ ⌞ G ⌟) β†’ represents-subgroup G H β†’ Group-on (Ξ£[ x ∈ ⌞ G ⌟ ] x ∈ H)
rep-subgroup→group-on {G = G} H sg = to-group-on sg′ where
  open Group-on (G .snd)
  open represents-subgroup sg
  sgβ€² : make-group (Ξ£[ x ∈ ⌞ G ⌟ ] x ∈ H)
  sgβ€² .make-group.group-is-set = hlevel!
  sgβ€² .make-group.unit = unit , has-unit
  sgβ€² .make-group.mul (x , x∈) (y , y∈) = x ⋆ y , has-⋆ x∈ y∈
  sgβ€² .make-group.inv (x , x∈) = x ⁻¹ , has-inv x∈
  sgβ€² .make-group.assoc x y z = Ξ£-prop-path (Ξ» x β†’ H x .is-tr) associative
  sgβ€² .make-group.invl x = Ξ£-prop-path (Ξ» x β†’ H x .is-tr) inversel
  sgβ€² .make-group.idl x = Ξ£-prop-path (Ξ» x β†’ H x .is-tr) idl

predicateβ†’subgroup : (H : β„™ ⌞ G ⌟) β†’ represents-subgroup G H β†’ Subgroup G
predicate→subgroup {G = G} H p = _ , record { mor = map ; monic = ism } where
  map : Groups.Hom (el! (Ξ£ _ (∣_∣ βŠ™ H))
    , rep-subgroup→group-on H p) G
  map .hom = fst
  map .preserves .is-group-hom.pres-⋆ x y = refl

  ism : Groups.is-monic map
  ism = Homomorphism-monic map (Ξ» p β†’ Ξ£-prop-path (Ξ» _ β†’ hlevel!) p)

Kernels and ImagesπŸ”—

To a group homomorphism f:Aβ†’Bf : A \to B we can associate two canonical subgroups, one of AA and one of BB: ff’s image factorisation, written im⁑f\operatorname*{im}f, is the subgroup of BB β€œreachable by mapping through ff”, and ff’s kernel, written ker⁑f\ker f, is the subgroup of AA which ff sends to the unit.

The kernel can be cheapily described as a limit: It is the equaliser of ff and the zero morphism — which, recall, is the unique map A→BA \to B which breaks down as A→0→BA \to 0 \to B.

module _ {β„“} where
  open Canonical-kernels (Groups β„“) βˆ…α΄³ Groups-equalisers public

  Ker-subgroup : βˆ€ {A B : Group β„“} β†’ Groups.Hom A B β†’ Subgroup A
  Ker-subgroup f =
    ker , record { mor = kernel
                 ; monic = Groups.is-equaliser→is-monic _ has-is-kernel }
    where
      open Kernel (Ker f)

Every group homomorphism f:Aβ†’Bf : A \to B has an image factorisation im⁑f\operatorname*{im}f, defined by equipping its set-theoretic image with a group structure inherited from BB. More concretely, we can describe the elements of im⁑f\operatorname*{im}f as the β€œmere fibres” of ff: They consist of a point y:By : B, together with (the truncation of) a fibre of ff over yy. We multiply xx (in the fibre over aa) with yy (in the fibre over bb), giving the element xyxy in the fibre over abab.

For reasons that will become clear later, we denote the image of ff, when regarded as its own group, by A/ker⁑(f)A/\ker(f), and reserve the notation im⁑f\operatorname*{im}f for that group regarded as a subgroup of BB.

The construction of a group structure on A/ker⁑(f)A/\ker(f) is unsurprising, so we leave it in this <details> tag for the curious reader.
    T : Type β„“
    T = image (f #_)

  A/ker[_] : Group β„“
  A/ker[_] = to-group grp where
    unit : T
    unit = B.unit , inc (A.unit , f.pres-id)

    inv : T β†’ T
    inv (x , p) = x B.⁻¹ ,
      βˆ₯-βˆ₯-map (Ξ» { (y , p) β†’ y A.⁻¹ , f.pres-inv βˆ™ ap B._⁻¹ p }) p

    mul : T β†’ T β†’ T
    mul (x , xp) (y , yp) = x B.⋆ y ,
      βˆ₯-βˆ₯-elimβ‚‚ (Ξ» _ _ β†’ squash)
        (Ξ» { (x* , xp) (y* , yp)
           β†’ inc (x* A.⋆ y* , f.pres-⋆ _ _ βˆ™ apβ‚‚ B._⋆_ xp yp) })
        xp yp

    grp : make-group T
    grp .make-group.group-is-set = Tset
    grp .make-group.unit = unit
    grp .make-group.mul = mul
    grp .make-group.inv = inv
    grp .make-group.assoc = Ξ» x y z β†’ Tpath B.associative
    grp .make-group.invl = Ξ» x β†’ Tpath B.inversel
    grp .make-group.idl = Ξ» x β†’ Tpath B.idl

That the canonical inclusion map A/ker⁑(f)β†ͺBA/\ker(f) \hookrightarrow B deserves the name β€œimage” comes from ff breaking down as a (regular) epimorphism into im⁑f\operatorname*{im}f (written Aβ†’im), followed by that map:

(Aβ†’fB)=(Aβ† fA/ker⁑(f)β†ͺB) (A \xrightarrow{f} B) = (A \xtwoheadrightarrow{f} A/\ker(f) \hookrightarrow B)

  A→im : Groups.Hom A A/ker[_]
  A→im .hom x = f # x , inc (x , refl)
  Aβ†’im .preserves .is-group-hom.pres-⋆ x y = Tpath (f.pres-⋆ _ _)

  im→B : Groups.Hom A/ker[_] B
  im→B .hom (b , _) = b
  imβ†’B .preserves .is-group-hom.pres-⋆ x y = refl

When this monomorphism is taken as primary, we refer to A/ker⁑(f)A/\ker(f) as im⁑f\operatorname*{im}f.

  Im[_] : Subgroup B
  Im[_] = _ , record { mor = imβ†’B ; monic = imβ†ͺB } where
    imβ†ͺB : Groups.is-monic imβ†’B
    imβ†ͺB = Homomorphism-monic imβ†’B Tpath

The first isomorphism theoremπŸ”—

The reason for denoting the set-theoretic image of f:Aβ†’Bf : A \to B (which is a subobject of BB, equipped with BB’s group operation) by A/ker⁑(f)A/\ker(f) is the first isomorphism theorem (though we phrase it more categorically): The image of ff serves as a quotient for (the congruence generated by) ker⁑f\ker f.

Note

In more classical texts, the first isomorphism theorem is phrased in terms of two pre-existing objects A/ker⁑(f)A/\ker(f) (defined as the set of cosets of ker⁑(f)\ker(f) regarded as a subgroup) and im⁑f\operatorname*{im}f (defined as above). Here we have opted for a more categorical phrasing of that theorem: We know what the universal property of A/ker⁑(f)A/\ker(f) is β€” namely that it is a specific colimit β€” so the specific construction used to implement it does not matter.

  1st-iso-theorem : Groups.is-coequaliser (Groups.Zero.zeroβ†’ βˆ…α΄³) Kerf.kernel Aβ†’im
  1st-iso-theorem = coeq where
    open Groups
    open is-coequaliser
    module Ak = Group-on (A/ker[_] .snd)

More specifically, in a diagram like the one below, the indicated dotted arrow always exists and is unique, witnessing that the map Aβ† A/ker⁑(f)A \twoheadrightarrow A/\ker(f) is a coequaliser (hence that it is a regular epi, as we mentioned above).

The condition placed on eβ€²e' is that 0=eβ€²βˆ˜ker⁑f0 = e' \circ \ker f; This means that it, like ff, sends everything in ker⁑f\ker f to zero (this is the defining property of ker⁑f\ker f). Note that in the code below we do not elide the zero composite eβ€²βˆ˜0e' \circ 0.

    elim
      : βˆ€ {F} {e' : Groups.Hom A F}
          (p : e' Groups.∘ Zero.zeroβ†’ βˆ…α΄³ ≑ e' Groups.∘ Kerf.kernel)
      β†’ βˆ€ {x} β†’ βˆ₯ fibre (f #_) x βˆ₯ β†’ _
    elim {F = F} {e' = e'} p {x} =
      βˆ₯-βˆ₯-rec-set ((e' #_) βŠ™ fst) const (F .snd .Group-on.has-is-set) where abstract
      module e' = is-group-hom (e' .preserves)
      module F = Group-on (F .snd)

To eliminate from under a propositional truncation, we must prove that the map eβ€²e' is constant when thought of as a map fβˆ—(x)β†’Ff^*(x) \to F; In other words, it means that eβ€²e' is β€œindependent of the choice of representative”. This follows from algebraic manipulation of group homomorphisms + the assumed identity 0=eβ€²βˆ˜ker⁑f0 = e' \circ \ker f;

      constβ€² : βˆ€ (x y : fibre (f #_) x)
             β†’ e' # (x .fst) F.β€” e' # (y .fst) ≑ F.unit
      constβ€² (y , q) (z , r) =
        e' # y F.β€” e' # z  β‰‘Λ˜βŸ¨ e'.pres-diff βŸ©β‰‘Λ˜
        e' # (y A.β€” z)     β‰‘βŸ¨ happly (sym (ap hom p)) (y A.β€” z , aux) βŸ©β‰‘
        e' # A.unit        β‰‘βŸ¨ e'.pres-id βŸ©β‰‘
        F.unit             ∎
        where

This assumption allows us to reduce β€œshow that eβ€²e' is constant on a specific subset” to β€œshow that f(yβˆ’z)=0f(y - z) = 0 when f(y)=f(z)=xf(y) = f(z) = x”; But that’s just algebra, hence uninteresting:

          aux : f # (y A.β€” z) ≑ B.unit
          aux =
            f # (y A.β€” z)     β‰‘βŸ¨ f.pres-diff βŸ©β‰‘
            f # y B.β€” f # z   β‰‘βŸ¨ apβ‚‚ B._β€”_ q r βŸ©β‰‘
            x B.β€” x           β‰‘βŸ¨ B.inverser βŸ©β‰‘
            B.unit            ∎

      const : βˆ€ (x y : fibre (f #_) x) β†’ e' # (x .fst) ≑ e' # (y .fst)
      const a b = F.zero-diff (constβ€² a b)

The rest of the construction is almost tautological: By definition, if x:ker⁑fx : \ker f, then f(x)=0f(x) = 0, so the quotient map Aβ† A/ker⁑(f)A \twoheadrightarrow A/\ker(f) does indeed coequalise ker⁑fβ†ͺA\ker f \hookrightarrow A and 00. As a final word on the rest of the construction, most of it is applying induction (βˆ₯-βˆ₯-elim and friends) so that our colimiting map elim will compute.

    coeq : is-coequaliser _ _ A→im
    coeq .coequal = Forget-is-faithful (funext path) where
      path : (x : ⌞ Kerf.ker ⌟) β†’ Aβ†’im # A.unit ≑ Aβ†’im # (x .fst)
      path (x* , p) = Tpath (f.pres-id βˆ™ sym p)

    coeq .universal {F = F} {eβ€² = e'} p = gh where
      module F = Group-on (F .snd)
      module e' = is-group-hom (e' .preserves)

      gh : Groups.Hom _ _
      gh .hom (x , t) = elim {e' = e'} p t
      gh .preserves .is-group-hom.pres-⋆ (x , q) (y , r) =
        βˆ₯-βˆ₯-elimβ‚‚
          {P = Ξ» q r β†’ elim p (((x , q) Ak.⋆ (y , r)) .snd) ≑ elim p q F.⋆ elim p r}
          (Ξ» _ _ β†’ F.has-is-set _ _) (Ξ» x y β†’ e'.pres-⋆ _ _) q r

    coeq .factors = Forget-is-faithful refl

    coeq .unique {F} {p = p} {colim = colim} prf = Forget-is-faithful (funext path)
      where abstract
        module F = Group-on (F .snd)
        path : βˆ€ x β†’ colim # x ≑ elim p (x .snd)
        path (x , t) =
          βˆ₯-βˆ₯-elim
            {P = Ξ» q β†’ colim # (x , q) ≑ elim p q}
            (Ξ» _ β†’ F.has-is-set _ _)
            (Ξ» { (f , fp) β†’ ap (colim #_) (Ξ£-prop-path (Ξ» _ β†’ squash) (sym fp))
                          βˆ™ (happly (ap hom prf) f) })
            t

Representing kernelsπŸ”—

If an evil wizard kidnaps your significant others and demands that you find out whether a predicate P:Gβ†’PropP : G \to \mathrm{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 PP definitely represents a subgroup, in the sense introduced above β€” so there’s definitely a group homomorphism Ξ£Gβ†ͺG\Sigma G \hookrightarrow G. All we need to figure out is whether there exists a group HH and a map f:Gβ†’Hf : G \to H, such that Ξ£Gβ‰…ker⁑f\Sigma G \cong \ker f as subgroups of GG.

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 00 is inhabited, and they are closed under multiplication and inverses, though we shall not make note of that here).

module _ {β„“} {A B : Group β„“} (f : Groups.Hom A B) where private
  module Ker[f] = Kernel (Ker f)
  module f = is-group-hom (f .preserves)
  module A = Group-on (A .snd)
  module B = Group-on (B .snd)

  kerf : ⌞ Ker[f].ker ⌟ β†’ ⌞ A ⌟
  kerf = Ker[f].kernel .hom

  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\ker f is also closed under conjugation by elements of the enveloping group, in that if f(x)=1f(x) = 1 (quickly switching to β€œmultiplicative” notation for the unit), then f(yxyβˆ’1)f(yxy^{-1}) must be 11 as well: for we have f(y)f(x)f(yβˆ’1)=f(y)1f(yβˆ’1)=f(yyβˆ’1)=f(1)=1f(y)f(x)f(y^{-1}) = f(y)1f(y^{-1}) = f(yy^{-1}) = f(1) = 1.

  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 # (y A.⋆ (x A.β€” y))         β‰‘βŸ¨ ap (f #_) A.associative βŸ©β‰‘
      f # ((y A.⋆ x) A.β€” y)         β‰‘βŸ¨ f.pres-diff βŸ©β‰‘
      ⌜ f # (y A.⋆ x) ⌝ B.β€” f # y   β‰‘βŸ¨ ap! (f.pres-⋆ y x) βŸ©β‰‘
      ⌜ f # y B.⋆ f # x ⌝ B.β€” f # y β‰‘βŸ¨ ap! (ap (_ B.⋆_) (ap (f #_) (sym q) βˆ™ p) βˆ™ B.idr) βŸ©β‰‘
      f # y B.β€” f # y               β‰‘Λ˜βŸ¨ f.pres-diff βŸ©β‰‘Λ˜
      f # (y A.β€” y)                 β‰‘βŸ¨ ap (f #_) 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 HH is closed under conjugation, then HH generates an equivalence relation on the set underlying GG (namely, (xβˆ’y)∈H(x - y) \in H), and equip the quotient of this equivalence relation with a group structure. The kernel of the quotient map Gβ†’G/HG \to G/H is then HH. We call a predicate representing a kernel a normal subgroup, and we denote this in shorthand by H⊴GH \unlhd G.

record normal-subgroup (G : Group β„“) (H : β„™ ⌞ G ⌟) : 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Β‘ associative βŸ©β‰‘Λ˜
        x ⁻¹ ⋆ x ⋆ y ⋆ ⌜ x ⁻¹ ⁻¹ ⌝   β‰‘βŸ¨ ap! inv-inv βŸ©β‰‘
        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⊴GH \unlhd G. We define the underlying type of the quotient G/HG/H to be the quotient of the relation R(x,y)=(xβˆ’y)∈HR(x, y) = (x - y) \in H; It can be equipped with a group operation inherited from GG, but this is incredibly tedious to do.

    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 _⋆_ 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)∈H(yw - zx) \in H whenever wβˆ’xw - x and yβˆ’zy - z are both in HH, which is a tedious but straightforward calculation:

      module
        _ (w x y z : G0)
          (w-x∈ : (w ⋆ inv x) ∈ H)
          (y-z∈ : (y ⋆ inv z) ∈ H) where abstract
        rem₁ : ((w β€” x) ⋆ (inv z ⋆ y)) ∈ H
        rem₁ = has-⋆ w-x∈ (has-comm y-z∈)

        remβ‚‚ : ((w ⋆ (inv x β€” z)) ⋆ y) ∈ H
        remβ‚‚ = subst (_∈ H) (associative βˆ™ ap (_⋆ y) (sym associative)) rem₁

        rem₃ : ((y ⋆ w) β€” (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)∈H(x - y) \in H, we also have (xβˆ’1βˆ’y)∈H(x^{-1} - y) \in H.

    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 β€” y) ∈ H β†’ (inv x β€” 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 GG rather directly:

    Group-on-G/H : make-group G/H
    Group-on-G/H .make-group.group-is-set = squash
    Group-on-G/H .make-group.unit = inc unit
    Group-on-G/H .make-group.mul = op
    Group-on-G/H .make-group.inv = inverse
    Group-on-G/H .make-group.assoc =
      Coeq-elim-prop₃ (Ξ» _ _ _ β†’ squash _ _) Ξ» x y z i β†’
        inc (associative {x = x} {y} {z} i)
    Group-on-G/H .make-group.invl =
      Coeq-elim-prop (Ξ» _ β†’ squash _ _) Ξ» x i β†’ inc (inversel {x = x} i)
    Group-on-G/H .make-group.idl =
      Coeq-elim-prop (Ξ» _ β†’ squash _ _) Ξ» x i β†’ inc (idl {x = x} i)

  _/α΄³_ : Group _
  _/α΄³_ = to-group Group-on-G/H

  incl : Groups.Hom Grp _/α΄³_
  incl .hom = inc
  incl .preserves .is-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 GG), we must show that the relation (xβˆ’y)∈H(x - y) \in H is an equivalence relation; We can then appeal to effectivity of quotients to conclude that, if inc(x)=inc(y)\mathrm{inc}(x) = \mathrm{inc}(y), then (xβˆ’y)∈H(x - y) \in H.

  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! associative βŸ©β‰‘
          x ⋆ ⌜ (y ⁻¹ ⋆ y) β€” z ⌝ β‰‘βŸ¨ ap! (ap (_⋆ _) inversel βˆ™ idl) βŸ©β‰‘
          x β€” z                  ∎

  open Congruence
  normal-subgroup→congruence : Congruence _ _
  normal-subgroupβ†’congruence ._∼_ = rel
  normal-subgroup→congruence .has-is-prop x y = hlevel!
  normal-subgroupβ†’congruence .reflᢜ = rel-refl _
  normal-subgroupβ†’congruence ._βˆ™αΆœ_ = rel-trans
  normal-subgroupβ†’congruence .symᢜ = rel-sym

  /α΄³-effective : βˆ€ {x y} β†’ Path G/H (inc x) (inc y) β†’ rel x y
  /ᴳ-effective = equiv→inverse (effective normal-subgroup→congruence)

The two halves of the isomorphism are now very straightforward to define: If we have inc(x)=inc(0)\mathrm{inc}(x) = \mathrm{inc}(0), then xβˆ’0∈Hx - 0 \in H by effectivity, and x∈Hx \in H by the group laws. Conversely, if x∈Hx \in H, then xβˆ’0∈Hx - 0 \in H, thus they are identified in the quotient. Thus, the predicate inc(x)=inc(0)\mathrm{inc}(x) = \mathrm{inc}(0) recovers the subgroup HH; And (the total space of) that predicate is exactly the kernel of inc\mathrm{inc}!

  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 .hom (x , p) = x , subst (_∈ H) (ap (_ ⋆_) inv-unit βˆ™ idr) x-0∈H where
      x-0∈H = /ᴳ-effective p
    to .preserves .is-group-hom.pres-⋆ _ _ = Ξ£-prop-path (Ξ» _ β†’ H _ .is-tr) refl

    from : Groups.Hom _ _
    from .hom (x , p) = x , quot (subst (_∈ H) (sym idr βˆ™ ap (_ ⋆_) (sym inv-unit)) p)
    from .preserves .is-group-hom.pres-⋆ _ _ = Ξ£-prop-path (Ξ» _ β†’ squash _ _) refl

    il = Homomorphism-path Ξ» x β†’ Ξ£-prop-path (Ξ» _ β†’ H _ .is-tr) refl
    ir = Homomorphism-path Ξ» x β†’ Ξ£-prop-path (Ξ» _ β†’ squash _ _) refl

To show that these are equal as subgroups of GG, 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 .fst = to
    ker≀H .snd = Forget-is-faithful refl

    H≀ker : H-sg ≀ Ker-sg
    H≀ker .fst = from
    H≀ker .snd = Forget-is-faithful refl