Source: ProCGroups.GroupTheory.Subgroups
1import Mathlib.GroupTheory.QuotientGroup.Basic
2import Mathlib.Topology.Algebra.OpenSubgroup
4/-!
5# Quotients by kernels
7This module realizes the quotient by the kernel of a homomorphism as an injective homomorphism
8into the target and records its value on quotient representatives.
9-/
11namespace ProCGroups.GroupTheory
13universe u
15variable {G : Type u} [Group G]
17/-- The canonical embedding of a kernel quotient into the target range, viewed in the target. -/
18noncomputable def quotientKerEmbedding
19 {G T : Type u} [Group G] [Group T] (φ : G →* T) :
20 G ⧸ φ.ker →* T :=
21 φ.range.subtype.comp (QuotientGroup.quotientKerEquivRange φ).toMonoidHom
23/-- The quotient-kernel embedding is injective. -/
24theorem quotientKerEmbedding_injective
25 {G T : Type u} [Group G] [Group T] (φ : G →* T) :
26 Function.Injective (quotientKerEmbedding φ) := by
27 exact
28 φ.range.subtype_injective.comp
29 (QuotientGroup.quotientKerEquivRange φ).injective
31/-- The quotient-kernel embedding sends a representative to the corresponding kernel coset. -/
32theorem quotientKerEmbedding_mk
33 {G T : Type u} [Group G] [Group T] (φ : G →* T) (x : G) :
34 quotientKerEmbedding φ (QuotientGroup.mk' φ.ker x) = φ x := by
35 rfl
37end ProCGroups.GroupTheory