theorem Q2Presentation.Induction.TerminalBridge.isProP2_ofFiniteGrp {Q : Type} [Group Q] [Finite Q] (hQ : IsPGroup 2 Q) : IsProP2 (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of Q))

A finite 2-group is pro-2.

theorem Q2Presentation.Induction.TerminalBridge.factor_through_of_iso (Γ : ProfiniteGrp.{0}) (e : MaximalPro2Quotient Γ ≅ PiGrp) (π : Γ ⟶ PiGrp) (hπ : CategoryTheory.CategoryStruct.comp (maxPro2Proj Γ) e.hom = π) (Qf : ProfiniteGrp.{0}) (hQf : IsProP2 Qf) (g : Γ ⟶ Qf) : ∃! gbar : PiGrp ⟶ Qf, CategoryTheory.CategoryStruct.comp π gbar = g

Generic factorization: if π = maxPro2Proj ≫ e.hom for an iso e : Γ(2) ≅ Π, then maps to pro-2 targets factor uniquely through π.

theorem Q2Presentation.Induction.TerminalBridge.candidate_pro2_factorization (Qf : ProfiniteGrp.{0}) (hQf : IsProP2 Qf) (g : GammaA ⟶ Qf) : ∃! gbar : PiGrp ⟶ Qf, CategoryTheory.CategoryStruct.comp boundaryPackage_GammaA.pro2Map gbar = g

Candidate-side factorization through boundaryPackage_GammaA.pro2Map = p.

theorem Q2Presentation.Induction.TerminalBridge.local_pro2_factorization (Qf : ProfiniteGrp.{0}) (hQf : IsProP2 Qf) (g : GQ2Profinite ⟶ Qf) : ∃! gbar : PiGrp ⟶ Qf, CategoryTheory.CategoryStruct.comp boundaryPackage_GQ2.pro2Map gbar = g

Local-side factorization through boundaryPackage_GQ2.pro2Map = pro2Map_loc.