module Algebra.Group.Subgroup where
Subgroupsπ
A subgroup of a group is a monomorphism , that is, an object of the poset of subobjects . Since group homomorphisms are injective exactly when their underlying function is an embedding, we can alternatively describe this as a condition on a predicate .
Subgroup : Group β β Type (lsuc β) Subgroup {β = β} G = Ξ£ (Group β) Ξ» H β H Groups.βͺ G
A proposition
of a group
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 represents a subgroup, then its total space inherits a group structure from , and the first projection 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 we can associate two canonical subgroups, one of and one of : βs image factorisation, written , is the subgroup of βreachable by mapping through β, and βs kernel, written , is the subgroup of which sends to the unit.
The kernel can be cheapily described as a limit: It is the equaliser of and the zero morphism β which, recall, is the unique map which breaks down as .
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
has an image factorisation
,
defined by equipping its set-theoretic image
with a group structure
inherited from
.
More concretely, we can describe the elements of
as the βmere fibresβ of
:
They consist of a point
,
together with (the truncation of) a fibre of
over
.
We multiply
(in the fibre over
)
with
(in the fibre over
),
giving the element
in the fibre over
.
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 (f #_)} β x .fst β‘ y .fst β x β‘ y Tpath {x} {y} p = Ξ£-prop-path (Ξ» _ β squash) p abstract Tset : is-set (image (f #_)) Tset = hlevel 2 module Kerf = Kernel (Ker f)
For reasons that will become clear later, we denote the image of , when regarded as its own group, by , and reserve the notation for that group regarded as a subgroup of .
The construction of a group structure on
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
deserves the name βimageβ comes from
breaking down as a (regular) epimorphism into
(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 as .
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 (which is a subobject of , equipped with βs group operation) by is the first isomorphism theorem (though we phrase it more categorically): The image of serves as a quotient for (the congruence generated by) .
In more classical texts, the first isomorphism theorem is phrased in terms of two pre-existing objects (defined as the set of cosets of regarded as a subgroup) and (defined as above). Here we have opted for a more categorical phrasing of that theorem: We know what the universal property of 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 is a coequaliser (hence that it is a regular epi, as we mentioned above).
The condition placed on is that ; This means that it, like , sends everything in to zero (this is the defining property of ). Note that in the code below we do not elide the zero composite .
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 is constant when thought of as a map ; In other words, it means that is βindependent of the choice of representativeβ. This follows from algebraic manipulation of group homomorphisms + the assumed identity ;
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 is constant on a specific subsetβ to βshow that when β; 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
,
then
,
so the quotient map
does indeed coequalise
and
.
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 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 definitely represents a subgroup, in the sense introduced above β so thereβs definitely a group homomorphism . All we need to figure out is whether there exists a group and a map , such that as subgroups of .
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 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 is also closed under conjugation by elements of the enveloping group, in that if (quickly switching to βmultiplicativeβ notation for the unit), then must be as well: for we have .
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 is closed under conjugation, then generates an equivalence relation on the set underlying (namely, ), and equip the quotient of this equivalence relation with a group structure. The kernel of the quotient map is then . We call a predicate representing a kernel a normal subgroup, and we denote this in shorthand by .
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 . We define the underlying type of the quotient to be the quotient of the relation ; It can be equipped with a group operation inherited from , 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
whenever
and
are both in
,
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 , we also have .
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 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 ), we must show that the relation is an equivalence relation; We can then appeal to effectivity of quotients to conclude that, if , then .
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)
private module Ker[incl] = Kernel (Ker incl) Ker-sg = Ker-subgroup incl H-sg = predicateβsubgroup H has-rep H-g = H-sg .fst
The two halves of the isomorphism are now very straightforward to define: If we have , then by effectivity, and by the group laws. Conversely, if , then , thus they are identified in the quotient. Thus, the predicate recovers the subgroup ; And (the total space of) that predicate is exactly the kernel of !
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 , 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