Euler-characteristic collapse, the μ₂ bricks, and polar self-duality

The opening GQ2.DeepPart layer: the Euler-characteristic collapse #H¹ = #M (B7 with trivial H⁰, H²) together with the H⁰-vanishing and fixed-point-transport lemmas; the μ₂ ≅ ℤ/2 bricks with trivial Galois action; and the polar self-duality V ≃+ Hom(V, μ₂) yielding #H² = 1 (§6.3 step 2, Ax B6 via the Tate-duality parameter D).

This file is part of the GQ2.DeepPart split (the deep-part proof); see GQ2/DeepPart.lean for the overview.

theorem GQ2.DeepPart.card_H1_eq_card_of_H0_H2_trivial {M : Type u_1} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction AbsGalQ2 M] [ContinuousSMul AbsGalQ2 M] [Finite M] (hH0 : Nat.card ↥(ContCoh.H0 AbsGalQ2 M) = 1) (hH2 : Nat.card (ContCoh.H2 AbsGalQ2 M) = 1) {k : ℕ} (hk : Nat.card M = 2 ^ k) : Nat.card (ContCoh.H1 AbsGalQ2 M) = Nat.card M

Euler-characteristic collapse: for a finite 2-power-order G_ℚ₂-module with trivial H⁰ and H², the local Euler characteristic (B7) reads #H¹ = #M.

theorem GQ2.DeepPart.card_H0_eq_one_iff {M : Type u_1} [AddCommGroup M] [DistribMulAction AbsGalQ2 M] : Nat.card ↥(ContCoh.H0 AbsGalQ2 M) = 1 ↔ ∀ (m : M), (∀ (g : AbsGalQ2), g • m = m) → m = 0

H⁰(G_ℚ₂, M) = 0 (as Nat.card = 1) iff M has no nonzero G_ℚ₂-fixed vector.

