Classification half of Proposition 3.8

The kernel and conjugacy analysis completing the lifting result.

See GQ2.AnabelianBridge for the paper-facing overview, source citations, and deviations.

Proposition 3.8, classification half

Every χ₀-preserving continuous automorphism of B = D₀^{ab} is α_{u,b} for a unique (u, b) ∈ ℤ₂ˣ × ℤ₂ (paper (18)). Engine: the Lemmas 3.4–3.5 proof's coordinate surjectivity D0ab_coord, the torsion analysis of t, and the ℤ₂-powering development's η-injectivity; the (−1)^ε-component is killed by the mod-4 argument (η-powers are ≡ 1 (mod 4), −1 is not).

@[implicit_reducible]

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

Equations

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

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

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

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

noncomputable def GQ2.sBar (c : ℤ_[2]) : topAbelianization ↑D0.toProfinite.toTop

Shorthand: S̄-powers in D₀^{ab}.

Equations

• GQ2.sBar c = GQ2.zpowZtwo GQ2.SectionThree.isProP_two_topAb_D0 (GQ2.SectionThree.abMk GQ2.d0S) c

theorem GQ2.bE_sBar (B : SectionThree.BDecomposition) (c : ℤ_[2]) : B.e (sBar c) = Multiplicative.ofAdd (0, c, 0)

B.e reads S̄-powers in the second coordinate.

theorem GQ2.sBar_injective (B : SectionThree.BDecomposition) : Function.Injective sBar

S̄-powers are injective in the exponent.

theorem GQ2.sq_eq_one_iff (B : SectionThree.BDecomposition) (z : topAbelianization ↑D0.toProfinite.toTop) : z ^ 2 = 1 ↔ z = 1 ∨ z = SectionThree.abMk (d0A * d0S ^ 2)

The 2-torsion of D₀^{ab} is {1, t}, t = abMk (A·S²) (read off the coordinates: the ℤ₂-components of a square-trivial element vanish).

theorem GQ2.xi_zpow (ξ : topAbelianization ↑D0.toProfinite.toTop ≃ₜ* topAbelianization ↑D0.toProfinite.toTop) (x : topAbelianization ↑D0.toProfinite.toTop) (c : ℤ_[2]) : ξ (zpowZtwo SectionThree.isProP_two_topAb_D0 x c) = zpowZtwo SectionThree.isProP_two_topAb_D0 (ξ x) c

ξ-naturality of 2-adic powers.

theorem GQ2.xi_fixes_t (B : SectionThree.BDecomposition) (ξ : topAbelianization ↑D0.toProfinite.toTop ≃ₜ* topAbelianization ↑D0.toProfinite.toTop) : ξ (SectionThree.abMk (d0A * d0S ^ 2)) = SectionThree.abMk (d0A * d0S ^ 2)

Any continuous automorphism fixes t (the unique nontrivial 2-torsion element).

theorem GQ2.eta_pow_mod4 (y₀ : ℤ_[2]ˣ) (hy₀ : ↑y₀ = -3) (w : ℤ_[2]) : (PadicInt.toZModPow 2) ↑(zpowZtwo isProP_two_unitsPadicInt y₀⁻¹ w) = 1

The paper's η ^ w ≡ 1 (mod 4) (the image of zpowZtwo η lies in 1 + 4ℤ₂).

theorem GQ2.chi_row_extract (y₀ : ℤ_[2]ˣ) (hy₀ : ↑y₀ = -3) (a y w : ℤ_[2]) (h : (-1) ^ ((PadicInt.toZModPow 1) a).val * zpowZtwo isProP_two_unitsPadicInt y₀⁻¹ y = zpowZtwo isProP_two_unitsPadicInt y₀⁻¹ w) : 2 ∣ a ∧ y = w

The χ-row extraction: from (−1)^r · η^y = η^w conclude 2 ∣ a (r = a mod 2 = 0, by the mod-4 elimination) and y = w (η-injectivity, the ℤ₂-powering development (iii)).

theorem GQ2.abMk_relation : SectionThree.abMk d0A ^ 2 * SectionThree.abMk d0S ^ 4 = 1

Abelianized relation: Ā² S̄⁴ = 1 in D₀^{ab}.

theorem GQ2.aPow_even (a : ℤ_[2]) (h2 : 2 ∣ a) : zpowZtwo SectionThree.isProP_two_topAb_D0 (SectionThree.abMk d0A) a = sBar (-2 * a)

Even Ā-powers are S̄-powers: Ā^{2a₁} = S̄^{−4a₁}.

