This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Epimorphisms in groups

module group-theory.epimorphisms-groups where

open import category-theory.epimorphisms-in-large-precategories

open import foundation.propositions
open import foundation.universe-levels

open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.isomorphisms-groups
open import group-theory.precategory-of-groups

Idea

A group homomorphism f : G → H is an epimorphism if the precomposition function

  - ∘ f : hom-set-Group H K → hom-set-Group G K

is an embedding for any group K. In other words, f is an epimorphism if for any two group homomorphisms g h : H → K we have that g ∘ f = h ∘ f implies g = h.

Definition

module _
  {l1 l2 : Level} (l3 : Level) (G : Group l1)
  (H : Group l2) (f : hom-Group G H)
  where

  is-epi-prop-hom-Group : Prop (l1 ⊔ l2 ⊔ lsuc l3)
  is-epi-prop-hom-Group =
    is-epi-prop-Large-Precategory Group-Large-Precategory l3 G H f

  is-epi-hom-Group : UU (l1 ⊔ l2 ⊔ lsuc l3)
  is-epi-hom-Group = type-Prop is-epi-prop-hom-Group

  is-prop-is-epi-hom-Group : is-prop is-epi-hom-Group
  is-prop-is-epi-hom-Group = is-prop-type-Prop is-epi-prop-hom-Group

Properties

Isomorphisms are epimorphisms

module _
  {l1 l2 : Level} (l3 : Level) (G : Group l1)
  (H : Group l2) (f : iso-Group G H)
  where

  is-epi-iso-Group : is-epi-hom-Group l3 G H (hom-iso-Group G H f)
  is-epi-iso-Group =
    is-epi-iso-Large-Precategory Group-Large-Precategory l3 G H f

A group homomorphism is surjective if and only if it is an epimorphism

Proof using the law of excluded middle: The forward direction of this claim is the easier of the two directions, and this part of the proof doesn't require the law of excluded middle. If f is surjective and g h : H → K are two group homomorphisms such that g ∘ f ＝ h ∘ f, then to show that g ＝ h it suffices to show that g y ＝ h y for any y : H. Since we are proving a proposition and f is assumed to be surjective, we may assume x : G equipped with an identification f x ＝ y. It therefore suffices to show that g (f x) ＝ h (f x), which was assumed.

For the converse, suppose that f : G → H is an epimorphism and consider the image subgroup I := im f of H. We first show that I is normal, and then we show that I ＝ H.

In order to show that I is normal, we want to show that I has only one conjugacy class, namely itself. Consider the group K of permutations of the set of conjugate subgroups of the subgroup I of H. There is a group homomorphism α : H → K given by h ↦ J ↦ hJh⁻¹, where J ranges over the conjugacy classes of I. Notice that I itself is a fixed point of the conjugation operation J ↦ f(x)Jf(x)⁻¹, i.e., I is a fixed point of α(f(x)). We claim that there is another homomorphism β : H → K given by h ↦ α(h) ∘ (I h⁻¹Ih), where we precompose with the transposition (I h⁻¹Ih). This transposition is defined using the law of excluded middle. However, note that I is always a fixed point of β(h), for any h : H. Furthermore, we have α(f(x)) ＝ β(f(x)). Therefore it follows from the assumption that f is an epimorphism that α ＝ β. In other words, I is a fixed point of any conjugation operation J ↦ hJh⁻¹. We conclude that I is normal.

Since I is normal, we may consider the quotient group H/I. Now we observe that the quotient map maps f(x) to the unit of H/I. Using the assumption that f is an epimorphism once more, we conclude that the quotient map H → H/I is the trivial homomorphism. Therefore it follows that I ＝ H. This completes the proof.