module Algebra.Group.Subgroup where

private variable ℓ ℓ' : Level G : Group ℓ private module _ {ℓ} where open Cat.Displayed.Instances.Subobjects (Groups ℓ) public

# Subgroups🔗

A **subgroup**
$m$
of a group
$G$
is a monomorphism
$Hm G,$
that is, an object of the poset
of subobjects
$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→Prop.$

Subgroup : Group ℓ → Type (lsuc ℓ) Subgroup {ℓ = ℓ} G = Subobject G

A proposition
$H:G→Prop$
of a group
$(G,⋆)$
**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 $H$ represents a subgroup, then its total space $ΣH$ inherits a group structure from $G,$ and the first projection $ΣH→G$ is a group homomorphism.

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 2 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! associative sg' .make-group.invl x = Σ-prop-path! inversel sg' .make-group.idl x = Σ-prop-path! idl predicate→subgroup : (H : ℙ ⌞ G ⌟) → represents-subgroup G H → Subgroup G predicate→subgroup {G = G} H p = record { map = it ; monic = ism } where it : Groups.Hom (el! (Σ _ (∣_∣ ⊙ H)) , rep-subgroup→group-on H p) G it .hom = fst it .preserves .is-group-hom.pres-⋆ x y = refl ism : Groups.is-monic it ism = Homomorphism-monic it λ p → Σ-prop-path! p

# Kernels and images🔗

To a group homomorphism
$f:A→B$
we can associate two canonical subgroups, one of
$A$
and one of
$B:$
$f’s$
**image
factorisation**, written
$imf,$
is the subgroup of
$B$
“reachable by mapping through
$f$”,
and
$f’s$
**kernel**,
written
$kerf,$
is the subgroup of
$A$
which
$f$
sends to the unit.

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

module _ {ℓ} where open Canonical-kernels (Groups ℓ) ∅ᴳ Groups-equalisers public Ker-subgroup : ∀ {A B : Group ℓ} → Groups.Hom A B → Subgroup A Ker-subgroup f = record { map = kernel ; monic = is-equaliser→is-monic _ has-is-kernel } where open Kernel (Ker f)

Every group homomorphism
$f:A→B$
has an image factorisation
$imf,$
defined by equipping its set-theoretic `image`

with a group structure
inherited from
$B.$
More concretely, we can describe the elements of
$imf$
as the “mere fibres” of
$f:$
They consist of a point
$y:B,$
together with (the truncation of) a fibre of
$f$
over
$y.$
We multiply
$x$
(in the fibre over
$a)$
with
$y$
(in the fibre over
$b),$
giving the element
$xy$
in the fibre over
$ab.$

module _ {ℓ} {A B : Group ℓ} (f : Groups.Hom A B) where private module A = Group-on (A .snd) module B = Group-on (B .snd) module f = is-group-hom (f .preserves) Tpath : {x y : image (apply f)} → x .fst ≡ y .fst → x ≡ y Tpath {x} {y} p = Σ-prop-path! p abstract Tset : is-set (image (apply f)) Tset = hlevel 2 module Kerf = Kernel (Ker f)

For reasons that will become clear later, we denote the image of
$f,$
when regarded as its own group, by
$A/ker(f),$
and reserve the notation
$imf$
for that group regarded *as a subgroup of
$B$*.

##
The construction of a group structure on
$A/ker(f)$
is unsurprising, so we leave it in this `<details>`

tag
for the curious reader.

T : Type ℓ T = image (apply 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)↪B$
deserves the name “image” comes from
$f$
breaking down as a (regular) epimorphism into
$imf$
(written `A→im`

), followed by that
map:

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)$ as $imf.$

Im[_] : Subgroup B Im[_] = record { map = 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→B$
(which is a subobject **of
$B$**,
equipped with
$B’s$
group operation) by
$A/ker(f)$
is the **first isomorphism theorem** (though we phrase it
more categorically): The image of
$f$
serves as a quotient for (the
congruence generated by)
$kerf.$

In more classical texts, the first isomorphism theorem is phrased in
terms of two *pre-existing* objects
$A/ker(f)$
(defined as the set of *cosets* of
$ker(f)$
regarded as a subgroup) and
$imf$
(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)$
is — namely that it is a specific colimit — so the specific construction
used to implement it does not matter.

1st-iso-theorem : 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)$
is a coequaliser (hence that it is a regular epi, as we mentioned
above).

The condition placed on $e_{′}$ is that $0=e_{′}∘kerf;$ This means that it, like $f,$ sends everything in $kerf$ to zero (this is the defining property of $kerf).$ Note that in the code below we do not elide the zero composite $e_{′}∘0.$

