Properties of the Canonical Projection — Statement & Proof

Properties of the Canonical Projection (Theorem # 2700)

Theorem

Edit Issues Pull Requests Attributions Admin

theorem T2700_homomorphism (g h : G) :
    QuotientGroup.mk' N (g * h) = QuotientGroup.mk' N g * QuotientGroup.mk' N h

theorem T2700_kernel :
    (QuotientGroup.mk' N).ker = N

theorem T2700_surjective :
    Function.Surjective (QuotientGroup.mk' N)

Discussion

No discussion available for this theorem.

Proof

[proofplan] The three claims — homomorphism, kernel, surjectivity — each reduce to a single direct verification using the structure of the [Quotient Group](/theorems/790). The homomorphism property is read off the coset multiplication rule $(gN)(hN) = (gh)N$ that defines the operation on $G/N$. The kernel computation uses the fact that the identity of $G/N$ is the coset $N$ itself, and that $gN = N$ exactly when $g \in N$. Surjectivity is immediate from the definition of $G/N$ as the set of all cosets $\{gN : g \in G\}$. [/proofplan] [step:Verify that $\pi$ respects the group operation] Declare the map under consideration as \begin{align*} \pi: G &\to G/N \\ g &\mapsto gN. \end{align*} Let $g, h \in G$. By the [Quotient Group](/theorems/790), the binary operation on $G/N$ is the well-defined coset multiplication $(gN)(hN) = (gh)N$, where well-definedness uses the hypothesis $N \trianglelefteq G$. We compute \begin{align*} \pi(gh) &= (gh)N = (gN)(hN) = \pi(g)\,\pi(h). \end{align*} Since $g, h$ were arbitrary, $\pi$ is a group homomorphism. [/step] [step:Identify the kernel as $N$] The identity element of $G/N$ is the coset $eN = N$, where $e$ is the identity of $G$. By definition of the kernel, \begin{align*} \ker \pi &= \{g \in G : \pi(g) = N\} = \{g \in G : gN = N\}. \end{align*} We now show $\{g \in G : gN = N\} = N$ by double inclusion. For the inclusion $N \subseteq \ker\pi$: if $g \in N$, then for every $n \in N$ we have $gn \in N$ (closure of $N$ under the group operation), so $gN \subseteq N$. Conversely, for $n \in N$, the element $g^{-1}n$ lies in $N$ (since $g \in N$ implies $g^{-1} \in N$), so $n = g(g^{-1}n) \in gN$, giving $N \subseteq gN$. Hence $gN = N$. For the inclusion $\ker\pi \subseteq N$: if $gN = N$, then in particular $g = ge \in gN = N$, so $g \in N$. Combining the two inclusions, $\ker \pi = N$. [/step] [step:Read off surjectivity from the definition of $G/N$] By the [Quotient Group](/theorems/790), the underlying set of $G/N$ is \begin{align*} G/N &= \{gN : g \in G\}. \end{align*} Thus every element of $G/N$ has the form $gN = \pi(g)$ for some $g \in G$, and $\pi$ is surjective. This completes the verification of all three properties. [/step]

Lean Formalization

Verified

import Mathlib.GroupTheory.QuotientGroup.Basic

/-!
# Androma Theorem #2700: Properties of the Canonical Projection
#
# Androma page: Quotient Group (related)
# Date of formalization: 2026-05-09
#
# Let G be a group and N ⊴ G. The canonical projection π : G → G/N defined by
# π(g) = gN is a group homomorphism. Its kernel is ker π = N, and it is surjective.
#
# We prove the three properties in separate lemmas, mirroring the three steps of
# the Androma proof.
#
# Mathlib equivalents:
#   - Surjectivity: QuotientGroup.mk'_surjective
#   - Kernel:       QuotientGroup.ker_mk'
-/

variable {G : Type*} [Group G] (N : Subgroup G) [N.Normal]

/-- Step 1: π respects the group operation, i.e. π is a group homomorphism.

Androma proof step 1: π(gh) = (gh)N = (gN)(hN) = π(g)π(h) by the coset multiplication
rule that defines the group operation on G/N. Since g, h are arbitrary, π is a
group homomorphism.

In Lean/Mathlib, `QuotientGroup.mk' N` is constructed as a `MonoidHom`, so the
homomorphism property holds by definition. We verify it explicitly via map_mul. -/
theorem T2700_homomorphism (g h : G) :
    QuotientGroup.mk' N (g * h) = QuotientGroup.mk' N g * QuotientGroup.mk' N h :=
  map_mul (QuotientGroup.mk' N) g h

/-- Step 2: The kernel of π equals N, i.e. ker π = N.

Androma proof step 2:
  The identity of G/N is eN = N.
  ker π = {g ∈ G : gN = N}.
  (N ⊆ ker π) If g ∈ N then gN = N, so π(g) = eN, hence g ∈ ker π.
  (ker π ⊆ N) If gN = N then g = ge ∈ gN = N, so g ∈ N.
  Hence ker π = N.

-- Mathlib equivalent: QuotientGroup.ker_mk' -/
theorem T2700_kernel :
    (QuotientGroup.mk' N).ker = N := by
  ext g
  -- Androma proof step 2a: unfold membership in ker π as π(g) = eN
  simp only [MonoidHom.mem_ker, QuotientGroup.mk'_apply]
  constructor
  · -- Androma proof step 2b (ker π ⊆ N): gN = N implies g ∈ N
    intro hg
    rwa [QuotientGroup.eq_one_iff] at hg
  · -- Androma proof step 2c (N ⊆ ker π): g ∈ N implies gN = N
    intro hg
    rwa [QuotientGroup.eq_one_iff]

/-- Step 3: π is surjective — every element of G/N is of the form gN = π(g).

Androma proof step 3: Every element of G/N has the form gN = π(g) for some g ∈ G,
so π is surjective. The induction principle Quotient.inductionOn witnesses this
in Lean by reducing an arbitrary element of G/N to a representative g ∈ G.

-- Mathlib equivalent: QuotientGroup.mk'_surjective -/
theorem T2700_surjective :
    Function.Surjective (QuotientGroup.mk' N) := by
  intro q
  -- Androma proof step 3: reduce arbitrary q : G/N to a coset representative g ∈ G
  induction q using Quotient.inductionOn with
  | h g =>
    -- π(g) = gN = q, witnessing surjectivity
    exact ⟨g, rfl⟩

Lean Lean (version 4.29.1, arm64-apple-darwin24.6.0, commit f72c35b3f637c8c6571d353742168ab66cc22c00, Release) 5/9/2026

Mathlib: QuotientGroup.ker_mk', QuotientGroup.mk'_surjective

Explore Further

Complete Reducibility for Finite Groups Representation Theory Conjugacy Classes in $\operatorname{SU}(2)$ Representation Theory Normal Extensions Are Splitting Fields Algebra Row Rank Equals Column Rank Linear Algebra Character of the Dual Representation Representation Theory Second Inequality Algebra Simple Roots Form a Base Algebra Second Uniqueness Theorem Algebra Algebra Area Group Theory Subarea

What brings you to Androma?

Start with a route through the knowledge graph.

Properties of the Canonical Projection (Theorem # 2700)

Discussion

Proof

Lean Formalization

Explore Further

Sign in to Androma

Check your inbox

One last step

Properties of the Canonical Projection (Theorem # 2700)

Discussion

Proof

Lean Formalization

Explore Further