The common tame–pro-2 boundary ∂_bd = T_A ×_{ℤ₂} Π and the boundary package (Stage C)

This file assembles the compatible tame and maximal pro-2 quotient maps of a profinite group Γ into a single boundary condition, realising manuscript §sec:boundary (reference/q2_manuscript.tex, l.1135–1161) and plan reference/plan_4turns.md Turn 4 §6–7.

Main contents:

• BoundaryPackage Γ — the uniform data of a tame quotient tameMap : Γ ↠ Ttame, a pro-2 quotient pro2Map : Γ ↠ PiGrp, and a common unramified character nu : Γ ⟶ ℤ₂ through which both factor (tameMap ≫ nu_t = nu = pro2Map ≫ nu_2).
• Boundary : ProfiniteGrp — the fibre product T_A ×_{ℤ₂} Π = pullback nu_t nu_2 (eq:boundaryobject). ProfiniteGrp has all limits, hence pullbacks.
• BoundaryPackage.toBoundary : Γ ⟶ Boundary — the boundary map b_Γ of eq:boundarymap, the pullback.lift of the compatible square.
• boundaryPackage_toBoundary_surjective — profinite Goursat surjectivity of b_Γ. Manuscript: "Surjectivity follows from profinite Goursat. Any common quotient of T_A and the pro-2 group Π is a pro-2 quotient of T_A, hence a quotient of its maximal pro-2 quotient ℤ₂."

The Goursat argument (manuscript)

Write S = range(b_Γ), a closed subgroup of Boundary = T_A ×_{ℤ₂} Π projecting onto both factors (tameMap, pro2Map surjective). Surjectivity reduces, by elementary group manipulation against the two surjections and the shared character, to the single Goursat core (tameMap_ker_pro2Map_ge):

every t₀ ∈ ker(ν_t) is tameMap ε for some ε ∈ ker(pro2Map).

i.e. ker(ν_t) ⊆ tameMap (ker pro2Map). This is the assertion that the common quotient T_A / tameMap(ker pro2Map) — being a quotient of the pro-2 group Π — is pro-2, hence (since ℤ₂ = MaximalPro2Quotient T_A via ν_t, Ttame_maximal_pro2) factors through ν_t, forcing ker ν_t ⊆ tameMap(ker pro2Map). The reverse inclusion is the compatibility tameMap ≫ ν_t = pro2Map ≫ ν_2 evaluated on ker pro2Map.

The boundary package

structure Q2Presentation.BoundaryPackage (Γ : ProfiniteGrp.{0}) : Type

A boundary package on a profinite group Γ: the uniform Stage-C data of a tame quotient, a maximal pro-2 quotient, and a common unramified character ℤ₂ through which both factor (manuscript Prop 3.14, prop:compatiblemarking; plan Turn 4 §6). The compatibility tameMap ≫ ν_t = ν = pro2Map ≫ ν_2 records that the two markings agree on the full unramified coordinate, not merely modulo 2.

• tameMap : Γ ⟶ Ttame

  The tame quotient map Γ ↠ T_A.

• tame_surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.tameMap)

  The tame quotient map is surjective.

• pro2Map : Γ ⟶ PiGrp

  The maximal pro-2 quotient map Γ ↠ Π.

• pro2_surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.pro2Map)

  The pro-2 quotient map is surjective.

• nu : Γ ⟶ ProfiniteZ2

  The common unramified character Γ ⟶ ℤ₂.

• tame_nu : CategoryTheory.CategoryStruct.comp self.tameMap nu_t = self.nu

  The tame map composed with the tame unramified character is ν.

• pro2_nu : CategoryTheory.CategoryStruct.comp self.pro2Map nu_2 = self.nu

  The pro-2 map composed with the pro-2 unramified character is ν.