elim : ∀ {F} {e' : Groups.Hom A F} (p : e' Groups.∘ Zero.zero→ ∅ᴳ ≡ e' Groups.∘ Kerf.kernel) → ∀ {x : ⌞ B ⌟} → ∥ fibre (apply f) x ∥ → _ elim {F = F} {e' = e'} p {x} = ∥-∥-rec-set (F .snd .Group-on.has-is-set) ((e' #_) ⊙ fst) const 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_{′}$ is constant when thought of as a map $f_{∗}(x)→F;$ In other words, it means that $e_{′}$ is “independent of the choice of representative”. This follows from algebraic manipulation of group homomorphisms + the assumed identity $0=e_{′}∘kerf;$

const' : ∀ (x y : fibre (apply 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_{′}$ is constant on a specific subset” to “show that $f(y−z)=0$ when $f(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 (apply 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:kerf,$
then
$f(x)=0,$
so the quotient map
$A↠A/ker(f)$
does indeed coequalise
$kerf↪A$
and
$0.$
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 (Groups ℓ) (Zero.zero→ ∅ᴳ) Kerf.kernel A→im coeq .coequal = ext λ x p → 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 = Grp↪Sets-is-faithful refl coeq .unique {F} {p = p} {colim = colim} prf = ext λ x y p → ap# colim (Σ-prop-path! (sym p)) ∙ happly (ap hom prf) y

## Representing kernels🔗

If an evil wizard kidnaps your significant others and demands that you find out whether a predicate $P:G→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 — so there’s definitely a group homomorphism $ΣG↪G.$ All we need to figure out is whether there exists a group $H$ and a map $f:G→H,$ such that $ΣG≅kerf$ 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.

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
$kerf$
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.$

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₂ B._—_ (f.pres-⋆ y x) refl ⟩≡ ⌜ f # y B.⋆ f # x ⌝ B.— f # y ≡⟨ ap₂ B._—_ (ap (_ B.⋆_) (ap (f #_) (sym q) ∙ p) ∙ B.idr) refl ⟩≡ 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
$H$
is closed under conjugation, then
$H$
generates an equivalence relation on the set underlying
$G$
(namely,
$(x−y)∈H),$
and equip the quotient of
this equivalence relation with a group structure. The kernel of the
quotient map
$G→G/H$
is then
$H.$
We call a predicate representing a kernel a **normal
subgroup**, and we denote this in shorthand by
$H⊴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} mem = subst (_∈ H) p (has-conjugate mem) 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⊴G.$
We define the underlying type of the quotient
$G/H$
to be the quotient of the relation
$R(x,y)=(x−y)∈H;$
It can be equipped with a group operation inherited from
$G,$
but this is *incredibly* tedious to do.

module _ (Grp : Group ℓ) {H : ℙ ⌞ Grp ⌟} (N : normal-subgroup Grp H) where open normal-subgroup N open Group-on (Grp .snd) renaming (inverse to inv) private G0 = ⌞ Grp ⌟ rel : G0 → G0 → Type _ rel x y = (x ⋆ y ⁻¹) ∈ H rel-refl : ∀ x → rel x x rel-refl _ = subst (_∈ H) (sym inverser) has-unit

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$
whenever
$w−x$
and
$y−z$
are both in
$H,$
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,$ we also have $(x_{−1}−y)∈H.$

inverse : G/H → G/H inverse = Coeq-rec (λ 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 $G$ 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 = elim! λ x y z → ap Coeq.inc associative 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 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 $G),$ we must show that the relation $(x−y)∈H$ is an equivalence relation; We can then appeal to effectivity of quotients to conclude that, if $inc(x)=inc(y),$ then $(x−y)∈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 1 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 = effective normal-subgroup→congruence

private module Ker[incl] = Kernel (Ker incl) Ker-sg = Ker-subgroup incl H-sg = predicate→subgroup H has-rep H-g = H-sg .domain

The two halves of the isomorphism are now very straightforward to define: If we have $inc(x)=inc(0),$ then $x−0∈H$ by effectivity, and $x∈H$ by the group laws. Conversely, if $x∈H,$ then $x−0∈H,$ thus they are identified in the quotient. Thus, the predicate $inc(x)=inc(0)$ recovers the subgroup $H;$ And (the total space of) that predicate is exactly the kernel of $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! 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! refl il = ext λ x x∈H → Σ-prop-path! refl ir = ext λ x x∈H → Σ-prop-path! 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 = done where open Precategory (Sub Grp) open Groups._≅_ Ker[incl]≅H-group ker≤H : Ker-sg ≤ₘ H-sg ker≤H .map = to ker≤H .sq = Grp↪Sets-is-faithful refl H≤ker : H-sg ≤ₘ Ker-sg H≤ker .map = from H≤ker .sq = Grp↪Sets-is-faithful refl done = Sub-is-category Groups-is-category .to-path (Sub-antisym ker≤H H≤ker)