The maximal pro-2 quotient of the candidate is Π (Stage C, Proposition 3.10)

This file proves the identification

maxPro2GammaA_iso_PiGrp : MaximalPro2Quotient GammaA ≅ PiGrp

i.e. the manuscript's Proposition 3.10 (reference/q2_manuscript.tex, prop:pro2, l.962–996): the maximal pro-2 quotient of the candidate Γ_A is the profinite pro-2 group Π = ⟨σ, x₀, x₁ ∣ x₀^{σ²} x₀ [x₁,σ] = 1⟩_{pro-2} (with τ = 1).

Method (universal property of the maximal pro-2 quotient)

We exhibit the canonical surjection p : GammaA ⟶ PiGrp (sending σ ↦ piSigma, τ ↦ 1, x₀ ↦ piX0, x₁ ↦ piX1) and show that the comparison morphism it induces through the universal property is an isomorphism:

1. IsProP2 PiGrp — Π is pro-2 (it is the inverse limit of finite 2-groups Fin A.n). Proved on the explicit limit model (isProP2_piModel, mirroring maxPro2_isProP2) and transported along piIso (isProP2_of_iso).
2. p : GammaA ⟶ PiGrp — assembled from the per-coordinate surjections Γ_A ↠ Fin A.n supplied by the epimorphism semantics (GammaA_epi_equiv_admissible) applied to the admissible marking of every A : PiMarkedFinite (admissible because A is pi-marked, admissible_twoGroup_iff_piMarked). It is surjective (p_surjective).
3. BigPhi := maxPro2Lift p with maxPro2Proj GammaA ≫ BigPhi = p. It is surjective because p is.
4. For each pro-2 index U of Γ_A (open normal with Γ_A ⧸ U a 2-group), the quotient is again pi-marked, so it skeletalizes to a PiMarkedFinite object and yields a coordinate map θ U : PiGrp ⟶ Γ_A ⧸ U with p ≫ θ U = proj U. Hence coordProj U = BigPhi ≫ θ U, so BigPhi is injective (maxPro2_ext).
5. A bijective continuous homomorphism of profinite groups is an isomorphism (profiniteGrpIsoOfBijective, via ContinuousMulEquiv.toProfiniteGrpIso).

Γ_A-independent pro-2 infrastructure

profiniteGrpIsoOfBijective, isProP2_of_iso, isProP2_piModel, piCME and isProP2_PiGrp now live in Boundary/PiPro2.lean (imported above), so that the Γ-generic boundary package can consume isProP2_PiGrp without depending on Γ_A.

Generator extensionality for morphisms out of Γ_A

theorem Q2Presentation.gammaGen_hom_ext {R : ProfiniteGrp.{0}} [T2Space ↑R.toProfinite.toTop] {f g : GammaA ⟶ R} (h : ∀ (a : Gen), (ProfiniteGrp.Hom.hom f) (gammaGen a) = (ProfiniteGrp.Hom.hom g) (gammaGen a)) : f = g

Two morphisms Γ_A ⟶ R into a profinite (Hausdorff) group agreeing on the four universal generators gammaGen are equal (the generators topologically generate Γ_A). Mirrors EpiSemantics.epiHom_ext.

The canonical surjection p : Γ_A ⟶ Π

def Q2Presentation.piMarking (A : PiMarkedFinite) : Marking (Fin A.n)

The admissible marking of Fin A.n attached to a pi-marked finite object A (σ ↦ A.sigma, τ ↦ 1, x₀ ↦ A.x0, x₁ ↦ A.x1).

Equations

• Q2Presentation.piMarking A Q2Presentation.Gen.sigma = A.sigma
• Q2Presentation.piMarking A Q2Presentation.Gen.tau = 1
• Q2Presentation.piMarking A Q2Presentation.Gen.x0 = A.x0
• Q2Presentation.piMarking A Q2Presentation.Gen.x1 = A.x1

theorem Q2Presentation.piMarking_admissible (A : PiMarkedFinite) : Admissible (piMarking A)

