mathlib3 documentation

linear_algebra.finsupp

Properties of the module α →₀ M #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given an R-module M, the R-module structure on α →₀ M is defined in data.finsupp.basic.

In this file we define finsupp.supported s to be the set {f : α →₀ M | f.support ⊆ s} interpreted as a submodule of α →₀ M. We also define linear_map versions of various maps:

Tags #

function with finite support, module, linear algebra

source
noncomputable def finsupp.lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (a : α) :
M →ₗ[R] α →₀ M

Interpret finsupp.single a as a linear map.

Equations
source
theorem finsupp.lhom_ext {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ (a : α) (b : M), ⇑φ (finsupp.single a b) = ⇑ψ (finsupp.single a b)) :
φ = ψ

Two R-linear maps from finsupp X M which agree on each single x y agree everywhere.

source
@[ext]
theorem finsupp.lhom_ext' {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ (a : α), φ.comp (finsupp.lsingle a) = ψ.comp (finsupp.lsingle a)) :
φ = ψ

Two R-linear maps from finsupp X M which agree on each single x y agree everywhere.

We formulate this fact using equality of linear maps φ.comp (lsingle a) and ψ.comp (lsingle a) so that the ext tactic can apply a type-specific extensionality lemma to prove equality of these maps. E.g., if M = R, then it suffices to verify φ (single a 1) = ψ (single a 1).

