§3 statements, marked-quotient half: Prop. 3.10 and Prop. 3.14 #
Theorems implementing the paper's Prop. 3.10 (maximal pro-2 quotient of Γ_A is Π,
eq. (20); marked local identification (Π, ν₂) ≅ (G_{ℚ₂}(2), ν_ur), via Cor. 3.12) and
Prop. 3.14 (fully marked tame and pro-2 quotients — the eq. (27) boundary epimorphisms),
phrased against the definitions in GQ2/BoundaryFrame.lean (Ttame, PiBd, nuT, nuTwo,
BoundaryMaps).
This stays separate from GQ2/SectionThree.lean because it imports the boundary layer, while the
core §3 statements remain upstream. Everything is nevertheless in namespace
GQ2.SectionThree. The local marked equivalence uses Prop. 1.1, the Nielsen transform of
Prop. 3.11/Cor. 3.12, and the Z₂ bridge below; the final BoundaryMaps witness is constructed
in GQ2/BoundaryMapsWitness.lean.
Proposition 3.10 — the maximal pro-2 quotient of Γ_A is Π #
Paper (20)/(21): Π = ⟨σ, x₀, x₁ ∣ x₀^{σ²} x₀ [x₁,σ] = 1⟩_{pro-2} with
ν₂(σ, x₀, x₁) = (1, 0, 0). The paper's proof: in a finite 2-group quotient Lemma 3.1
forces τ = 1 and ω₂ acts as the identity, so the auxiliary words collapse
(u_i = x_i, d₀ = c₀ = d_g = h_c = 1, g₀ = σ², h₀ = x₀^{σ²}x₀) and relation (6)
becomes the relator of (20); conversely every finite quotient of (20) is admissible with
τ = 1.
Prop. 3.10, Γ_A half: the maximal pro-2 quotient of Γ_A is Π, canonically —
the isomorphism matches the marked generators (σ ↦ σ, x₀ ↦ x₀, x₁ ↦ x₁; τ dies).
The proof is the word-collapse computation above, through the profinite-exponentiation API and
the literal Γ_A construction.
Prop. 3.10, local half = Cor. 3.12 (fully marked form): (Π, ν₂) is isomorphic to
the fully unramified marked pair (G_{ℚ₂}(2), ν_ur). The ℤ₂-identification between the
two ν-targets (Ztwo = maxProPQuotient 2 ℤ̂ on the boundary side, Multiplicative ℤ₂ on
the B5 side) is quantified explicitly as a continuous isomorphism ι pinned by
ι(1) = ofAdd 1; the ν_ur-values are read through arbitrary lifts, as in prop_1_1.
The proof combines Prop. 1.1, the Nielsen transform (23)/(24) of Prop. 3.11, and the
Ztwo ≅ ℤ₂ bridge.
Proposition 3.14 — fully marked tame and pro-2 quotients #
Paper: ν_t : T_tame ↠ ℤ₂ (σ ↦ 1, τ ↦ 0) and ν₂ : Π ↠ ℤ₂ (eq. (21)); for each source
Γ ∈ {Γ_A, G_{ℚ₂}} the tame and maximal pro-2 quotient maps may be chosen with equal
ν-composites — the common unramified character ν_Γ : Γ ↠ ℤ₂. The chosen-maps data is
exactly the boundary-frame design's BoundaryMaps bundle (eq. (27)); the two surjectivity claims below are the
↠-content of the displayed arrows (flagged in BoundaryFrame.lean as the §3 statement layer/Prop. 3.2 scope).
Prop. 3.14 (with Cor. 3.12 supplying the G_{ℚ₂}-side): the eq. (27) boundary data
exists — tame and maximal pro-2 quotient maps for both sources, ν-compatible, jointly
surjective onto the fibred boundary, with the Γ_A-side taking the marked generator values
and the G_{ℚ₂}-side pinned intrinsically (Lemma 3.3 2-core kernel; proPKernel kernel).
The construction instantiates BoundaryMaps from Prop. 3.2 and Prop. 1.1.
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- Cor 3.12 = ⟦cor-relativeDemushkin⟧
- eq. (20) = ⟦eq-Pi⟧
- eq. (21) = ⟦eq-nu2⟧
- eq. (27) = ⟦eq-boundarymap⟧
- Lemma 3.1 = ⟦lem-tamefinite⟧
- Lemma 3.3 = ⟦lem-o2tame⟧
- Prop 1.1 = ⟦prop-markedDem⟧
- Prop 3.10 = ⟦prop-pro2⟧
- Prop 3.11 = ⟦prop-abstractDemushkin⟧
- Prop 3.14 = ⟦prop-compatiblemarking⟧