§3 boundary construction — Prop 3.10 (both halves) and Prop 3.14 #
Proofs of the three §3-marked statements declared in GQ2/SectionThreeMarked.lean:
- Prop 3.10,
Γ_Ahalf (prop_3_10_gammaA): the maximal pro-2quotient ofΓ_AisΠ, matching the marked generators (σ ↦ πσ,τ ↦ 1,x₀ ↦ πx₀,x₁ ↦ πx₁). - Prop 3.10, local half (
prop_3_10_local_marked):(Π, ν₂) ≅ (G_{ℚ₂}(2), ν_ur). - Prop 3.14 (
prop_3_14 : Nonempty BoundaryMaps): the eq. (27) boundary data.
The analytical heart is the word collapse: at τ = 1 (forced in every finite 2-group
quotient by Lemma 3.1, Tame.tame_odd_order, since τ then has both odd and 2-power order)
the auxiliary words trivialise (u_i = x_i, d₀ = c₀ = d_g = h_c = 1, g₀ = σ²,
h₀ = σ⁻²x₀σ²·x₀) and the wild relator (6) becomes the pro-2 relator (20) = piRelator.
Everything downstream mirrors GQ2/Prop32.lean's Γ_A-side Prop 3.2 (phiA/chiW/tameAEquiv,
isAdmissible_tameClassifier_level, NA_le_ker_tameClassifier) one presentation up, using the
maximal-pro-2-quotient universal property (GQ2/MaxProP.lean: proPKernel_le_ker,
maxProPHomEquiv, isProP_quotient_proPKernel).
The three public statements are supplied by prop_3_10_gammaA_proved in this file,
prop_3_10_local_marked_proved in GQ2/LocalMarked.lean, and prop_3_14_proved in
GQ2/BoundaryMapsWitness.lean. Their separation follows the import graph: the two marked
isomorphisms are constructed before the final BoundaryMaps witness bundles both sources.
The wild-relator collapse at τ = 1 #
The word collapse. With τ = 1 and ω₂ acting as the identity on σ, x₀, x₁
(automatic in a 2-group, where every element has 2-power order), the wild relator word (6)
h₀ · u₁⁻¹ · x₁^σ · c₀ equals the pro-2 relator word (20)
σ⁻²x₀σ² · x₀ · [x₁, σ].
The wild relation at (σ, 1, x₀, x₁) is equivalent to the pro-2 relator vanishing, under
the ω₂-fixes hypotheses.
Both target groups are pro-2 #
Π is a pro-2 group (a maximal pro-2 quotient).
The maximal pro-2 quotient of Γ_A is a pro-2 group.
Topological generation of Π and the relator word #
The evaluation F₃ → Π, σ ↦ πσ, x₀ ↦ πx₀, x₁ ↦ πx₁ (presentation projection then max
pro-2 projection).
Equations
- GQ2.SectionThree.evalPi = (GQ2.maxProPMk 2 ↑(GQ2.profinitePresentation {GQ2.piRelator}).toProfinite.toTop).comp (GQ2.quotientMk (GQ2.relatorSubgroup {GQ2.piRelator}))
Instances For
Π is topologically generated by πσ, πx₀, πx₁.
In every discrete continuous quotient of Π, the images of πσ, πx₀, πx₁ generate.
The forward descent Γ_A → Π #
The pro-2 classifier F₄ ⟶ Π: σ ↦ πσ, τ ↦ 1, x₀ ↦ πx₀, x₁ ↦ πx₁.
Equations
- GQ2.SectionThree.piClassifier = (GQ2.FreeProfiniteGroup.homEquiv (Fin 4) GQ2.PiBd).symm ![GQ2.piSigma, 1, GQ2.piX0, GQ2.piX1]
Instances For
Through every finite 2-group level of Π, the marking pushed from the pro-2 classifier is
admissible: τ ↦ 1, and the wild relator collapses to piRelator, which vanishes.
N_A is contained in the kernel of the pro-2 classifier (each finite level is admissible).
The descent φ_Π : Γ_A → Π (σ ↦ πσ, τ ↦ 1, x₀ ↦ πx₀, x₁ ↦ πx₁) — Prop 3.14's pro2A.
Equations
- GQ2.SectionThree.phiP = GQ2.quotientLift GQ2.NA (ProfiniteGrp.Hom.hom GQ2.SectionThree.piClassifier) GQ2.SectionThree.NA_le_ker_piClassifier
Instances For
The backward descent Π → Γ_A(2) #
The marked tame relation holds in Γ_A (relation (5) dies in the admissible limit).
τ dies in the maximal pro-2 quotient of Γ_A (Lemma 3.1): in every finite 2-group
level the image of τ has both odd order (tame relation) and 2-power order, hence is trivial.
The pro-2 relator (20) holds in the maximal pro-2 quotient of Γ_A. In every finite
2-group level the wild relation (6) holds (it dies in Γ_A, wildRelator_mem_NA) and τ ↦ 1,
so the collapse gives piRelator = 1; separated by finite quotients, it vanishes in the limit.
The marked isomorphism Γ_A(2) ≅ Π (Prop 3.10, Γ_A half) #
The forward map Φ : Γ_A(2) → Π, the descent of φ_Π through the maximal pro-2 quotient
(Π is pro-2, so φ_Π kills proPKernel).
Equations
- GQ2.SectionThree.PhiMax = GQ2.quotientLift (GQ2.proPKernel 2 ↑GQ2.GammaA.toProfinite.toTop) GQ2.SectionThree.phiP GQ2.SectionThree.PhiMax._proof_2
Instances For
The backward base map F₃ → Γ_A(2), σ ↦ [σ], x₀ ↦ [x₀], x₁ ↦ [x₁].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The base map kills piRelator (that is the backward collapse piRelatorWord_maxA_eq_one).
The lift through the presentation Π(pre) → Γ_A(2).
Equations
- GQ2.SectionThree.psiPres = GQ2.presentationLift {GQ2.piRelator} (ProfiniteGrp.Hom.hom GQ2.SectionThree.psiBase) GQ2.SectionThree.psiPres._proof_3
Instances For
The backward map Ψ : Π → Γ_A(2) (through the max pro-2 universal property).
Equations
Instances For
Γ_A(2) is topologically generated by the images of the four marked generators.
Φ ∘ Ψ = id on Π (both fix πσ, πx₀, πx₁; density).
Ψ ∘ Φ = id on Γ_A(2) (checked on the four marked generator images; density).
The marked isomorphism Γ_A(2) ≅ Π (Prop 3.10, Γ_A half).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prop 3.10, Γ_A half (proved): the maximal pro-2 quotient of Γ_A is Π, matching
the marked generators.
Γ_A is topologically generated by its four marked generators.
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- Cor 3.12 = ⟦cor-relativeDemushkin⟧
- eq. (27) = ⟦eq-boundarymap⟧
- Lemma 3.1 = ⟦lem-tamefinite⟧
- Prop 3.10 = ⟦prop-pro2⟧
- Prop 3.14 = ⟦prop-compatiblemarking⟧
- Prop 3.2 = ⟦prop-tamequotient⟧