Reading a vector off a one-point coordinate support

A vector whose coordinates in a basis vanish outside a single index is that one coordinate times the corresponding basis vector. This repackages Module.Basis.repr_symm_single, which it runs through in the same direction, for the common situation where what one holds is a bound on the support rather than an explicit Finsupp.single.

Nothing here needs more than a semiring of scalars, since only Finsupp.support_subset_singleton and the coordinate isomorphism are involved.

Main results

• Module.Basis.eq_smul_of_repr_support_subset_singleton: a vector supported on one coordinate is that coordinate times the corresponding basis vector.
• Module.Basis.coord_map_apply: the coordinates with respect to a basis transported along a linear equivalence are the coordinates of the vector transported back.

theorem Module.Basis.eq_smul_of_repr_support_subset_singleton {ι : Type u_1} {K : Type u_2} {V : Type u_3} [Semiring K] [AddCommMonoid V] [Module K V] (b : Basis ι K V) {w : V} {i : ι} (h : (b.repr w).support ⊆ {i}) : w = (b.repr w) i • b i

A vector whose only possibly nonzero coordinate is the i-th one is that coordinate times the i-th basis vector.

theorem Module.Basis.repr_map_eq_of_map_basis {R : Type u_4} {M : Type u_5} {N : Type u_6} {ι : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (b : Basis ι R M) (c : Basis ι R N) (f : M →ₗ[R] N) (hf : ∀ (i : ι), f (b i) = c i) (x : M) : c.repr (f x) = b.repr x

A linear map carrying one basis to another preserves the corresponding coordinates.

theorem Module.Basis.coord_map_apply {R : Type u_4} {M : Type u_5} {M' : Type u_6} {ι : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (f : M ≃ₗ[R] M') (i : ι) (x : M') : ((b.map f).coord i) x = (b.coord i) (f.symm x)

The coordinates with respect to the basis b.map f transported along a linear equivalence f are the coordinates with respect to b of the vector transported back along f. Not a simp lemma: simp already unfolds the left side through Module.Basis.coord_apply.