The pi-marking of A is admissible (Proposition 3.10, backward direction).

noncomputable def Q2Presentation.pSurj (A : PiMarkedFinite) : Profinite.SurjContHom GammaA (piDiagram.obj A)

The canonical surjection Γ_A ↠ Fin A.n at the pi-marked object A, from the epimorphism semantics applied to the admissible pi-marking.

Equations

• Q2Presentation.pSurj A = (Q2Presentation.GammaA_epi_equiv_admissible (Fin A.n)).symm ⟨Q2Presentation.piMarking A, ⋯⟩

theorem Q2Presentation.pSurj_gen (A : PiMarkedFinite) (a : Gen) : (ProfiniteGrp.Hom.hom (pSurj A).hom) (gammaGen a) = piMarking A a

The surjection pSurj A sends gammaGen a to the marked generator piMarking A a.

theorem Q2Presentation.pSurj_natural {A B : PiMarkedFinite} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (pSurj A).hom (piDiagram.map f) = (pSurj B).hom

The surjections pSurj A form a cone: they are compatible with the transition maps of piDiagram.

noncomputable def Q2Presentation.pCone : CategoryTheory.Limits.Cone piDiagram

The cone over piDiagram with apex Γ_A assembled from pSurj.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Q2Presentation.p : GammaA ⟶ PiGrp

The canonical surjection p : Γ_A ⟶ Π.

Equations

• Q2Presentation.p = CategoryTheory.Limits.limit.lift Q2Presentation.piDiagram Q2Presentation.pCone

theorem Q2Presentation.p_proj (A : PiMarkedFinite) : CategoryTheory.CategoryStruct.comp p (CategoryTheory.Limits.limit.π piDiagram A) = (pSurj A).hom

p followed by the coordinate projection at A is the surjection pSurj A.

theorem Q2Presentation.p_gammaGen_sigma : (ProfiniteGrp.Hom.hom p) (gammaGen Gen.sigma) = piSigma

theorem Q2Presentation.p_gammaGen_x0 : (ProfiniteGrp.Hom.hom p) (gammaGen Gen.x0) = piX0

theorem Q2Presentation.p_gammaGen_x1 : (ProfiniteGrp.Hom.hom p) (gammaGen Gen.x1) = piX1

theorem Q2Presentation.p_gammaGen_tau : (ProfiniteGrp.Hom.hom p) (gammaGen Gen.tau) = 1

theorem Q2Presentation.p_denseRange : DenseRange ⇑(ProfiniteGrp.Hom.hom p)

p has dense range: its range is a subgroup containing the topological generators piSigma, piX0, piX1 of Π.

theorem Q2Presentation.p_surjective : Function.Surjective ⇑(ProfiniteGrp.Hom.hom p)

p is surjective.

The comparison morphism BigPhi and its surjectivity

noncomputable def Q2Presentation.BigPhi : MaximalPro2Quotient GammaA ⟶ PiGrp

The comparison morphism MaximalPro2Quotient Γ_A ⟶ Π, the universal lift of the surjection p (Π is pro-2).

Equations

• Q2Presentation.BigPhi = Q2Presentation.maxPro2Lift Q2Presentation.p Q2Presentation.isProP2_PiGrp

theorem Q2Presentation.BigPhi_fac : CategoryTheory.CategoryStruct.comp (maxPro2Proj GammaA) BigPhi = p

theorem Q2Presentation.BigPhi_surjective : Function.Surjective ⇑(ProfiniteGrp.Hom.hom BigPhi)

The coordinate maps θ U and injectivity of BigPhi

noncomputable def Q2Presentation.quotMarking (U : Pro2Index GammaA) : Marking (↑GammaA.toProfinite.toTop ⧸ ↑U.obj.toOpenSubgroup)

The admissible marking of the finite 2-group quotient Γ_A ⧸ U attached to a pro-2 index U (forward direction of the epimorphism semantics applied to the canonical surjection Γ_A ↠ Γ_A ⧸ U).

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.quotMarking_proj (U : Pro2Index GammaA) (a : Gen) : quotMarking U a = (ProfiniteGrp.Hom.hom (ProfiniteGrp.proj U.obj)) (gammaGen a)

