The maximal pro-2 quotient of a profinite group (Stage C, work order: MaximalPro2)

This file is a general, Q₂-independent module of profinite group theory. For an arbitrary profinite group P it constructs the maximal pro-2 quotient MaximalPro2Quotient P, the canonical surjection maxPro2Proj P, and proves the universal property characterising it. In the manuscript (reference/q2_manuscript.tex) this is the construction underlying Proposition 3.10 (prop:pro2, the maximal pro-2 quotient Π of the candidate Γ_A) and the marked local Demushkin comparison (the maximal pro-2 quotient of G_{Q₂} is ≅ ℤ₂ on the unramified line); the boundary isomorphisms consume maxPro2_universal as their load-bearing tool.

Mathlib status

Mathlib v4.28.0 has no pro-p / maximal pro-p notion (a search for IsProP, MaximalPro, "pro-p" finds only unrelated CategoryTheory.ObjectProperty.Ind files). We therefore build it here, mirroring three proven mathlib/​project templates:

• the cofiltered-limit idioms of Candidate/GammaA.lean and Boundary/Ttame.lean;
• ProfiniteGrp.diagram/proj/cone/isLimitCone and ProfiniteGrp.limit from Mathlib.Topology.Algebra.Category.ProfiniteGrp.{Basic,Limits};
• ProfiniteGrp.ProfiniteCompletion.lift/lift_unique from …/ProfiniteGrp/Completion.lean (the universal property of a limit of finite quotients), which the universal property here mirrors essentially verbatim.

Construction

The index is the full subcategory Pro2Index P of OpenNormalSubgroup P on those open normal U whose quotient P ⧸ U is a finite 2-group (Pro2Prop). It is cofiltered (instIsCofilteredPro2Index): closed under ⊓ because P ⧸ (U ⊓ V) embeds in P ⧸ U × P ⧸ V, a product of 2-groups. The maximal pro-2 quotient is the inverse limit, in ProfiniteGrp, of the restricted finite-quotient diagram (pro2Diagram = (Pro2Prop P).ι ⋙ ProfiniteGrp.diagram P):

• MaximalPro2Quotient P : ProfiniteGrp := ProfiniteGrp.limit (pro2Diagram P);
• maxPro2Proj P : P ⟶ MaximalPro2Quotient P, the canonical projection (mirrors ProfiniteGrp.toLimit), surjective (maxPro2Proj_surjective);
• maxPro2_isProP2 : IsProP2 (MaximalPro2Quotient P) — every finite continuous quotient is a 2-group;
• maxPro2_universal — for any IsProP2 Q and f : P ⟶ Q there is a unique g : MaximalPro2Quotient P ⟶ Q with f = maxPro2Proj P ≫ g.

Pro-2 groups

def Q2Presentation.IsProP2 (P : ProfiniteGrp.{u}) : Prop

A profinite group P is pro-2 if every finite continuous quotient is a 2-group. Finite continuous quotients are exactly the quotients P ⧸ U by open normal subgroups U, so this says P ⧸ U is a 2-group for every U : OpenNormalSubgroup P.

Equations

• Q2Presentation.IsProP2 P = ∀ (U : OpenNormalSubgroup ↑P.toProfinite.toTop), IsPGroup 2 (↑P.toProfinite.toTop ⧸ ↑U.toOpenSubgroup)

A 2-group from an intersection: the inf-closure ingredient

theorem Q2Presentation.isPGroup_two_prod {A : Type u_1} {B : Type u_2} [Group A] [Group B] (hA : IsPGroup 2 A) (hB : IsPGroup 2 B) : IsPGroup 2 (A × B)

A product of two 2-groups is a 2-group (used to show the pro-2 index is closed under ⊓).

noncomputable def Q2Presentation.quotInfProdHom {G : Type u_1} [Group G] (U V : Subgroup G) [U.Normal] [V.Normal] : G ⧸ U ⊓ V →* (G ⧸ U) × G ⧸ V

