# mathlibdocumentation

linear_algebra.finsupp

# Properties of the module α →₀ M#

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:

• finsupp.lsingle a : M →ₗ[R] ι →₀ M: finsupp.single a as a linear map;

• finsupp.lapply a : (ι →₀ M) →ₗ[R] M: the map λ f, f a as a linear map;

• finsupp.lsubtype_domain (s : set α) : (α →₀ M) →ₗ[R] (s →₀ M): restriction to a subtype as a linear map;

• finsupp.restrict_dom: finsupp.filter as a linear map to finsupp.supported s;

• finsupp.lsum: finsupp.sum or finsupp.lift_add_hom as a linear_map;

• finsupp.total α M R (v : ι → M): sends l : ι → R to the linear combination of v i with coefficients l i;

• finsupp.total_on: a restricted version of finsupp.total with domain finsupp.supported R R s and codomain submodule.span R (v '' s);

• finsupp.supported_equiv_finsupp: a linear equivalence between the functions α →₀ M supported on s and the functions s →₀ M;

• finsupp.lmap_domain: a linear map version of finsupp.map_domain;

• finsupp.dom_lcongr: a linear_equiv version of finsupp.dom_congr;

• finsupp.congr: if the sets s and t are equivalent, then supported M R s is equivalent to supported M R t;

• finsupp.lcongr: a linear_equivalence between α →₀ M and β →₀ N constructed using e : α ≃ β and e' : M ≃ₗ[R] N.

## 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] [ 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] [ M] [ N] ⦃φ ψ : →₀ M) →ₗ[R] N⦄ (h : ∀ (a : α) (b : M), φ b) = ψ 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] [ M] [ N] ⦃φ ψ : →₀ M) →ₗ[R] N⦄ (h : ∀ (a : α), φ.comp = ψ.comp ) :
φ = ψ

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] [ M] (a : α) :
→₀ M) →ₗ[R] M

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

