Odd-averaging equivariant splitting (generic)

Pure group/module theory backing the §7 shear-splitting residual: for a finite group H acting linearly on ZMod 2-modules M and V through ρM : H →* (M ≃ₗ M), ρV : H →* (V ≃ₗ V), with an equivariant surjection π : M →ₗ V whose kernel is fixed pointwise, an H-equivariant linear section of π exists as soon as there is an odd normal subgroup A ≤ H that is either everything (Maschke averaging) or has no nonzero fixed vectors on V (averaging over A, then norm-trick rigidity kills the H-defects).

Also: in a finite group generated by s, t with the tame relation s⁻¹ t s = t², the cyclic subgroup ⟨t⟩ is normal (manuscript Lemma 3.1 mechanism, extracted standalone).

theorem Q2Presentation.OddSplitting.odd_nsmul_eq_self' {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] {n : ℕ} (hn : Odd n) (x : V) : n • x = x

Odd-multiple identity in characteristic 2.

theorem Q2Presentation.OddSplitting.rho_mul_apply {H : Type u_1} [Group H] {V : Type u_3} [AddCommGroup V] [Module (ZMod 2) V] (ρV : H →* V ≃ₗ[ZMod 2] V) (a b : H) (v : V) : (ρV (a * b)) v = (ρV a) ((ρV b) v)

theorem Q2Presentation.OddSplitting.rho_one_apply {H : Type u_1} [Group H] {V : Type u_3} [AddCommGroup V] [Module (ZMod 2) V] (ρV : H →* V ≃ₗ[ZMod 2] V) (v : V) : (ρV 1) v = v

theorem Q2Presentation.OddSplitting.rho_inv_cancel_apply {H : Type u_1} [Group H] {V : Type u_3} [AddCommGroup V] [Module (ZMod 2) V] (ρV : H →* V ≃ₗ[ZMod 2] V) (a : H) (v : V) : (ρV a) ((ρV a⁻¹) v) = v

def Q2Presentation.OddSplitting.conjSecG {H : Type u_1} [Group H] {M : Type u_2} {V : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup V] [Module (ZMod 2) V] (ρM : H →* M ≃ₗ[ZMod 2] M) (ρV : H →* V ≃ₗ[ZMod 2] V) (h : H) (L : V →ₗ[ZMod 2] M) : V →ₗ[ZMod 2] M

The h-conjugate of a candidate section.

Equations

• Q2Presentation.OddSplitting.conjSecG ρM ρV h L = ↑(ρM h) ∘ₗ L ∘ₗ ↑(ρV h⁻¹)

@[simp]

theorem Q2Presentation.OddSplitting.conjSecG_apply {H : Type u_1} [Group H] {M : Type u_2} {V : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup V] [Module (ZMod 2) V] (ρM : H →* M ≃ₗ[ZMod 2] M) (ρV : H →* V ≃ₗ[ZMod 2] V) (h : H) (L : V →ₗ[ZMod 2] M) (v : V) : (conjSecG ρM ρV h L) v = (ρM h) (L ((ρV h⁻¹) v))

theorem Q2Presentation.OddSplitting.conjSecG_section {H : Type u_1} [Group H] {M : Type u_2} {V : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup V] [Module (ZMod 2) V] (ρM : H →* M ≃ₗ[ZMod 2] M) (ρV : H →* V ≃ₗ[ZMod 2] V) (π : M →ₗ[ZMod 2] V) (hcomm : ∀ (h : H) (x : M), π ((ρM h) x) = (ρV h) (π x)) (h : H) (L : V →ₗ[ZMod 2] M) (hL : ∀ (v : V), π (L v) = v) (v : V) : π ((conjSecG ρM ρV h L) v) = v

A conjugate of a section is a section (needs only equivariance of π).

def Q2Presentation.OddSplitting.avgSecG {H : Type u_1} [Group H] {M : Type u_2} {V : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup V] [Module (ZMod 2) V] (ρM : H →* M ≃ₗ[ZMod 2] M) (ρV : H →* V ≃ₗ[ZMod 2] V) (A : Subgroup H) [Fintype ↥A] (L : V →ₗ[ZMod 2] M) : V →ₗ[ZMod 2] M

