Tameness of the split-case simple factors #
For a nontrivial simple 𝔽₂[C]-module V at a marking whose tame/wild inertia (τ, x₀, x₁) acts
trivially and which generates C, the C-action factors through the cyclic ⟨σ̄⟩, so it is
abelian. Two consequences, which prop_5_15 (the Prop. 5.15 proof) feeds to lemma_5_13_split:
sigma2_smul_trivial(hU) — the 2-primary partσ₂ = σ^{ω₂}acts trivially. Because the action is abelian,σ₂is central, so its fixed spaceV^{σ₂}is aC-submodule;⟨σ₂⟩is a 2-group, so (p-group fixed points, char 2)V^{σ₂} ≠ 0; simplicity forcesV^{σ₂} = V.fixedPoints_sigma_eq_zero(hVS) —V^S = 0whenσacts nontrivially:V^σis aC-submodule (σ central), so⊥or⊤; nontriviality kills⊤.
The central-fixed-point mechanism is central_pow2_smul_trivial, the analogue of lemma_5_12 with
centrality in place of normality. No finite-field / image-group construction is needed.
The set of c : C whose action commutes with a fixed automorphism g • is a subgroup.
Equations
- GQ2.FoxH.actionCommutant g = { carrier := {c : C | ∀ (v : V), g • c • v = c • g • v}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
Dually: the set of h : C commuting (in the action) with the whole C-action is a subgroup.
Used to promote centrality of g to centrality of every zpower of g.
Equations
- GQ2.FoxH.actionCentre = { carrier := {h : C | ∀ (c : C) (v : V), h • c • v = c • h • v}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
The central fixed-point lemma (analogue of lemma_5_12 with centrality for normality):
a 2-power-order element g whose action commutes with the whole C-action acts trivially on a
simple char-2 module. Its fixed space is C-stable (centrality) and nonzero (p-group fixed
points, char 2), so simplicity makes it everything.
orderOf (powOmega2 x) ∣ 2 ^ v₂(orderOf x): the 2-primary projection has 2-power order.
The odd part m = n / 2^a of n = orderOf x divides ω₂ (oddPart_dvd_omega2Exp), so
n = 2^a·m ∣ ω₂·2^a, whence (x^{ω₂})^{2^a} = 1.
⟨powOmega2 x⟩ is a 2-group — needed to feed central_pow2_smul_trivial with g = σ₂.
With τ, x₀, x₁ acting trivially and the marking generating C, any g whose action commutes
with σ's is central for the whole C-action. The commutant {c | g·c = c·g on V} is a subgroup
containing the four generators (three act trivially, σ by hypothesis), hence is all of C.
the tame representation-theory proof output hU: on a nontrivial simple char-2 module at a generating split-tame marking
(τ, x₀, x₁ trivial), the 2-primary part σ₂ acts trivially. σ₂ is central (σ₂ is a power of
σ, and the module is generated) and of 2-power order, so central_pow2_smul_trivial applies.
The stable fixed-point lemma (the central_pow2_smul_trivial mechanism with C-stability
of the fixed space assumed instead of derived from centrality): a 2-power-order g whose fixed
space is C-stable acts trivially on a simple char-2 module. This is what the ramified tame
providers need — there powOmega2 τ is not central (σ conjugates it to its square), but its
fixed space is still C-stable via the tame relation.
The tame relation conjugates the 2-primary part of τ to its square:
σ⁻¹ · τ^{ω₂} · σ = (τ^{ω₂})² — powOmega2 naturality under MulAut.conj σ⁻¹ plus
powOmega2 (τ²) = (powOmega2 τ)² (exponent independence powOmega2_pow_eq).
the tame representation-theory proof ramified output hTodd: on a simple char-2 module at a generating admissible-style
marking, the 2-primary part τ^{ω₂} of the tame generator acts trivially — i.e. τ acts with odd
order. Its fixed space is C-stable: σ preserves it via conj_powOmega2_tau (a τ^{ω₂}-fixed
vector is fixed by (τ^{ω₂})²), τ commutes with its own power, and x₀, x₁ act trivially
(wild_acts_trivially); ⟨τ^{ω₂}⟩ is a 2-group, so pow2_smul_trivial_of_stable closes. Unlike
the split hU = sigma2_smul_trivial, no hypothesis on how τ acts is needed.
The ramified pairing operator 1 + U + U⁻¹ is injective for U = σ₂ on a char-2 module —
with no hypothesis on how σ₂ acts. U has 2-power order (orderOf_powOmega2_dvd_two_pow),
so in char 2 the operator is unipotent: writing E_j(w) = U^{2^j}w + w = (U+1)^{2^j}w, the
U-scaled kernel equation gives E_1(v) = Uv, squaring inductively gives
E_{j+1}(v) = U^{2^j}v, and at 2^j = the order both sides collapse to 0 = v. This is the
nondegeneracy engine for the ramified pairing λ((1+U+U⁻¹)c) of lemma_5_13_pairing_ramified.
the tame representation-theory proof output hVS: on a nontrivial simple char-2 module at a generating split-tame
marking
where σ acts nontrivially, V^S = 0 (the 1 + S⁻¹-invertibility feeding lemma_5_13_split).
V^σ is a C-submodule (σ central), so ⊥ or ⊤; the nontriviality hσ kills ⊤.