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

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 : α) :

Interpret finsupp.single a as a linear map.

Equations
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.

@[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).

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
@[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) (ᾰ : α) :
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
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 α) :

Interpret finsupp.subtype_domain s as a linear map.

Equations
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) :
@[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) :
@[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) :
@[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 : α) :
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)
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] :
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] :
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))
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 : α) :
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
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) :
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
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) :
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) :
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)
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 α) :

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

Equations
@[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
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 α) :
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 α) :
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) :
@[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] :
@[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] :
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)
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 α) :
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)
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 α) :
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) :
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 α} :
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 α) :

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

Equations
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
@[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))
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))
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
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 : α) :
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
@[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)
@[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)
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
@[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
@[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)
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
@[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) :
@[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] :
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 : α' α'') :
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 α') :
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 α) :
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) :
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
@[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
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)
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)
@[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
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
@[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
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
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) :
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) :
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) :

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.

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} :
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)
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)
@[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
@[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
@[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
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) :

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

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) :
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
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 α) :
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
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) :
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
@[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
@[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.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
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 α) :
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)
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)
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)
@[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
@[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) :
@[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] :
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₂ : α₂ α₃) :
@[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 : α₁ α₂) :
@[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) :
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) :

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

Equations
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
@[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) :
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) :
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
@[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) :
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
@[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)
@[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))
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)
@[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) :
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
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 : α) :
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 : β) :
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 : α) :
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 : β) :
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
@[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) :
@[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) :
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
@[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 : β) :
@[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 : α × β) :
@[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
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)
@[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
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) :
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) :
@[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) :
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.

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.

@[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)) :

Pick some representation of x : span R w as a linear combination in w, using the axiom of choice.

Equations
@[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)) :
@[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
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
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
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

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
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.

@[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) :
@[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) :
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] :

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

Equations
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
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