prop_3_14 : Nonempty BoundaryMaps — the eq. (27) boundary data

This file constructs the third SectionThreeMarked.lean ingredient: the full 21-field BoundaryMaps bundle (GQ2/BoundaryFrame.lean), i.e. tame + maximal-pro-2 quotient maps for both sources Γ_A and G_{ℚ₂}, ν-compatible, jointly surjective onto the fibred boundary ∂bd = T_tame ×_{ℤ₂} Π.

Structure of the construction

Everything reduces to a small kit:

• fiberProductExists (pure algebra) — surjectivity onto a fibred product A ×_C B from f : G ↠ A surjective, the square α∘f = β∘h commuting, and h(ker f) ⊇ ker β.
• proPKernel_image_ge — for a surjection φ : G ↠ H of profinite groups, proPKernel p H ⊆ φ(proPKernel p G).
• ker_nuT_le_proPKernel — ker ν_t ⊆ proPKernel 2 T_tame: ν_t : T_tame ↠ ℤ₂ is (contained in) the maximal pro-2 quotient, because the tame relation τ^σ = τ² forces τ ↦ 1 in every finite 2-group quotient.

With these, the kernel hypothesis of fiberProductExists (h(ker f) ⊇ ker β) becomes ker ν₂ ⊆ pro2X(ker tameX), discharged uniformly by hker_uniform.

• Γ_A side: tameA = φ_A (Prop. 3.2), pro2A = φ_Π (the marked pro-2 isomorphisms prop_3_10_gammaA), compatA by density on the four marked generators.
• G_{ℚ₂} side: tameF from prop_3_2_local (B10 LocalTameQuotient + Lemma 3.3 maximality), pro2F from prop_3_10_local_marked (the marked pro-2 isomorphisms) with R = GQ2.localReciprocity (B5).

The arithmetic compatibility: compatF (tame_reciprocity)

compatF : ∀ g, ν_t(tameF g) = ν₂(pro2F g) is the internal tame-vs-pro-2 compatibility on G_{ℚ₂}. Via prop_3_10_local_marked it reduces to the tame reciprocity statement ι(ν_t(tameF g)) = ν_ur(toAb g) — the tame quotient's unramified character equals ν_ur. The oriented B10 bundle now pins its tame quotient to the B5 reciprocity map. The two generator values supplied by B10, together with padic_hom_eq_of_gens, prove tame_reciprocity below; there is no remaining gap.

The pure-algebra fibred-product surjectivity kit

theorem GQ2.SectionThree.fiberProductExists {G : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Group G] [Group A] [Group B] [Group C] (α : A →* C) (β : B →* C) (f : G →* A) (h : G →* B) (hf : Function.Surjective ⇑f) (hcompat : ∀ (g : G), α (f g) = β (h g)) (hker : ∀ (b : B), β b = 1 → ∃ (g : G), f g = 1 ∧ h g = b) (t : A) (p : B) (hmem : α t = β p) : ∃ (g : G), f g = t ∧ h g = p

Fibred-product surjectivity (algebra). If f is surjective, the square commutes (α ∘ f = β ∘ h), and h maps ker f onto ker β, then every fibred-product point (t, p) with α t = β p is (f g, h g) for some g.

The two structural lemmas (see module docstring)

theorem GQ2.SectionThree.proPKernel_image_ge {p : ℕ} {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] (φ : G →ₜ* H) (hφ : Function.Surjective ⇑φ) : proPKernel p H ≤ Subgroup.map φ.toMonoidHom (proPKernel p G)

Surjective image of the pro-p kernel. For a surjection φ : G ↠ H of profinite groups, proPKernel p H ⊆ φ(proPKernel p G): H / φ(proPKernel p G) is a quotient of the pro-p group G(p), hence pro-p, so it kills proPKernel p H.

The Γ_A side

theorem GQ2.SectionThree.phiA_surjective : Function.Surjective ⇑phiA

φ_A : Γ_A ↠ T_tame is surjective (Prop 3.2, via tameAEquiv).

theorem GQ2.SectionThree.phiP_surjective : Function.Surjective ⇑phiP

φ_Π : Γ_A ↠ Π is surjective (the marked pro-2 isomorphisms prop_3_10_gammaA, via maxAEquiv).

theorem GQ2.SectionThree.compatA_proved (g : ↑GammaA.toProfinite.toTop) : GQ2.nuT (phiA g) = nuTwo (phiP g)

ν_t ∘ φ_A = ν₂ ∘ φ_Π on Γ_A: density on the four marked generators.