theorem Q2Presentation.BoundaryPackage.nu_t_tameMap {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (γ : ↑Γ.toProfinite.toTop) : (ProfiniteGrp.Hom.hom nu_t) ((ProfiniteGrp.Hom.hom B.tameMap) γ) = (ProfiniteGrp.Hom.hom nu_2) ((ProfiniteGrp.Hom.hom B.pro2Map) γ)

The compatibility square. Both quotient maps induce the same unramified character: ν_t ∘ tameMap = ν_2 ∘ pro2Map pointwise.

The boundary object ∂_bd = T_A ×_{ℤ₂} Π

instance Q2Presentation.instPreservesLimitsOfShapeProfiniteGrpWalkingCospanForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite_q2Presentation : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget ProfiniteGrp.{0})

forget ProfiniteGrp preserves limits of shape WalkingCospan (hence pullbacks): it factors as forget₂ ProfiniteGrp Profinite ⋙ forget Profinite, both of which preserve limits. Needed for the concrete element description of the boundary pullback.

noncomputable def Q2Presentation.Boundary : ProfiniteGrp.{0}

The common tame–pro-2 boundary ∂_bd = T_A ×_{ℤ₂} Π, the fibre product of the two unramified characters ν_t : T_A ⟶ ℤ₂ and ν_2 : Π ⟶ ℤ₂ (manuscript eq:boundaryobject). ProfiniteGrp has all limits, so the pullback exists.

Equations

• Q2Presentation.Boundary = CategoryTheory.Limits.pullback Q2Presentation.nu_t Q2Presentation.nu_2

noncomputable def Q2Presentation.BoundaryPackage.toBoundary {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) : Γ ⟶ Boundary

The boundary map b_Γ : Γ ⟶ ∂_bd (manuscript eq:boundarymap), the universal map into the fibre product induced by the compatible pair (tameMap, pro2Map).

Equations

• B.toBoundary = CategoryTheory.Limits.pullback.lift B.tameMap B.pro2Map ⋯

@[simp]

theorem Q2Presentation.BoundaryPackage.toBoundary_fst {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (γ : ↑Γ.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.pullback.fst nu_t nu_2)) ((ProfiniteGrp.Hom.hom B.toBoundary) γ) = (ProfiniteGrp.Hom.hom B.tameMap) γ

@[simp]

theorem Q2Presentation.BoundaryPackage.toBoundary_snd {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (γ : ↑Γ.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.pullback.snd nu_t nu_2)) ((ProfiniteGrp.Hom.hom B.toBoundary) γ) = (ProfiniteGrp.Hom.hom B.pro2Map) γ

Concrete description of the boundary pullback

theorem Q2Presentation.boundary_ext {x y : ↑Boundary.toProfinite.toTop} (h1 : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.pullback.fst nu_t nu_2)) x = (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.pullback.fst nu_t nu_2)) y) (h2 : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.pullback.snd nu_t nu_2)) x = (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.pullback.snd nu_t nu_2)) y) : x = y

Boundary extensionality. Two boundary points agree once their two coordinate projections agree. forget ProfiniteGrp preserves the pullback, so a boundary point is determined by its pullback.fst/pullback.snd coordinates (Concrete.pullbackMk).

Profinite infrastructure for the Goursat core

The single non-elementary ingredient of the Goursat core (tameMap_ker_pro2Map_ge) is a profinite-topology fact absent from mathlib in usable form: the common quotient T_A / tameMap(ker pro2Map) is pro-2, which via the maximality of ν_t (nu_t_ker_le) forces ker ν_t ⊆ tameMap(ker pro2Map). We supply it in two reusable pieces:

• isPGroup_two_of_isProP2 — a finite discrete continuous quotient of a pro-2 group is a 2-group (the kernel is open normal, so it is one of the defining quotients).
• boundaryQuot_isPGroup_two — for a boundary package, every open normal N ⊴ T_A containing M = tameMap(ker pro2Map) has T_A ⧸ N a 2-group: the quotient map T_A ↠ T_A ⧸ N, precomposed with the surjection tameMap, kills ker pro2Map, hence descends along the quotient map pro2Map to a continuous surjection Π ↠ T_A ⧸ N; apply the previous lemma to the pro-2 group Π (isProP2_PiGrp).

