Composition with linear functionals on division semirings #
A nonzero linear functional with values in a division semiring is surjective. Consequently, composing it, after restriction of scalars, with any nonzero linear map gives a nonzero map. This applies in particular to compositions of transfer functionals in a tower of field extensions.
theorem
LinearMap.comp_restrictScalars_ne_zero
{K : Type u_1}
{L : Type u_2}
{E : Type u_3}
{M : Type u_4}
[Semiring K]
[DivisionSemiring L]
[AddCommMonoid E]
[AddCommMonoid M]
[Module K L]
[Module K E]
[Module L E]
[Module K M]
[CompatibleSMul E L K L]
(s : L →ₗ[K] M)
(t : E →ₗ[L] L)
(hs : s ≠ 0)
(ht : t ≠ 0)
:
Composing a nonzero linear map with a nonzero linear functional on a division semiring, after restricting scalars, gives a nonzero map.