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 LinearMap 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 fun f ↦ f a as a linear map;
• Finsupp.lsubtypeDomain (s : Set α) : (α →₀ M) →ₗ[R] (s →₀ M): restriction to a subtype as a linear map;
• Finsupp.restrictDom: Finsupp.filter as a linear map to Finsupp.supported s;
• Finsupp.lsum: Finsupp.sum or Finsupp.liftAddHom as a LinearMap;
• Finsupp.total α M R (v : ι → M): sends l : ι → R to the linear combination of v i with coefficients l i;
• Finsupp.totalOn: a restricted version of Finsupp.total with domain Finsupp.supported R R s and codomain Submodule.span R (v '' s);
• Finsupp.supportedEquivFinsupp: a linear equivalence between the functions α →₀ M supported on s and the functions s →₀ M;
• Finsupp.lmapDomain: a linear map version of Finsupp.mapDomain;
• Finsupp.domLCongr: a LinearEquiv version of Finsupp.domCongr;
• 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 LinearEquivalence between α →₀ M and β →₀ N constructed using e : α ≃ β and e' : M ≃ₗ[R] N.

Tags #

function with finite support, module, linear algebra

theorem Finsupp.smul_sum {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_4} [Zero β] [] [] {v : α →₀ β} {c : R} {h : αβM} :
c v.sum h = v.sum fun (a : α) (b : β) => c h a b
@[simp]
theorem Finsupp.sum_smul_index_linearMap' {α : Type u_1} {R : Type u_3} {M : Type u_4} {M₂ : Type u_5} [] [] [Module R M] [] [Module R M₂] {v : α →₀ M} {c : R} {h : αM →ₗ[R] M₂} :
((c v).sum fun (a : α) => (h a)) = c v.sum fun (a : α) => (h a)
@[simp]
theorem Finsupp.linearEquivFunOnFinite_apply (R : Type u_1) (M : Type u_3) (α : Type u_4) [] [] [] [Module R M] :
∀ (a : α →₀ M) (a_1 : α), () a a_1 = a a_1
noncomputable def Finsupp.linearEquivFunOnFinite (R : Type u_1) (M : Type u_3) (α : Type u_4) [] [] [] [Module R M] :
(α →₀ M) ≃ₗ[R] αM

Given Finite α, linearEquivFunOnFinite R is the natural R-linear equivalence between α →₀ β and α → β.

Equations
• = let __src := Finsupp.equivFunOnFinite; { toFun := DFunLike.coe, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem Finsupp.linearEquivFunOnFinite_single (R : Type u_1) (M : Type u_3) (α : Type u_4) [] [] [] [Module R M] [] (x : α) (m : M) :
() () =
@[simp]
theorem Finsupp.linearEquivFunOnFinite_symm_single (R : Type u_1) (M : Type u_3) (α : Type u_4) [] [] [] [Module R M] [] (x : α) (m : M) :
().symm () =
@[simp]
theorem Finsupp.linearEquivFunOnFinite_symm_coe (R : Type u_1) (M : Type u_3) (α : Type u_4) [] [] [] [Module R M] (f : α →₀ M) :
().symm f = f
noncomputable def Finsupp.LinearEquiv.finsuppUnique (R : Type u_1) (M : Type u_3) [] [] [Module R M] (α : Type u_4) [] :
(α →₀ M) ≃ₗ[R] M

If α has a unique term, then the type of finitely supported functions α →₀ M is R-linearly equivalent to M.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Finsupp.LinearEquiv.finsuppUnique_apply {R : Type u_1} {M : Type u_3} [] [] [Module R M] (α : Type u_4) [] (f : α →₀ M) :
f = f default
@[simp]
theorem Finsupp.LinearEquiv.finsuppUnique_symm_apply {R : Type u_1} {M : Type u_3} [] [] [Module R M] {α : Type u_4} [] (m : M) :
.symm m = Finsupp.single default m
def Finsupp.lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (a : α) :

Interpret Finsupp.single a as a linear map.

Equations
• = let __src := ; { toFun := (__src).toFun, map_add' := , map_smul' := }
Instances For
theorem Finsupp.lhom_ext {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] ⦃φ : (α →₀ M) →ₗ[R] N ⦃ψ : (α →₀ M) →ₗ[R] N (h : ∀ (a : α) (b : M), φ () = ψ ()) :
φ = ψ

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

theorem Finsupp.lhom_ext' {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] ⦃φ : (α →₀ M) →ₗ[R] N ⦃ψ : (α →₀ M) →ₗ[R] N (h : ∀ (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} [] [] [Module R M] (a : α) :
(α →₀ M) →ₗ[R] M

Interpret fun f : α →₀ M ↦ f a as a linear map.

Equations
• = let __src := ; { toFun := (__src).toFun, map_add' := , map_smul' := }
Instances For
instance LinearMap.CompatibleSMul.finsupp_dom (R : Type u_7) (S : Type u_8) (M : Type u_9) (N : Type u_10) (ι : Type u_11) [] [] [] [Module S M] [Module S N] [] [] [] :
Equations
• =
instance LinearMap.CompatibleSMul.finsupp_cod (R : Type u_7) (S : Type u_8) (M : Type u_9) (N : Type u_10) (ι : Type u_11) [] [] [] [Module S M] [Module S N] [SMul R M] [] [] :
Equations
• =
@[simp]
theorem Finsupp.lcoeFun_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] :
∀ (a : α →₀ M) (a_1 : α), Finsupp.lcoeFun a a_1 = a a_1
def Finsupp.lcoeFun {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] :
(α →₀ M) →ₗ[R] αM

