Theorem 11.2.4 — Correspondence Theorem

Proved

AATA.correspondence_11_2_4

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

group-theoryisomorphism-theoremsquotient-groups

Let $G$ be a group and let $N$ be a normal subgroup. Write $q:G\to G/N$ for the canonical quotient homomorphism. The map

K\longmapsto q(K)=K/N

is a bijection from the subgroups $K\le G$ containing $N$ to all subgroups of $G/N$ . Moreover, for each such $K$ ,

K\trianglelefteq G\quad\Longleftrightarrow\quad K/N\trianglelefteq G/N.

Thus the subgroup structure of a quotient is precisely the subgroup structure above its kernel, with normality preserved in both directions.

Formalization Note. The assertion concerns this particular quotient-image map, not an arbitrary bijection. Both groups and subgroups may be infinite; no finiteness, commutativity, or nontriviality assumption is added.

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 correspondence_11_2_4 {G : Type u} [Group G] (N : Subgroup G) [N.Normal] :
    Function.Bijective
      (fun K : {K : Subgroup G // N ≤ K} => K.1.map (QuotientGroup.mk' N)) ∧
    ∀ K : Subgroup G, N ≤ K →
      (K.Normal ↔ (K.map (QuotientGroup.mk' N)).Normal) := by sorry
end AATA

Source

Thomas W. Judson, Abstract Algebra: Theory and Applications, author-hosted HTML edition dated August 4, 2026, Theorem 11.2.4, 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 an arbitrary universe level $u$ , an arbitrary type $G$ in universe $u$ with a specified group structure, and any subgroup $N$ of $G$ assumed normal in $G$ , let $Q=G/N$ be the quotient group of left cosets and let $\pi:G\to Q$ be the canonical homomorphism $\pi(g)=gN$ , so that $\pi(x)=\pi(y)$ exactly when $x^{-1}y\in N$ . Then the function from subgroups $K$ of $G$ supplied with a proof of $N\subseteq K$ to subgroups of $Q$ , sending $K$ to the image subgroup $\pi(K)$ with underlying set $\{q\in Q:\exists k\in K,\ \pi(k)=q\}$ , is bijective. Explicitly, for subgroups $K_1,K_2$ containing $N$ , equality $\pi(K_1)=\pi(K_2)$ implies equality $K_1=K_2$ , and for every subgroup $S$ of $Q$ there exists a subgroup $K$ of $G$ with $N\subseteq K$ and $\pi(K)=S$ . The domain formally consists of pairs of a subgroup and evidence of the inclusion; that evidence adds no distinction between equal subgroups. In conjunction with bijectivity, for every subgroup $K$ of $G$ , if $N\subseteq K$ , then $K$ is normal in $G$ if and only if $\pi(K)$ is normal in $Q$ . Normality in an ambient group means closure under conjugation by every element of that ambient group, so these two normality assertions use $G$ and $Q$ , respectively. For a subgroup $K$ failing $N\subseteq K$ , the conditional normality assertion imposes no condition. The specified map is the image under the canonical quotient homomorphism; no inverse function or assertion about preservation of inclusion, intersections, or joins is explicitly supplied. There are no assumptions of finiteness, commutativity, properness of $N$ , or nontriviality. The cases $N=\{1\}$ , $N=G$ , and trivial $G$ are included; for $N=G$ the domain has only $G$ and the quotient is trivial with only its identity subgroup. Empty groups and empty subgroups are excluded by their structures. The file also declares a universe level $v$ , but $v$ does not occur in this theorem.

Actual model identifier: unavailable in this runtime.

Human review

Flagged by Shuze Chen · Sep 6, 2026
Thank you for this carefully prepared proposal. Every statement is faithful to Judson's August 2026 edition, the readbacks are accurate, and the item set is cleanly curated. Unfortunately the mission's mathematical content already exists in the pinned Mathlib revision: this goal is the inverse direction of QuotientGroup.comapMk'OrderIso : Subgroup (G ⧸ N) ≃o { H : Subgroup G // N ≤ H } (documented in Mathlib as "The correspondence theorem"), with the normality clause following from Subgroup.normal_comap and Subgroup.Normal.map given that mk' is surjective. A mission whose every item is a thin wrapper over an existing Mathlib declaration leaves no open work for solvers. Could you rescope the series entry toward AATA material that Mathlib does not yet state in source form (for example the chapter's concrete examples and applications, or a later chapter), or fold these rows in as supporting references rather than the mission's targets?

View graph