Proposition 1.1 — the assembly

GQ2/PropOneOne.lean supplied the ν_ur-descent infrastructure; this file assembles the marked isomorphism itself. Paper: "there exist topological generators a, s, y of D = G_{ℚ₂}(2) with D ≅ ⟨a,s,y | a²s⁴[s,y]⟩ and ν_ur(a,s,y) = (−2,1,0)."

Proof structure (paper §3, "composes B3c/B4 with Lemma 3.5 and Prop. 3.8")

• B3c (dyadicOrientation) provides a group isomorphism equiv : G_{ℚ₂}(2) ≅ D₀ whose descended cyclotomic character chiTwo takes the marked values (−1, 1, (−3)⁻¹) on A, S, Y.
• Lemma 3.5 (lemma_3_5_marked_abelianization) provides an abelianization isomorphism e_ab : D₀^{ab} ≅ G_{ℚ₂}(2)^{ab} sending Ā, S̄, Ȳ to the reciprocity classes π(rec −4), π(rec 1/2), π(rec −3) — which carry the ν_ur-row (−2, 1, 0).
• The two isomorphisms need not agree on abelianizations; they differ by a χ-preserving automorphism Θ of D₀^{ab}, which by Prop. 3.8 (the Lemmas 3.6–3.8 proof: prop_3_8_classification + prop_3_8_lift) is some α_{u,b} and hence lifts to a group automorphism Ψ of D₀. Then e := Ψ ∘ equiv induces e_ab on abelianizations, so e.symm(A/S/Y) have the marked reciprocity classes, and the ν_ur-rows read off through nu_ur_recip_*.

e_ab is Lemma 3.5, using the theorem markedHom_bijective from GQ2/SectionThree.lean. Everything here (functorial abelianization, the χ-descent, the Θ-classification/lift, the ν_ur-readoff) is std-3 + B3c + B8.

Functorial abelianization of a continuous isomorphism

The repo's topAbelianization (G ⧸ closure⁅G,G⁆) is not packaged as a functor; we supply just enough — the pushforward of a continuous hom, and its promotion to an equivalence — for the comparison e_ab vs equiv. As elsewhere (SectionThree, AnabelianBridge) the CommGroup/Compact/T2/TotDisc instances on topAbelianization are file-local.

@[implicit_reducible]

noncomputable def GQ2.instCommGroupTopAbP10 {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : CommGroup (topAbelianization G)

Equations

• GQ2.instCommGroupTopAbP10 = { toGroup := inferInstance, mul_comm := ⋯ }

theorem GQ2.instCompactSpaceTopAbP10 {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] : CompactSpace (topAbelianization G)

theorem GQ2.instT2SpaceTopAbP10 {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] : T2Space (topAbelianization G)

theorem GQ2.instTotallyDisconnectedSpaceTopAbP10 {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] : TotallyDisconnectedSpace (topAbelianization G)

noncomputable def GQ2.topAbLiftHom {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] (f : G →ₜ* H) : topAbelianization G →ₜ* topAbelianization H

Pushforward of a continuous hom f : G → H to the topological abelianizations, abMk g ↦ abMk (f g) (well-defined: abMk_H ∘ f kills closure⁅G,G⁆).

Equations

• GQ2.topAbLiftHom f = { toMonoidHom := QuotientGroup.lift (commutator G).topologicalClosure (GQ2.SectionThree.abMk.comp f.toMonoidHom) ⋯, continuous_toFun := ⋯ }

noncomputable def GQ2.topAbCongr {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) : topAbelianization G ≃ₜ* topAbelianization H

Functorial abelianization of a continuous isomorphism φ : G ≅ H.

Equations

• GQ2.topAbCongr φ = GQ2.continuousMulEquivOfBijective (GQ2.topAbLiftHom { toMonoidHom := φ.toMonoidHom, continuous_toFun := ⋯ }) ⋯

noncomputable def GQ2.abDescend {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u_2} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [T2Space A] (f : G →ₜ* A) : topAbelianization G →ₜ* A

Descent of a continuous hom f : G → A (A abelian Hausdorff) through abMk.

Equations

• GQ2.abDescend f = { toMonoidHom := QuotientGroup.lift (commutator G).topologicalClosure f.toMonoidHom ⋯, continuous_toFun := ⋯ }

theorem GQ2.d0ab_hom_ext {A : Type} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A] (hA : IsProP 2 A) (φ ψ : topAbelianization ↑D0.toProfinite.toTop →ₜ* A) (hAgen : φ (SectionThree.abMk d0A) = ψ (SectionThree.abMk d0A)) (hS : φ (SectionThree.abMk d0S) = ψ (SectionThree.abMk d0S)) (hY : φ (SectionThree.abMk d0Y) = ψ (SectionThree.abMk d0Y)) (z : topAbelianization ↑D0.toProfinite.toTop) : φ z = ψ z

Extensionality for D₀^{ab} homs into a pro-2 group: two continuous homs agreeing on Ā, S̄, Ȳ agree everywhere (every element is Ā^a S̄^s Ȳ^y by D0ab_coord, and continuous homs commute with zpowZtwo).

The assembly

