Relative trace and tame-kernel foundations for Lemma 6.11

The odd-index relative trace and the finite tame-group kernel facts used by the regular-summand argument. See GQ2.RegularSummand for the paper-facing overview and references.

The odd-index relative trace

regular_summand_of_subgroup_summand is the paper's "Sylow criterion for modular projectivity" in the concrete split-pair shape: an equivariant split summand of a regular module over an odd-index subgroup P ≤ C is one over C. Everything is function-level — no induced-module formalism: ι v n g := j (g⁻¹ • v) n 1 and ρ F := ∑_{gP ∈ C/P} g • q (F n (g·—)) (the relative trace, well-defined on cosets by the P-equivariance of q), with ρ ∘ ι = [C : P] • id = id because the index is odd and V is 2-torsion. This reduces lemma_6_11 to its weight-orbit kernel sylow_split_pair_of_ramified below (pp. 29–30, steps 1–2 of the plan).

theorem GQ2.regular_summand_of_subgroup_summand {C : Type} [Group C] [Finite C] {V : Type} [AddCommGroup V] [DistribMulAction C V] (hV2 : ∀ (v : V), v + v = 0) (P : Subgroup C) (hodd : Odd P.index) {r : ℕ} (j : V →+ Fin r → ↥P → ZMod 2) (q : (Fin r → ↥P → ZMod 2) →+ V) (hj : ∀ (p : ↥P) (v : V) (n : Fin r) (x : ↥P), j (↑p • v) n x = j v n (p⁻¹ * x)) (hq : ∀ (p : ↥P) (F : Fin r → ↥P → ZMod 2), (q fun (n : Fin r) (x : ↥P) => F n (p⁻¹ * x)) = ↑p • q F) (hqj : ∀ (v : V), q (j v) = v) : ∃ (N : ℕ) (ι : V →+ Fin N → C → ZMod 2) (ρ : (Fin N → C → ZMod 2) →+ V), (∀ (h : C) (v : V) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) ∧ (∀ (h : C) (F : Fin N → C → ZMod 2), (ρ fun (n : Fin N) (x : C) => F n (h⁻¹ * x)) = h • ρ F) ∧ ∀ (v : V), ρ (ι v) = v

The odd-index relative trace (the "Sylow criterion" step of Lemma 6.11): if V is an equivariant split summand of a regular module over a subgroup P ≤ C of odd index, then it is an equivariant split summand of a regular module over C (same rank).

Kernel toolbox: structure facts for the weight-orbit argument

Abstract (s, t)-forms (apply at s := c tameSigma, t := c tameTau via tame_relation, the odd_orderOf_tameInertia pattern): the quotient by the odd normal inertia ⟨t⟩ is cyclic, every 2-subgroup is cyclic (step 1 of the discharge plan), and on a ramified simple module the inertia fixed space vanishes.

theorem GQ2.quotient_zpowers_isCyclic_of_tame {C : Type} [Group C] {s t : C} [(Subgroup.zpowers t).Normal] (hgen : Subgroup.closure {s, t} = ⊤) : IsCyclic (C ⧸ Subgroup.zpowers t)

With ⟨t⟩ normal (supplied by Tame.zpowers_normal_of_tame at the call sites), the quotient of a {s, t}-generated group by ⟨t⟩ is cyclic, generated by the image of s (the image of t is trivial, and generation passes to the quotient).

theorem GQ2.isCyclic_of_isPGroup_two_of_tame {C : Type} [Group C] [Finite C] {s t : C} (hgen : Subgroup.closure {s, t} = ⊤) (hrel : s⁻¹ * t * s = t ^ 2) (Q : Subgroup C) (hQ : IsPGroup 2 ↥Q) : IsCyclic ↥Q

Every 2-subgroup of a finite tame-generated group is cyclic (step 1 of the discharge plan): its intersection with the odd inertia ⟨t⟩ is trivial by coprimality, so it embeds in the cyclic quotient C/⟨t⟩. In particular the Sylow 2-subgroup in sylow_split_pair_of_ramified is cyclic.

theorem GQ2.fixedPoints_tame_inertia_eq_zero {C : Type} [Group C] [Finite C] {V : Type} [AddCommGroup V] [DistribMulAction C V] {s t : C} (hgen : Subgroup.closure {s, t} = ⊤) (hrel : s⁻¹ * t * s = t ^ 2) (hsimple : ∀ (W : AddSubgroup V), (∀ (h : C), ∀ w ∈ W, h • w ∈ W) → W = ⊥ ∨ W = ⊤) (hram : ∃ (v : V), t • v ≠ v) (v : V) : t • v = v → v = 0

The inertia fixed space vanishes on a ramified simple module: {v | t • v = v} is a C-stable additive subgroup (conjugates of t lie in the normal ⟨t⟩, and the stabilizer of a fixed vector contains all of ⟨t⟩), so simplicity forces it to be ⊥ — it is not ⊤ because the module is ramified.