Equivariant lifting from Lemma 6.11

The projectivity-style lifting consequence of the regular-summand package. See GQ2.RegularSummand for the paper-facing overview and references.

The consequence: equivariant lifting (Hom(V, −)-exactness)

Proved from the summand package fields alone; consumers apply it to the lemma_6_11 output (now itself std-3, so the whole chain is sorryAx-free). This is the "deep-count multiplicativity" input of docs/orchestration/p15f1-dimcount-scoping.md §2: every equivariant map out of V lifts along equivariant surjections.

noncomputable def GQ2.regBasis {C : Type} (N : ℕ) (n : Fin N) (x : C) : Fin N → C → ZMod 2

The (n, x)-indicator basis vector of the regular module Fin N → C → ZMod 2.

Equations

• GQ2.regBasis N n x m y = if m = n ∧ y = x then 1 else 0

theorem GQ2.regBasis_decomp {C : Type} [Fintype C] {N : ℕ} (F : Fin N → C → ZMod 2) : F = ∑ n : Fin N, ∑ x : C, F n x • regBasis N n x

Every element of the regular module is the sum of its coordinates against regBasis.

theorem GQ2.regBasis_translate {C : Type} [Group C] {N : ℕ} (h : C) (n : Fin N) (x : C) : (fun (m : Fin N) (y : C) => regBasis N n x m (h⁻¹ * y)) = regBasis N n (h * x)

Left translation carries regBasis N n x to regBasis N n (h·x).

theorem GQ2.equivariant_lift_of_regular_summand {C : Type} [Group C] {V W W' : Type} [AddCommGroup V] [AddCommGroup W] [AddCommGroup W'] [DistribMulAction C V] [DistribMulAction C W] [DistribMulAction C W'] [Finite C] (h2W : ∀ (w : W), w + w = 0) (h2W' : ∀ (w : W'), w + w = 0) {N : ℕ} (ι : V →+ Fin N → C → ZMod 2) (r : (Fin N → C → ZMod 2) →+ V) (hι : ∀ (h : C) (v : V) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) (hr : ∀ (h : C) (F : Fin N → C → ZMod 2), (r fun (n : Fin N) (x : C) => F n (h⁻¹ * x)) = h • r F) (hri : ∀ (v : V), r (ι v) = v) (π : W →+ W') (hπeq : ∀ (h : C) (w : W), π (h • w) = h • π w) (hπ : Function.Surjective ⇑π) (f : V →+ W') (hfeq : ∀ (h : C) (v : V), f (h • v) = h • f v) : ∃ (g : V →+ W), (∀ (h : C) (v : V), g (h • v) = h • g v) ∧ ∀ (v : V), π (g v) = f v

Equivariant lifting along an equivariant surjection, from a regular-summand package (the Hom(V, −)-exactness consequence of Lemma 6.11). W, W' are 2-torsion (all consumers are).