Injectivity in semilinear Galois descent #
Over a finite Galois extension L/k, an injective k-linear map into the invariant vectors
of a semilinear representation stays injective after extending scalars to L. Together with
the spanning theorem for invariant vectors, this identifies a semilinear representation with
the scalar extension of its invariants. The result applies to infinite-dimensional vector
spaces and does not require the Galois group order to be invertible.
References #
- J. S. Milne, Algebraic Groups (2017), Appendix A.64 (Galois descent).
theorem
TauCeti.GaloisDescent.liftBaseChange_injective_of_invariant
{k : Type u_1}
{L : Type u_2}
{V : Type u_3}
{W : Type u_4}
[Field k]
[Field L]
[Algebra k L]
[AddCommGroup V]
[Module k V]
[Module L V]
[IsScalarTower k L V]
[AddCommGroup W]
[Module k W]
[FiniteDimensional k L]
[IsGalois k L]
{ρ : Representation k Gal(L/k) V}
{f : W →ₗ[k] V}
(hf : Function.Injective ⇑f)
(hsemi : ∀ (σ : Gal(L/k)) (a : L) (w : W), (ρ σ) (a • f w) = σ a • f w)
:
An injective map into invariant vectors of a semilinear Galois representation remains injective after scalar extension. Semilinearity is only required on scalar multiples of the image of the map. No dimension restriction is imposed on either module.