The common tame quotient map Γ_A ⟶ T_A (Stage C, Proposition 3.2)

This file constructs the manuscript's common tame quotient surjection

gammaTameMap : GammaA ⟶ Ttame

i.e. the candidate-side half of Proposition 3.2 (reference/q2_manuscript.tex, prop:tamequotient, l.421–434): there is a canonical map Γ_A → T_A realising Γ_A/W_A ≅ T_A (with the wild generators x₀, x₁ killed). Together with Lemma 3.3 (lem:o2tame, l.436–446, O₂(Γ_A) = W_A) this exhibits T_A as the common tame quotient. The kernel characterisation ker = W_A is not proved here — it is left for the boundary package; this file delivers the map, its surjectivity, and the generator-image lemmas needed downstream.

Method (universal property of the limit T_A)

This mirrors Boundary/CandidatePro2.lean's construction of p : Γ_A ⟶ Π, but on the tame side. We exhibit the canonical surjection sending σ ↦ tameSigma, τ ↦ tameTau, x₀ ↦ 1, x₁ ↦ 1 by assembling, for every tame index A : TameMarkedFinite, the per-coordinate surjection Γ_A ↠ Fin A.n supplied by the epimorphism semantics (GammaA_epi_equiv_admissible) applied to the tame marking σ ↦ A.s, τ ↦ A.t, x₀ ↦ 1, x₁ ↦ 1 of Fin A.n.

The substantive new ingredient (relative to the pi side) is tameMarking_admissible: this marking is admissible. Generation is A.generates (the extra 1's do not enlarge the closure), the tame relator is A.tame, and — the crux — the wild relator vanishes: with x₀ = x₁ = 1 every wild-word atom collapses, the only surviving ω₂-power is (x_i τ)^{ω₂} = τ^{ω₂}, which is 1 because τ = A.t has odd order in a finite tame quotient (finite_tame_tau_odd A.tame), so powOmega2 (A.t) = 1 (powOmega2_eq_one_of_odd_order). This is the manuscript's "in the quotient by W_A the elements x₀, x₁ vanish and τ has odd order, so the wild relation disappears" (Prop 3.2 proof).

The surjections form a cone over tameDiagram; gammaTameMap is the induced map into the limit T_A. It is surjective because its range is closed (continuous image of the compact Γ_A) and dense (it contains the topological generators tameSigma, tameTau of T_A).

Generator extensionality for morphisms out of Γ_A

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

theorem Q2Presentation.gammaTameGen_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

The tame marking of Fin A.n and its admissibility

def Q2Presentation.tameMarking (A : TameMarkedFinite) : Marking (Fin A.n)

The admissible marking of Fin A.n attached to a tame-marked finite object A (σ ↦ A.s, τ ↦ A.t, x₀ ↦ 1, x₁ ↦ 1): the wild generators are killed.

Equations

• Q2Presentation.tameMarking A Q2Presentation.Gen.sigma = A.s
• Q2Presentation.tameMarking A Q2Presentation.Gen.tau = A.t
• Q2Presentation.tameMarking A Q2Presentation.Gen.x0 = 1
• Q2Presentation.tameMarking A Q2Presentation.Gen.x1 = 1

@[simp]

theorem Q2Presentation.tameMarking_sigma (A : TameMarkedFinite) : tameMarking A Gen.sigma = A.s

@[simp]

theorem Q2Presentation.tameMarking_tau (A : TameMarkedFinite) : tameMarking A Gen.tau = A.t

@[simp]

theorem Q2Presentation.tameMarking_x0 (A : TameMarkedFinite) : tameMarking A Gen.x0 = 1

@[simp]

theorem Q2Presentation.tameMarking_x1 (A : TameMarkedFinite) : tameMarking A Gen.x1 = 1

theorem Q2Presentation.tameMarking_admissible (A : TameMarkedFinite) : Admissible (tameMarking A)

The tame marking of A is admissible (Proposition 3.2).

• generates: A.s, A.t already generate (A.generates); the extra 1's do not enlarge the closure.
• tameRel: reduces to rconj A.t A.s = A.t², which is A.tame.
• wildRel: with x₀ = x₁ = 1 the wild word collapses to a product of ω₂-powers of τ = A.t; since A.t has odd order in the tame quotient (finite_tame_tau_odd A.tame), powOmega2 (A.t) = 1, so the relator vanishes.
• x₀, x₁ ∈ O₂: both images are 1 ∈ twoCore.

The canonical surjection Γ_A ↠ T_A

noncomputable def Q2Presentation.pSurjTame (A : TameMarkedFinite) : Profinite.SurjContHom GammaA (tameDiagram.obj A)

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

Equations

• Q2Presentation.pSurjTame A = (Q2Presentation.GammaA_epi_equiv_admissible (Fin A.n)).symm ⟨Q2Presentation.tameMarking A, ⋯⟩

theorem Q2Presentation.pSurjTame_gen (A : TameMarkedFinite) (a : Gen) : (ProfiniteGrp.Hom.hom (pSurjTame A).hom) (gammaGen a) = tameMarking A a

The surjection pSurjTame A sends gammaGen a to the marked generator tameMarking A a.

theorem Q2Presentation.pSurjTame_natural {A B : TameMarkedFinite} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (pSurjTame A).hom (tameDiagram.map f) = (pSurjTame B).hom

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

noncomputable def Q2Presentation.tameCone : CategoryTheory.Limits.Cone tameDiagram

The cone over tameDiagram with apex Γ_A assembled from pSurjTame.

Equations

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

noncomputable def Q2Presentation.gammaTameMap : GammaA ⟶ Ttame

The common tame quotient map gammaTameMap : Γ_A ⟶ T_A (Proposition 3.2).

Equations

• Q2Presentation.gammaTameMap = CategoryTheory.Limits.limit.lift Q2Presentation.tameDiagram Q2Presentation.tameCone

theorem Q2Presentation.gammaTameMap_proj (A : TameMarkedFinite) : CategoryTheory.CategoryStruct.comp gammaTameMap (CategoryTheory.Limits.limit.π tameDiagram A) = (pSurjTame A).hom

gammaTameMap followed by the coordinate projection at A is the surjection pSurjTame A.

The generator-image lemmas (needed downstream for the boundary package)

theorem Q2Presentation.gammaTameMap_apply_sigma : (ProfiniteGrp.Hom.hom gammaTameMap) (gammaGen Gen.sigma) = tameSigma

theorem Q2Presentation.gammaTameMap_apply_tau : (ProfiniteGrp.Hom.hom gammaTameMap) (gammaGen Gen.tau) = tameTau

theorem Q2Presentation.gammaTameMap_apply_x0 : (ProfiniteGrp.Hom.hom gammaTameMap) (gammaGen Gen.x0) = 1

theorem Q2Presentation.gammaTameMap_apply_x1 : (ProfiniteGrp.Hom.hom gammaTameMap) (gammaGen Gen.x1) = 1

Surjectivity of gammaTameMap

theorem Q2Presentation.gammaTameMap_denseRange : DenseRange ⇑(ProfiniteGrp.Hom.hom gammaTameMap)

gammaTameMap has dense range: its range is a subgroup containing the topological generators tameSigma, tameTau of T_A. Mirrors CandidatePro2.p_denseRange.

theorem Q2Presentation.gammaTameMap_surjective : Function.Surjective ⇑(ProfiniteGrp.Hom.hom gammaTameMap)

gammaTameMap is surjective. Its range is closed (continuous image of the compact Γ_A) and dense (gammaTameMap_denseRange), hence everything.

Acceptance checks