The maximal pro-2 quotient of the tame group is ℤ₂ (Stage C)

This file identifies the maximal pro-2 quotient of the profinite tame group Ttame with the unramified ℤ₂ (manuscript reference/q2_manuscript.tex, Lemma 3.1 lem:tamefinite, Prop 3.2 prop:tamequotient; plan reference/plan_4turns.md Turn 4 §2).

The unramified character nu_t : Ttame ⟶ ProfiniteZ2 (σ ↦ 1, τ ↦ 0) exhibits ℤ₂ as the maximal pro-2 quotient: it is surjective, ℤ₂ is pro-2, and every finite 2-group quotient of Ttame kills τ (Lemma 3.1: τ has odd order, hence = 1 in a 2-group), so the quotient factors through the unramified ⟨σ⟩ = ℤ₂ direction. Combining the universal property of MaximalPro2Quotient both ways gives the isomorphism Ttame_maximal_pro2.

The tame relation holds in Ttame

theorem Q2Presentation.Ttame_tame_rel : rconj tameTau tameSigma = tameTau ^ 2

The tame relation τ^σ = τ² holds in Ttame (not merely after projection): the universal generators satisfy rconj τ σ = τ².

τ dies in every finite 2-group quotient (Lemma 3.1)

theorem Q2Presentation.tameTau_mem_pro2 (U : Pro2Index Ttame) : tameTau ∈ ↑U.obj.toOpenSubgroup

In every pro-2 index of Ttame, τ lies in the subgroup. Equivalently, the image of τ in any finite 2-group quotient Ttame ⧸ U is 1: the tame relation forces τ to have odd order (finite_tame_tau_odd), but in a 2-group every order is a power of 2, so the order is 1.

ℤ₂ is pro-2

theorem Q2Presentation.isPGroup_two_C2Pow (n : ℕ) : IsPGroup 2 (C2Pow n)

Each finite layer C2Pow n = Multiplicative (ZMod (2ⁿ)) is a 2-group.

theorem Q2Presentation.z2_exists_dominating (J : Finset ℕᵒᵖ) : ∃ (B : ℕᵒᵖ), ∀ j ∈ J, Nonempty (B ⟶ j)

Finite cofiltered domination in ℕᵒᵖ. Any finite set of layer indices is dominated by a single index B admitting a reduction morphism to each.

theorem Q2Presentation.exists_z2Projection_ker_le (W : OpenNormalSubgroup ↑ProfiniteZ2.toProfinite.toTop) : ∃ (n : ℕ), (ProfiniteGrp.Hom.hom (z2Projection n)).ker ≤ ↑W.toOpenSubgroup

Coordinate domination for ℤ₂. Every open normal subgroup W ⊴ ℤ₂ contains the kernel of some coordinate projection z2Projection n (the coordinate kernels form a neighbourhood basis of 1). Mirrors exists_coordProj_ker_le.

theorem Q2Presentation.profiniteZ2_isProP2 : IsProP2 ProfiniteZ2

ℤ₂ is pro-2: every finite continuous quotient of ℤ₂ is a 2-group. Given an open normal W, the domination lemma supplies a coordinate projection φ = z2Projection n with ker φ ≤ W; then ℤ₂ ⧸ ker φ ≅ range φ ≤ C2Pow n is a 2-group, and ℤ₂ ⧸ W is a quotient of it. Mirrors maxPro2_isProP2.

nu_t is surjective

theorem Q2Presentation.tameLayerHom_surjective (n : ℕ) : Function.Surjective ⇑(tameLayerHom n)

Each unramified layer hom tameLayerHom n : Ttame →* C2Pow n is surjective (its image contains the additive generator ofAdd 1 = tameLayerHom n σ, which generates C2Pow n).

theorem Q2Presentation.nu_t_denseRange : DenseRange ⇑(ProfiniteGrp.Hom.hom nu_t)

The image of nu_t is dense: a basic open set fixes finitely many ℤ₂ coordinates; a single dominating layer B collapses them; surjectivity of tameLayerHom B.unop lifts the target value, and inverse-limit compatibility propagates the match to the smaller layers. Mirrors maxPro2Proj_denseRange.

theorem Q2Presentation.nu_t_surjective : Function.Surjective ⇑(ProfiniteGrp.Hom.hom nu_t)

The unramified character nu_t : Ttame ⟶ ℤ₂ is surjective. Its range is closed (continuous image of the compact Ttame) and dense (nu_t_denseRange), hence everything.

Maximality: ker nu_t is contained in every pro-2 index (Lemma 3.1)

theorem Q2Presentation.nu_t_ker_le (U : Pro2Index Ttame) {x : ↑Ttame.toProfinite.toTop} (hx : (ProfiniteGrp.Hom.hom nu_t) x = 1) : x ∈ ↑U.obj.toOpenSubgroup

The maximality core. If nu_t x = 1 then x lies in every pro-2 index U of Ttame. Each finite 2-group quotient F = Ttame ⧸ U is cyclic generated by the image y = mk σ (because τ ↦ 1, tameTau_mem_pro2), so the quotient map factors through the k-th unramified layer (k with Nat.card F = 2ᵏ): mk = ψ ∘ tameLayerHom k, where ψ : C2Pow k →* F sends the additive generator to y. Since tameLayerHom k x = z2Projection k (nu_t x) = 1, we get mk x = ψ 1 = 1, i.e. x ∈ U.

The identification MaximalPro2Quotient Ttame ≅ ℤ₂

noncomputable def Q2Presentation.Ttame_maximal_pro2 : MaximalPro2Quotient Ttame ≅ ProfiniteZ2

The maximal pro-2 quotient of the tame group is the unramified ℤ₂ (manuscript Lemma 3.1 + Prop 3.2). The unramified character nu_t lifts (since ℤ₂ is pro-2) to a canonical comparison g : MaximalPro2Quotient Ttame ⟶ ℤ₂; it is surjective because nu_t is, and injective by the maximality core nu_t_ker_le (every finite 2-group quotient of Ttame kills τ, hence factors through the unramified line), so it is an isomorphism.

Equations

• Q2Presentation.Ttame_maximal_pro2 = CategoryTheory.asIso (Q2Presentation.maxPro2Lift Q2Presentation.nu_t Q2Presentation.profiniteZ2_isProP2)