The A-averaged section.

Equations

• Q2Presentation.OddSplitting.avgSecG ρM ρV A L = ∑ a : ↥A, Q2Presentation.OddSplitting.conjSecG ρM ρV (↑a) L

theorem Q2Presentation.OddSplitting.avgSecG_apply {H : Type u_1} [Group H] {M : Type u_2} {V : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup V] [Module (ZMod 2) V] (ρM : H →* M ≃ₗ[ZMod 2] M) (ρV : H →* V ≃ₗ[ZMod 2] V) (A : Subgroup H) [Fintype ↥A] (L : V →ₗ[ZMod 2] M) (v : V) : (avgSecG ρM ρV A L) v = ∑ a : ↥A, (conjSecG ρM ρV (↑a) L) v

theorem Q2Presentation.OddSplitting.avgSecG_section {H : Type u_1} [Group H] {M : Type u_2} {V : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup V] [Module (ZMod 2) V] (ρM : H →* M ≃ₗ[ZMod 2] M) (ρV : H →* V ≃ₗ[ZMod 2] V) (π : M →ₗ[ZMod 2] V) (A : Subgroup H) [Fintype ↥A] (hodd : Odd (Nat.card ↥A)) (hcomm : ∀ (h : H) (x : M), π ((ρM h) x) = (ρV h) (π x)) (L : V →ₗ[ZMod 2] M) (hL : ∀ (v : V), π (L v) = v) (v : V) : π ((avgSecG ρM ρV A L) v) = v

theorem Q2Presentation.OddSplitting.avgSecG_equivariant {H : Type u_1} [Group H] {M : Type u_2} {V : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup V] [Module (ZMod 2) V] (ρM : H →* M ≃ₗ[ZMod 2] M) (ρV : H →* V ≃ₗ[ZMod 2] V) (A : Subgroup H) [Fintype ↥A] (L : V →ₗ[ZMod 2] M) (a : H) (ha : a ∈ A) (v : V) : (ρM a) ((avgSecG ρM ρV A L) v) = (avgSecG ρM ρV A L) ((ρV a) v)

The average is A-equivariant.

theorem Q2Presentation.OddSplitting.exists_equivariant_section {H : Type u_1} [Group H] {M : Type u_2} {V : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup V] [Module (ZMod 2) V] (ρM : H →* M ≃ₗ[ZMod 2] M) (ρV : H →* V ≃ₗ[ZMod 2] V) (π : M →ₗ[ZMod 2] V) [Finite H] (hπ : Function.Surjective ⇑π) (hcomm : ∀ (h : H) (x : M), π ((ρM h) x) = (ρV h) (π x)) (hker : ∀ (h : H) (x : M), π x = 0 → (ρM h) x = x) (A : Subgroup H) (hA : A.Normal) (hodd : Odd (Nat.card ↥A)) (hcase : (∀ (h : H), h ∈ A) ∨ ∀ (v : V), (∀ a ∈ A, (ρV a) v = v) → v = 0) : ∃ (σ : V →ₗ[ZMod 2] M), (∀ (v : V), π (σ v) = v) ∧ ∀ (h : H) (v : V), (ρM h) (σ v) = σ ((ρV h) v)

Equivariant section existence over an odd normal subgroup: either the whole group is odd (hcase left) or the odd normal A has no nonzero fixed vectors on V (hcase right), and then averaging plus the norm-trick rigidity produce an H-equivariant linear section of π.

The tame cyclic direction is normal

theorem Q2Presentation.OddSplitting.tame_zpowers_normal {G : Type u_4} [Group G] [Finite G] {s t : G} (hgen : Subgroup.closure {s, t} = ⊤) (htame : s⁻¹ * t * s = t ^ 2) (htodd : Odd (orderOf t)) : (Subgroup.zpowers t).Normal

In a finite group generated by s, t with the tame relation s⁻¹ t s = t², the subgroup ⟨t⟩ is normal (manuscript Lemma 3.1 mechanism).