Equations
noncomputable def finsupp.lsubtype_domain {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring 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] [ M] (s : set α) (f : α →₀ M) :
= finsupp.subtype_domain (λ (x : α), x s) f
@[simp]
theorem finsupp.lsingle_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] (a : α) (b : M) :
b =
@[simp]
theorem finsupp.lapply_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] (a : α) (f : α →₀ M) :
f = f a
@[simp]
theorem finsupp.ker_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] (a : α) :
theorem finsupp.lsingle_range_le_ker_lapply {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] (s t : set α) (h : t) :
(⨆ (a : α) (H : a s), ⨅ (a : α) (H : a t),
theorem finsupp.infi_ker_lapply_le_bot {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] :
(⨅ (a : α),
theorem finsupp.supr_lsingle_range {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] :
(⨆ (a : α), =
theorem finsupp.disjoint_lsingle_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] (s t : set α) (hs : t) :
disjoint (⨆ (a : α) (H : a s), (⨆ (a : α) (H : a t),
theorem finsupp.span_single_image {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] (s : set M) (a : α) :
'' s) = s)
def finsupp.supported {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [ M] (s : set α) :
→₀ 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] [ M] {s : set α} (p : α →₀ M) :
p s (p.support) s
theorem finsupp.mem_supported' {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [ M] {s : set α} (p : α →₀ M) :
p s ∀ (x : α), x sp x = 0
theorem finsupp.mem_supported_support {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [ M] (p : α →₀ M) :
theorem finsupp.single_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [ M] {s : set α} {a : α} (b : M) (h : a s) :
s
theorem finsupp.supported_eq_span_single {α : Type u_1} (R : Type u_5) [semiring R] (s : set α) :
s = ((λ (i : α), 1) '' s)
noncomputable def finsupp.restrict_dom {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [ M] (s : set α) :
→₀ M) →ₗ[R] s)

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] [ M] (s : set α) (l : α →₀ M) :
( 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] [ M] (s : set α) :
theorem finsupp.range_restrict_dom {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] (s : set α) :
theorem finsupp.supported_mono {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] {s t : set α} (st : s t) :
s t
@[simp]
theorem finsupp.supported_empty {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] :
@[simp]
theorem finsupp.supported_univ {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] :
theorem finsupp.supported_Union {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] {δ : Type u_3} (s : δ → set α) :
(⋃ (i : δ), s i) = ⨆ (i : δ), (s i)
theorem finsupp.supported_union {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] (s t : set α) :
(s t) = s t
theorem finsupp.supported_Inter {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] {ι : Type u_3} (s : ι → set α) :
(⋂ (i : ι), s i) = ⨅ (i : ι), (s i)
theorem finsupp.supported_inter {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] (s t : set α) :
(s t) = s t
theorem finsupp.disjoint_supported_supported {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] {s t : set α} (h : t) :
disjoint s) t)
theorem finsupp.disjoint_supported_supported_iff {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] [nontrivial M] {s t : set α} :
disjoint s) t) t
noncomputable def finsupp.supported_equiv_finsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring 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] [ M] [ N] [ N] [ 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] [ M] [ N] [ N] [ 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] [ M] [ N] [ N] [ 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] [ M] [ N] [ N] [ N] (f : α → (M →ₗ[R] N)) (i : α) (m : M) :
((finsupp.lsum S) f) 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] [ M] [ N] [ N] [ N] (f : →₀ M) →ₗ[R] N) (x : α) :
((finsupp.lsum S).symm) f x = f.comp
noncomputable def finsupp.lift (M : Type u_2) (R : Type u_5) [semiring 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] [ M] (X : Type u_7) (f : (X →₀ R) →ₗ[R] M) (x : X) :
((finsupp.lift M R X).symm) f x = f 1)
@[simp]
theorem finsupp.lift_apply (M : Type u_2) (R : Type u_5) [semiring R] [ M] (X : Type u_7) (f : X → M) (g : X →₀ R) :
( R X) f) g = g.sum (λ (x : X) (r : R), r f x)
noncomputable def finsupp.lmap_domain {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring 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] [ M] {α' : Type u_7} (f : α → α') (l : α →₀ M) :
f) l =
@[simp]
theorem finsupp.lmap_domain_id {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [ M] :
theorem finsupp.lmap_domain_comp {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [ M] {α' : Type u_7} {α'' : Type u_8} (f : α → α') (g : α' → α'') :
(g f) = g).comp f)
theorem finsupp.supported_comap_lmap_domain {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [ M] {α' : Type u_7} (f : α → α') (s : set α') :
(f ⁻¹' s) s)
theorem finsupp.lmap_domain_supported {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [ M] {α' : Type u_7} [nonempty α] (f : α → α') (s : set α) :
submodule.map f) s) = (f '' s)
theorem finsupp.lmap_domain_disjoint_ker {α : Type u_1} (M : Type u_2) (R : Type u_5) [semiring R] [ M] {α' : Type u_7} (f : α → α') {s : set α} (H : ∀ (a : α), a s∀ (b : α), b sf a = f ba = b) :
@[protected]
noncomputable def finsupp.total (α : Type u_1) (M : Type u_2) (R : Type u_5) [semiring 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] [ M] {v : α → M} (l : α →₀ R) :
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] [ M] {v : α → M} {l : α →₀ R} {s : finset α} (hs : l s) :
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] [ M] {v : α → M} (c : R) (a : α) :
M R v) c) = c v a
theorem finsupp.apply_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [ M] {M' : Type u_8} [add_comm_monoid M'] [ M'] (f : M →ₗ[R] M') (v : α → M) (l : α →₀ R) :
f ( M R v) l) = M' R (f v)) l
theorem finsupp.total_unique {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [ M] [unique α] (l : α →₀ R) (v : α → M) :
M R v) l =
theorem finsupp.total_surjective {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring 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] [ M] {v : α → M} (h : function.surjective v) :
theorem finsupp.total_id_surjective (R : Type u_5) [semiring R] (M : Type u_1) [ M] :

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] [ M] {v : α → M} :
theorem finsupp.lmap_domain_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [ M] {α' : Type u_7} {M' : Type u_8} [add_comm_monoid M'] [ M'] {v : α → M} {v' : α' → M'} (f : α → α') (g : M →ₗ[R] M') (h : ∀ (i : α), g (v i) = v' (f i)) :
M' R v').comp f) = g.comp M R v)
@[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'] [ M'] {v' : α' → M'} (f : α α') (l : α →₀ R) :
M' R v') l) = 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'] [ M'] {v' : α' → M'} (f : α → α') (hf : function.injective f) (l : α →₀ R) :
M' R v') l) = 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'] [ M'] {v' : α' → M'} (f : α α') (l : α →₀ R) :
M' R v') = M' R (v' f)) l
theorem finsupp.span_eq_range_total {M : Type u_2} (R : Type u_5) [semiring 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] [ M] (s : set M) (x : M) :
x ∃ (l : s →₀ R), M R coe) l = x
theorem finsupp.span_image_eq_map_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [ M] {v : α → M} (s : set α) :
(v '' s) = submodule.map M R v) s)
theorem finsupp.mem_span_image_iff_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [ M] {v : α → M} {s : set α} {x : M} :
x (v '' s) ∃ (l : α →₀ R) (H : l s), M R v) l = x
theorem finsupp.total_option {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [ M] (v : → M) (f : →₀ R) :
(finsupp.total (option α) M R v) f = + M R (v option.some)) f.some
theorem finsupp.total_total {M : Type u_2} (R : Type u_5) [semiring R] [ M] {α : Type u_1} {β : Type u_3} (A : α → M) (B : β → α →₀ R) (f : β →₀ R) :
M R A) ( →₀ R) R B) f) = M R (λ (b : β), M R A) (B b))) f
@[simp]
theorem finsupp.total_fin_zero {M : Type u_2} (R : Type u_5) [semiring 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] [ M] (v : α → M) (s : set α) :
s) →ₗ[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
theorem finsupp.total_on_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [ M] {v : α → M} (s : set α) :
theorem finsupp.total_comp {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [ M] {α' : Type u_7} {v : α → M} (f : α' → α) :
M R (v f) = M R v).comp f)
theorem finsupp.total_comap_domain {α : Type u_1} {M : Type u_2} (R : Type u_5) [semiring R] [ M] {α' : Type u_7} {v : α → M} (f : α → α') (l : α' →₀ R) (hf : (f ⁻¹' (l.support))) :
M R v) 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] [ M] {s : finset α} {f : α → R} (g : α → M) (hf : ∀ (a : α), f a 0a s) :
M R g) hf) = s.sum (λ (x : α), f x g x)
@[protected]
noncomputable def finsupp.dom_lcongr {M : Type u_2} {R : Type u_5} [semiring 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] [ M] {α₁ : Type u_1} {α₂ : Type u_3} (e : α₁ α₂) (v : α₁ →₀ M) :
v = v
@[simp]
theorem finsupp.dom_lcongr_refl {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring R] [ M] :
= →₀ M)
theorem finsupp.dom_lcongr_trans {M : Type u_2} {R : Type u_5} [semiring 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] [ M] {α₁ : Type u_1} {α₂ : Type u_3} (f : α₁ α₂) :
@[simp]
theorem finsupp.dom_lcongr_single {M : Type u_2} {R : Type u_5} [semiring R] [ M] {α₁ : Type u_1} {α₂ : Type u_3} (e : α₁ α₂) (i : α₁) (m : M) :
m) = finsupp.single (e i) m
noncomputable def finsupp.congr {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring 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] [ M] [ 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] [ M] [ N] (f : M →ₗ[R] N) (g : α →₀ M) :
= g
@[simp]
theorem finsupp.map_range.linear_map_id {α : Type u_1} {M : Type u_2} {R : Type u_5} [semiring 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] [ M] [ N] [ P] (f : N →ₗ[R] P) (f₂ : M →ₗ[R] N) :
@[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] [ M] [ N] (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] [ M] [ 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] [ M] [ 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] [ 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] [ M] [ N] [ 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] [ M] [ N] (f : M ≃ₗ[R] N) :
@[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] [ M] [ N] (f : M ≃ₗ[R] N) :
@[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] [ M] [ N] (f : M ≃ₗ[R] N) :
noncomputable def finsupp.lcongr {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [ M] [ 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
• e₂ =
@[simp]
theorem finsupp.lcongr_single {M : Type u_2} {N : Type u_3} {R : Type u_5} [semiring R] [ M] [ N] {ι : Type u_1} {κ : Type u_4} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) (i : ι) (m : M) :
e₂) 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] [ M] [ N] {ι : Type u_1} {κ : Type u_4} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) (f : ι →₀ M) (k : κ) :
( 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] [ M] [ N] {ι : Type u_1} {κ : Type u_4} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) (k : κ) (n : N) :
((finsupp.lcongr e₁ e₂).symm) 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] [ M] [ N] {ι : Type u_1} {κ : Type u_4} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) :
e₂).symm = e₂.symm
noncomputable def finsupp.sum_finsupp_lequiv_prod_finsupp {M : Type u_2} (R : Type u_5) [semiring 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] [ 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] [ 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] [ M] {α : Type u_1} {β : Type u_3} (f : α β →₀ M) (x : α) :
.fst) x = f (sum.inl x)
theorem finsupp.snd_sum_finsupp_lequiv_prod_finsupp {M : Type u_2} (R : Type u_5) [semiring R] [ M] {α : Type u_1} {β : Type u_3} (f : α β →₀ M) (y : β) :
.snd) y = f (sum.inr y)
theorem finsupp.sum_finsupp_lequiv_prod_finsupp_symm_inl {M : Type u_2} (R : Type u_5) [semiring R] [ M] {α : Type u_1} {β : Type u_3} (fg : →₀ M) × →₀ M)) (x : α) :
fg) (sum.inl x) = (fg.fst) x
theorem finsupp.sum_finsupp_lequiv_prod_finsupp_symm_inr {M : Type u_2} (R : Type u_5) [semiring R] [ M] {α : Type u_1} {β : Type u_3} (fg : →₀ M) × →₀ M)) (y : β) :
fg) (sum.inr y) = (fg.snd) 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} [ 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} [ M] (f : (Σ (j : η), ιs j) →₀ M) (j : η) (i : ιs j) :
i = f j, i⟩
@[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} [ M] (f : Π (j : η), ιs j →₀ M) (ji : Σ (j : η), ιs j) :
ji = (f ji.fst) ji.snd
noncomputable def finsupp.finsupp_prod_lequiv {α : Type u_1} {β : Type u_2} (R : Type u_3) {M : Type u_4} [semiring 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] [ M] (f : α × β →₀ M) (x : α) (y : β) :
( f) x) y = f (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] [ M] (f : α →₀ β →₀ M) (xy : α × β) :
( f) xy = (f xy.fst) xy.snd
@[irreducible]
noncomputable def span.repr (R : Type u_1) {M : Type u_2} [semiring R] [ M] (w : set M) (x : 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] [ M] {w : set M} (x : w)) :
M R coe) w x) = x
@[protected]
theorem submodule.finsupp_sum_mem {R : Type u_1} {M : Type u_2} [semiring R] [ M] {ι : Type u_3} {β : Type u_4} [has_zero β] (S : M) (f : ι →₀ β) (g : ι → β → M) (h : ∀ (c : ι), f c 0g 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] [ M] [ N] (f : M →ₗ[R] N) {ι : Type u_4} {g : ι → M} (l : ι →₀ R) :
f ( M R g) l) = N R (f g)) l
theorem submodule.exists_finset_of_mem_supr {R : Type u_1} {M : Type u_2} [semiring R] [ M] {ι : Type u_3} (p : ι → 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] [ M] {ι : Type u_3} {p : ι → 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] [ M] {s : finset M} {x : M} :
x ∃ (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] [ M] {m : M} {s : set M} :
m ∃ (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] [ M] (f : ι →₀ R) :
ι).symm) f = 0
@[simp]
theorem module.subsingleton_equiv_apply (R : Type u_1) (M : Type u_2) (ι : Type u_3) [semiring R] [subsingleton R] [ M] (m : M) :
ι) m = 0
def module.subsingleton_equiv (R : Type u_1) (M : Type u_2) (ι : Type u_3) [semiring R] [subsingleton 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] [ 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
theorem linear_map.splitting_of_finsupp_surjective_splits {R : Type u_1} {M : Type u_2} [semiring R] [ M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : function.surjective f) :
theorem linear_map.left_inverse_splitting_of_finsupp_surjective {R : Type u_1} {M : Type u_2} [semiring R] [ M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : function.surjective f) :
theorem linear_map.splitting_of_finsupp_surjective_injective {R : Type u_1} {M : Type u_2} [semiring R] [ M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : function.surjective f) :
noncomputable def linear_map.splitting_of_fun_on_fintype_surjective {R : Type u_1} {M : Type u_2} [semiring 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
theorem linear_map.splitting_of_fun_on_fintype_surjective_splits {R : Type u_1} {M : Type u_2} [semiring R] [ M] {α : Type u_4} [fintype α] (f : M →ₗ[R] α → R) (s : function.surjective f) :
theorem linear_map.left_inverse_splitting_of_fun_on_fintype_surjective {R : Type u_1} {M : Type u_2} [semiring R] [ M] {α : Type u_4} [fintype α] (f : M →ₗ[R] α → R) (s : function.surjective f) :
theorem linear_map.splitting_of_fun_on_fintype_surjective_injective {R : Type u_1} {M : Type u_2} [semiring R] [ M] {α : Type u_4} [fintype α] (f : M →ₗ[R] α → R) (s : function.surjective f) :