The bridge from these per-N statements to t₀ ∈ M is mathlib's ProfiniteGrp.closedSubgroup_eq_sInf_open (a closed subgroup of a profinite group is the intersection of the open subgroups containing it), reduced to the normal core.

theorem Q2Presentation.isPGroup_two_of_isProP2 {P : ProfiniteGrp.{0}} (hP : IsProP2 P) {K : Type u_1} [Group K] [TopologicalSpace K] [DiscreteTopology K] (f : ↑P.toProfinite.toTop →* K) (hcont : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : IsPGroup 2 K

A finite discrete continuous quotient of a pro-2 group is a 2-group. If P is pro-2 and f : P →* K is a continuous surjection onto a discrete group K, then K is a 2-group: ker f is open (preimage of the open point 1) and normal, so it is an OpenNormalSubgroup V with P ⧸ V ≅ K (first isomorphism theorem); IsProP2 P makes P ⧸ V a 2-group.

def Q2Presentation.BoundaryPackage.tameKerImage {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) : Subgroup ↑Ttame.toProfinite.toTop

The closed normal subgroup M = tameMap(ker pro2Map) ⊴ T_A (the tame image of the pro-2 kernel), as a Subgroup Ttame.

Equations

• B.tameKerImage = Subgroup.map (ProfiniteGrp.Hom.hom B.tameMap).toMonoidHom (ProfiniteGrp.Hom.hom B.pro2Map).ker

theorem Q2Presentation.BoundaryPackage.tameKerImage_isClosed {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) : IsClosed ↑B.tameKerImage

instance Q2Presentation.BoundaryPackage.tameKerImage_normal {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) : B.tameKerImage.Normal

theorem Q2Presentation.BoundaryPackage.boundaryQuot_isPGroup_two {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (N : OpenNormalSubgroup ↑Ttame.toProfinite.toTop) (hMN : B.tameKerImage ≤ ↑N.toOpenSubgroup) : IsPGroup 2 (↑Ttame.toProfinite.toTop ⧸ ↑N.toOpenSubgroup)

Every open normal N ⊴ T_A containing M = tameMap(ker pro2Map) has T_A ⧸ N a 2-group. The composite q : Γ ↠ T_A ⧸ N (mk ∘ tameMap) kills ker pro2Map (since tameMap(ker pro2Map) = M ⊆ N), so it descends along the quotient map pro2Map (a continuous surjection of profinite groups, hence a topological quotient map) to a continuous surjection q̄ : Π ↠ T_A ⧸ N. As Π is pro-2 (isProP2_PiGrp), isPGroup_two_of_isProP2 makes T_A ⧸ N a 2-group.

The Goursat core

theorem Q2Presentation.tameMap_ker_pro2Map_ge {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) {t₀ : ↑Ttame.toProfinite.toTop} (ht₀ : (ProfiniteGrp.Hom.hom nu_t) t₀ = 1) : ∃ (ε : ↑Γ.toProfinite.toTop), (ProfiniteGrp.Hom.hom B.tameMap) ε = t₀ ∧ (ProfiniteGrp.Hom.hom B.pro2Map) ε = 1

The Goursat core (manuscript §sec:boundary): for a boundary package on Γ, the tame image of ker(pro2Map) contains the kernel of the unramified character ν_t, i.e. ker ν_t ⊆ tameMap (ker pro2Map). This is the single load-bearing content of "Surjectivity follows from profinite Goursat"; everything else (exists_pro2_of_ker_nu_2, exists_preimage, toBoundary_surjective) is the elementary group-theoretic reduction to it, proved below.

MATHEMATICAL PROOF. Let M := tameMap (ker pro2Map), a closed normal subgroup of T_A (continuous image of the compact ker pro2Map), with M ⊆ ker ν_t (compatibility: k ∈ ker pro2Map ⟹ ν_t (tameMap k) = ν_2 (pro2Map k) = ν_2 1 = 1). The common quotient T_A / M is pro-2: every open normal V ⊇ M gives a finite quotient T_A / V that is the image of the surjection q_V ∘ tameMap : Γ ↠ T_A / V, whose kernel contains ker pro2Map (as tameMap (ker pro2Map) = M ⊆ V); hence T_A / V is a finite continuous quotient of Γ / ker pro2Map ≅ Π, a 2-group by isProP2_PiGrp. Since ν_t : T_A ↠ ℤ₂ realises the maximal pro-2 quotient (Ttame_maximal_pro2; nu_t_ker_le is the kernel half), the pro-2 quotient T_A / M factors through ν_t, forcing ker ν_t ⊆ M. Surjectivity of tameMap on ker ν_t onto its image in M then yields the witness ε.

FORMALISATION. The two non-elementary ingredients are supplied above: (1) mathlib's ProfiniteGrp.closedSubgroup_eq_sInf_open (a closed subgroup of a profinite group is the intersection of the open subgroups containing it) reduces t₀ ∈ M to "t₀ ∈ N for every open subgroup N ⊇ M", and passing to the normal core N₀ (Subgroup.normal_le_normalCore, Subgroup.normalCore_isClosed, Subgroup.isOpen_of_isClosed_of_finiteIndex) makes N₀ an open normal subgroup; (2) boundaryQuot_isPGroup_two shows T_A ⧸ N₀ is a 2-group, exhibiting N₀ as a Pro2Index Ttame, whereupon the existing maximality core nu_t_ker_le gives t₀ ∈ N₀ ⊆ N. M is closed (tameKerImage_isClosed) and normal (tameKerImage_normal).

Profinite Goursat surjectivity

theorem Q2Presentation.BoundaryPackage.exists_pro2_of_ker_nu_2 {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) {p₀ : ↑PiGrp.toProfinite.toTop} (hp₀ : (ProfiniteGrp.Hom.hom nu_2) p₀ = 1) : ∃ (γ₀ : ↑Γ.toProfinite.toTop), (ProfiniteGrp.Hom.hom B.tameMap) γ₀ = 1 ∧ (ProfiniteGrp.Hom.hom B.pro2Map) γ₀ = p₀

Goursat step B. Every p₀ ∈ ker(ν_2) is pro2Map γ₀ for some γ₀ ∈ ker(tameMap). Reduction to the Goursat core via surjectivity of pro2Map and the compatibility square.

theorem Q2Presentation.BoundaryPackage.exists_preimage {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) {t : ↑Ttame.toProfinite.toTop} {p : ↑PiGrp.toProfinite.toTop} (hcompat : (ProfiniteGrp.Hom.hom nu_t) t = (ProfiniteGrp.Hom.hom nu_2) p) : ∃ (γ : ↑Γ.toProfinite.toTop), (ProfiniteGrp.Hom.hom B.tameMap) γ = t ∧ (ProfiniteGrp.Hom.hom B.pro2Map) γ = p

Goursat step A (full preimage). Every compatible pair (t, p) (with ν_t t = ν_2 p) is (tameMap γ, pro2Map γ) for some γ. Reduction to step B via surjectivity of tameMap and the compatibility square.

theorem Q2Presentation.BoundaryPackage.toBoundary_surjective {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) : Function.Surjective ⇑(ProfiniteGrp.Hom.hom B.toBoundary)

Profinite Goursat surjectivity of the boundary map (manuscript eq:boundarymap, "Surjectivity follows from profinite Goursat"). The boundary map b_Γ : Γ ↠ ∂_bd is surjective for every boundary package.

theorem Q2Presentation.boundaryPackage_toBoundary_surjective {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) : Function.Surjective ⇑(ProfiniteGrp.Hom.hom B.toBoundary)

Profinite Goursat surjectivity (top-level alias matching the plan/task target).

Acceptance checks