The homomorphism P ⧸ (U ⊓ V) →* (P ⧸ U) × (P ⧸ V) induced by the two quotient maps; it is injective, exhibiting P ⧸ (U ⊓ V) as (isomorphic to) a subgroup of the 2-group P ⧸ U × P ⧸ V.

Equations

• Q2Presentation.quotInfProdHom U V = (QuotientGroup.map (U ⊓ V) U (MonoidHom.id G) ⋯).prod (QuotientGroup.map (U ⊓ V) V (MonoidHom.id G) ⋯)

theorem Q2Presentation.quotInfProdHom_injective {G : Type u_1} [Group G] (U V : Subgroup G) [U.Normal] [V.Normal] : Function.Injective ⇑(quotInfProdHom U V)

theorem Q2Presentation.isPGroup_two_quotient_inf {G : Type u_1} [Group G] {U V : Subgroup G} [U.Normal] [V.Normal] (hU : IsPGroup 2 (G ⧸ U)) (hV : IsPGroup 2 (G ⧸ V)) : IsPGroup 2 (G ⧸ U ⊓ V)

The quotient by an intersection of two open normal subgroups with 2-group quotients is again a 2-group.

The pro-2 index category

def Q2Presentation.Pro2Prop (P : ProfiniteGrp.{u}) : CategoryTheory.ObjectProperty (OpenNormalSubgroup ↑P.toProfinite.toTop)

The property selecting the open normal subgroups U ⊴ P whose quotient P ⧸ U is a 2-group.

Equations

• Q2Presentation.Pro2Prop P U = IsPGroup 2 (↑P.toProfinite.toTop ⧸ ↑U.toOpenSubgroup)

@[reducible, inline]

abbrev Q2Presentation.Pro2Index (P : ProfiniteGrp.{u}) : Type u

The pro-2 index category: the full subcategory of OpenNormalSubgroup P on the open normal subgroups with 2-group quotient. The maximal pro-2 quotient is the limit over this category.

Equations

• Q2Presentation.Pro2Index P = (Q2Presentation.Pro2Prop P).FullSubcategory

def Q2Presentation.topOpenNormal (P : ProfiniteGrp.{u}) : OpenNormalSubgroup ↑P.toProfinite.toTop

The whole group ⊤ as an open normal subgroup.

Equations

