Recognizing the invariant vectors by scalar extension #
An invariant subspace of a semilinear representation over a finite Galois extension is the whole space of invariants if its scalar extension surjects onto the representation. This criterion identifies tensor products of descended vector spaces with invariant tensors. It works in arbitrary characteristic, using an element of field trace one instead of dividing by the order of the Galois group.
References #
- J. S. Milne, Algebraic Groups (2017), Appendix A.64 (Galois descent).
theorem
TauCeti.GaloisDescent.range_eq_invariants_of_liftBaseChange_surjective
{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}
(hsemi : ∀ (σ : Gal(L/k)) (a : L) (v : V), (ρ σ) (a • v) = σ a • (ρ σ) v)
(hinv : ∀ (σ : Gal(L/k)) (w : W), (ρ σ) (f w) = f w)
(hf : Function.Surjective ⇑(LinearMap.liftBaseChange L f))
:
An invariant linear map whose scalar extension is surjective has image equal to all the invariant vectors. Neither vector space needs to be finite-dimensional.