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 = Subobject 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 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 we can associate two canonical subgroups, one of and one of image factorisation, written is the subgroup of “reachable by mapping through ”, and 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 =
    record { map   = kernel
           ; monic = 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

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 (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 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 { 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 (which is a subobject of , equipped with 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)

Note

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 : 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 : ⌞ 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 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 (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 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 (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 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 (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 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₂ 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 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} 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 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.

    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 (λ 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 = 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

  _/á´³_ : 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 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

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! 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 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)