Prove2Me

Theorem 11.2.1 — First Isomorphism Theorem

Proved
AATA.first_isomorphism_11_2_1

by wamlart · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

group-theoryisomorphism-theoremsquotient-groups

Let G,HG,H be groups, let f:G→Hf:G\to H be a group homomorphism, and put K=ker⁡(f)K=\ker(f). Then KK is normal in GG. For the canonical quotient homomorphism q:G→G/Kq:G\to G/K, there exists a unique group isomorphism

e:G/K⟶f(G),e(q(g))=f(g)(g∈G).e:G/K\longrightarrow f(G),\qquad e(q(g))=f(g)\quad(g\in G).

The isomorphism identifies the image of a homomorphism with the quotient by exactly the elements sent to the identity. Uniqueness refers to isomorphisms satisfying the displayed commuting equation.

Formalization Note. The codomain is the range subgroup f(G)f(G), not all of HH. Kernel normality is included explicitly. The groups may be infinite or trivial.

Preamble
import Mathlib.GroupTheory.QuotientGroup.Basic
import Mathlib.Tactic

set_option autoImplicit false
set_option maxHeartbeats 200000
universe u v
Formal statement
namespace AATA
theorem first_isomorphism_11_2_1 {G : Type u} {H : Type v} [Group G] [Group H] (f : G →* H) :
    f.ker.Normal ∧ ∃! e : G ⧸ f.ker ≃* f.range,
      ∀ g : G, e (QuotientGroup.mk' f.ker g) = f.rangeRestrict g := by sorry
end AATA
Source
Thomas W. Judson, Abstract Algebra: Theory and Applications, author-hosted HTML edition dated August 4, 2026, Theorem 11.2.1, https://judsonbooks.org/aata-files/aata-html/homomorph-section-group-isomorphism-theorems.html
Read-back

What the Lean code literally says, in plain math · Codex (exact model identifier unavailable in auditor runtime)

For arbitrary universe levels uu and vv, arbitrary types GG in universe uu and HH in universe vv, specified group structures on both types, and any group homomorphism f:G→Hf:G\to H (already preserving multiplication and the identity), let D={g∈G:f(g)=1H}D=\{g\in G:f(g)=1_H\} be its kernel subgroup and let R={h∈H:∃g∈G, f(g)=h}R=\{h\in H:\exists g\in G,\ f(g)=h\} be its range subgroup, equipped with the group operations inherited from HH. Then DD is normal in GG, meaning ada−1∈Dada^{-1}\in D for every d∈Dd\in D and a∈Ga\in G, and there exists exactly one group isomorphism e:G/D→Re:G/D\to R satisfying e(gD)=f(g)e(gD)=f(g) for every g∈Gg\in G. Here G/DG/D is the group of left cosets, with xD=yDxD=yD precisely when x−1y∈Dx^{-1}y\in D, and the argument gDgD is the value of the canonical quotient homomorphism at gg. On the right side of the displayed equality, f(g)f(g) is an element of the subtype RR, supplied with the witness gg that it lies in the range; thus the equality is inside RR. A group isomorphism is a bijection with inverse that preserves multiplication. Uniqueness is among group isomorphisms satisfying the stated equation for every gg, and does not assert that these groups have only one isomorphism without that condition. The quotient group structure uses the library's automatic normality instance for kernels; no extra normality hypothesis is required from the caller. There are no assumptions of finiteness, commutativity, nontriviality, injectivity, or surjectivity of ff onto HH. In particular, the constant identity homomorphism is included: its kernel is all of GG, its range is the identity subgroup, and both groups connected by ee are trivial. Trivial GG or HH is also permitted; an empty group is excluded by the group structure.

Actual model identifier: unavailable in this runtime.

Human review

View graph