noncomputable def GQ2.orientBundle [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : DyadicOrientation

The B3c dyadic-orientation bundle (a fixed witness of the axiom dyadicOrientation).

Equations

• GQ2.orientBundle = GQ2.dyadicOrientation

noncomputable def GQ2.chiD0 [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : topAbelianization ↑D0.toProfinite.toTop →ₜ* ℤ_[2]ˣ

χ transported to D₀^{ab}: chiD0 (abMk d) = chiTwo (equiv.symm d). Its generator values are (−1, 1, (−3)⁻¹) (orientBundle.chi_A/S/Y).

Equations

• GQ2.chiD0 = GQ2.abDescend { toMonoidHom := GQ2.orientBundle.chiTwo.comp GQ2.orientBundle.equiv.symm.toMonoidHom, continuous_toFun := ⋯ }

noncomputable def GQ2.chiG [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : topAbelianization ↑(maxProPQuotient 2 AbsGalQ2).toProfinite.toTop →ₜ* ℤ_[2]ˣ

χ on G_{ℚ₂}(2)^{ab}: chiG (abMk h) = chiTwo h.

Equations

• GQ2.chiG = GQ2.abDescend { toMonoidHom := GQ2.orientBundle.chiTwo, continuous_toFun := ⋯ }

theorem GQ2.chiG_markedPi [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (x : AbsGalQ2ab) : chiG (SectionThree.markedPi x) = chiCycAb x

χ_G ∘ markedPi = chiCycAb: the cyclotomic values agree with markedPi's reciprocity classes (via chiTwo_factors).

theorem GQ2.chiD0_equivAb [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (w : topAbelianization ↑(maxProPQuotient 2 AbsGalQ2).toProfinite.toTop) : chiD0 ((topAbCongr orientBundle.equiv) w) = chiG w

chiD0 ∘ (topAbCongr equiv) = chiG.

noncomputable def GQ2.nuUrBarAb [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (R : LocalReciprocity) : topAbelianization ↑(maxProPQuotient 2 AbsGalQ2).toProfinite.toTop →ₜ* Multiplicative ℤ_[2]

ν_ur descended to G_{ℚ₂}(2)^{ab} (through abMk).

Equations

• GQ2.nuUrBarAb R = GQ2.abDescend (GQ2.PropOneOne.nuUrBar R)

theorem GQ2.nu_ur_eq_nuUrBarAb_markedPi [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (R : LocalReciprocity) (x : AbsGalQ2ab) : R.nu_ur x = (nuUrBarAb R) (SectionThree.markedPi x)

ν_ur = nuUrBarAb ∘ markedPi: the unramified coordinate reads off markedPi's classes.

Reciprocity values of the marked classes (std-3 + B5)

These consume only the bundle R, not the compactness of AbsGalQ2.

theorem GQ2.nu_ur_recip_unitNeg4 (R : LocalReciprocity) : R.nu_ur (R.recip SectionThree.unitNeg4) = Multiplicative.ofAdd ↑(-2)

ν_ur(rec(−4)) = −2.

theorem GQ2.nu_ur_recip_uniformizer' (R : LocalReciprocity) : R.nu_ur (R.recip uniformizer) = Multiplicative.ofAdd ↑(-1)

ν_ur(rec(2)) = −1.

theorem GQ2.nu_ur_recip_unitNeg3 (R : LocalReciprocity) : R.nu_ur (R.recip SectionThree.unitNeg3) = Multiplicative.ofAdd ↑0

ν_ur(rec(−3)) = 0.

noncomputable def GQ2.unitNegThree : ℤ_[2]ˣ

A unit of value −3.

Equations

• GQ2.unitNegThree = GQ2.unitNegThree._proof_1.unit

theorem GQ2.chiCycAb_recip_unitNeg4 (R : LocalReciprocity) : chiCycAb (R.recip SectionThree.unitNeg4) = -1

chiCycAb(rec(−4)) = −1.

theorem GQ2.chiCycAb_recip_unitNeg3 (R : LocalReciprocity) : chiCycAb (R.recip SectionThree.unitNeg3) = unitNegThree⁻¹

chiCycAb(rec(−3)) = unitNegThree⁻¹.

Proposition 1.1

theorem GQ2.SectionThree.prop_1_1 [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (R : LocalReciprocity) : ∃ (e : ↑(maxProPQuotient 2 AbsGalQ2).toProfinite.toTop ≃ₜ* ↑D0.toProfinite.toTop), (∀ (g : AbsGalQ2), (maxProPMk 2 AbsGalQ2) g = e.symm d0A → R.nu_ur (toAb g) = Multiplicative.ofAdd ↑(-2)) ∧ (∀ (g : AbsGalQ2), (maxProPMk 2 AbsGalQ2) g = e.symm d0S → R.nu_ur (toAb g) = Multiplicative.ofAdd ↑1) ∧ ∀ (g : AbsGalQ2), (maxProPMk 2 AbsGalQ2) g = e.symm d0Y → R.nu_ur (toAb g) = Multiplicative.ofAdd ↑0

Proposition 1.1. A marked isomorphism e : G_{ℚ₂}(2) ≅ D₀ with unramified coordinates ν_ur(a, s, y) = (−2, 1, 0). Assembled from B3c (orientBundle.equiv), Lemma 3.5 (lemma_3_5_marked_abelianization, using markedHom_bijective), and Prop. 3.8 (prop_3_8_classification/prop_3_8_lift). The statement is placed here to respect the import DAG; see the pointer in GQ2/SectionThree.lean.

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

• Lemma 3.5 = ⟦lem-markedinitialform⟧
• Proposition 1.1 = ⟦prop-markedDem⟧
• Prop 3.8 = ⟦prop-orientationlift⟧ (= proposition 3.9 in current tex)