mathlib documentation

linear_algebra.finsupp

Properties of the semimodule α →₀ M #

Given an R-semimodule M, the R-semimodule 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, semimodule, linear algebra

def finsupp.lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule R M] [add_comm_monoid N] [semimodule 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] [semimodule R M] [add_comm_monoid N] [semimodule 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).

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

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

Equations
def finsupp.lsubtype_domain {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule R M] (s t : set α) (h : disjoint s t) :
(⨆ (a : α) (H : a s), (finsupp.lsingle a).range) ⨅ (a : α) (H : a t), (finsupp.lapply a).ker
theorem finsupp.infi_ker_lapply_le_bot {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] :
(⨅ (a : α), (finsupp.lapply a).ker)
theorem finsupp.supr_lsingle_range {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] :
(⨆ (a : α), (finsupp.lsingle a).range) =
theorem finsupp.disjoint_lsingle_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] (s t : set α) (hs : disjoint s t) :
disjoint (⨆ (a : α) (H : a s), (finsupp.lsingle a).range) (⨆ (a : α) (H : a t), (finsupp.lsingle a).range)
theorem finsupp.span_single_image {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule R M] {s : set α} (p : α →₀ M) :
p finsupp.supported M R s ∀ (x : α), x sp x = 0
theorem finsupp.single_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule 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)
def finsupp.restrict_dom {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule R M] :
@[simp]
theorem finsupp.supported_univ {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] :
theorem finsupp.supported_Union {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule R M] [nontrivial M] {s t : set α} :
def finsupp.supported_equiv_finsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] (s : set α) :

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

Equations
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] [semimodule R M] [add_comm_monoid N] [semimodule R N] [semimodule 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] [semimodule R M] [add_comm_monoid N] [semimodule R N] [semimodule 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] [semimodule R M] [add_comm_monoid N] [semimodule R N] [semimodule 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] [semimodule R M] [add_comm_monoid N] [semimodule R N] [semimodule 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] [semimodule R M] [add_comm_monoid N] [semimodule R N] [semimodule S N] [smul_comm_class R S N] (f : →₀ M) →ₗ[R] N) (x : α) :
def finsupp.lift (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule 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] [semimodule 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)
def finsupp.lmap_domain {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule 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] [semimodule R M] :
theorem finsupp.lmap_domain_comp {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule R M] {α' : Type u_7} (f : α → α') {s : set α} (H : ∀ (a b : α), a sb sf a = f ba = b) :
def finsupp.total (α : Type u_1) (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule 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] [semimodule R M] {v : α → M} {l : α →₀ R} {s : finset α} (hs : l finsupp.supported R R s) :
(finsupp.total α M R v) l = ∑ (i : α) in s, 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] [semimodule R M] {v : α → M} (c : R) (a : α) :
(finsupp.total α M R v) (finsupp.single a c) = c v a
theorem finsupp.total_unique {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule R M] [unique α] (l : α →₀ R) (v : α → M) :
(finsupp.total α M R v) l = l (default α) v (default α)
theorem finsupp.total_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule R M] {v : α → M} (h : function.surjective v) :
theorem finsupp.range_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule R M] {α' : Type u_7} {M' : Type u_8} [add_comm_monoid M'] [semimodule 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_emb_domain {α : Type u_1} (R : Type u_5) [semiring R] {α' : Type u_7} {M' : Type u_8} [add_comm_monoid M'] [semimodule R M'] {v' : α' → M'} (f : α α') (l : α →₀ R) :
(finsupp.total α' M' R v') (finsupp.emb_domain f l) = (finsupp.total α M' R (v' f)) l
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'] [semimodule R M'] {v' : α' → M'} (f : α → α') (hf : function.injective f) (l : α →₀ R) :
(finsupp.total α' M' R v') (finsupp.map_domain f l) = (finsupp.total α M' R (v' f)) l
theorem finsupp.span_eq_map_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule R M] {v : α → M} (s : set α) :
theorem finsupp.mem_span_iff_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule 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
def finsupp.total_on (α : Type u_1) (M : Type u_2) (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule 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) = ∑ (i : α) in l.support.preimage f hf, 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] [semimodule R M] {s : finset α} {f : α → R} (g : α → M) (hf : ∀ (a : α), f a 0a s) :
(finsupp.total α M R g) (finsupp.on_finset s f hf) = ∑ (x : α) in s, f x g x
def finsupp.dom_lcongr {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule 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.

Equations
@[simp]
theorem finsupp.dom_lcongr_refl {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] :
theorem finsupp.dom_lcongr_trans {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule 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] [semimodule R M] {α₁ : Type u_1} {α₂ : Type u_3} (e : α₁ α₂) (i : α₁) (m : M) :
def finsupp.congr {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule 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
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] [semimodule R M] [add_comm_monoid N] [semimodule 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] [semimodule R M] [add_comm_monoid N] [semimodule R N] (f : M →ₗ[R] N) (g : α →₀ M) :
@[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] [semimodule R 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] [semimodule R M] [add_comm_monoid N] [semimodule R N] [add_comm_monoid P] [semimodule R P] (f : N →ₗ[R] P) (f₂ : M →ₗ[R] N) :
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] [semimodule R M] [add_comm_monoid N] [semimodule 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] [semimodule R M] [add_comm_monoid N] [semimodule R N] (e : M ≃ₗ[R] N) (g : α →₀ M) :
@[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] [semimodule R M] :
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] [semimodule R M] [add_comm_monoid N] [semimodule R N] [add_comm_monoid P] [semimodule R P] (f : M ≃ₗ[R] N) (f₂ : N ≃ₗ[R] P) :
@[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] [semimodule R M] [add_comm_monoid N] [semimodule R N] (f : M ≃ₗ[R] N) :
def finsupp.lcongr {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule 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] [semimodule R M] [add_comm_monoid N] [semimodule 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] [semimodule R M] [add_comm_monoid N] [semimodule 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] [semimodule R M] [add_comm_monoid N] [semimodule 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] [semimodule R M] [add_comm_monoid N] [semimodule R N] {ι : Type u_1} {κ : Type u_4} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) :
def finsupp.sum_finsupp_lequiv_prod_finsupp {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule 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
@[simp]
theorem finsupp.sum_finsupp_lequiv_prod_finsupp_apply {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule R M] {α : Type u_1} {β : Type u_3} (ᾰ : α β →₀ M) :
@[simp]
theorem finsupp.sum_finsupp_lequiv_prod_finsupp_symm_apply {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule R M] {α : Type u_1} {β : Type u_3} (ᾰ : →₀ M) × →₀ M)) :
theorem finsupp.fst_sum_finsupp_lequiv_prod_finsupp {M : Type u_2} (R : Type u_5) [semiring R] [add_comm_monoid M] [semimodule 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] [semimodule 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] [semimodule 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] [semimodule R M] {α : Type u_1} {β : Type u_3} (fg : →₀ M) × →₀ M)) (y : β) :
theorem linear_map.map_finsupp_total {R : Type u_1} {M : Type u_2} {N : Type u_3} [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule 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] [semimodule 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 mem_span_finset {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {s : finset M} {x : M} :
x submodule.span R s ∃ (f : M → R), ∑ (i : M) in s, f i i = x
theorem mem_span_set {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule 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.