Finsupp.linearCombination

Main definitions

• Finsupp.linearCombination R (v : ι → M): sends l : ι → R to the linear combination of v i with coefficients l i;
• Finsupp.linearCombinationOn: a restricted version of Finsupp.linearCombination with domain

Tags

function with finite support, module, linear algebra

def Finsupp.linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : α → M) : (α →₀ R) →ₗ[R] M

Interprets (l : α →₀ R) as a linear combination of the elements in the family (v : α → M) and evaluates this linear combination.

Equations

• Finsupp.linearCombination R v = (Finsupp.lsum ℕ) fun (i : α) => LinearMap.id.smulRight (v i)

theorem Finsupp.linearCombination_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (l : α →₀ R) : (linearCombination R v) l = l.sum fun (i : α) (a : R) => a • v i

theorem Finsupp.linearCombination_apply_of_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {l : α →₀ R} {s : Finset α} (hs : l ∈ supported R R ↑s) : (linearCombination R v) l = ∑ i ∈ s, l i • v i

@[simp]

theorem Finsupp.linearCombination_single {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (c : R) (a : α) : (linearCombination R v) (single a c) = c • v a

theorem Finsupp.linearCombination_zero_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (x : α →₀ R) : (linearCombination R 0) x = 0

@[simp]

theorem Finsupp.linearCombination_zero (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] : linearCombination R 0 = 0

@[simp]

theorem Finsupp.linearCombination_single_index (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (c : M) (a : α) (f : α →₀ R) [DecidableEq α] : (linearCombination R (Pi.single a c)) f = f a • c

theorem Finsupp.linearCombination_linear_comp {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v : α → M} (f : M →ₗ[R] M') : linearCombination R (⇑f ∘ v) = f ∘ₗ linearCombination R v

theorem Finsupp.apply_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (v : α → M) (l : α →₀ R) : f ((linearCombination R v) l) = (linearCombination R (⇑f ∘ v)) l

theorem Finsupp.apply_linearCombination_id {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (l : M →₀ R) : f ((linearCombination R id) l) = (linearCombination R ⇑f) l

theorem Finsupp.linearCombination_unique {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Unique α] (l : α →₀ R) (v : α → M) : (linearCombination R v) l = l default • v default

theorem Finsupp.linearCombination_surjective {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (h : Function.Surjective v) : Function.Surjective ⇑(linearCombination R v)

theorem Finsupp.linearCombination_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (h : Function.Surjective v) : LinearMap.range (linearCombination R v) = ⊤

theorem Finsupp.linearCombination_id_surjective (R : Type u_5) [Semiring R] (M : Type u_9) [AddCommMonoid M] [Module R M] : Function.Surjective ⇑(linearCombination R id)

Any module is a quotient of a free module. This is stated as surjectivity of Finsupp.linearCombination R id : (M →₀ R) →ₗ[R] M.

theorem Finsupp.range_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} : LinearMap.range (linearCombination R v) = Submodule.span R (Set.range v)

theorem Finsupp.lmapDomain_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v : α → M} {v' : α' → M'} (f : α → α') (g : M →ₗ[R] M') (h : ∀ (i : α), g (v i) = v' (f i)) : linearCombination R v' ∘ₗ lmapDomain R R f = g ∘ₗ linearCombination R v

theorem Finsupp.linearCombination_comp_lmapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α → α') : linearCombination R v' ∘ₗ lmapDomain R R f = linearCombination R (v' ∘ f)

@[simp]

theorem Finsupp.linearCombination_embDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α ↪ α') (l : α →₀ R) : (linearCombination R v') (embDomain f l) = (linearCombination R (v' ∘ ⇑f)) l

@[simp]

theorem Finsupp.linearCombination_mapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α → α') (l : α →₀ R) : (linearCombination R v') (mapDomain f l) = (linearCombination R (v' ∘ f)) l

@[simp]

theorem Finsupp.linearCombination_equivMapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α ≃ α') (l : α →₀ R) : (linearCombination R v') (equivMapDomain f l) = (linearCombination R (v' ∘ ⇑f)) l

theorem Finsupp.span_eq_range_linearCombination {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) : Submodule.span R s = LinearMap.range (linearCombination R Subtype.val)

A version of Finsupp.range_linearCombination which is useful for going in the other direction

theorem Finsupp.mem_span_iff_linearCombination {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (x : M) : x ∈ Submodule.span R s ↔ ∃ (l : ↑s →₀ R), (linearCombination R Subtype.val) l = x

theorem Finsupp.mem_span_range_iff_exists_finsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {x : M} : x ∈ Submodule.span R (Set.range v) ↔ ∃ (c : α →₀ R), (c.sum fun (i : α) (a : R) => a • v i) = x

theorem Finsupp.span_image_eq_map_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (s : Set α) : Submodule.span R (v '' s) = Submodule.map (linearCombination R v) (supported R R s)

theorem Finsupp.mem_span_image_iff_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {s : Set α} {x : M} : x ∈ Submodule.span R (v '' s) ↔ ∃ l ∈ supported R R s, (linearCombination R v) l = x

theorem Finsupp.linearCombination_option {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : Option α → M) (f : Option α →₀ R) : (linearCombination R v) f = f none • v none + (linearCombination R (v ∘ Option.some)) f.some

theorem Finsupp.linearCombination_linearCombination {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_9} {β : Type u_10} (A : α → M) (B : β → α →₀ R) (f : β →₀ R) : (linearCombination R A) ((linearCombination R B) f) = (linearCombination R fun (b : β) => (linearCombination R A) (B b)) f

theorem Finsupp.linearCombination_smul {α : Type u_1} {M : Type u_2} (R : Type u_5) {S : Type u_6} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] {α' : Type u_7} {v : α → M} [Module R S] [Module S M] [IsScalarTower R S M] {w : α' → S} : (linearCombination R fun (i : α × α') => w i.2 • v i.1) = ↑R (linearCombination S v) ∘ₗ mapRange.linearMap (linearCombination R w) ∘ₗ ↑(finsuppProdLEquiv R)

@[simp]

theorem Finsupp.linearCombination_fin_zero {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (f : Fin 0 → M) : linearCombination R f = 0

def Finsupp.linearCombinationOn (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : α → M) (s : Set α) : ↥(supported R R s) →ₗ[R] ↥(Submodule.span R (v '' s))

Finsupp.linearCombinationOn M v s interprets p : α →₀ R as a linear combination of a subset of the vectors in v, mapping it to the span of those vectors.

The subset is indicated by a set s : Set α of indices.

Equations

• Finsupp.linearCombinationOn α M R v s = LinearMap.codRestrict (Submodule.span R (v '' s)) (Finsupp.linearCombination R v ∘ₗ (Finsupp.supported R R s).subtype) ⋯

theorem Finsupp.linearCombinationOn_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (s : Set α) : LinearMap.range (linearCombinationOn α M R v s) = ⊤

theorem Finsupp.linearCombination_restrict {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (s : Set α) : linearCombination R (s.restrict v) = (Submodule.span R (v '' s)).subtype ∘ₗ linearCombinationOn α M R v s ∘ₗ ↑(supportedEquivFinsupp s).symm

theorem Finsupp.linearCombination_comp {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {v : α → M} (f : α' → α) : linearCombination R (v ∘ f) = linearCombination R v ∘ₗ lmapDomain R R f

theorem Finsupp.linearCombination_comapDomain {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {v : α → M} (f : α → α') (l : α' →₀ R) (hf : Set.InjOn f (f ⁻¹' ↑l.support)) : (linearCombination R v) (comapDomain f l hf) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i

theorem Finsupp.linearCombination_onFinset {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Finset α} {f : α → R} (g : α → M) (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) : (linearCombination R g) (onFinset s f hf) = ∑ x ∈ s, f x • g x

def Fintype.linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] : (α → M) →ₗ[S] (α → R) →ₗ[R] M

Fintype.linearCombination R S v f is the linear combination of vectors in v with weights in f. This variant of Finsupp.linearCombination is defined on fintype indexed vectors.

This map is linear in v if R is commutative, and always linear in f. See note [bundled maps over different rings] for why separate R and S semirings are used.

Equations

• Fintype.linearCombination R S = { toFun := fun (v : α → M) => { toFun := fun (f : α → R) => ∑ i : α, f i • v i, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

theorem Fintype.linearCombination_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) (f : α → R) : ((Fintype.linearCombination R S) v) f = ∑ i : α, f i • v i

@[simp]

theorem Fintype.linearCombination_apply_single {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) [DecidableEq α] (i : α) (r : R) : ((Fintype.linearCombination R S) v) (Pi.single i r) = r • v i

theorem Finsupp.linearCombination_eq_fintype_linearCombination_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) (x : α → R) : (linearCombination R v) ((linearEquivFunOnFinite R R α).symm x) = ((Fintype.linearCombination R S) v) x

theorem Finsupp.linearCombination_eq_fintype_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) : linearCombination R v ∘ₗ ↑(linearEquivFunOnFinite R R α).symm = (Fintype.linearCombination R S) v

@[simp]

theorem Fintype.range_linearCombination {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) : LinearMap.range ((Fintype.linearCombination R S) v) = Submodule.span R (Set.range v)

theorem mem_span_range_iff_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {x : M} : x ∈ Submodule.span R (Set.range v) ↔ ∃ (c : α → R), ∑ i : α, c i • v i = x

An element x lies in the span of v iff it can be written as sum ∑ cᵢ • vᵢ = x.

theorem top_le_span_range_iff_forall_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} : ⊤ ≤ Submodule.span R (Set.range v) ↔ ∀ (x : M), ∃ (c : α → R), ∑ i : α, c i • v i = x

A family v : α → V is generating V iff every element (x : V) can be written as sum ∑ cᵢ • vᵢ = x.

theorem mem_span_image_iff_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {x : M} {s : Set α} : x ∈ Submodule.span R (v '' s) ↔ ∃ (t : Finset α), ↑t ⊆ s ∧ ∃ (c : { x : α // x ∈ t } → R), ∑ i : { x : α // x ∈ t }, c i • v ↑i = x

theorem Fintype.mem_span_image_iff_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {x : M} {s : Set α} [Fintype ↑s] : x ∈ Submodule.span R (v '' s) ↔ ∃ (c : ↑s → R), ∑ i : ↑s, c i • v ↑i = x

@[irreducible]

def Span.repr (R : Type u_4) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (w : Set M) (x : ↥(Submodule.span R w)) : ↑w →₀ R

Pick some representation of x : span R w as a linear combination in w, ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose

Equations

• Span.repr R w x = ⋯.choose

theorem Span.repr_def (R : Type u_4) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (w : Set M) (x : ↥(Submodule.span R w)) : repr R w x = ⋯.choose

@[simp]

theorem Span.finsupp_linearCombination_repr (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {w : Set M} (x : ↥(Submodule.span R w)) : (Finsupp.linearCombination R Subtype.val) (repr R w x) = ↑x

theorem LinearMap.map_finsupp_linearCombination {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) {ι : Type u_4} {g : ι → M} (l : ι →₀ R) : f ((Finsupp.linearCombination R g) l) = (Finsupp.linearCombination R (⇑f ∘ g)) l

theorem mem_span_finset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s : Finset M} {x : M} : x ∈ Submodule.span R ↑s ↔ ∃ (f : M → R), ∑ i ∈ s, f i • i = x

theorem mem_span_set {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {m : M} {s : Set M} : m ∈ Submodule.span R s ↔ ∃ (c : M →₀ R), ↑c.support ⊆ s ∧ (c.sum fun (mi : M) (r : R) => r • mi) = m

An element m ∈ M is contained in the R-submodule spanned by a set s ⊆ M, if and only if m can be written as a finite R-linear combination of elements of s. The implementation uses Finsupp.sum.

theorem mem_span_set' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {m : M} {s : Set M} : m ∈ Submodule.span R s ↔ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → ↑s), ∑ i : Fin n, f i • ↑(g i) = m

An element m ∈ M is contained in the R-submodule spanned by a set s ⊆ M, if and only if m can be written as a finite R-linear combination of elements of s. The implementation uses a sum indexed by Fin n for some n.

theorem span_eq_iUnion_nat {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) : ↑(Submodule.span R s) = ⋃ (n : ℕ), (fun (f : Fin n → R × M) => ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s}

The span of a subset s is the union over all n of the set of linear combinations of at most n terms belonging to s.