Reciprocity-side reduction kit: tame_reciprocity ⟸ two atomic values

Both f₁ = ι∘ν_t∘tameF and ν_ur∘toAb factor through G_{ℚ₂}^{ab} (abelian target ℤ₂); by denseRange_recip they agree iff they agree on recip(ℚ₂ˣ). Two continuous homs ℚ₂ˣ → ℤ₂ agreeing on the square-class generators {−4, 2, −3} (units_gen) are equal — their quotient's range is infinitely 2-divisible in ℤ₂, hence 0. The −4-value is automatic (−4 = (−1)·2², −1 is 2-torsion into torsion-free ℤ₂), so only μ(2) and μ(−3) remain as atoms.

theorem GQ2.SectionThree.mult_padic_sq_eq_one {x : Multiplicative ℤ_[2]} (hx : x ^ 2 = 1) : x = 1

x² = 1 in Multiplicative ℤ₂ forces x = 1 (ℤ₂ torsion-free).

theorem GQ2.SectionThree.padicInt_eq_zero_of_forall_two_pow_dvd {z : ℤ_[2]} (h : ∀ (n : ℕ), 2 ^ n ∣ z) : z = 0

An element of ℤ_[2] divisible by 2^n for every n is 0.

theorem GQ2.SectionThree.padic_hom_eq_of_gens (φ ψ : ℚ_[2]ˣ →* Multiplicative ℤ_[2]) (h2 : φ uniformizer = ψ uniformizer) (h3 : φ unitNeg3 = ψ unitNeg3) (x : ℚ_[2]ˣ) : φ x = ψ x

Square-class rigidity of ℤ₂-characters of ℚ₂ˣ. Two continuous homs ℚ₂ˣ → ℤ₂ agreeing on {2, −3} are equal: the −4-value is automatic, and units_gen + infinite 2-divisibility force the rest.

The G_{ℚ₂} side

