The trivial module 𝔽₂ is self-dual

The base case of the prop_5_15 dévissage: IsSelfDual t A when C acts trivially on the finite elementary-2 module A (the trivial simple 𝔽₂[C]-module is 𝔽₂ with trivial action).

With every generator acting trivially the differentials collapse (d⁰ = 0, and — via the split wild row and d1Fun_tame, in char 2 — d¹ x = (x₁, x₁)), so the cohomology is elementary:

• Z¹ = {x | x₁ = 0} ≅ A³, B¹ = 0, H¹ = Z¹ ≅ A³;
• H² = (A×A)/Δ ≅ A, matching #(A^∨)^C = #A^∨ = #A;

which gives the two card clauses of IsSelfDual. The degree-one pairing is the traced mixed coordinate mixedB, whose perfection is the paper's table (25) — the 3×3 Gram computation.

theorem GQ2.FoxH.d1Fun_of_trivial {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) : t.WildRel → ∀ (htriv : ∀ (c : C) (a : A), c • a = a) (hA₂ : ∀ (a : A), a + a = 0) (x : Fin 4 → A), d1Fun t x = (x 1, x 1)

d¹ on the trivial module collapses to the diagonal x ↦ (x₁, x₁): the tame row (d1Fun_tame) is x₀−x₀ + x₁ − (x₁+x₁) = x₁ and the wild row (liftMarking_wildValue_u, x₁ + (1+S⁻¹)x₃) is x₁ + x₃ + x₃ = x₁, both in char 2 with every generator acting trivially.

theorem GQ2.FoxH.d1_of_trivial {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (htriv : ∀ (c : C) (a : A), c • a = a) (hA₂ : ∀ (a : A), a + a = 0) (x : Fin 4 → A) : (d1 t) x = (x 1, x 1)

d¹ bundled, on the trivial module.

theorem GQ2.FoxH.d0_of_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (t : Marking C) (htriv : ∀ (c : C) (a : A), c • a = a) (v : A) : (d0 t) v = 0

d⁰ = 0 on the trivial module.

The two cardinality clauses

theorem GQ2.FoxH.elemDual_smul_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (htriv : ∀ (c : C) (a : A), c • a = a) (g : C) (lam : ElemDual A) : g • lam = lam

Contragredience of a trivial action is trivial.

theorem GQ2.FoxH.card_fixedPts_elemDual_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (htriv : ∀ (c : C) (a : A), c • a = a) (hA₂ : ∀ (a : A), a + a = 0) : Nat.card ↑(fixedPts C (ElemDual A)) = Nat.card A

#(A^∨)^C = #A^∨ = #A: the dual of a finite elementary-2 module has the same cardinality (finite 𝔽₂-vector space is self-dual in cardinality), and every point is C-fixed here.

theorem GQ2.FoxH.card_range_d1_trivial {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (htriv : ∀ (c : C) (a : A), c • a = a) (hA₂ : ∀ (a : A), a + a = 0) : Nat.card ↥(d1 t).range = Nat.card A

On the trivial module range d¹ = Δ (the diagonal a ↦ (a,a)), of cardinality #A.

theorem GQ2.FoxH.card_H2w_trivial {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (htriv : ∀ (c : C) (a : A), c • a = a) (hA₂ : ∀ (a : A), a + a = 0) : Nat.card (H2w t) = Nat.card A

Card clause for H²: #H²w = #A on the trivial module (H² = (A×A)/Δ).

theorem GQ2.FoxH.card_Z1w_trivial {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (htriv : ∀ (c : C) (a : A), c • a = a) (hA₂ : ∀ (a : A), a + a = 0) : Nat.card ↥(Z1w t) = Nat.card A ^ 3

Card clause for Z¹: #Z¹w = (#A)³ on the trivial module (Z¹ = {x | x₁ = 0}).

IsSelfDual for the trivial module

The two card clauses are card_H2w_trivial/card_Z1w_trivial combined with card_fixedPts_elemDual_trivial. The degree-one pairing (clause 3) is the paper's table (25) — the 3×3 Gram matrix of mixedB on the cocycle basis {x₀, x₂, x₃} (recall Z¹ = {x | x₁ = 0}, B¹ = 0, so H¹ = Z¹).

The pairing is built in GQ2/MixedBilinear.lean (all std-3): mixedB bilinearity, and the closed form mixedB_cocycle : mixedB t x y = y₂(x₂) + y₃(x₀) − y₀(x₃) + u₁.z on cocycles, with the ω₂ scalar u₁.z confined to the (3,3) slot (heisMarking_u1_z_of_{x3,y3}_zero). The Gram matrix is therefore unit-determinant regardless of u₁.z, and elemDual_separates gives nondegeneracy. trivialSelfDual descends mixedB to H¹w = Z¹w via Quotient.lift₂ and closes both nondegeneracy conditions by the case analysis below (std-3).

theorem GQ2.FoxH.mem_Z1w_trivial_iff {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (htriv : ∀ (c : C) (a : A), c • a = a) (hA₂ : ∀ (a : A), a + a = 0) (x : Fin 4 → A) : x ∈ Z1w t ↔ x 1 = 0

On the trivial module Z¹w = {x | x₁ = 0}.

theorem GQ2.FoxH.B1w_trivial_eq_bot {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (t : Marking C) (htriv : ∀ (c : C) (a : A), c • a = a) : B1w t = ⊥

On the trivial module B¹w = ⊥ (d⁰ = 0), so H¹w = Z¹w and the class map is injective.

theorem GQ2.FoxH.trivialSelfDual {C : Type u_1} [Group C] [Finite C] {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (htriv : ∀ (c : C) (a : A), c • a = a) (hA₂ : ∀ (a : A), a + a = 0) : IsSelfDual t A

the Prop. 5.15 proof, part (i): the trivial module 𝔽₂ is self-dual. Both card clauses and the degree-one pairing (table (25)) are proven: mixedB descends to H¹w = Z¹w (since B¹w = ⊥), its closed form mixedB_cocycle = y₂(x₂)+y₃(x₀)−y₀(x₃)+u₁.z has unit-determinant Gram matrix (the ω₂ scalar u₁.z sits only on the (3,3) slot, killed by choosing the paired dual coordinate ≠ 3), and elemDual_separates supplies the nonzero dual functionals.