source
noncomputable def finsupp.lapply {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (a : α) :
(α →₀ M) →ₗ[R] M

Interpret λ (f : α →₀ M), f a as a linear map.

Equations
source
@[simp]
theorem finsupp.lcoe_fun_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (x : α →₀ M) (ᾰ : α) :
⇑finsupp.lcoe_fun x ᾰ = ⇑x ᾰ
source
def finsupp.lcoe_fun {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] :
(α →₀ M) →ₗ[R] α → M

Forget that a function is finitely supported.

This is the linear version of finsupp.to_fun.

Equations
source
noncomputable def finsupp.lsubtype_domain {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (s : set α) :
(α →₀ M) →ₗ[R] ↥s →₀ M

Interpret finsupp.subtype_domain s as a linear map.

Equations
source
theorem finsupp.lsubtype_domain_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (s : set α) (f : α →₀ M) :
⇑(finsupp.lsubtype_domain s) f = finsupp.subtype_domain (λ (x : α), x ∈ s) f
source
@[simp]
theorem finsupp.lsingle_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (a : α) (b : M) :
⇑(finsupp.lsingle a) b = finsupp.single a b
source
@[simp]
theorem finsupp.lapply_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (a : α) (f : α →₀ M) :
⇑(finsupp.lapply a) f = ⇑f a
source
@[simp]
theorem finsupp.ker_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (a : α) :
linear_map.ker (finsupp.lsingle a) = ⊥
source
theorem finsupp.lsingle_range_le_ker_lapply {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (s t : set α) (h : disjoint s t) :
(⨆ (a : α) (H : a ∈ s), linear_map.range (finsupp.lsingle a)) ≤ ⨅ (a : α) (H : a ∈ t), linear_map.ker (finsupp.lapply a)
source
theorem finsupp.infi_ker_lapply_le_bot {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] :
(⨅ (a : α), linear_map.ker (finsupp.lapply a)) ≤ ⊥
source
theorem finsupp.supr_lsingle_range {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] :
(⨆ (a : α), linear_map.range (finsupp.lsingle a)) = ⊤
source
theorem finsupp.disjoint_lsingle_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (s t : set α) (hs : disjoint s t) :
disjoint (⨆ (a : α) (H : a ∈ s), linear_map.range (finsupp.lsingle a)) (⨆ (a : α) (H : a ∈ t), linear_map.range (finsupp.lsingle a))
source
theorem finsupp.span_single_image {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (s : set M) (a : α) :
submodule.span R (finsupp.single a '' s) = submodule.map (finsupp.lsingle a) (submodule.span R s)
source
def finsupp.supported {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (s : set α) :
submodule R (α →₀ M)

finsupp.supported M R s is the R-submodule of all p : α →₀ M such that p.support ⊆ s.

Equations
source
theorem finsupp.mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {s : set α} (p : α →₀ M) :
p ∈ finsupp.supported M R s ↔ ↑(p.support) ⊆ s
source
theorem finsupp.mem_supported' {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {s : set α} (p : α →₀ M) :
p ∈ finsupp.supported M R s ↔ ∀ (x : α), x ∉ s → ⇑p x = 0
source
theorem finsupp.mem_supported_support {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (p : α →₀ M) :
p ∈ finsupp.supported M R ↑(p.support)
source
theorem finsupp.single_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {s : set α} {a : α} (b : M) (h : a ∈ s) :
finsupp.single a b ∈ finsupp.supported M R s
source
theorem finsupp.supported_eq_span_single {α : Type u_1} (R : Type u_5) [semiring R] (s : set α) :
finsupp.supported R R s = submodule.span R ((λ (i : α), finsupp.single i 1) '' s)
source
noncomputable def finsupp.restrict_dom {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (s : set α) :
(α →₀ M) →ₗ[R] ↥(finsupp.supported M R s)

Interpret finsupp.filter s as a linear map from α →₀ M to supported M R s.

Equations
source
@[simp]
theorem finsupp.restrict_dom_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (s : set α) (l : α →₀ M) :
↑(⇑(finsupp.restrict_dom M R s) l) = finsupp.filter (λ (_x : α), _x ∈ s) l
source
theorem finsupp.restrict_dom_comp_subtype {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (s : set α) :
(finsupp.restrict_dom M R s).comp (finsupp.supported M R s).subtype = linear_map.id
source
theorem finsupp.range_restrict_dom {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (s : set α) :
linear_map.range (finsupp.restrict_dom M R s) = ⊤
source
theorem finsupp.supported_mono {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {s t : set α} (st : s ⊆ t) :
finsupp.supported M R s ≤ finsupp.supported M R t
source
@[simp]
theorem finsupp.supported_empty {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] :
finsupp.supported M R ∅ = ⊥
source
@[simp]
theorem finsupp.supported_univ {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] :
finsupp.supported M R set.univ = ⊤
source
theorem finsupp.supported_Union {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {δ : Type u_3} (s : δ → set α) :
finsupp.supported M R (⋃ (i : δ), s i) = ⨆ (i : δ), finsupp.supported M R (s i)
source
theorem finsupp.supported_union {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (s t : set α) :
finsupp.supported M R (s ∪ t) = finsupp.supported M R s ⊔ finsupp.supported M R t
source
theorem finsupp.supported_Inter {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_3} (s : ι → set α) :
finsupp.supported M R (⋂ (i : ι), s i) = ⨅ (i : ι), finsupp.supported M R (s i)
source
theorem finsupp.supported_inter {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (s t : set α) :
finsupp.supported M R (s ∩ t) = finsupp.supported M R s ⊓ finsupp.supported M R t
source
theorem finsupp.disjoint_supported_supported {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {s t : set α} (h : disjoint s t) :
disjoint (finsupp.supported M R s) (finsupp.supported M R t)
source
theorem finsupp.disjoint_supported_supported_iff {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [nontrivial M] {s t : set α} :
disjoint (finsupp.supported M R s) (finsupp.supported M R t) ↔ disjoint s t
source
noncomputable def finsupp.supported_equiv_finsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] (s : set α) :
↥(finsupp.supported M R s) ≃ₗ[R] ↥s →₀ M

Interpret finsupp.restrict_support_equiv as a linear equivalence between supported M R s and s →₀ M.

Equations
source
noncomputable def finsupp.lsum {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [semiring R] [semiring S] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] [module S N] [smul_comm_class R S N] :
(α → (M →ₗ[R] N)) ≃ₗ[S] (α →₀ M) →ₗ[R] N

Lift a family of linear maps M →ₗ[R] N indexed by x : α to a linear map from α →₀ M to N using finsupp.sum. This is an upgraded version of finsupp.lift_add_hom.

See note [bundled maps over different rings] for why separate R and S semirings are used.

Equations
source
@[simp]
theorem finsupp.coe_lsum {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [semiring R] [semiring S] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] [module S N] [smul_comm_class R S N] (f : α → (M →ₗ[R] N)) :
⇑(⇑(finsupp.lsum S) f) = λ (d : α →₀ M), d.sum (λ (i : α), ⇑(f i))
source
theorem finsupp.lsum_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [semiring R] [semiring S] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] [module S N] [smul_comm_class R S N] (f : α → (M →ₗ[R] N)) (l : α →₀ M) :
⇑(⇑(finsupp.lsum S) f) l = l.sum (λ (b : α), ⇑(f b))
source
theorem finsupp.lsum_single {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [semiring R] [semiring S] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] [module S N] [smul_comm_class R S N] (f : α → (M →ₗ[R] N)) (i : α) (m : M) :
⇑(⇑(finsupp.lsum S) f) (finsupp.single i m) = ⇑(f i) m
source
theorem finsupp.lsum_symm_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [semiring R] [semiring S] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] [module S N] [smul_comm_class R S N] (f : (α →₀ M) →ₗ[R] N) (x : α) :
⇑((finsupp.lsum S).symm) f x = f.comp (finsupp.lsingle x)
source
noncomputable def finsupp.lift (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (X : Type u_7) :
(X → M) ≃+ ((X →₀ R) →ₗ[R] M)

A slight rearrangement from lsum gives us the bijection underlying the free-forgetful adjunction for R-modules.

Equations
source
@[simp]
theorem finsupp.lift_symm_apply (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (X : Type u_7) (f : (X →₀ R) →ₗ[R] M) (x : X) :
⇑((finsupp.lift M R X).symm) f x = ⇑f (finsupp.single x 1)
source
@[simp]
theorem finsupp.lift_apply (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (X : Type u_7) (f : X → M) (g : X →₀ R) :
⇑(⇑(finsupp.lift M R X) f) g = g.sum (λ (x : X) (r : R), r • f x)
source
noncomputable def finsupp.llift (M : Type u_2) (R : Type u_5) (S : Type u_6) [semiring R] [semiring S] [add_comm_monoid M] [module R M] (X : Type u_7) [module S M] [smul_comm_class R S M] :
(X → M) ≃ₗ[S] (X →₀ R) →ₗ[R] M

Given compatible S and R-module structures on M and a type X, the set of functions X → M is S-linearly equivalent to the R-linear maps from the free R-module on X to M.

Equations
source
@[simp]
theorem finsupp.llift_apply (M : Type u_2) (R : Type u_5) (S : Type u_6) [semiring R] [semiring S] [add_comm_monoid M] [module R M] (X : Type u_7) [module S M] [smul_comm_class R S M] (f : X → M) (x : X →₀ R) :
⇑(⇑(finsupp.llift M R S X) f) x = ⇑(⇑(finsupp.lift M R X) f) x
source
@[simp]
theorem finsupp.llift_symm_apply (M : Type u_2) (R : Type u_5) (S : Type u_6) [semiring R] [semiring S] [add_comm_monoid M] [module R M] (X : Type u_7) [module S M] [smul_comm_class R S M] (f : (X →₀ R) →ₗ[R] M) (x : X) :
⇑((finsupp.llift M R S X).symm) f x = ⇑f (finsupp.single x 1)
source
noncomputable def finsupp.lmap_domain {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α' : Type u_7} (f : α → α') :
(α →₀ M) →ₗ[R] α' →₀ M

Interpret finsupp.map_domain as a linear map.

Equations
source
@[simp]
theorem finsupp.lmap_domain_apply {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α' : Type u_7} (f : α → α') (l : α →₀ M) :
⇑(finsupp.lmap_domain M R f) l = finsupp.map_domain f l
source
@[simp]
theorem finsupp.lmap_domain_id {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] :
finsupp.lmap_domain M R id = linear_map.id
source
theorem finsupp.lmap_domain_comp {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α' : Type u_7} {α'' : Type u_8} (f : α → α') (g : α' → α'') :
finsupp.lmap_domain M R (g ∘ f) = (finsupp.lmap_domain M R g).comp (finsupp.lmap_domain M R f)
source
theorem finsupp.supported_comap_lmap_domain {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α' : Type u_7} (f : α → α') (s : set α') :
finsupp.supported M R (f ⁻¹' s) ≤ submodule.comap (finsupp.lmap_domain M R f) (finsupp.supported M R s)
source
theorem finsupp.lmap_domain_supported {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α' : Type u_7} [nonempty α] (f : α → α') (s : set α) :
submodule.map (finsupp.lmap_domain M R f) (finsupp.supported M R s) = finsupp.supported M R (f '' s)
source
theorem finsupp.lmap_domain_disjoint_ker {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α' : Type u_7} (f : α → α') {s : set α} (H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → f a = f b → a = b) :
disjoint (finsupp.supported M R s) (linear_map.ker (finsupp.lmap_domain M R f))
source
noncomputable def finsupp.lcomap_domain {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {β : Type u_7} (f : α → β) (hf : function.injective f) :
(β →₀ M) →ₗ[R] α →₀ M

Given f : α → β and a proof hf that f is injective, lcomap_domain f hf is the linear map sending l : β →₀ M to the finitely supported function from α to M given by composing l with f.

This is the linear version of finsupp.comap_domain.

Equations
source
@[protected]
noncomputable def finsupp.total (α : Type u_1) (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (v : α → M) :
(α →₀ R) →ₗ[R] M

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

Equations
source
theorem finsupp.total_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {v : α → M} (l : α →₀ R) :
⇑(finsupp.total α M R v) l = l.sum (λ (i : α) (a : R), a • v i)
source
theorem finsupp.total_apply_of_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {v : α → M} {l : α →₀ R} {s : finset α} (hs : l ∈ finsupp.supported R R ↑s) :
⇑(finsupp.total α M R v) l = s.sum (λ (i : α), ⇑l i • v i)
source
@[simp]
theorem finsupp.total_single {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {v : α → M} (c : R) (a : α) :
⇑(finsupp.total α M R v) (finsupp.single a c) = c • v a
source
theorem finsupp.total_zero_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (x : α →₀ R) :
⇑(finsupp.total α M R 0) x = 0
source
@[simp]
theorem finsupp.total_zero (α : Type u_1) (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] :
finsupp.total α M R 0 = 0
source
theorem finsupp.apply_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {M' : Type u_8} [add_comm_monoid M'] [module R M'] (f : M →ₗ[R] M') (v : α → M) (l : α →₀ R) :
⇑f (⇑(finsupp.total α M R v) l) = ⇑(finsupp.total α M' R (⇑f ∘ v)) l
source
theorem finsupp.total_unique {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] [unique α] (l : α →₀ R) (v : α → M) :
⇑(finsupp.total α M R v) l = ⇑l inhabited.default • v inhabited.default
source
theorem finsupp.total_surjective {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {v : α → M} (h : function.surjective v) :
function.surjective ⇑(finsupp.total α M R v)
source
theorem finsupp.total_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {v : α → M} (h : function.surjective v) :
linear_map.range (finsupp.total α M R v) = ⊤
source
theorem finsupp.total_id_surjective (R : Type u_5) [semiring R] (M : Type u_1) [add_comm_monoid M] [module R M] :
function.surjective ⇑(finsupp.total M M R id)

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

source
theorem finsupp.range_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {v : α → M} :
linear_map.range (finsupp.total α M R v) = submodule.span R (set.range v)
source
theorem finsupp.lmap_domain_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α' : Type u_7} {M' : Type u_8} [add_comm_monoid M'] [module R M'] {v : α → M} {v' : α' → M'} (f : α → α') (g : M →ₗ[R] M') (h : ∀ (i : α), ⇑g (v i) = v' (f i)) :
(finsupp.total α' M' R v').comp (finsupp.lmap_domain R R f) = g.comp (finsupp.total α M R v)
source
theorem finsupp.total_comp_lmap_domain {α : Type u_1} (R : Type u_5) [semiring R] {α' : Type u_7} {M' : Type u_8} [add_comm_monoid M'] [module R M'] {v' : α' → M'} (f : α → α') :
(finsupp.total α' M' R v').comp (finsupp.lmap_domain R R f) = finsupp.total α M' R (v' ∘ f)
source
@[simp]
theorem finsupp.total_emb_domain {α : Type u_1} (R : Type u_5) [semiring R] {α' : Type u_7} {M' : Type u_8} [add_comm_monoid M'] [module R M'] {v' : α' → M'} (f : α ↪ α') (l : α →₀ R) :
⇑(finsupp.total α' M' R v') (finsupp.emb_domain f l) = ⇑(finsupp.total α M' R (v' ∘ ⇑f)) l
source
@[simp]
theorem finsupp.total_map_domain {α : Type u_1} (R : Type u_5) [semiring R] {α' : Type u_7} {M' : Type u_8} [add_comm_monoid M'] [module R M'] {v' : α' → M'} (f : α → α') (l : α →₀ R) :
⇑(finsupp.total α' M' R v') (finsupp.map_domain f l) = ⇑(finsupp.total α M' R (v' ∘ f)) l
source
@[simp]
theorem finsupp.total_equiv_map_domain {α : Type u_1} (R : Type u_5) [semiring R] {α' : Type u_7} {M' : Type u_8} [add_comm_monoid M'] [module R M'] {v' : α' → M'} (f : α ≃ α') (l : α →₀ R) :
⇑(finsupp.total α' M' R v') (finsupp.equiv_map_domain f l) = ⇑(finsupp.total α M' R (v' ∘ ⇑f)) l
source
theorem finsupp.span_eq_range_total {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (s : set M) :
submodule.span R s = linear_map.range (finsupp.total ↥s M R coe)

A version of finsupp.range_total which is useful for going in the other direction

source
theorem finsupp.mem_span_iff_total {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (s : set M) (x : M) :
x ∈ submodule.span R s ↔ ∃ (l : ↥s →₀ R), ⇑(finsupp.total ↥s M R coe) l = x
source
theorem finsupp.mem_span_range_iff_exists_finsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {v : α → M} {x : M} :
x ∈ submodule.span R (set.range v) ↔ ∃ (c : α →₀ R), c.sum (λ (i : α) (a : R), a • v i) = x
source
theorem finsupp.span_image_eq_map_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {v : α → M} (s : set α) :
submodule.span R (v '' s) = submodule.map (finsupp.total α M R v) (finsupp.supported R R s)
source
theorem finsupp.mem_span_image_iff_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {v : α → M} {s : set α} {x : M} :
x ∈ submodule.span R (v '' s) ↔ ∃ (l : α →₀ R) (H : l ∈ finsupp.supported R R s), ⇑(finsupp.total α M R v) l = x
source
theorem finsupp.total_option {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (v : option α → M) (f : option α →₀ R) :
⇑(finsupp.total (option α) M R v) f = ⇑f option.none • v option.none + ⇑(finsupp.total α M R (v ∘ option.some)) f.some
source
theorem finsupp.total_total {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α : Type u_1} {β : Type u_3} (A : α → M) (B : β → α →₀ R) (f : β →₀ R) :
⇑(finsupp.total α M R A) (⇑(finsupp.total β (α →₀ R) R B) f) = ⇑(finsupp.total β M R (λ (b : β), ⇑(finsupp.total α M R A) (B b))) f
source
@[simp]
theorem finsupp.total_fin_zero {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (f : fin 0 → M) :
finsupp.total (fin 0) M R f = 0
source
@[protected]
noncomputable def finsupp.total_on (α : Type u_1) (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] (v : α → M) (s : set α) :
↥(finsupp.supported R R s) →ₗ[R] ↥(submodule.span R (v '' s))

finsupp.total_on 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
source
theorem finsupp.total_on_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {v : α → M} (s : set α) :
linear_map.range (finsupp.total_on α M R v s) = ⊤
source
theorem finsupp.total_comp {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α' : Type u_7} {v : α → M} (f : α' → α) :
finsupp.total α' M R (v ∘ f) = (finsupp.total α M R v).comp (finsupp.lmap_domain R R f)
source
theorem finsupp.total_comap_domain {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α' : Type u_7} {v : α → M} (f : α → α') (l : α' →₀ R) (hf : set.inj_on f (f ⁻¹' ↑(l.support))) :
⇑(finsupp.total α M R v) (finsupp.comap_domain f l hf) = (l.support.preimage f hf).sum (λ (i : α), ⇑l (f i) • v i)
source
theorem finsupp.total_on_finset {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {s : finset α} {f : α → R} (g : α → M) (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) :
⇑(finsupp.total α M R g) (finsupp.on_finset s f hf) = s.sum (λ (x : α), f x • g x)
source
@[protected]
noncomputable def finsupp.dom_lcongr {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {α₁ : Type u_1} {α₂ : Type u_3} (e : α₁ ≃ α₂) :
(α₁ →₀ M) ≃ₗ[R] α₂ →₀ M

An equivalence of domains induces a linear equivalence of finitely supported functions.

This is finsupp.dom_congr as a linear_equiv. See also linear_map.fun_congr_left for the case of arbitrary functions.

Equations
source
@[simp]
theorem finsupp.dom_lcongr_apply {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {α₁ : Type u_1} {α₂ : Type u_3} (e : α₁ ≃ α₂) (v : α₁ →₀ M) :
⇑(finsupp.dom_lcongr e) v = ⇑(finsupp.dom_congr e) v
source
@[simp]
theorem finsupp.dom_lcongr_refl {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] :
finsupp.dom_lcongr (equiv.refl α) = linear_equiv.refl R (α →₀ M)
source
theorem finsupp.dom_lcongr_trans {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {α₁ : Type u_1} {α₂ : Type u_3} {α₃ : Type u_4} (f : α₁ ≃ α₂) (f₂ : α₂ ≃ α₃) :
(finsupp.dom_lcongr f).trans (finsupp.dom_lcongr f₂) = finsupp.dom_lcongr (f.trans f₂)
source
@[simp]
theorem finsupp.dom_lcongr_symm {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {α₁ : Type u_1} {α₂ : Type u_3} (f : α₁ ≃ α₂) :
(finsupp.dom_lcongr f).symm = finsupp.dom_lcongr f.symm
source
@[simp]
theorem finsupp.dom_lcongr_single {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {α₁ : Type u_1} {α₂ : Type u_3} (e : α₁ ≃ α₂) (i : α₁) (m : M) :
⇑(finsupp.dom_lcongr e) (finsupp.single i m) = finsupp.single (⇑e i) m
source
noncomputable def finsupp.congr {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {α' : Type u_3} (s : set α) (t : set α') (e : ↥s ≃ ↥t) :
↥(finsupp.supported M R s) ≃ₗ[R] ↥(finsupp.supported M R t)

An equivalence of sets induces a linear equivalence of finsupps supported on those sets.

Equations
source
noncomputable def finsupp.map_range.linear_map {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (f : M →ₗ[R] N) :
(α →₀ M) →ₗ[R] α →₀ N

finsupp.map_range as a linear_map.

Equations
source
@[simp]
theorem finsupp.map_range.linear_map_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (f : M →ₗ[R] N) (g : α →₀ M) :
⇑(finsupp.map_range.linear_map f) g = finsupp.map_range ⇑f _ g
source
@[simp]
theorem finsupp.map_range.linear_map_id {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] :
finsupp.map_range.linear_map linear_map.id = linear_map.id
source
theorem finsupp.map_range.linear_map_comp {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] (f : N →ₗ[R] P) (f₂ : M →ₗ[R] N) :
finsupp.map_range.linear_map (f.comp f₂) = (finsupp.map_range.linear_map f).comp (finsupp.map_range.linear_map f₂)
source
@[simp]
theorem finsupp.map_range.linear_map_to_add_monoid_hom {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (f : M →ₗ[R] N) :
(finsupp.map_range.linear_map f).to_add_monoid_hom = finsupp.map_range.add_monoid_hom f.to_add_monoid_hom
source
noncomputable def finsupp.map_range.linear_equiv {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (e : M ≃ₗ[R] N) :
(α →₀ M) ≃ₗ[R] α →₀ N

finsupp.map_range as a linear_equiv.

Equations
source
@[simp]
theorem finsupp.map_range.linear_equiv_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (e : M ≃ₗ[R] N) (g : α →₀ M) :
⇑(finsupp.map_range.linear_equiv e) g = finsupp.map_range ⇑e _ g
source
@[simp]
theorem finsupp.map_range.linear_equiv_refl {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] :
finsupp.map_range.linear_equiv (linear_equiv.refl R M) = linear_equiv.refl R (α →₀ M)
source
theorem finsupp.map_range.linear_equiv_trans {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] (f : M ≃ₗ[R] N) (f₂ : N ≃ₗ[R] P) :
finsupp.map_range.linear_equiv (f.trans f₂) = (finsupp.map_range.linear_equiv f).trans (finsupp.map_range.linear_equiv f₂)
source
@[simp]
theorem finsupp.map_range.linear_equiv_symm {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (f : M ≃ₗ[R] N) :
(finsupp.map_range.linear_equiv f).symm = finsupp.map_range.linear_equiv f.symm
source
@[simp]
theorem finsupp.map_range.linear_equiv_to_add_equiv {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (f : M ≃ₗ[R] N) :
(finsupp.map_range.linear_equiv f).to_add_equiv = finsupp.map_range.add_equiv f.to_add_equiv
source
@[simp]
theorem finsupp.map_range.linear_equiv_to_linear_map {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (f : M ≃ₗ[R] N) :
(finsupp.map_range.linear_equiv f).to_linear_map = finsupp.map_range.linear_map f.to_linear_map
source
noncomputable def finsupp.lcongr {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] {ι : Type u_1} {κ : Type u_4} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) :
(ι →₀ M) ≃ₗ[R] κ →₀ N

An equivalence of domain and a linear equivalence of codomain induce a linear equivalence of the corresponding finitely supported functions.

Equations
source
@[simp]
theorem finsupp.lcongr_single {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] {ι : Type u_1} {κ : Type u_4} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (i : ι) (m : M) :
⇑(finsupp.lcongr e₁ e₂) (finsupp.single i m) = finsupp.single (⇑e₁ i) (⇑e₂ m)
source
@[simp]
theorem finsupp.lcongr_apply_apply {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] {ι : Type u_1} {κ : Type u_4} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (f : ι →₀ M) (k : κ) :
⇑(⇑(finsupp.lcongr e₁ e₂) f) k = ⇑e₂ (⇑f (⇑(e₁.symm) k))
source
theorem finsupp.lcongr_symm_single {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] {ι : Type u_1} {κ : Type u_4} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (k : κ) (n : N) :
⇑((finsupp.lcongr e₁ e₂).symm) (finsupp.single k n) = finsupp.single (⇑(e₁.symm) k) (⇑(e₂.symm) n)
source
@[simp]
theorem finsupp.lcongr_symm {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] {ι : Type u_1} {κ : Type u_4} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) :
(finsupp.lcongr e₁ e₂).symm = finsupp.lcongr e₁.symm e₂.symm
source
noncomputable def finsupp.sum_finsupp_lequiv_prod_finsupp {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α : Type u_1} {β : Type u_3} :
(α ⊕ β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M)

The linear equivalence between (α ⊕ β) →₀ M and (α →₀ M) × (β →₀ M).

This is the linear_equiv version of finsupp.sum_finsupp_equiv_prod_finsupp.

Equations
source
@[simp]
theorem finsupp.sum_finsupp_lequiv_prod_finsupp_apply {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α : Type u_1} {β : Type u_3} (ᾰ : α ⊕ β →₀ M) :
⇑(finsupp.sum_finsupp_lequiv_prod_finsupp R) ᾰ = finsupp.sum_finsupp_add_equiv_prod_finsupp.to_fun ᾰ
source
@[simp]
theorem finsupp.sum_finsupp_lequiv_prod_finsupp_symm_apply {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α : Type u_1} {β : Type u_3} (ᾰ : (α →₀ M) × (β →₀ M)) :
⇑((finsupp.sum_finsupp_lequiv_prod_finsupp R).symm) ᾰ = finsupp.sum_finsupp_add_equiv_prod_finsupp.inv_fun ᾰ
source
theorem finsupp.fst_sum_finsupp_lequiv_prod_finsupp {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α : Type u_1} {β : Type u_3} (f : α ⊕ β →₀ M) (x : α) :
⇑((⇑(finsupp.sum_finsupp_lequiv_prod_finsupp R) f).fst) x = ⇑f (sum.inl x)
source
theorem finsupp.snd_sum_finsupp_lequiv_prod_finsupp {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α : Type u_1} {β : Type u_3} (f : α ⊕ β →₀ M) (y : β) :
⇑((⇑(finsupp.sum_finsupp_lequiv_prod_finsupp R) f).snd) y = ⇑f (sum.inr y)
source
theorem finsupp.sum_finsupp_lequiv_prod_finsupp_symm_inl {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α : Type u_1} {β : Type u_3} (fg : (α →₀ M) × (β →₀ M)) (x : α) :
⇑(⇑((finsupp.sum_finsupp_lequiv_prod_finsupp R).symm) fg) (sum.inl x) = ⇑(fg.fst) x
source
theorem finsupp.sum_finsupp_lequiv_prod_finsupp_symm_inr {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [module R M] {α : Type u_1} {β : Type u_3} (fg : (α →₀ M) × (β →₀ M)) (y : β) :
⇑(⇑((finsupp.sum_finsupp_lequiv_prod_finsupp R).symm) fg) (sum.inr y) = ⇑(fg.snd) y
source
noncomputable def finsupp.sigma_finsupp_lequiv_pi_finsupp (R : Type u_5) [semiring R] {η : Type u_7} [fintype η] {M : Type u_1} {ιs : η → Type u_2} [add_comm_monoid M] [module R M] :
((Σ (j : η), ιs j) →₀ M) ≃ₗ[R] Π (j : η), ιs j →₀ M

On a fintype η, finsupp.split is a linear equivalence between (Σ (j : η), ιs j) →₀ M and Π j, (ιs j →₀ M).

This is the linear_equiv version of finsupp.sigma_finsupp_add_equiv_pi_finsupp.

Equations
source
@[simp]
theorem finsupp.sigma_finsupp_lequiv_pi_finsupp_apply (R : Type u_5) [semiring R] {η : Type u_7} [fintype η] {M : Type u_1} {ιs : η → Type u_2} [add_comm_monoid M] [module R M] (f : (Σ (j : η), ιs j) →₀ M) (j : η) (i : ιs j) :
⇑(⇑(finsupp.sigma_finsupp_lequiv_pi_finsupp R) f j) i = ⇑f ⟨j, i⟩
source
@[simp]
theorem finsupp.sigma_finsupp_lequiv_pi_finsupp_symm_apply (R : Type u_5) [semiring R] {η : Type u_7} [fintype η] {M : Type u_1} {ιs : η → Type u_2} [add_comm_monoid M] [module R M] (f : Π (j : η), ιs j →₀ M) (ji : Σ (j : η), ιs j) :
⇑(⇑((finsupp.sigma_finsupp_lequiv_pi_finsupp R).symm) f) ji = ⇑(f ji.fst) ji.snd
source
noncomputable def finsupp.finsupp_prod_lequiv {α : Type u_1} {β : Type u_2} (R : Type u_3) {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :
(α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M

The linear equivalence between α × β →₀ M and α →₀ β →₀ M.

This is the linear_equiv version of finsupp.finsupp_prod_equiv.

Equations
source
@[simp]
theorem finsupp.finsupp_prod_lequiv_apply {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (f : α × β →₀ M) (x : α) (y : β) :
⇑(⇑(⇑(finsupp.finsupp_prod_lequiv R) f) x) y = ⇑f (x, y)
source
@[simp]
theorem finsupp.finsupp_prod_lequiv_symm_apply {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (f : α →₀ β →₀ M) (xy : α × β) :
⇑(⇑((finsupp.finsupp_prod_lequiv R).symm) f) xy = ⇑(⇑f xy.fst) xy.snd
source
@[protected]
def fintype.total {α : Type u_1} {M : Type u_2} (R : Type u_3) [fintype α] [semiring R] [add_comm_monoid M] [module R M] (S : Type u_4) [semiring S] [module S M] [smul_comm_class R S M] :
(α → M) →ₗ[S] (α → R) →ₗ[R] M

fintype.total R S v f is the linear combination of vectors in v with weights in f. This variant of finsupp.total 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
source
theorem fintype.total_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [fintype α] [semiring R] [add_comm_monoid M] [module R M] {S : Type u_4} [semiring S] [module S M] [smul_comm_class R S M] (v : α → M) (f : α → R) :
⇑(⇑(fintype.total R S) v) f = finset.univ.sum (λ (i : α), f i • v i)
source
@[simp]
theorem fintype.total_apply_single {α : Type u_1} {M : Type u_2} (R : Type u_3) [fintype α] [semiring R] [add_comm_monoid M] [module R M] {S : Type u_4} [semiring S] [module S M] [smul_comm_class R S M] (v : α → M) (i : α) (r : R) :
⇑(⇑(fintype.total R S) v) (pi.single i r) = r • v i
source
theorem finsupp.total_eq_fintype_total_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [fintype α] [semiring R] [add_comm_monoid M] [module R M] (S : Type u_4) [semiring S] [module S M] [smul_comm_class R S M] (v : α → M) (x : α → R) :
⇑(finsupp.total α M R v) (⇑((finsupp.linear_equiv_fun_on_finite R R α).symm) x) = ⇑(⇑(fintype.total R S) v) x
source
theorem finsupp.total_eq_fintype_total {α : Type u_1} {M : Type u_2} (R : Type u_3) [fintype α] [semiring R] [add_comm_monoid M] [module R M] (S : Type u_4) [semiring S] [module S M] [smul_comm_class R S M] (v : α → M) :
(finsupp.total α M R v).comp (finsupp.linear_equiv_fun_on_finite R R α).symm.to_linear_map = ⇑(fintype.total R S) v
source
@[simp]
theorem fintype.range_total {α : Type u_1} {M : Type u_2} (R : Type u_3) [fintype α] [semiring R] [add_comm_monoid M] [module R M] {S : Type u_4} [semiring S] [module S M] [smul_comm_class R S M] (v : α → M) :
linear_map.range (⇑(fintype.total R S) v) = submodule.span R (set.range v)
source
theorem mem_span_range_iff_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [fintype α] [semiring R] [add_comm_monoid M] [module R M] {v : α → M} {x : M} :
x ∈ submodule.span R (set.range v) ↔ ∃ (c : α → R), finset.univ.sum (λ (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.

source
theorem top_le_span_range_iff_forall_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [fintype α] [semiring R] [add_comm_monoid M] [module R M] {v : α → M} :
⊤ ≤ submodule.span R (set.range v) ↔ ∀ (x : M), ∃ (c : α → R), finset.univ.sum (λ (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.

source
@[irreducible]
noncomputable def span.repr (R : Type u_1) {M : Type u_2} [semiring R] [add_comm_monoid 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, using the axiom of choice.

Equations
source
@[simp]
theorem span.finsupp_total_repr (R : Type u_1) {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {w : set M} (x : ↥(submodule.span R w)) :
⇑(finsupp.total ↥w M R coe) (span.repr R w x) = ↑x
source
@[protected]
theorem submodule.finsupp_sum_mem {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_3} {β : Type u_4} [has_zero β] (S : submodule R M) (f : ι →₀ β) (g : ι → β → M) (h : ∀ (c : ι), ⇑f c ≠ 0 → g c (⇑f c) ∈ S) :
f.sum g ∈ S
source
theorem linear_map.map_finsupp_total {R : Type u_1} {M : Type u_2} {N : Type u_3} [semiring R] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (f : M →ₗ[R] N) {ι : Type u_4} {g : ι → M} (l : ι →₀ R) :
⇑f (⇑(finsupp.total ι M R g) l) = ⇑(finsupp.total ι N R (⇑f ∘ g)) l
source
theorem submodule.exists_finset_of_mem_supr {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_3} (p : ι → submodule R M) {m : M} (hm : m ∈ ⨆ (i : ι), p i) :
∃ (s : finset ι), m ∈ ⨆ (i : ι) (H : i ∈ s), p i
source
theorem submodule.mem_supr_iff_exists_finset {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_3} {p : ι → submodule R M} {m : M} :
(m ∈ ⨆ (i : ι), p i) ↔ ∃ (s : finset ι), m ∈ ⨆ (i : ι) (H : i ∈ s), p i

submodule.exists_finset_of_mem_supr as an iff

source
theorem mem_span_finset {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {s : finset M} {x : M} :
x ∈ submodule.span R ↑s ↔ ∃ (f : M → R), s.sum (λ (i : M), f i • i) = x
source
theorem mem_span_set {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {m : M} {s : set M} :
m ∈ submodule.span R s ↔ ∃ (c : M →₀ R), ↑(c.support) ⊆ s ∧ c.sum (λ (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.

source
@[simp]
theorem module.subsingleton_equiv_symm_apply (R : Type u_1) (M : Type u_2) (ι : Type u_3) [semiring R] [subsingleton R] [add_comm_monoid M] [module R M] (f : ι →₀ R) :
⇑((module.subsingleton_equiv R M ι).symm) f = 0
source
@[simp]
theorem module.subsingleton_equiv_apply (R : Type u_1) (M : Type u_2) (ι : Type u_3) [semiring R] [subsingleton R] [add_comm_monoid M] [module R M] (m : M) :
⇑(module.subsingleton_equiv R M ι) m = 0
source
def module.subsingleton_equiv (R : Type u_1) (M : Type u_2) (ι : Type u_3) [semiring R] [subsingleton R] [add_comm_monoid M] [module R M] :
M ≃ₗ[R] ι →₀ R

If subsingleton R, then M ≃ₗ[R] ι →₀ R for any type ι.

Equations
source
noncomputable def linear_map.splitting_of_finsupp_surjective {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : function.surjective ⇑f) :
(α →₀ R) →ₗ[R] M

A surjective linear map to finitely supported functions has a splitting.

Equations
source
theorem linear_map.splitting_of_finsupp_surjective_splits {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : function.surjective ⇑f) :
f.comp (f.splitting_of_finsupp_surjective s) = linear_map.id
source
theorem linear_map.left_inverse_splitting_of_finsupp_surjective {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : function.surjective ⇑f) :
function.left_inverse ⇑f ⇑(f.splitting_of_finsupp_surjective s)
source
theorem linear_map.splitting_of_finsupp_surjective_injective {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : function.surjective ⇑f) :
function.injective ⇑(f.splitting_of_finsupp_surjective s)
source
noncomputable def linear_map.splitting_of_fun_on_fintype_surjective {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_4} [fintype α] (f : M →ₗ[R] α → R) (s : function.surjective ⇑f) :
(α → R) →ₗ[R] M

A surjective linear map to functions on a finite type has a splitting.

Equations
source
theorem linear_map.splitting_of_fun_on_fintype_surjective_splits {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_4} [fintype α] (f : M →ₗ[R] α → R) (s : function.surjective ⇑f) :
f.comp (f.splitting_of_fun_on_fintype_surjective s) = linear_map.id
source
theorem linear_map.left_inverse_splitting_of_fun_on_fintype_surjective {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_4} [fintype α] (f : M →ₗ[R] α → R) (s : function.surjective ⇑f) :
function.left_inverse ⇑f ⇑(f.splitting_of_fun_on_fintype_surjective s)
source
theorem linear_map.splitting_of_fun_on_fintype_surjective_injective {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {α : Type u_4} [fintype α] (f : M →ₗ[R] α → R) (s : function.surjective ⇑f) :
function.injective ⇑(f.splitting_of_fun_on_fintype_surjective s)