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.
Correspondence theorem: subgroups of correspond to subgroups of containing , with normality preserved
Statement
Correspondence theorem: subgroups of correspond to subgroups of containing , with normality preserved.
For , the maps and are inverse inclusion-preserving bijections between subgroups with and subgroups ; they preserve normality.
Facts & Assumptions
Given: A normal subgroup and the quotient map .
is surjective with kernel (The canonical projection , , is a surjective group homomorphism).
Kernels and images are defined by inverse images and values (The kernel and image of a group homomorphism).
Images are subgroups and kernels are normal (The image of a group homomorphism is a subgroup and its kernel is a normal subgroup).
The subgroup criterion is closure under (One-step subgroup test: a nonempty is a subgroup iff for all ; the identity and the inverses of are then those of ).
Normality has the conjugation and coset characterisations (Equivalent characterisations of a normal subgroup by conjugates and left and right cosets).
is the quotient group of cosets (The quotient group and coset product ).
Proof
For , is a subgroup, while is a subgroup containing .
Surjectivity gives , and gives ; both assignments therefore preserve inclusion and are inverse.
The image and preimage calculation of step 2.1 also preserves normality.
Depends on
- The canonical projection $\pi:G\to G/N$, $\pi(g)=gN$, is a surjective group homomorphism
- The kernel and image of a group homomorphism
- The image of a group homomorphism is a subgroup and its kernel is a normal subgroup
- One-step subgroup test: a nonempty $H \subseteq G$ is a subgroup iff $gh^{-1} \in H$ for all $g, h \in H$; the identity and the inverses of $H$ are then those of $G$
- Equivalent characterisations of a normal subgroup by conjugates and left and right cosets
- The quotient group $G/N$ and coset product $(gN)(hN)=ghN$
Used by
- An extraspecial p-group is the product of two maximal abelian subgroups meeting in its centre Corollary
- Converse of Lagrange for finite abelian groups: every divisor occurs as a subgroup order Corollary
- Generation of a finite group is detected modulo its Frattini subgroup Corollary
- Maximal subgroups of a finite p-group are the inverse images of Frattini hyperplanes Corollary
- The upper central series Definition
- In an extraspecial p-group of order p¹⁺²ⁿ every maximal abelian subgroup has order p¹⁺ⁿ Proposition
- Φ(P/N)=Φ(P)N/N for a normal subgroup of a finite p-group Proposition
- A maximal-order cyclic subgroup splits off a finite abelian p-group Theorem
- A p-primary component has the full p-power order and is the unique subgroup of that order Theorem
- Every finite group has a composition series Theorem
- Every finite p-group is nilpotent Theorem
- F(G/Φ(G))=F(G)/Φ(G) for every finite group Theorem
- Nilpotence lifts over the Frattini subgroup of a finite group Theorem
- Philip Hall: in a finite solvable group the Fitting subgroup contains its own centralizer Theorem
- Sylow and maximal-subgroup characterizations of finite nilpotence Theorem
- The Frattini quotient is the largest elementary abelian quotient of a finite p-group Theorem
- The Jordan–Hölder theorem for groups Theorem
Dependency tree · two levels
18 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
- Judson, Abstract Algebra: Theory and Applications, Isomorphism Theorems (standard reference, not scraped)