theorem Q2Presentation.quotMarking_admissible (U : Pro2Index GammaA) : Admissible (quotMarking U)

theorem Q2Presentation.quotMarking_tau (U : Pro2Index GammaA) : quotMarking U Gen.tau = 1

theorem Q2Presentation.quotMarking_gen (U : Pro2Index GammaA) : Subgroup.closure {quotMarking U Gen.sigma, quotMarking U Gen.x0, quotMarking U Gen.x1} = ⊤

theorem Q2Presentation.quotMarking_rel (U : Pro2Index GammaA) : rconj (quotMarking U Gen.x0) (quotMarking U Gen.sigma ^ 2) * quotMarking U Gen.x0 * commutatorW (quotMarking U Gen.x1) (quotMarking U Gen.sigma) = 1

noncomputable def Q2Presentation.indexPiObj (U : Pro2Index GammaA) : PiMarkedFinite

The pi-marked finite object obtained by skeletalizing the 2-group quotient Γ_A ⧸ U with its pi-marking.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Q2Presentation.indexSkelEquiv (U : Pro2Index GammaA) : Fin (indexPiObj U).n ≃* ↑GammaA.toProfinite.toTop ⧸ ↑U.obj.toOpenSubgroup

The transport equivalence Fin (indexPiObj U).n ≃* Γ_A ⧸ U.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Q2Presentation.theta (U : Pro2Index GammaA) : PiGrp ⟶ (pro2Diagram GammaA).obj U

The coordinate map θ U : Π ⟶ Γ_A ⧸ U: project Π to the coordinate Fin (indexPiObj U).n and transport along indexSkelEquiv U.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.theta_piSigma (U : Pro2Index GammaA) : (ProfiniteGrp.Hom.hom (theta U)) piSigma = quotMarking U Gen.sigma

theorem Q2Presentation.theta_piX0 (U : Pro2Index GammaA) : (ProfiniteGrp.Hom.hom (theta U)) piX0 = quotMarking U Gen.x0

theorem Q2Presentation.theta_piX1 (U : Pro2Index GammaA) : (ProfiniteGrp.Hom.hom (theta U)) piX1 = quotMarking U Gen.x1

theorem Q2Presentation.p_theta (U : Pro2Index GammaA) : CategoryTheory.CategoryStruct.comp p (theta U) = ProfiniteGrp.proj U.obj

p followed by θ U is the canonical quotient projection Γ_A ↠ Γ_A ⧸ U.

theorem Q2Presentation.coordProj_eq_apply (U : Pro2Index GammaA) (m : ↑(MaximalPro2Quotient GammaA).toProfinite.toTop) : (ProfiniteGrp.Hom.hom (coordProj U)) m = (ProfiniteGrp.Hom.hom (theta U)) ((ProfiniteGrp.Hom.hom BigPhi) m)

The coordinate projection coordProj U factors as BigPhi ≫ θ U.

theorem Q2Presentation.BigPhi_injective : Function.Injective ⇑(ProfiniteGrp.Hom.hom BigPhi)

BigPhi is injective. Its coordinate projections recover those of MaximalPro2Quotient Γ_A, which separate points (maxPro2_ext).

The identification

theorem Q2Presentation.BigPhi_bijective : Function.Bijective ⇑(ProfiniteGrp.Hom.hom BigPhi)

noncomputable def Q2Presentation.maxPro2GammaA_iso_PiGrp : MaximalPro2Quotient GammaA ≅ PiGrp

Proposition 3.10. The maximal pro-2 quotient of the candidate Γ_A is the profinite pro-2 group Π.

Equations

• Q2Presentation.maxPro2GammaA_iso_PiGrp = Q2Presentation.profiniteGrpIsoOfBijective Q2Presentation.BigPhi Q2Presentation.BigPhi_bijective

Acceptance checks