noncomputable def GQ2.SectionThree.locTame [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : LocalTameQuotient

The chosen local tame quotient: the B10′ oriented witness (GQ2.tameQuotient), with Lemma 3.3's maximality attached (tameData_maximal). Using the axiom's witness directly (not prop_3_2_local.some) keeps the orientation clauses nuT_recip_unit/nuT_recip_uniformizer available for the two tame_recip_* atoms below.

Equations

• GQ2.SectionThree.locTame = { toTameQuotientData := GQ2.tameQuotient.toTameQuotientData, maximal := ⋯ }

noncomputable def GQ2.SectionThree.locPro2 [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : ∃ (ι : ↑Ztwo.toProfinite.toTop ≃ₜ* Multiplicative ℤ_[2]), ι ztwoOne = Multiplicative.ofAdd ↑1 ∧ ∃ (e : ↑(maxProPQuotient 2 AbsGalQ2).toProfinite.toTop ≃ₜ* ↑PiBd.toProfinite.toTop), ∀ (g : AbsGalQ2), localReciprocity.nu_ur (toAb g) = ι (nuTwo (e ((maxProPMk 2 AbsGalQ2) g)))

The chosen local pro-2 marked iso (the marked pro-2 isomorphisms prop_3_10_local_marked) at R = localReciprocity.

Equations

• ⋯ = ⋯

noncomputable def GQ2.SectionThree.tameFHom [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : AbsGalQ2 →ₜ* ↑Ttame.toProfinite.toTop

tameF : G_{ℚ₂} ↠ T_tame, the tame quotient map (composite G ↠ G/W ≅ T_tame).

Equations

• GQ2.SectionThree.tameFHom = { toMonoidHom := GQ2.SectionThree.locTame.equiv.toMonoidHom, continuous_toFun := ⋯ }.comp (GQ2.quotientMk GQ2.SectionThree.locTame.W)

noncomputable def GQ2.SectionThree.pro2FHom [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : AbsGalQ2 →ₜ* ↑PiBd.toProfinite.toTop

pro2F : G_{ℚ₂} ↠ Π, the maximal pro-2 quotient map (composite G ↠ G(2) ≅ Π).

Equations

• GQ2.SectionThree.pro2FHom = { toMonoidHom := ⋯.choose.toMonoidHom, continuous_toFun := ⋯ }.comp (GQ2.maxProPMk 2 GQ2.AbsGalQ2)

theorem GQ2.SectionThree.ker_tameFHom [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : tameFHom.ker = locTame.W

ker tameF = W.

theorem GQ2.SectionThree.ker_pro2FHom [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : pro2FHom.ker = proPKernel 2 AbsGalQ2

ker pro2F = proPKernel 2 G_{ℚ₂}.

noncomputable def GQ2.SectionThree.tameCharRaw [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : AbsGalQ2 →ₜ* Multiplicative ℤ_[2]

The tame unramified character f₁ = ι∘ν_t∘tameF : G_{ℚ₂} → Multiplicative ℤ₂.

Equations

• GQ2.SectionThree.tameCharRaw = { toMonoidHom := ⋯.choose.toMonoidHom, continuous_toFun := ⋯ }.comp (GQ2.nuT.comp GQ2.SectionThree.tameFHom)

noncomputable def GQ2.SectionThree.tameChar [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : AbsGalQ2ab →ₜ* Multiplicative ℤ_[2]

f₁ descended through the topological abelianization G_{ℚ₂}^{ab}.

Equations

• GQ2.SectionThree.tameChar = GQ2.SectionThree.abLiftG GQ2.SectionThree.tameCharRaw

theorem GQ2.SectionThree.tame_recip_uniformizer [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : tameChar (localReciprocity.recip uniformizer) = Multiplicative.ofAdd ↑(-1)

Atom (F) — the uniformizer: f₁(rec 2) = ofAdd(−1) (arithmetic Frobenius, geometric coordinate −1). Discharged by the B10′ orientation clause nuT_recip_uniformizer.

theorem GQ2.SectionThree.tame_recip_unitNeg3 [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : tameChar (localReciprocity.recip unitNeg3) = 1

Atom (U₋₃) — the unit −3: f₁(rec(−3)) = 1 (unramified-trivial). Discharged by the B10′ orientation clause nuT_recip_unit at the unit −3 (odd, hence a ℤ₂-unit).

theorem GQ2.SectionThree.tame_reciprocity [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (g : AbsGalQ2) : ⋯.choose (GQ2.nuT (tameFHom g)) = localReciprocity.nu_ur (toAb g)

Tame reciprocity (the boundary-witness reduction reduction): ι(ν_t(tameF g)) = ν_ur(toAb g). Both sides factor through G_{ℚ₂}^{ab}; agree on the dense image of recip by padic_hom_eq_of_gens, whose two generator inputs are exactly the atoms tame_recip_uniformizer (F) and tame_recip_unitNeg3 (U₋₃) matched against nu_ur_recip_*.

theorem GQ2.SectionThree.compatF_proved [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (g : AbsGalQ2) : GQ2.nuT (tameFHom g) = nuTwo (pro2FHom g)

ν_t ∘ tameF = ν₂ ∘ pro2F on G_{ℚ₂} — from tame_reciprocity and prop_3_10_local_marked.

Assembling the boundary maps

theorem GQ2.SectionThree.hker_uniform {dom : Type u_1} [Group dom] [TopologicalSpace dom] [IsTopologicalGroup dom] [CompactSpace dom] [T2Space dom] [TotallyDisconnectedSpace dom] (tameX : dom →ₜ* ↑Ttame.toProfinite.toTop) (pro2X : dom →ₜ* ↑PiBd.toProfinite.toTop) (htame : Function.Surjective ⇑tameX) (hpro : Function.Surjective ⇑pro2X) (hkerpro : proPKernel 2 dom ≤ pro2X.ker) (hcompat : ∀ (g : dom), GQ2.nuT (tameX g) = nuTwo (pro2X g)) (b : ↑PiBd.toProfinite.toTop) (hb : nuTwo b = 1) : ∃ (g : dom), tameX g = 1 ∧ pro2X g = b

The kernel hypothesis for fiberProductExists, uniformly: pro2X maps ker tameX onto ker ν₂, via ker ν_t ⊆ proPKernel 2 T_tame ⊆ tameX(proPKernel 2 dom) ⊆ tameX(ker tameX) (the last since proPKernel 2 dom ≤ ker pro2X and we correct within ker pro2X).

noncomputable def GQ2.SectionThree.boundaryMapsWitness [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : BoundaryMaps

prop_3_14 witness: the full BoundaryMaps bundle.

Equations

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

theorem GQ2.SectionThree.prop_3_14_proved [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : Nonempty BoundaryMaps

Prop. 3.14: the eq. (27) boundary data exists.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• eq. (27) = ⟦eq-boundarymap⟧
• Lemma 3.3 = ⟦lem-o2tame⟧
• Prop 3.14 = ⟦prop-compatiblemarking⟧
• Prop 3.2 = ⟦prop-tamequotient⟧