Theorem 11.2.3 — Second Isomorphism Theorem

Proved

AATA.second_isomorphism_11_2_3

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

group-theoryisomorphism-theoremsquotient-groups

Let $G$ be a group, let $K\le G$ be a subgroup, and let $N$ be a normal subgroup of $G$ . The product set $KN=\{kn:k\in K,n\in N\}$ is a subgroup of $G$ , the intersection $K\cap N$ is normal in $K$ , and

K/(K\cap N)\cong KN/N.

This identifies the part of the quotient $G/N$ reached by $K$ . The subgroup $K$ is not required to be normal, and it is not assumed to map onto all of $G/N$ .

Formalization Note. The subgroup join is explicitly equated with the product set $KN$ . Subgroup restrictions represent $K\cap N$ inside $K$ and the contained copy of $N$ inside $KN$ .

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 second_isomorphism_11_2_3 {G : Type u} [Group G] (K N : Subgroup G) [N.Normal] :
    ((K ⊔ N : Subgroup G) : Set G) =
      {g : G | ∃ k ∈ K, ∃ n ∈ N, k*n = g} ∧
    (N.subgroupOf K).Normal ∧
    Nonempty (K ⧸ N.subgroupOf K ≃*
      (K ⊔ N : Subgroup G) ⧸ N.subgroupOf (K ⊔ N)) := by sorry
end AATA

Source

Thomas W. Judson, Abstract Algebra: Theory and Applications, author-hosted HTML edition dated August 4, 2026, Theorem 11.2.3, 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 arbitrary subgroups $K$ and $N$ of $G$ , assume that $N$ is normal in $G$ , meaning $ana^{-1}\in N$ for every $n\in N$ and $a\in G$ . Let $J=K\vee N$ be the least subgroup of $G$ containing both $K$ and $N$ , let $A=\{k\in K:k\text{ belongs to }N\text{ when viewed in }G\}$ be a subgroup of the group $K$ , and let $B=\{j\in J:j\text{ belongs to }N\text{ when viewed in }G\}$ be a subgroup of the group $J$ . Then the underlying set of $J$ is exactly $\{g\in G:\exists k\in K,\ \exists n\in N,\ kn=g\}$ , the subgroup $A$ is normal in $K$ , and there exists a group isomorphism $K/A\to J/B$ , that is, a bijection preserving multiplication. The product in the set equality is specifically an element of $K$ followed by an element of $N$ . Here $A$ represents $K\cap N$ inside $K$ , and $B$ represents $N\cap J$ inside $J$ (with $N\subseteq J$ following from the definition of $J$ ); neither occurrence is a quotient by a subgroup of an unrelated ambient group. Both quotients use left cosets, where two representatives $x,y$ represent the same coset exactly when $x^{-1}y$ belongs to the relevant denominator subgroup. Their group structures use the normality of $N$ restricted to $K$ and $J$ , supplied by library instances from the assumed normality of $N$ in $G$ . The isomorphism assertion only states that the type of such isomorphisms is inhabited: it gives neither a particular map on cosets nor a uniqueness or compatibility condition. No assumption says that $K$ is normal in $G$ , that either subgroup contains the other, or that any group is finite, commutative, or nontrivial. The cases $K=\{1\}$ , $K=G$ , $N=\{1\}$ , $N=G$ , $K\subseteq N$ , and a trivial $G$ are included; when $K\subseteq N$ , both displayed quotient groups are trivial. 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

Endorsed by Shuze Chen · Sep 6, 2026
Flagged by Shuze Chen · Sep 6, 2026
Same concern as on the goal: this is Mathlib's QuotientGroup.quotientInfEquivProdNormalQuotient in nearly identical subgroupOf and join form (plus Subgroup.mul_normal for the product set clause). The wrapper is well made, but there is no open formalization content here.

View graph