Lifting a norm decomposition of the identity from k/pk #
Let G be a finite group of order p ^ m acting on a projective k-module V on which
multiplication by p is injective. If the identity of the reduction (k/pk) ⊗ V is a norm
y ↦ ∑ g, ρ g (π (ρ g⁻¹ y)) for the conjugation action of G, then so is the identity of V
(Serre, Local Fields, IX §5). This reduces the identity-norm condition for p-groups over k
to the same condition over k/pk.
Main statements #
Representation.id_mem_range_norm_linHom_of_baseChange: the lifting statement above.
References #
- J.-P. Serre, Local Fields, Chapter IX, §5.
theorem
Representation.id_mem_range_norm_linHom_of_baseChange
{k : Type u_1}
{G : Type u_2}
{V : Type u_3}
[CommRing k]
[Group G]
[Fintype G]
[AddCommGroup V]
[Module k V]
[Module.Projective k V]
(ρ : Representation k G V)
{p m : ℕ}
(hcard : Fintype.card G = p ^ m)
(hp : ∀ (v : V), ↑p • v = 0 → v = 0)
(h :
LinearMap.id ∈ LinearMap.range ((baseChange (k ⧸ Ideal.span {↑p}) ρ).linHom (baseChange (k ⧸ Ideal.span {↑p}) ρ)).norm)
:
Lifting a norm decomposition of the identity from k/pk. Let G have order p ^ m and
act on a projective k-module V on which multiplication by p is injective. If the identity of
(k/pk) ⊗ V is a norm for the conjugation action of G, then so is the identity of V.