Forget that a function is finitely supported.

This is the linear version of Finsupp.toFun.

Equations
• Finsupp.lcoeFun = { toFun := DFunLike.coe, map_add' := , map_smul' := }
Instances For
def Finsupp.lsubtypeDomain {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (s : Set α) :
(α →₀ M) →ₗ[R] s →₀ M

Interpret Finsupp.subtypeDomain s as a linear map.

Equations
Instances For
theorem Finsupp.lsubtypeDomain_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (s : Set α) (f : α →₀ M) :
= Finsupp.subtypeDomain (fun (x : α) => x s) f
@[simp]
theorem Finsupp.lsingle_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (a : α) (b : M) :
() b =
@[simp]
theorem Finsupp.lapply_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (a : α) (f : α →₀ M) :
() f = f a
@[simp]
theorem Finsupp.lapply_comp_lsingle_same {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (a : α) :
= LinearMap.id
@[simp]
theorem Finsupp.lapply_comp_lsingle_of_ne {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (a : α) (a' : α) (h : a a') :
= 0
@[simp]
theorem Finsupp.ker_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (a : α) :
theorem Finsupp.lsingle_range_le_ker_lapply {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (s : Set α) (t : Set α) (h : Disjoint s t) :
as, at,
theorem Finsupp.iInf_ker_lapply_le_bot {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] :
⨅ (a : α),
theorem Finsupp.iSup_lsingle_range {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] :
⨆ (a : α), =
theorem Finsupp.disjoint_lsingle_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (s : Set α) (t : Set α) (hs : Disjoint s t) :
Disjoint (as, ) (at, )
theorem Finsupp.span_single_image {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (s : Set M) (a : α) :
def Finsupp.supported {α : Type u_1} (M : Type u_2) (R : Type u_5) [] [] [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
• = { carrier := {p : α →₀ M | p.support s}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
theorem Finsupp.mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {s : Set α} (p : α →₀ M) :
p p.support s
theorem Finsupp.mem_supported' {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {s : Set α} (p : α →₀ M) :
p xs, p x = 0
theorem Finsupp.mem_supported_support {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] (p : α →₀ M) :
p Finsupp.supported M R p.support
theorem Finsupp.single_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {s : Set α} {a : α} (b : M) (h : a s) :
theorem Finsupp.supported_eq_span_single {α : Type u_1} (R : Type u_5) [] (s : Set α) :
= Submodule.span R ((fun (i : α) => ) '' s)
def Finsupp.restrictDom {α : Type u_1} (M : Type u_2) (R : Type u_5) [] [] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x s] :
(α →₀ M) →ₗ[R] ()

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

Equations
Instances For
@[simp]
theorem Finsupp.restrictDom_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (s : Set α) (l : α →₀ M) [DecidablePred fun (x : α) => x s] :
(() l) = Finsupp.filter (fun (x : α) => x s) l
theorem Finsupp.restrictDom_comp_subtype {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x s] :
∘ₗ ().subtype = LinearMap.id
theorem Finsupp.range_restrictDom {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x s] :
theorem Finsupp.supported_mono {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] {s : Set α} {t : Set α} (st : s t) :
@[simp]
theorem Finsupp.supported_empty {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] :
@[simp]
theorem Finsupp.supported_univ {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] :
Finsupp.supported M R Set.univ =
theorem Finsupp.supported_iUnion {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] {δ : Type u_7} (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} [] [] [Module R M] (s : Set α) (t : Set α) :
theorem Finsupp.supported_iInter {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] {ι : Type u_7} (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} [] [] [Module R M] (s : Set α) (t : Set α) :
theorem Finsupp.disjoint_supported_supported {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] {s : Set α} {t : Set α} (h : Disjoint s t) :
Disjoint () ()
theorem Finsupp.disjoint_supported_supported_iff {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] [] {s : Set α} {t : Set α} :
def Finsupp.supportedEquivFinsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] (s : Set α) :
() ≃ₗ[R] s →₀ M

Interpret Finsupp.restrictSupportEquiv as a linear equivalence between supported M R s and s →₀ M.

Equations
• = let F := ; F.toLinearEquiv
Instances For
def Finsupp.lsum {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [] [] [] [Module R M] [] [Module R N] [Module 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.liftAddHom.

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Finsupp.coe_lsum {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [] [] [] [Module R M] [] [Module R N] [Module S N] [] (f : αM →ₗ[R] N) :
(() f) = fun (d : α →₀ M) => d.sum fun (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) [] [] [] [Module R M] [] [Module R N] [Module S N] [] (f : αM →ₗ[R] N) (l : α →₀ M) :
(() f) l = l.sum fun (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) [] [] [] [Module R M] [] [Module R N] [Module S N] [] (f : αM →ₗ[R] N) (i : α) (m : M) :
(() f) () = (f i) m
@[simp]
theorem Finsupp.lsum_comp_lsingle {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [] [] [] [Module R M] [] [Module R N] [Module S N] [] (f : αM →ₗ[R] N) (i : α) :
() f ∘ₗ = f i
theorem Finsupp.lsum_symm_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [] [] [] [Module R M] [] [Module R N] [Module S N] [] (f : (α →₀ M) →ₗ[R] N) (x : α) :
().symm f x = f ∘ₗ
noncomputable def Finsupp.lift (M : Type u_2) (R : Type u_5) [] [] [Module R M] (X : Type u_7) :
(XM) ≃+ ((X →₀ R) →ₗ[R] M)

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

Equations
Instances For
@[simp]
theorem Finsupp.lift_symm_apply (M : Type u_2) (R : Type u_5) [] [] [Module R M] (X : Type u_7) (f : (X →₀ R) →ₗ[R] M) (x : X) :
(Finsupp.lift M R X).symm f x = f ()
@[simp]
theorem Finsupp.lift_apply (M : Type u_2) (R : Type u_5) [] [] [Module R M] (X : Type u_7) (f : XM) (g : X →₀ R) :
((Finsupp.lift M R X) f) g = g.sum fun (x : X) (r : R) => r f x
noncomputable def Finsupp.llift (M : Type u_2) (R : Type u_5) (S : Type u_6) [] [] [] [Module R M] (X : Type u_7) [Module S M] [] :
(XM) ≃ₗ[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
• Finsupp.llift M R S X = let __src := Finsupp.lift M R X; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem Finsupp.llift_apply (M : Type u_2) (R : Type u_5) (S : Type u_6) [] [] [] [Module R M] (X : Type u_7) [Module S M] [] (f : XM) (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) [] [] [] [Module R M] (X : Type u_7) [Module S M] [] (f : (X →₀ R) →ₗ[R] M) (x : X) :
(Finsupp.llift M R S X).symm f x = f ()
def Finsupp.lmapDomain {α : Type u_1} (M : Type u_2) (R : Type u_5) [] [] [Module R M] {α' : Type u_7} (f : αα') :
(α →₀ M) →ₗ[R] α' →₀ M

Interpret Finsupp.mapDomain as a linear map.

Equations
• = { toFun := , map_add' := , map_smul' := }
Instances For
@[simp]
theorem Finsupp.lmapDomain_apply {α : Type u_1} (M : Type u_2) (R : Type u_5) [] [] [Module R M] {α' : Type u_7} (f : αα') (l : α →₀ M) :
() l =
@[simp]
theorem Finsupp.lmapDomain_id {α : Type u_1} (M : Type u_2) (R : Type u_5) [] [] [Module R M] :
= LinearMap.id
theorem Finsupp.lmapDomain_comp {α : Type u_1} (M : Type u_2) (R : Type u_5) [] [] [Module R M] {α' : Type u_7} {α'' : Type u_8} (f : αα') (g : α'α'') :
Finsupp.lmapDomain M R (g f) = ∘ₗ
theorem Finsupp.supported_comap_lmapDomain {α : Type u_1} (M : Type u_2) (R : Type u_5) [] [] [Module R M] {α' : Type u_7} (f : αα') (s : Set α') :
theorem Finsupp.lmapDomain_supported {α : Type u_1} (M : Type u_2) (R : Type u_5) [] [] [Module R M] {α' : Type u_7} (f : αα') (s : Set α) :
theorem Finsupp.lmapDomain_disjoint_ker {α : Type u_1} (M : Type u_2) (R : Type u_5) [] [] [Module R M] {α' : Type u_7} (f : αα') {s : Set α} (H : as, bs, f a = f ba = b) :
def Finsupp.lcomapDomain {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] {β : Type u_7} (f : αβ) (hf : ) :
(β →₀ M) →ₗ[R] α →₀ M

Given f : α → β and a proof hf that f is injective, lcomapDomain 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.comapDomain.

Equations
• = { toFun := fun (l : β →₀ M) => , map_add' := , map_smul' := }
Instances For
def Finsupp.total (α : Type u_1) (M : Type u_2) (R : Type u_5) [] [] [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
Instances For
theorem Finsupp.total_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {v : αM} (l : α →₀ R) :
(Finsupp.total α M R v) l = l.sum fun (i : α) (a : R) => a v i
theorem Finsupp.total_apply_of_mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {v : αM} {l : α →₀ R} {s : } (hs : l ) :
(Finsupp.total α M R v) l = is, l i v i
@[simp]
theorem Finsupp.total_single {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {v : αM} (c : R) (a : α) :
(Finsupp.total α M R v) () = c v a
theorem Finsupp.total_zero_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [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) [] [] [Module R M] :
Finsupp.total α M R 0 = 0
theorem Finsupp.apply_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {M' : Type u_8} [] [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.apply_total_id {M : Type u_2} (R : Type u_5) [] [] [Module R M] {M' : Type u_8} [] [Module R M'] (f : M →ₗ[R] M') (l : M →₀ R) :
f ((Finsupp.total M M R id) l) = (Finsupp.total M M' R f) l
theorem Finsupp.total_unique {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] [] (l : α →₀ R) (v : αM) :
(Finsupp.total α M R v) l = l default v default
theorem Finsupp.total_surjective {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {v : αM} (h : ) :
theorem Finsupp.total_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {v : αM} (h : ) :
theorem Finsupp.total_id_surjective (R : Type u_5) [] (M : Type u_9) [] [Module R 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) [] [] [Module R M] {v : αM} :
theorem Finsupp.lmapDomain_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {α' : Type u_7} {M' : Type u_8} [] [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' ∘ₗ = g ∘ₗ Finsupp.total α M R v
theorem Finsupp.total_comp_lmapDomain {α : Type u_1} (R : Type u_5) [] {α' : Type u_7} {M' : Type u_8} [] [Module R M'] {v' : α'M'} (f : αα') :
Finsupp.total α' M' R v' ∘ₗ = Finsupp.total α M' R (v' f)
@[simp]
theorem Finsupp.total_embDomain {α : Type u_1} (R : Type u_5) [] {α' : Type u_7} {M' : Type u_8} [] [Module R M'] {v' : α'M'} (f : α α') (l : α →₀ R) :
(Finsupp.total α' M' R v') () = (Finsupp.total α M' R (v' f)) l
@[simp]
theorem Finsupp.total_mapDomain {α : Type u_1} (R : Type u_5) [] {α' : Type u_7} {M' : Type u_8} [] [Module R M'] {v' : α'M'} (f : αα') (l : α →₀ R) :
(Finsupp.total α' M' R v') () = (Finsupp.total α M' R (v' f)) l
@[simp]
theorem Finsupp.total_equivMapDomain {α : Type u_1} (R : Type u_5) [] {α' : Type u_7} {M' : Type u_8} [] [Module R M'] {v' : α'M'} (f : α α') (l : α →₀ R) :
(Finsupp.total α' M' R v') () = (Finsupp.total α M' R (v' f)) l
theorem Finsupp.span_eq_range_total {M : Type u_2} (R : Type u_5) [] [] [Module R M] (s : Set M) :
= LinearMap.range (Finsupp.total (s) M R Subtype.val)

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) [] [] [Module R M] (s : Set M) (x : M) :
x ∃ (l : s →₀ R), (Finsupp.total (s) M R Subtype.val) l = x
theorem Finsupp.mem_span_range_iff_exists_finsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] {v : αM} {x : M} :
x ∃ (c : α →₀ R), (c.sum fun (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) [] [] [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) [] [] [Module R M] {v : αM} {s : Set α} {x : M} :
x Submodule.span R (v '' s) l, (Finsupp.total α M R v) l = x
theorem Finsupp.total_option {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] (v : M) (f : →₀ R) :
(Finsupp.total () M R v) f = f none v none + (Finsupp.total α M R (v some)) f.some
theorem Finsupp.total_total {M : Type u_2} (R : Type u_5) [] [] [Module R M] {α : Type u_9} {β : Type u_10} (A : αM) (B : βα →₀ R) (f : β →₀ R) :
(Finsupp.total α M R A) ((Finsupp.total β (α →₀ R) R B) f) = (Finsupp.total β M R fun (b : β) => (Finsupp.total α M R A) (B b)) f
@[simp]
theorem Finsupp.total_fin_zero {M : Type u_2} (R : Type u_5) [] [] [Module R M] (f : Fin 0M) :
Finsupp.total (Fin 0) M R f = 0
def Finsupp.totalOn (α : Type u_1) (M : Type u_2) (R : Type u_5) [] [] [Module R M] (v : αM) (s : Set α) :
() →ₗ[R] (Submodule.span R (v '' s))

Finsupp.totalOn 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
Instances For
theorem Finsupp.totalOn_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {v : αM} (s : Set α) :
theorem Finsupp.total_comp {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {α' : Type u_7} {v : αM} (f : α'α) :
Finsupp.total α' M R (v f) = Finsupp.total α M R v ∘ₗ
theorem Finsupp.total_comapDomain {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {α' : Type u_7} {v : αM} (f : αα') (l : α' →₀ R) (hf : Set.InjOn f (f ⁻¹' l.support)) :
(Finsupp.total α M R v) () = il.support.preimage f hf, l (f i) v i
theorem Finsupp.total_onFinset {α : Type u_1} {M : Type u_2} (R : Type u_5) [] [] [Module R M] {s : } {f : αR} (g : αM) (hf : ∀ (a : α), f a 0a s) :
(Finsupp.total α M R g) (Finsupp.onFinset s f hf) = xs, f x g x
def Finsupp.domLCongr {M : Type u_2} {R : Type u_5} [] [] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} (e : α₁ α₂) :
(α₁ →₀ M) ≃ₗ[R] α₂ →₀ M

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

This is Finsupp.domCongr as a LinearEquiv. See also LinearMap.funCongrLeft for the case of arbitrary functions.

Equations
• = ().toLinearEquiv
Instances For
@[simp]
theorem Finsupp.domLCongr_apply {M : Type u_2} {R : Type u_5} [] [] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} (e : α₁ α₂) (v : α₁ →₀ M) :
v = () v
@[simp]
theorem Finsupp.domLCongr_refl {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] :
theorem Finsupp.domLCongr_trans {M : Type u_2} {R : Type u_5} [] [] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} {α₃ : Type u_9} (f : α₁ α₂) (f₂ : α₂ α₃) :
= Finsupp.domLCongr (f.trans f₂)
@[simp]
theorem Finsupp.domLCongr_symm {M : Type u_2} {R : Type u_5} [] [] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} (f : α₁ α₂) :
.symm = Finsupp.domLCongr f.symm
theorem Finsupp.domLCongr_single {M : Type u_2} {R : Type u_5} [] [] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} (e : α₁ α₂) (i : α₁) (m : M) :
() = Finsupp.single (e i) m
noncomputable def Finsupp.congr {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] {α' : Type u_7} (s : Set α) (t : Set α') (e : s t) :
() ≃ₗ[R] ()

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

Equations
• = ≪≫ₗ ( ≪≫ₗ .symm)
Instances For
def Finsupp.mapRange.linearMap {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] (f : M →ₗ[R] N) :
(α →₀ M) →ₗ[R] α →₀ N

Finsupp.mapRange as a LinearMap.

Equations
Instances For
@[simp]
theorem Finsupp.mapRange.linearMap_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] (f : M →ₗ[R] N) (g : α →₀ M) :
= Finsupp.mapRange f g
@[simp]
theorem Finsupp.mapRange.linearMap_id {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] :
Finsupp.mapRange.linearMap LinearMap.id = LinearMap.id
theorem Finsupp.mapRange.linearMap_comp {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {R : Type u_5} [] [] [Module R M] [] [Module R N] [] [Module R P] (f : N →ₗ[R] P) (f₂ : M →ₗ[R] N) :
@[simp]
theorem Finsupp.mapRange.linearMap_toAddMonoidHom {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] (f : M →ₗ[R] N) :
def Finsupp.mapRange.linearEquiv {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] (e : M ≃ₗ[R] N) :
(α →₀ M) ≃ₗ[R] α →₀ N

Finsupp.mapRange as a LinearEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Finsupp.mapRange.linearEquiv_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] (e : M ≃ₗ[R] N) (g : α →₀ M) :
@[simp]
theorem Finsupp.mapRange.linearEquiv_refl {α : Type u_1} {M : Type u_2} {R : Type u_5} [] [] [Module R M] :
theorem Finsupp.mapRange.linearEquiv_trans {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {R : Type u_5} [] [] [Module R M] [] [Module R N] [] [Module R P] (f : M ≃ₗ[R] N) (f₂ : N ≃ₗ[R] P) :
@[simp]
theorem Finsupp.mapRange.linearEquiv_symm {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] (f : M ≃ₗ[R] N) :
.symm =
@[simp]
theorem Finsupp.mapRange.linearEquiv_toAddEquiv {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] (f : M ≃ₗ[R] N) :
@[simp]
theorem Finsupp.mapRange.linearEquiv_toLinearMap {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] (f : M ≃ₗ[R] N) :
def Finsupp.lcongr {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] {ι : Type u_7} {κ : Type u_8} (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
Instances For
@[simp]
theorem Finsupp.lcongr_single {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] {ι : Type u_7} {κ : Type u_8} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) (i : ι) (m : M) :
(Finsupp.lcongr e₁ e₂) () = Finsupp.single (e₁ i) (e₂ m)
@[simp]
theorem Finsupp.lcongr_apply_apply {M : Type u_2} {N : Type u_3} {R : Type u_5} [] [] [Module R M] [] [Module R N] {ι : Type u_7} {κ : Type u_8} (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} [] [] [Module R M] [] [Module R N] {ι : Type u_7} {κ : Type u_8} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) (k : κ) (n : N) :
(Finsupp.lcongr e₁ e₂).symm () = 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} [] [] [Module R M] [] [Module R N] {ι : Type u_7} {κ : Type u_8} (e₁ : ι κ) (e₂ : M ≃ₗ[R] N) :
(Finsupp.lcongr e₁ e₂).symm = Finsupp.lcongr e₁.symm e₂.symm
@[simp]
theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_apply {M : Type u_2} (R : Type u_5) [] [] [Module R M] {α : Type u_7} {β : Type u_8} :
∀ (a : (α →₀ M) × (β →₀ M)), .symm a = Finsupp.sumFinsuppAddEquivProdFinsupp.invFun a
@[simp]
theorem Finsupp.sumFinsuppLEquivProdFinsupp_apply {M : Type u_2} (R : Type u_5) [] [] [Module R M] {α : Type u_7} {β : Type u_8} :
∀ (a : α β →₀ M), = Finsupp.sumFinsuppAddEquivProdFinsupp.toFun a
def Finsupp.sumFinsuppLEquivProdFinsupp {M : Type u_2} (R : Type u_5) [] [] [Module R M] {α : Type u_7} {β : Type u_8} :
(α β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M)

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

This is the LinearEquiv version of Finsupp.sumFinsuppEquivProdFinsupp.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Finsupp.fst_sumFinsuppLEquivProdFinsupp {M : Type u_2} (R : Type u_5) [] [] [Module R M] {α : Type u_7} {β : Type u_8} (f : α β →₀ M) (x : α) :
.1 x = f ()
theorem Finsupp.snd_sumFinsuppLEquivProdFinsupp {M : Type u_2} (R : Type u_5) [] [] [Module R M] {α : Type u_7} {β : Type u_8} (f : α β →₀ M) (y : β) :
.2 y = f ()
theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl {M : Type u_2} (R : Type u_5) [] [] [Module R M] {α : Type u_7} {β : Type u_8} (fg : (α →₀ M) × (β →₀ M)) (x : α) :
(.symm fg) () = fg.1 x
theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr {M : Type u_2} (R : Type u_5) [] [] [Module R M] {α : Type u_7} {β : Type u_8} (fg : (α →₀ M) × (β →₀ M)) (y : β) :
(.symm fg) () = fg.2 y
noncomputable def Finsupp.sigmaFinsuppLEquivPiFinsupp (R : Type u_5) [] {η : Type u_7} [] {M : Type u_9} {ιs : ηType u_10} [] [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 LinearEquiv version of Finsupp.sigmaFinsuppAddEquivPiFinsupp.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Finsupp.sigmaFinsuppLEquivPiFinsupp_apply (R : Type u_5) [] {η : Type u_7} [] {M : Type u_9} {ιs : ηType u_10} [] [Module R M] (f : (j : η) × ιs j →₀ M) (j : η) (i : ιs j) :
() i = f j, i
@[simp]
theorem Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply (R : Type u_5) [] {η : Type u_7} [] {M : Type u_9} {ιs : ηType u_10} [] [Module R M] (f : (j : η) → ιs j →₀ M) (ji : (j : η) × ιs j) :
(.symm f) ji = (f ji.fst) ji.snd
noncomputable def Finsupp.finsuppProdLEquiv {α : Type u_7} {β : Type u_8} (R : Type u_9) {M : Type u_10} [] [] [Module R M] :
(α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M

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

This is the LinearEquiv version of Finsupp.finsuppProdEquiv.

Equations
• = let __src := Finsupp.finsuppProdEquiv; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem Finsupp.finsuppProdLEquiv_apply {α : Type u_7} {β : Type u_8} {R : Type u_9} {M : Type u_10} [] [] [Module R M] (f : α × β →₀ M) (x : α) (y : β) :
(() x) y = f (x, y)
@[simp]
theorem Finsupp.finsuppProdLEquiv_symm_apply {α : Type u_7} {β : Type u_8} {R : Type u_9} {M : Type u_10} [] [] [Module R M] (f : α →₀ β →₀ M) (xy : α × β) :
(.symm f) xy = (f xy.1) xy.2
instance Finsupp.instCountableSubtypeMemSubmoduleSpanRange {M : Type u_2} {R : Type u_5} [] [] [Module R M] {ι : Type u_7} [] [] (v : ιM) :
Countable ()

If R is countable, then any R-submodule spanned by a countable family of vectors is countable.

Equations
• =
def Fintype.total {α : Type u_1} {M : Type u_2} (R : Type u_3) [] [] [] [Module R M] (S : Type u_4) [] [Module 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
• = { toFun := fun (v : αM) => { toFun := fun (f : αR) => i : α, f i v i, map_add' := , map_smul' := }, map_add' := , map_smul' := }
Instances For
theorem Fintype.total_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [] [] [] [Module R M] {S : Type u_4} [] [Module S M] [] (v : αM) (f : αR) :
(() v) f = i : α, f i v i
@[simp]
theorem Fintype.total_apply_single {α : Type u_1} {M : Type u_2} (R : Type u_3) [] [] [] [Module R M] {S : Type u_4} [] [Module S M] [] (v : αM) [] (i : α) (r : R) :
(() v) () = r v i
theorem Finsupp.total_eq_fintype_total_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [] [] [] [Module R M] (S : Type u_4) [] [Module S M] [] (v : αM) (x : αR) :
(Finsupp.total α M R v) (().symm x) = (() v) x
theorem Finsupp.total_eq_fintype_total {α : Type u_1} {M : Type u_2} (R : Type u_3) [] [] [] [Module R M] (S : Type u_4) [] [Module S M] [] (v : αM) :
Finsupp.total α M R v ∘ₗ ().symm = () v
@[simp]
theorem Fintype.range_total {α : Type u_1} {M : Type u_2} (R : Type u_3) [] [] [] [Module R M] {S : Type u_4} [] [Module S M] [] (v : αM) :
theorem mem_span_range_iff_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [] [] [] [Module R M] {v : αM} {x : M} :
x ∃ (c : αR), i : α, c i v i = x

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

theorem top_le_span_range_iff_forall_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [] [] [] [Module R M] {v : αM} :
∀ (x : M), ∃ (c : αR), i : α, c i v i = x

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

@[irreducible]
def Span.repr (R : Type u_4) {M : Type u_5} [] [] [Module R M] (w : Set M) (x : ()) :
w →₀ R

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

Equations
Instances For
theorem Span.repr_def (R : Type u_4) {M : Type u_5} [] [] [Module R M] (w : Set M) (x : ()) :
Span.repr R w x = .choose
@[simp]
theorem Span.finsupp_total_repr (R : Type u_1) {M : Type u_2} [] [] [Module R M] {w : Set M} (x : ()) :
(Finsupp.total (w) M R Subtype.val) (Span.repr R w x) = x
theorem Submodule.finsupp_sum_mem {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_4} {β : Type u_5} [Zero β] (S : ) (f : ι →₀ β) (g : ιβM) (h : ∀ (c : ι), f c 0g c (f c) S) :
f.sum g S
theorem LinearMap.map_finsupp_total {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [Module R M] [] [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_iSup {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_4} (p : ι) {m : M} (hm : m ⨆ (i : ι), p i) :
∃ (s : ), m is, p i
theorem Submodule.mem_iSup_iff_exists_finset {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ι : Type u_4} {p : ι} {m : M} :
m ⨆ (i : ι), p i ∃ (s : ), m is, p i

Submodule.exists_finset_of_mem_iSup as an iff

theorem Submodule.mem_sSup_iff_exists_finset {R : Type u_1} {M : Type u_2} [] [] [Module R M] {S : Set ()} {m : M} :
m sSup S ∃ (s : Finset ()), s S m is, i
theorem mem_span_finset {R : Type u_1} {M : Type u_2} [] [] [Module R M] {s : } {x : M} :
x ∃ (f : MR), is, f i i = x
theorem mem_span_set {R : Type u_1} {M : Type u_2} [] [] [Module R M] {m : M} {s : Set M} :
m ∃ (c : M →₀ R), c.support s (c.sum fun (mi : M) (r : R) => r mi) = m

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

theorem mem_span_set' {R : Type u_1} {M : Type u_2} [] [] [Module R M] {m : M} {s : Set M} :
m ∃ (n : ) (f : Fin nR) (g : Fin ns), i : Fin n, f i (g i) = m

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

theorem span_eq_iUnion_nat {R : Type u_1} {M : Type u_2} [] [] [Module R M] (s : Set M) :
() = ⋃ (n : ), (fun (f : Fin nR × M) => i : Fin n, (f i).1 (f i).2) '' {f : Fin nR × M | ∀ (i : Fin n), (f i).2 s}

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

@[simp]
theorem Module.subsingletonEquiv_apply (R : Type u_4) (M : Type u_5) (ι : Type u_6) [] [] [] [Module R M] :
∀ (x : M), () x = 0
@[simp]
theorem Module.subsingletonEquiv_symm_apply (R : Type u_4) (M : Type u_5) (ι : Type u_6) [] [] [] [Module R M] :
∀ (x : ι →₀ R), ().symm x = 0
def Module.subsingletonEquiv (R : Type u_4) (M : Type u_5) (ι : Type u_6) [] [] [] [Module R M] :

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

Equations
• = { toFun := fun (x : M) => 0, map_add' := , map_smul' := , invFun := fun (x : ι →₀ R) => 0, left_inv := , right_inv := }
Instances For
def LinearMap.splittingOfFinsuppSurjective {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : ) :
(α →₀ R) →ₗ[R] M

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

Equations
• f.splittingOfFinsuppSurjective s = (Finsupp.lift M R α) fun (x : α) => .choose
Instances For
theorem LinearMap.splittingOfFinsuppSurjective_splits {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : ) :
f ∘ₗ f.splittingOfFinsuppSurjective s = LinearMap.id
theorem LinearMap.leftInverse_splittingOfFinsuppSurjective {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : ) :
Function.LeftInverse f (f.splittingOfFinsuppSurjective s)
theorem LinearMap.splittingOfFinsuppSurjective_injective {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : ) :
Function.Injective (f.splittingOfFinsuppSurjective s)
def LinearMap.splittingOfFunOnFintypeSurjective {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_4} [] (f : M →ₗ[R] αR) (s : ) :
(αR) →ₗ[R] M

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

Equations
• f.splittingOfFunOnFintypeSurjective s = ((Finsupp.lift M R α) fun (x : α) => .choose) ∘ₗ ().symm
Instances For
theorem LinearMap.splittingOfFunOnFintypeSurjective_splits {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_4} [] (f : M →ₗ[R] αR) (s : ) :
f ∘ₗ f.splittingOfFunOnFintypeSurjective s = LinearMap.id
theorem LinearMap.leftInverse_splittingOfFunOnFintypeSurjective {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_4} [] (f : M →ₗ[R] αR) (s : ) :
Function.LeftInverse f (f.splittingOfFunOnFintypeSurjective s)
theorem LinearMap.splittingOfFunOnFintypeSurjective_injective {R : Type u_1} {M : Type u_2} [] [] [Module R M] {α : Type u_4} [] (f : M →ₗ[R] αR) (s : ) :
Function.Injective (f.splittingOfFunOnFintypeSurjective s)
theorem LinearMap.coe_finsupp_sum {R : Type u_4} {R₂ : Type u_5} {M : Type u_6} {M₂ : Type u_7} {ι : Type u_8} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_9} [Zero γ] (t : ι →₀ γ) (g : ιγM →ₛₗ[σ₁₂] M₂) :
(t.sum g) = (t.sum fun (i : ι) (d : γ) => g i d)
@[simp]
theorem LinearMap.finsupp_sum_apply {R : Type u_4} {R₂ : Type u_5} {M : Type u_6} {M₂ : Type u_7} {ι : Type u_8} [] [Semiring R₂] [] [] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_9} [Zero γ] (t : ι →₀ γ) (g : ιγM →ₛₗ[σ₁₂] M₂) (b : M) :
(t.sum g) b = t.sum fun (i : ι) (d : γ) => (g i d) b
def Submodule.mulLeftMap {R : Type u_1} [] {S : Type u_4} [] [Module R S] [] [] {M : } (N : ) {ι : Type u_5} (m : ιM) :
(ι →₀ N) →ₗ[R] S

If M and N are submodules of an R-algebra S, m : ι → M is a family of elements, then there is an R-linear map from ι →₀ N to S which maps { n_i } to the sum of m_i * n_i. This is used in the definition of linearly disjointness.

Equations
• = () fun (i : ι) => (m i) N.subtype
Instances For
theorem Submodule.mulLeftMap_apply {R : Type u_1} [] {S : Type u_4} [] [Module R S] [] [] {M : } {N : } {ι : Type u_5} (m : ιM) (n : ι →₀ N) :
() n = n.sum fun (i : ι) (n : N) => (m i) * n
@[simp]
theorem Submodule.mulLeftMap_apply_single {R : Type u_1} [] {S : Type u_4} [] [Module R S] [] [] {M : } {N : } {ι : Type u_5} (m : ιM) (i : ι) (n : N) :
() () = (m i) * n
def Submodule.mulRightMap {R : Type u_1} [] {S : Type u_4} [] [Module R S] [] [] (M : ) {N : } {ι : Type u_5} (n : ιN) :
(ι →₀ M) →ₗ[R] S

If M and N are submodules of an R-algebra S, n : ι → N is a family of elements, then there is an R-linear map from ι →₀ M to S which maps { m_i } to the sum of m_i * n_i. This is used in the definition of linearly disjointness.

Equations
Instances For
theorem Submodule.mulRightMap_apply {R : Type u_1} [] {S : Type u_4} [] [Module R S] [] [] {M : } {N : } {ι : Type u_5} (n : ιN) (m : ι →₀ M) :
(M.mulRightMap n) m = m.sum fun (i : ι) (m : M) => m * (n i)
@[simp]
theorem Submodule.mulRightMap_apply_single {R : Type u_1} [] {S : Type u_4} [] [Module R S] [] [] {M : } {N : } {ι : Type u_5} (n : ιN) (i : ι) (m : M) :
(M.mulRightMap n) () = m * (n i)
theorem Submodule.mulLeftMap_eq_mulRightMap_of_commute {R : Type u_1} [] {S : Type u_4} [] [Module R S] [] [] [] {M : } (N : ) {ι : Type u_5} (m : ιM) (hc : ∀ (i : ι) (n : N), Commute (m i) n) :
= N.mulRightMap m
theorem Submodule.mulLeftMap_eq_mulRightMap {R : Type u_1} [] {S : Type u_5} [] [Module R S] [] [] [] {M : } (N : ) {ι : Type u_6} (m : ιM) :
= N.mulRightMap m