theorem GQ2.chi_coord (χ : topAbelianization ↑D0.toProfinite.toTop →* ℤ_[2]ˣ) (hχ : Continuous ⇑χ) (y₀ : ℤ_[2]ˣ) (hχA : χ (SectionThree.abMk d0A) = -1) (hχS : χ (SectionThree.abMk d0S) = 1) (hχY' : χ (SectionThree.abMk d0Y) = y₀⁻¹) (a s y : ℤ_[2]) : χ (zpowZtwo SectionThree.isProP_two_topAb_D0 (SectionThree.abMk d0A) a * zpowZtwo SectionThree.isProP_two_topAb_D0 (SectionThree.abMk d0S) s * zpowZtwo SectionThree.isProP_two_topAb_D0 (SectionThree.abMk d0Y) y) = (-1) ^ ((PadicInt.toZModPow 1) a).val * zpowZtwo isProP_two_unitsPadicInt y₀⁻¹ y

The χ-value on coordinates: χ(Ā^a S̄^s Ȳ^y) = (−1)^{a mod 2} η^y.

theorem GQ2.xi_S_row (ξ : topAbelianization ↑D0.toProfinite.toTop ≃ₜ* topAbelianization ↑D0.toProfinite.toTop) (χ : topAbelianization ↑D0.toProfinite.toTop →* ℤ_[2]ˣ) (hχ : Continuous ⇑χ) (y₀ : ℤ_[2]ˣ) (hy₀ : ↑y₀ = -3) (hχA : χ (SectionThree.abMk d0A) = -1) (hχS : χ (SectionThree.abMk d0S) = 1) (hχY' : χ (SectionThree.abMk d0Y) = y₀⁻¹) (hpres : ∀ (x : topAbelianization ↑D0.toProfinite.toTop), χ (ξ x) = χ x) : ∃ (u : ℤ_[2]), ξ (SectionThree.abMk d0S) = sBar u

The S̄-row of a χ-preserving automorphism is a pure S̄-power.

theorem GQ2.xi_Y_row (ξ : topAbelianization ↑D0.toProfinite.toTop ≃ₜ* topAbelianization ↑D0.toProfinite.toTop) (χ : topAbelianization ↑D0.toProfinite.toTop →* ℤ_[2]ˣ) (hχ : Continuous ⇑χ) (y₀ : ℤ_[2]ˣ) (hy₀ : ↑y₀ = -3) (hχA : χ (SectionThree.abMk d0A) = -1) (hχS : χ (SectionThree.abMk d0S) = 1) (hχY' : χ (SectionThree.abMk d0Y) = y₀⁻¹) (hpres : ∀ (x : topAbelianization ↑D0.toProfinite.toTop), χ (ξ x) = χ x) : ∃ (b : ℤ_[2]), ξ (SectionThree.abMk d0Y) = sBar b * SectionThree.abMk d0Y

The Ȳ-row of a χ-preserving automorphism is S̄-power times Ȳ.

theorem GQ2.SectionThree.prop_3_8_classification (B : BDecomposition) (ξ : topAbelianization ↑D0.toProfinite.toTop ≃ₜ* topAbelianization ↑D0.toProfinite.toTop) (χ : topAbelianization ↑D0.toProfinite.toTop →* ℤ_[2]ˣ) (hχ : Continuous ⇑χ) (hχA : χ (abMk d0A) = -1) (hχS : χ (abMk d0S) = 1) (hχY : ∀ (y : ℤ_[2]ˣ), ↑y = -3 → χ (abMk d0Y) = y⁻¹) (hpres : ∀ (x : topAbelianization ↑D0.toProfinite.toTop), χ (ξ x) = χ x) : ∃! p : ℤ_[2]ˣ × ℤ_[2], B.e (ξ (abMk d0A)) = Multiplicative.ofAdd (1, -2 * ↑p.1, 0) ∧ B.e (ξ (abMk d0S)) = Multiplicative.ofAdd (0, ↑p.1, 0) ∧ B.e (ξ (abMk d0Y)) = Multiplicative.ofAdd (0, p.2, 1)

Proposition 3.8, classification half (paper (18); statement moved from GQ2/SectionThree.lean, see the pointer there). Every continuous χ₀-preserving automorphism ξ of B = D₀^{ab} is α_{u,b} for a unique (u, b) ∈ ℤ₂ˣ × ℤ₂: in the coordinates of the B-decomposition it sends S̄ ↦ S̄^u, Ȳ ↦ S̄^b Ȳ, and (forced by preservation of the torsion element t = Ā S̄² and the relation Ā² S̄⁴ = 1) Ā ↦ t S̄^{-2u}. The S̄-exponent u is a unit because the same row analysis applies to ξ⁻¹. Axiom-free: the abelianized D₀ and its coordinate frame are concrete.