theorem GQ2.DeepPart.card_H0_eq_one_of_surjective {M : Type u_1} [AddCommGroup M] [DistribMulAction AbsGalQ2 M] {C : Type u_2} [Group C] [DistribMulAction C M] (ρ : AbsGalQ2 →* C) (hρsurj : Function.Surjective ⇑ρ) (hρ : ∀ (g : AbsGalQ2) (m : M), g • m = ρ g • m) (hsimple : ∀ (W : AddSubgroup M), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (h₀ : C) (hmoves : ∃ (m : M), h₀ • m ≠ m) : Nat.card ↥(ContCoh.H0 AbsGalQ2 M) = 1

H⁰-vanishing (§6.3 step 2, V^{G_ℚ₂} = 0): if the G_ℚ₂-action on M factors through a surjective ρ : G_ℚ₂ →* C, the C-module M is simple, and some element of C moves some vector, then #H⁰ = 1. (V^{im ρ} = V^C is C-stable — even pointwise fixed — so simplicity forces it to ⊥ or ⊤, and ⊤ contradicts the moving element.)

theorem GQ2.DeepPart.card_H0_congr {A : Type u_2} {B : Type u_3} [AddCommGroup A] [AddCommGroup B] [DistribMulAction AbsGalQ2 A] [DistribMulAction AbsGalQ2 B] (e : A ≃+ B) (he : ∀ (g : AbsGalQ2) (a : A), e (g • a) = g • e a) : Nat.card ↥(ContCoh.H0 AbsGalQ2 B) = Nat.card ↥(ContCoh.H0 AbsGalQ2 A)

Fixed-point transport: an equivariant additive iso induces a cardinality equality of H⁰s (it restricts to a bijection of the fixed-point subgroups).

The μ₂ bricks: μ₂ ≅ ℤ/2 with trivial Galois action

MuN 2 = Additive (rootsOfUnity 2 ℚ̄₂) = {1, −1} additively: classified by the value of the underlying root, Galois-fixed because an additive automorphism of a two-element group is the identity.

noncomputable def GQ2.DeepPart.muTwoGen : MuN 2

−1 as the nonzero element of the additive μ₂.

Equations

• GQ2.DeepPart.muTwoGen = Additive.ofMul ⟨-1, GQ2.DeepPart.muTwoGen._proof_1⟩

theorem GQ2.DeepPart.muTwoGen_ne_zero : muTwoGen ≠ 0

theorem GQ2.DeepPart.muTwo_eq_zero_or_gen (x : MuN 2) : x = 0 ∨ x = muTwoGen

Classification: μ₂ has exactly the elements 0 and muTwoGen.

noncomputable def GQ2.DeepPart.zmodTwoToMuTwo : ZMod 2 →+ MuN 2

The hom ℤ/2 →+ μ₂, 1 ↦ −1.

Equations

• GQ2.DeepPart.zmodTwoToMuTwo = (ZMod.lift 2) ⟨(zmultiplesHom (GQ2.MuN 2)) GQ2.DeepPart.muTwoGen, GQ2.DeepPart.zmodTwoToMuTwo._proof_1⟩

theorem GQ2.DeepPart.zmodTwoToMuTwo_one : zmodTwoToMuTwo 1 = muTwoGen

noncomputable def GQ2.DeepPart.zmodTwoEquivMuTwo : ZMod 2 ≃+ MuN 2

ℤ/2 ≃+ μ₂ (additive), 1 ↦ −1.

Equations

• GQ2.DeepPart.zmodTwoEquivMuTwo = AddEquiv.ofBijective GQ2.DeepPart.zmodTwoToMuTwo ⋯

theorem GQ2.DeepPart.muTwo_smul_trivial (g : AbsGalQ2) (x : MuN 2) : g • x = x

The Galois action on μ₂ is trivial — an additive automorphism of the two-element group is the identity.

The polar self-duality V ≃+ Hom(V, μ₂) and #H² = 1 (§6.3 step 2, Ax B6 via D)

A nonsingular Galois-invariant 𝔽₂ quadratic form identifies V with its μ₂-dual equivariantly, so #H⁰(M′) = #H⁰(V); Tate duality's (0,2) clause at M := V then reads #H²(V) = #Hom(H²(V), ℤ/2) = #H⁰(M′) = #H⁰(V) — no dual-simplicity argument needed.

theorem GQ2.DeepPart.polar_smul_smul (V : Type) [AddCommGroup V] [DistribMulAction AbsGalQ2 V] (q : V → ZMod 2) (hqG : ∀ (g : AbsGalQ2) (v : V), q (g • v) = q v) (g : AbsGalQ2) (a b : V) : QuadraticFp2.polar q (g • a) (g • b) = QuadraticFp2.polar q a b

A Galois-invariant form has Galois-invariant polar form.

theorem GQ2.DeepPart.exists_polarSelfDual (V : Type) [AddCommGroup V] [DistribMulAction AbsGalQ2 V] [Finite V] (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (h2 : ∀ (v : V), v + v = 0) (hqG : ∀ (g : AbsGalQ2) (v : V), q (g • v) = q v) : ∃ (e : V ≃+ MuDual 2 V), ∀ (g : AbsGalQ2) (v : V), e (g • v) = g • e v

Polar self-duality: a nonsingular Galois-invariant quadratic form on a finite exp-2 module induces an equivariant additive iso V ≃+ Hom(V, μ₂).

theorem GQ2.DeepPart.h2_add_self (V : Type) [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [DistribMulAction AbsGalQ2 V] (h2 : ∀ (v : V), v + v = 0) (x : ContCoh.H2 AbsGalQ2 V) : x + x = 0

H² of an exponent-2 module has exponent 2 (pointwise, by quotient induction).

theorem GQ2.DeepPart.card_H2_eq_one_of_card_H0_eq_one (V : Type) [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [DistribMulAction AbsGalQ2 V] [ContinuousSMul AbsGalQ2 V] [Finite V] (D : TateDuality 2) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (h2 : ∀ (v : V), v + v = 0) (hqG : ∀ (g : AbsGalQ2) (v : V), q (g • v) = q v) (hfin : Finite (ContCoh.H2 AbsGalQ2 V)) (hH0 : Nat.card ↥(ContCoh.H0 AbsGalQ2 V) = 1) : Nat.card (ContCoh.H2 AbsGalQ2 V) = 1

#H² = 1 from #H⁰ = 1 (Tate duality B6 via the parameter D, (0,2) clause at M := V, through the polar self-duality and exp-2 Pontryagin duality).

theorem GQ2.DeepPart.card_eq_two_pow_of_exp_two {A : Type u_2} [AddCommGroup A] [Finite A] (h2 : ∀ (a : A), a + a = 0) : ∃ (k : ℕ), Nat.card A = 2 ^ k

A finite exponent-2 group has 2-power order.

theorem GQ2.DeepPart.card_H1_eq_card_of_simple (V : Type) [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [DistribMulAction AbsGalQ2 V] [ContinuousSMul AbsGalQ2 V] [Finite V] (D : TateDuality 2) {C : Type u_2} [Group C] [DistribMulAction C V] (ρ : AbsGalQ2 →* C) (hρsurj : Function.Surjective ⇑ρ) (hρ : ∀ (g : AbsGalQ2) (v : V), g • v = ρ g • v) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (h₀ : C) (hmoves : ∃ (v : V), h₀ • v ≠ v) (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : ∀ (c : C) (v : V), q (c • v) = q v) (h2 : ∀ (v : V), v + v = 0) : Nat.card (ContCoh.H1 AbsGalQ2 V) = Nat.card V

#H¹ = #V in the §6.3 setting (steps 1–2 of lemma_6_17_dim / Prop 6.18 assembled): simple C-module, surjective classifying map, an element moving a vector, a nonsingular invariant form. Ax: B6 (via D), B7 (finite_H2 + the Euler collapse).