Spans of the images of a basis #
A semilinear map has the same scalar-extended image span when evaluated on a basis as when evaluated
on its entire domain. Over a coefficient algebra A of the scalars, the A-span of one basis lies
in that of another when the change-of-basis matrix has entries in the image of A.
theorem
Module.Basis.span_range_eq_span_range_basis
{R : Type u_1}
{R' : Type u_2}
{S : Type u_3}
{M : Type u_4}
{N : Type u_5}
{ι : Type u_6}
[Semiring R]
[Semiring R']
[Semiring S]
[SMul R' S]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R' N]
[Module S N]
[IsScalarTower R' S N]
{σ : R →+* R'}
(b : Basis ι R M)
(f : M →ₛₗ[σ] N)
:
Over a scalar extension, the image of a semilinear map is spanned by its values on any basis. The ring homomorphism defining semilinearity need not be surjective.
theorem
Module.Basis.span_range_le_span_range_of_forall_toMatrix_mem
{A : Type u_1}
{S : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{ι' : Type u_5}
[CommSemiring A]
[CommSemiring S]
[Algebra A S]
[AddCommMonoid N]
[Module S N]
[Module A N]
[IsScalarTower A S N]
(b : Basis ι S N)
(b' : Basis ι' S N)
(h : ∀ (i : ι) (j : ι'), b.toMatrix (⇑b') i j ∈ Set.range ⇑(algebraMap A S))
:
If every entry of the change-of-basis matrix from b to b' lies in the image of A, then
the A-span of b' lies in the A-span of b.