How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
A homomorphism that kills a normal subgroup factors uniquely through the quotient group
Statement
A homomorphism that kills a normal subgroup factors uniquely through the quotient group.
If , is a homomorphism, and , then there is a unique homomorphism such that and .
Facts & Assumptions
Given: , a homomorphism , and .
is the group of cosets of a normal subgroup (The quotient group and coset product ).
The quotient map is a surjective homomorphism (The canonical projection , , is a surjective group homomorphism).
means that for every (The kernel and image of a group homomorphism).
Equal kernel cosets have equal images under a homomorphism (Two elements have the same image under a homomorphism if and only if they lie in the same coset of its kernel).
A group homomorphism preserves products (Monoid homomorphism and group homomorphism).
Proof
Define ; if , then , so [L4] proves that this value is independent of the representative.
For cosets, , and .
The surjectivity used in step 2.1 forces any such factor map to have these values, hence proves uniqueness.
Depends on
- The quotient group $G/N$ and coset product $(gN)(hN)=ghN$
- The canonical projection $\pi:G\to G/N$, $\pi(g)=gN$, is a surjective group homomorphism
- The kernel and image of a group homomorphism
- Two elements have the same image under a homomorphism if and only if they lie in the same coset of its kernel
- Monoid homomorphism and group homomorphism
Used by
- The canonical group solution set on a two-element set Example
- A group pushout is the quotient of a free product by the amalgamating relations Theorem
- A module homomorphism vanishing on N factors uniquely through M/N Theorem
- A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring Theorem
- Abelianisation is left adjoint to the inclusion of abelian groups Theorem
- Automorphisms act linearly on the Frattini quotient Theorem
- First isomorphism theorem for groups: G/ker f congimf Theorem
- Grp is complete and cocomplete Theorem
- Normal-subgroup quotients of a fixed free group give a canonical solution set for the underlying-set functor on groups Theorem
- The abelianisation of a free group on X is a free abelian group on X Theorem
- The derived subgroup is characteristic and the abelianization is universal Theorem
- Torsion-free abelian groups form a reflective full subcategory of abelian groups Theorem
- Universal property of the tensor product for balanced maps into abelian groups Theorem
- Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group Theorem
Dependency tree · two levels
16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Milne, Group Theory, Kernels and Quotients (standard reference, not scraped)