Lemmas 9.1–9.2 — finite group theory feeding the induction #
- Lemma 9.1 (coprime-kernel subdirect products / fibre products) — statement scaffold.
- Lemma 9.2 core (odd normal subgroup with 2-group quotient splits) — proved via Mathlib's Schur–Zassenhaus.
theorem
GQ2.FiniteGroup.coprime_fiber_product
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
[Group A]
[Group B]
[Group C]
[Finite A]
[Finite B]
(f : A →* C)
(g : B →* C)
(hf : Function.Surjective ⇑f)
(hg : Function.Surjective ⇑g)
(hcop : (Nat.card ↥f.ker).Coprime (Nat.card ↥g.ker))
(J : Subgroup (A × B))
(hJsub : ∀ p ∈ J, f p.1 = g p.2)
(hJA : Function.Surjective fun (p : ↥J) => (↑p).1)
(hJB : Function.Surjective fun (p : ↥J) => (↑p).2)
(p : A × B)
:
f p.1 = g p.2 → p ∈ J
Lemma 9.1 (coprime-kernel subdirect product). Let f : A ↠ C and g : B ↠ C be finite
epimorphisms whose kernels have coprime orders. A subgroup J of A × B that lies in the fibre
product {(a,b) | f a = g b} and projects onto both factors is the entire fibre product.
Proof via Goursat: J.goursatFst ≤ ker f and J.goursatSnd ≤ ker g, and Goursat's isomorphism
A/goursatFst ≃ B/goursatSnd gives |goursatFst|·|ker g| = |goursatSnd|·|ker f|. Coprimality of
|ker f|, |ker g| then forces ker g ≤ J.goursatSnd, which is exactly the missing wild direction
needed to hit every fibre-product element.
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- Lemma 9.1 = ⟦lem-coprimesubdirect⟧
- Lemma 9.2 = ⟦lem-scalarterminal⟧