Linear maps out of free modules in terms of their values on the basis

A linear map out of the free module ι →₀ A is determined by its values on the basis vectors Finsupp.single i 1. This file records the resulting expansion of f z as a finite sum, and its coordinatewise form for maps between free modules, where the values f (Finsupp.single i 1) j are the matrix coefficients of f.

Main results

• LinearMap.apply_eq_finsuppSum_smul: f z = z.sum fun i a ↦ a • f (Finsupp.single i 1).
• LinearMap.apply_apply_eq_finsuppSum_mul: the j-th coordinate of f z is z.sum fun i a ↦ a * f (Finsupp.single i 1) j.

theorem LinearMap.apply_eq_finsuppSum_smul {A : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring A] [AddCommMonoid M] [Module A M] (f : (ι →₀ A) →ₗ[A] M) (z : ι →₀ A) : f z = z.sum fun (i : ι) (a : A) => a • f (Finsupp.single i 1)

A linear map out of a free module is the finite sum of its values on the basis vectors, weighted by the coordinates.

theorem LinearMap.apply_apply_eq_finsuppSum_mul {A : Type u_1} {ι : Type u_3} {κ : Type u_4} [Semiring A] (f : (ι →₀ A) →ₗ[A] κ →₀ A) (z : ι →₀ A) (j : κ) : (f z) j = z.sum fun (i : ι) (a : A) => a * (f (Finsupp.single i 1)) j

A linear map between free modules is determined by its matrix coefficients: the j-th coordinate of f z is ∑ i, z i * (f (Finsupp.single i 1)) j.