• Q2Presentation.topOpenNormal P = { toOpenSubgroup := ⊤, isNormal' := ⋯ }

def Q2Presentation.topIndex (P : ProfiniteGrp.{u}) : Pro2Index P

The whole group as a pro-2 index object (P ⧸ ⊤ is trivial, hence a 2-group); witnesses nonemptiness of the index.

Equations

• Q2Presentation.topIndex P = { obj := Q2Presentation.topOpenNormal P, property := ⋯ }

def Q2Presentation.infIndex {P : ProfiniteGrp.{u}} (X Y : Pro2Index P) : Pro2Index P

The intersection of two pro-2 index objects, again a pro-2 index object (isPGroup_two_quotient_inf).

Equations

• Q2Presentation.infIndex X Y = { obj := X.obj ⊓ Y.obj, property := ⋯ }

instance Q2Presentation.instIsCofilteredPro2Index {P : ProfiniteGrp.{u}} : CategoryTheory.IsCofiltered (Pro2Index P)

The pro-2 index category is cofiltered. Binary cones are intersections infIndex; the parallel-arrow half is automatic (the index is a preorder, hence thin); nonemptiness is topIndex.

theorem Q2Presentation.pro2_exists_dominating {P : ProfiniteGrp.{u}} (J : Finset (Pro2Index P)) : ∃ (B : Pro2Index P), ∀ A ∈ J, Nonempty (B ⟶ A)

Finite cofiltered domination. Any finite set of pro-2 indices is dominated by a single index admitting a morphism to each (mirrors GammaA.exists_dominating).

The maximal pro-2 quotient as an inverse limit

noncomputable def Q2Presentation.pro2Diagram (P : ProfiniteGrp.{u}) : CategoryTheory.Functor (Pro2Index P) ProfiniteGrp.{u}

The restricted finite-quotient diagram: each pro-2 index U maps to the finite 2-group P ⧸ U (viewed as a discrete profinite group).

Equations

• Q2Presentation.pro2Diagram P = (Q2Presentation.Pro2Prop P).ι.comp P.diagram

noncomputable def Q2Presentation.MaximalPro2Quotient (P : ProfiniteGrp.{u}) : ProfiniteGrp.{u}

The maximal pro-2 quotient MaximalPro2Quotient P, the cofiltered inverse limit (in ProfiniteGrp) of the finite 2-group quotients of P.

Equations

• Q2Presentation.MaximalPro2Quotient P = ProfiniteGrp.limit (Q2Presentation.pro2Diagram P)

noncomputable def Q2Presentation.coordProj {P : ProfiniteGrp.{u}} (U : Pro2Index P) : MaximalPro2Quotient P ⟶ (pro2Diagram P).obj U

The coordinate projection MaximalPro2Quotient P ⟶ P ⧸ U at a pro-2 index U (evaluation of the compatible family at U; mirrors Boundary/Z2Limit.z2Projection).

Equations

• Q2Presentation.coordProj U = (ProfiniteGrp.limitCone (Q2Presentation.pro2Diagram P)).π.app U

@[simp]

theorem Q2Presentation.coordProj_apply {P : ProfiniteGrp.{u}} (U : Pro2Index P) (x : ↑(MaximalPro2Quotient P).toProfinite.toTop) : (ProfiniteGrp.Hom.hom (coordProj U)) x = ↑x U

theorem Q2Presentation.maxPro2_ext {P : ProfiniteGrp.{u}} {x y : ↑(MaximalPro2Quotient P).toProfinite.toTop} (h : ∀ (U : Pro2Index P), (ProfiniteGrp.Hom.hom (coordProj U)) x = (ProfiniteGrp.Hom.hom (coordProj U)) y) : x = y

Two points of MaximalPro2Quotient P agree once all their coordinate projections agree.

noncomputable def Q2Presentation.maxPro2ProjMonoidHom (P : ProfiniteGrp.{u}) : ↑P.toProfinite.toTop →* ↑(MaximalPro2Quotient P).toProfinite.toTop

The underlying monoid homomorphism of the canonical projection: p ↦ (U ↦ mk p) (mirrors ProfiniteGrp.toLimitFun).

Equations

• Q2Presentation.maxPro2ProjMonoidHom P = { toFun := fun (p : ↑P.toProfinite.toTop) => ⟨fun (x : Q2Presentation.Pro2Index P) => ↑p, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem Q2Presentation.maxPro2ProjMonoidHom_continuous (P : ProfiniteGrp.{u}) : Continuous ⇑(maxPro2ProjMonoidHom P)

noncomputable def Q2Presentation.maxPro2Proj (P : ProfiniteGrp.{u}) : P ⟶ MaximalPro2Quotient P

The canonical projection maxPro2Proj P : P ⟶ MaximalPro2Quotient P (mirrors ProfiniteGrp.toLimit).

Equations

• Q2Presentation.maxPro2Proj P = ProfiniteGrp.ofHom (let __src := Q2Presentation.maxPro2ProjMonoidHom P; { toMonoidHom := __src, continuous_toFun := ⋯ })

@[simp]

theorem Q2Presentation.maxPro2Proj_apply {P : ProfiniteGrp.{u}} (p : ↑P.toProfinite.toTop) (U : Pro2Index P) : ↑((ProfiniteGrp.Hom.hom (maxPro2Proj P)) p) U = ↑p

theorem Q2Presentation.maxPro2Proj_comp_coordProj {P : ProfiniteGrp.{u}} (U : Pro2Index P) : CategoryTheory.CategoryStruct.comp (maxPro2Proj P) (coordProj U) = ProfiniteGrp.proj U.obj

The canonical projection followed by the coordinate at U is the finite quotient projection P ⟶ P ⧸ U.

The maximal pro-2 quotient is pro-2

theorem Q2Presentation.exists_coordProj_ker_le {P : ProfiniteGrp.{u}} (W : OpenNormalSubgroup ↑(MaximalPro2Quotient P).toProfinite.toTop) : ∃ (U : Pro2Index P), (ProfiniteGrp.Hom.hom (coordProj U)).ker ≤ ↑W.toOpenSubgroup

Coordinate domination. Every open normal subgroup W of MaximalPro2Quotient P contains the kernel of some coordinate projection coordProj U. (The coordinate kernels form a neighbourhood basis of 1; a single pro-2 index U dominates the finitely many coordinates pinned down by the open set W, using cofilteredness of the index.)

theorem Q2Presentation.maxPro2_isProP2 (P : ProfiniteGrp.{u}) : IsProP2 (MaximalPro2Quotient P)

The maximal pro-2 quotient is pro-2: every finite continuous quotient of MaximalPro2Quotient P is a 2-group. Given an open normal W, the domination lemma provides a coordinate projection φ = coordProj U with ker φ ≤ W; then M ⧸ ker φ ≅ range φ ≤ P ⧸ U is a 2-group, and M ⧸ W is a quotient of it.

The canonical projection is surjective

theorem Q2Presentation.maxPro2Proj_denseRange (P : ProfiniteGrp.{u}) : DenseRange ⇑(ProfiniteGrp.Hom.hom (maxPro2Proj P))

The image of maxPro2Proj P is dense (mirrors ProfiniteGrp.denseRange_toLimit): a nonempty open set fixes finitely many coordinates; a single dominating pro-2 index U₀ collapses them; and P surjects onto the coordinate P ⧸ U₀, so the lift of the chosen value agrees with the target point on those coordinates.

theorem Q2Presentation.maxPro2Proj_surjective (P : ProfiniteGrp.{u}) : Function.Surjective ⇑(ProfiniteGrp.Hom.hom (maxPro2Proj P))

The canonical projection is surjective. Its range is closed (continuous image of a compact space) and dense (maxPro2Proj_denseRange), hence everything.

The universal property

For a pro-2 target Q and f : P ⟶ Q, every open normal V ⊴ Q pulls back to a pro-2 index comapIndex f hQ V = f⁻¹V of P (its quotient embeds in the 2-group Q ⧸ V). The induced finite quotient maps P ⧸ f⁻¹V ⟶ Q ⧸ V form a cone over diagram Q with apex MaximalPro2Quotient P; lifting it through Q.isLimitCone yields the universal g. This mirrors ProfiniteGrp.ProfiniteCompletion.lift/lift_unique.

theorem Q2Presentation.isPGroup_two_quotient_comap {G : Type u_1} {H : Type u_2} [Group G] [Group H] (φ : G →* H) {V : Subgroup H} [V.Normal] (hV : IsPGroup 2 (H ⧸ V)) : IsPGroup 2 (G ⧸ Subgroup.comap φ V)

Pulling back an open normal subgroup V ⊴ Q along f to a pro-2 index of P: its quotient P ⧸ f⁻¹V injects into the 2-group Q ⧸ V.

noncomputable def Q2Presentation.comapIndex {P Q : ProfiniteGrp.{u}} (f : P ⟶ Q) (hQ : IsProP2 Q) (V : OpenNormalSubgroup ↑Q.toProfinite.toTop) : Pro2Index P

The pro-2 index f⁻¹V of P attached to an open normal V ⊴ Q (with Q pro-2).

Equations

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

noncomputable def Q2Presentation.comapIndexHom {P Q : ProfiniteGrp.{u}} (f : P ⟶ Q) (hQ : IsProP2 Q) {V W : OpenNormalSubgroup ↑Q.toProfinite.toTop} (h : V ≤ W) : comapIndex f hQ V ⟶ comapIndex f hQ W

Monotonicity of comapIndex: a transition V ⟶ W of open normals of Q induces a transition f⁻¹V ⟶ f⁻¹W of pro-2 indices of P.

Equations

• Q2Presentation.comapIndexHom f hQ h = CategoryTheory.ObjectProperty.homMk (CategoryTheory.homOfLE ⋯)

noncomputable def Q2Presentation.quotientMapFG {P Q : ProfiniteGrp.{u}} (f : P ⟶ Q) (hQ : IsProP2 Q) (V : OpenNormalSubgroup ↑Q.toProfinite.toTop) : (pro2Diagram P).obj (comapIndex f hQ V) ⟶ Q.diagram.obj V

The finite quotient map P ⧸ f⁻¹V ⟶ Q ⧸ V induced by f.

Equations

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

noncomputable def Q2Presentation.liftCone {P Q : ProfiniteGrp.{u}} (f : P ⟶ Q) (hQ : IsProP2 Q) : CategoryTheory.Limits.Cone Q.diagram

The cone over diagram Q with apex MaximalPro2Quotient P assembling the induced finite quotient maps; its limit lift is the universal morphism.

Equations

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

noncomputable def Q2Presentation.maxPro2Lift {P Q : ProfiniteGrp.{u}} (f : P ⟶ Q) (hQ : IsProP2 Q) : MaximalPro2Quotient P ⟶ Q

The universal morphism MaximalPro2Quotient P ⟶ Q lifting f : P ⟶ Q (for Q pro-2).

Equations

• Q2Presentation.maxPro2Lift f hQ = Q.isLimitCone.lift (Q2Presentation.liftCone f hQ)

theorem Q2Presentation.proj_comp_quotientMapFG {P Q : ProfiniteGrp.{u}} (f : P ⟶ Q) (hQ : IsProP2 Q) (V : OpenNormalSubgroup ↑Q.toProfinite.toTop) : CategoryTheory.CategoryStruct.comp (ProfiniteGrp.proj (comapIndex f hQ V).obj) (quotientMapFG f hQ V) = CategoryTheory.CategoryStruct.comp f (ProfiniteGrp.proj V)

The induced finite quotient projection P ⟶ P ⧸ f⁻¹V followed by the quotient map P ⧸ f⁻¹V ⟶ Q ⧸ V equals f followed by Q ⟶ Q ⧸ V.

theorem Q2Presentation.maxPro2Lift_fac {P Q : ProfiniteGrp.{u}} (f : P ⟶ Q) (hQ : IsProP2 Q) : CategoryTheory.CategoryStruct.comp (maxPro2Proj P) (maxPro2Lift f hQ) = f

Factorisation: f = maxPro2Proj P ≫ maxPro2Lift f hQ.

theorem Q2Presentation.maxPro2Lift_unique {P Q : ProfiniteGrp.{u}} (f : P ⟶ Q) (hQ : IsProP2 Q) (g : MaximalPro2Quotient P ⟶ Q) (hg : CategoryTheory.CategoryStruct.comp (maxPro2Proj P) g = f) : g = maxPro2Lift f hQ

Uniqueness: any g with f = maxPro2Proj P ≫ g equals maxPro2Lift f hQ. Two such morphisms agree on the dense range of maxPro2Proj P.

theorem Q2Presentation.maxPro2_universal {P Q : ProfiniteGrp.{u}} (f : P ⟶ Q) (hQ : IsProP2 Q) : ∃! g : MaximalPro2Quotient P ⟶ Q, f = CategoryTheory.CategoryStruct.comp (maxPro2Proj P) g

Universal property of the maximal pro-2 quotient. For any pro-2 group Q and continuous f : P ⟶ Q, there is a unique g : MaximalPro2Quotient P ⟶ Q with f = maxPro2Proj P ≫ g. This is the load-bearing tool used by the boundary isomorphisms.