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 β] [AddCommMonoid M] [DistribSMul R M] {v : α →₀ β} {c : R} {h : α → β → M} : c • Finsupp.sum v h = Finsupp.sum v 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} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {v : α →₀ M} {c : R} {h : α → M →ₗ[R] M₂} : (Finsupp.sum (c • v) fun (a : α) => ⇑(h a)) = c • Finsupp.sum v fun (a : α) => ⇑(h a)

@[simp]

theorem Finsupp.linearEquivFunOnFinite_apply (R : Type u_1) (M : Type u_3) (α : Type u_4) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] : ∀ (a : α →₀ M) (a_1 : α), (Finsupp.linearEquivFunOnFinite R M α) a a_1 = a a_1

noncomputable def Finsupp.linearEquivFunOnFinite (R : Type u_1) (M : Type u_3) (α : Type u_4) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] : (α →₀ M) ≃ₗ[R] α → M

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.linearEquivFunOnFinite_single (R : Type u_1) (M : Type u_3) (α : Type u_4) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] [DecidableEq α] (x : α) (m : M) : (Finsupp.linearEquivFunOnFinite R M α) (Finsupp.single x m) = Pi.single x m

@[simp]

theorem Finsupp.linearEquivFunOnFinite_symm_single (R : Type u_1) (M : Type u_3) (α : Type u_4) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] [DecidableEq α] (x : α) (m : M) : (LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R M α)) (Pi.single x m) = Finsupp.single x m

@[simp]

theorem Finsupp.linearEquivFunOnFinite_symm_coe (R : Type u_1) (M : Type u_3) (α : Type u_4) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] (f : α →₀ M) : (LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R M α)) ⇑f = f

noncomputable def Finsupp.LinearEquiv.finsuppUnique (R : Type u_1) (M : Type u_3) [AddCommMonoid M] [Semiring R] [Module R M] (α : Type u_4) [Unique α] : (α →₀ 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.

@[simp]

theorem Finsupp.LinearEquiv.finsuppUnique_apply {R : Type u_1} {M : Type u_3} [AddCommMonoid M] [Semiring R] [Module R M] (α : Type u_4) [Unique α] (f : α →₀ M) : (Finsupp.LinearEquiv.finsuppUnique R M α) f = f default

@[simp]

theorem Finsupp.LinearEquiv.finsuppUnique_symm_apply {R : Type u_1} {M : Type u_3} [AddCommMonoid M] [Semiring R] [Module R M] {α : Type u_4} [Unique α] (m : M) : (LinearEquiv.symm (Finsupp.LinearEquiv.finsuppUnique R M α)) m = Finsupp.single default m

def Finsupp.lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) : M →ₗ[R] α →₀ M

Interpret Finsupp.single a as a linear map.

Equations

• Finsupp.lsingle a = let __src := Finsupp.singleAddHom a; { toAddHom := { toFun := __src.toFun, map_add' := ⋯ }, map_smul' := ⋯ }

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

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

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

Equations

• Finsupp.lapply a = let __src := Finsupp.applyAddHom a; { toAddHom := { toFun := __src.toFun, map_add' := ⋯ }, map_smul' := ⋯ }

instance LinearMap.CompatibleSMul.finsupp_dom (R : Type u_7) (S : Type u_8) (M : Type u_9) (N : Type u_10) (ι : Type u_11) [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module S M] [Module S N] [SMulZeroClass R M] [DistribSMul R N] [LinearMap.CompatibleSMul M N R S] : LinearMap.CompatibleSMul (ι →₀ M) N R S

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) [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module S M] [Module S N] [SMul R M] [SMulZeroClass R N] [LinearMap.CompatibleSMul M N R S] : LinearMap.CompatibleSMul M (ι →₀ N) R S

Equations

• ⋯ = ⋯

@[simp]

theorem Finsupp.lcoeFun_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [AddCommMonoid M] [Module R M] : (α →₀ M) →ₗ[R] α → M

Forget that a function is finitely supported.

This is the linear version of Finsupp.toFun.

Equations

• Finsupp.lcoeFun = { toAddHom := { toFun := DFunLike.coe, map_add' := ⋯ }, map_smul' := ⋯ }

def Finsupp.lsubtypeDomain {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) : (α →₀ M) →ₗ[R] ↑s →₀ M

Interpret Finsupp.subtypeDomain s as a linear map.

Equations

• Finsupp.lsubtypeDomain s = { toAddHom := { toFun := Finsupp.subtypeDomain fun (x : α) => x ∈ s, map_add' := ⋯ }, map_smul' := ⋯ }

theorem Finsupp.lsubtypeDomain_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (f : α →₀ M) : (Finsupp.lsubtypeDomain s) f = Finsupp.subtypeDomain (fun (x : α) => x ∈ s) f

@[simp]

theorem Finsupp.lsingle_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) (b : M) : (Finsupp.lsingle a) b = Finsupp.single a b

@[simp]

theorem Finsupp.lapply_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) (f : α →₀ M) : (Finsupp.lapply a) f = f a

@[simp]

theorem Finsupp.lapply_comp_lsingle_same {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) : Finsupp.lapply a ∘ₗ Finsupp.lsingle a = LinearMap.id

@[simp]

theorem Finsupp.lapply_comp_lsingle_of_ne {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) (a' : α) (h : a ≠ a') : Finsupp.lapply a ∘ₗ Finsupp.lsingle a' = 0

@[simp]

theorem Finsupp.ker_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a : α) : LinearMap.ker (Finsupp.lsingle a) = ⊥

theorem Finsupp.lsingle_range_le_ker_lapply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (t : Set α) (h : Disjoint s t) : ⨆ a ∈ s, LinearMap.range (Finsupp.lsingle a) ≤ ⨅ a ∈ t, LinearMap.ker (Finsupp.lapply a)

theorem Finsupp.iInf_ker_lapply_le_bot {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : ⨅ (a : α), LinearMap.ker (Finsupp.lapply a) ≤ ⊥

theorem Finsupp.iSup_lsingle_range {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : ⨆ (a : α), LinearMap.range (Finsupp.lsingle a) = ⊤

theorem Finsupp.disjoint_lsingle_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (t : Set α) (hs : Disjoint s t) : Disjoint (⨆ a ∈ s, LinearMap.range (Finsupp.lsingle a)) (⨆ a ∈ t, LinearMap.range (Finsupp.lsingle a))

theorem Finsupp.span_single_image {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (a : α) : Submodule.span R (Finsupp.single a '' s) = Submodule.map (Finsupp.lsingle a) (Submodule.span R s)

def Finsupp.supported {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid 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

• Finsupp.supported M R s = { toAddSubmonoid := { toAddSubsemigroup := { carrier := {p : α →₀ M | ↑p.support ⊆ s}, add_mem' := ⋯ }, zero_mem' := ⋯ }, smul_mem' := ⋯ }

theorem Finsupp.mem_supported {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} (p : α →₀ M) : p ∈ Finsupp.supported M R s ↔ ↑p.support ⊆ s

theorem Finsupp.mem_supported' {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} (p : α →₀ M) : p ∈ Finsupp.supported M R s ↔ ∀ x ∉ s, p x = 0

theorem Finsupp.mem_supported_support {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [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) [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {a : α} (b : M) (h : a ∈ s) : Finsupp.single a b ∈ Finsupp.supported M R 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 ((fun (i : α) => Finsupp.single i 1) '' s)

def Finsupp.restrictDom {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] : (α →₀ M) →ₗ[R] ↥(Finsupp.supported M R s)

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

Equations

• Finsupp.restrictDom M R s = LinearMap.codRestrict (Finsupp.supported M R s) { toAddHom := { toFun := Finsupp.filter fun (x : α) => x ∈ s, map_add' := ⋯ }, map_smul' := ⋯ } ⋯

@[simp]

theorem Finsupp.restrictDom_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (l : α →₀ M) [DecidablePred fun (x : α) => x ∈ s] : ↑((Finsupp.restrictDom M R 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} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] : Finsupp.restrictDom M R s ∘ₗ Submodule.subtype (Finsupp.supported M R s) = LinearMap.id

theorem Finsupp.range_restrictDom {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] : LinearMap.range (Finsupp.restrictDom M R s) = ⊤

theorem Finsupp.supported_mono {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {t : Set α} (st : s ⊆ t) : Finsupp.supported M R s ≤ Finsupp.supported M R t

@[simp]

theorem Finsupp.supported_empty {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : Finsupp.supported M R ∅ = ⊥

@[simp]

theorem Finsupp.supported_univ {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : Finsupp.supported M R Set.univ = ⊤

theorem Finsupp.supported_iUnion {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (t : Set α) : Finsupp.supported M R (s ∪ t) = Finsupp.supported M R s ⊔ Finsupp.supported M R t

theorem Finsupp.supported_iInter {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (t : Set α) : Finsupp.supported M R (s ∩ t) = Finsupp.supported M R s ⊓ Finsupp.supported M R t

theorem Finsupp.disjoint_supported_supported {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set α} {t : Set α} (h : Disjoint s t) : Disjoint (Finsupp.supported M R s) (Finsupp.supported M R t)

theorem Finsupp.disjoint_supported_supported_iff {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] {s : Set α} {t : Set α} : Disjoint (Finsupp.supported M R s) (Finsupp.supported M R t) ↔ Disjoint s t

def Finsupp.supportedEquivFinsupp {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) : ↥(Finsupp.supported M R s) ≃ₗ[R] ↑s →₀ M

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

Equations

• Finsupp.supportedEquivFinsupp s = let F := Finsupp.restrictSupportEquiv s M; Equiv.toLinearEquiv F ⋯

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] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass 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.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.

@[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] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass R S N] (f : α → M →ₗ[R] N) : ⇑((Finsupp.lsum S) f) = fun (d : α →₀ M) => Finsupp.sum d 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) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass R S N] (f : α → M →ₗ[R] N) (l : α →₀ M) : ((Finsupp.lsum S) f) l = Finsupp.sum l 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) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass R S N] (f : α → M →ₗ[R] N) (i : α) (m : M) : ((Finsupp.lsum S) f) (Finsupp.single i m) = (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) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass R S N] (f : α → M →ₗ[R] N) (i : α) : (Finsupp.lsum S) f ∘ₗ Finsupp.lsingle i = 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) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [SMulCommClass R S N] (f : (α →₀ M) →ₗ[R] N) (x : α) : (LinearEquiv.symm (Finsupp.lsum S)) f x = f ∘ₗ Finsupp.lsingle x

noncomputable def Finsupp.lift (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.lift_symm_apply (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (X : Type u_7) (f : (X →₀ R) →ₗ[R] M) (x : X) : (AddEquiv.symm (Finsupp.lift M R X)) f x = f (Finsupp.single x 1)

@[simp]

theorem Finsupp.lift_apply (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (X : Type u_7) (f : X → M) (g : X →₀ R) : ((Finsupp.lift M R X) f) g = Finsupp.sum g fun (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] [AddCommMonoid M] [Module R M] (X : Type u_7) [Module S M] [SMulCommClass 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.llift_apply (M : Type u_2) (R : Type u_5) (S : Type u_6) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] (X : Type u_7) [Module S M] [SMulCommClass 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] [AddCommMonoid M] [Module R M] (X : Type u_7) [Module S M] [SMulCommClass R S M] (f : (X →₀ R) →ₗ[R] M) (x : X) : (LinearEquiv.symm (Finsupp.llift M R S X)) f x = f (Finsupp.single x 1)

def Finsupp.lmapDomain {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : α → α') : (α →₀ M) →ₗ[R] α' →₀ M

Interpret Finsupp.mapDomain as a linear map.

Equations

• Finsupp.lmapDomain M R f = { toAddHom := { toFun := Finsupp.mapDomain f, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem Finsupp.lmapDomain_apply {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : α → α') (l : α →₀ M) : (Finsupp.lmapDomain M R f) l = Finsupp.mapDomain f l

@[simp]

theorem Finsupp.lmapDomain_id {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] : Finsupp.lmapDomain M R id = LinearMap.id

theorem Finsupp.lmapDomain_comp {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {α'' : Type u_8} (f : α → α') (g : α' → α'') : Finsupp.lmapDomain M R (g ∘ f) = Finsupp.lmapDomain M R g ∘ₗ Finsupp.lmapDomain M R f

theorem Finsupp.supported_comap_lmapDomain {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : α → α') (s : Set α') : Finsupp.supported M R (f ⁻¹' s) ≤ Submodule.comap (Finsupp.lmapDomain M R f) (Finsupp.supported M R s)

theorem Finsupp.lmapDomain_supported {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : α → α') (s : Set α) : Submodule.map (Finsupp.lmapDomain M R f) (Finsupp.supported M R s) = Finsupp.supported M R (f '' s)

theorem Finsupp.lmapDomain_disjoint_ker {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (f : α → α') {s : Set α} (H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b) : Disjoint (Finsupp.supported M R s) (LinearMap.ker (Finsupp.lmapDomain M R f))

def Finsupp.lcomapDomain {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid 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, 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

• Finsupp.lcomapDomain f hf = { toAddHom := { toFun := fun (l : β →₀ M) => Finsupp.comapDomain f l ⋯, map_add' := ⋯ }, map_smul' := ⋯ }

def Finsupp.total (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid 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

• Finsupp.total α M R v = (Finsupp.lsum ℕ) fun (i : α) => LinearMap.smulRight LinearMap.id (v i)

theorem Finsupp.total_apply {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (l : α →₀ R) : (Finsupp.total α M R v) l = Finsupp.sum l 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) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {l : α →₀ R} {s : Finset α} (hs : l ∈ Finsupp.supported R R ↑s) : (Finsupp.total α M R v) l = Finset.sum s fun (i : α) => l i • v i

@[simp]

theorem Finsupp.total_single {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid 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] [AddCommMonoid 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] [AddCommMonoid 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] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid 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.apply_total_id {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_8} [AddCommMonoid M'] [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) [Semiring R] [AddCommMonoid M] [Module R M] [Unique α] (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) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (h : Function.Surjective v) : Function.Surjective ⇑(Finsupp.total α M R v)

theorem Finsupp.total_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (h : Function.Surjective v) : LinearMap.range (Finsupp.total α M R v) = ⊤

theorem Finsupp.total_id_surjective (R : Type u_5) [Semiring R] (M : Type u_9) [AddCommMonoid M] [Module R M] : Function.Surjective ⇑(Finsupp.total M M R id)

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

theorem Finsupp.range_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} : LinearMap.range (Finsupp.total α M R v) = Submodule.span R (Set.range v)

theorem Finsupp.lmapDomain_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid 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' ∘ₗ Finsupp.lmapDomain R R f = g ∘ₗ Finsupp.total α M R v

theorem Finsupp.total_comp_lmapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α → α') : Finsupp.total α' M' R v' ∘ₗ Finsupp.lmapDomain R R f = Finsupp.total α M' R (v' ∘ f)

@[simp]

theorem Finsupp.total_embDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α ↪ α') (l : α →₀ R) : (Finsupp.total α' M' R v') (Finsupp.embDomain f l) = (Finsupp.total α M' R (v' ∘ ⇑f)) l

@[simp]

theorem Finsupp.total_mapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α → α') (l : α →₀ R) : (Finsupp.total α' M' R v') (Finsupp.mapDomain f l) = (Finsupp.total α M' R (v' ∘ f)) l

@[simp]

theorem Finsupp.total_equivMapDomain {α : Type u_1} (R : Type u_5) [Semiring R] {α' : Type u_7} {M' : Type u_8} [AddCommMonoid M'] [Module R M'] {v' : α' → M'} (f : α ≃ α') (l : α →₀ R) : (Finsupp.total α' M' R v') (Finsupp.equivMapDomain 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] [AddCommMonoid M] [Module R M] (s : Set M) : Submodule.span R s = 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) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (x : M) : x ∈ Submodule.span R s ↔ ∃ (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} [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {x : M} : x ∈ Submodule.span R (Set.range v) ↔ ∃ (c : α →₀ R), (Finsupp.sum c 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) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (s : Set α) : Submodule.span R (v '' s) = Submodule.map (Finsupp.total α M R v) (Finsupp.supported R R s)

theorem Finsupp.mem_span_image_iff_total {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {s : Set α} {x : M} : x ∈ Submodule.span R (v '' s) ↔ ∃ 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] [AddCommMonoid M] [Module R M] (v : Option α → M) (f : Option α →₀ R) : (Finsupp.total (Option α) M R v) f = f none • v none + (Finsupp.total α M R (v ∘ some)) (Finsupp.some f)

theorem Finsupp.total_total {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [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) [Semiring R] [AddCommMonoid M] [Module R M] (f : Fin 0 → M) : Finsupp.total (Fin 0) M R f = 0

def Finsupp.totalOn (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (v : α → M) (s : Set α) : ↥(Finsupp.supported R R s) →ₗ[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

• Finsupp.totalOn α M R v s = LinearMap.codRestrict (Submodule.span R (v '' s)) (LinearMap.comp (Finsupp.total α M R v) (Submodule.subtype (Finsupp.supported R R s))) ⋯

theorem Finsupp.totalOn_range {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} (s : Set α) : LinearMap.range (Finsupp.totalOn α M R v s) = ⊤

theorem Finsupp.total_comp {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {v : α → M} (f : α' → α) : Finsupp.total α' M R (v ∘ f) = Finsupp.total α M R v ∘ₗ Finsupp.lmapDomain R R f

theorem Finsupp.total_comapDomain {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} {v : α → M} (f : α → α') (l : α' →₀ R) (hf : Set.InjOn f (f ⁻¹' ↑l.support)) : (Finsupp.total α M R v) (Finsupp.comapDomain f l hf) = Finset.sum (Finset.preimage l.support f hf) fun (i : α) => l (f i) • v i

theorem Finsupp.total_onFinset {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {s : Finset α} {f : α → R} (g : α → M) (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) : (Finsupp.total α M R g) (Finsupp.onFinset s f hf) = Finset.sum s fun (x : α) => f x • g x

def Finsupp.domLCongr {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [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

• Finsupp.domLCongr e = AddEquiv.toLinearEquiv (Finsupp.domCongr e) ⋯

@[simp]

theorem Finsupp.domLCongr_apply {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} (e : α₁ ≃ α₂) (v : α₁ →₀ M) : (Finsupp.domLCongr e) v = (Finsupp.domCongr e) v

@[simp]

theorem Finsupp.domLCongr_refl {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : Finsupp.domLCongr (Equiv.refl α) = LinearEquiv.refl R (α →₀ M)

theorem Finsupp.domLCongr_trans {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} {α₃ : Type u_9} (f : α₁ ≃ α₂) (f₂ : α₂ ≃ α₃) : Finsupp.domLCongr f ≪≫ₗ Finsupp.domLCongr f₂ = Finsupp.domLCongr (f.trans f₂)

@[simp]

theorem Finsupp.domLCongr_symm {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} (f : α₁ ≃ α₂) : LinearEquiv.symm (Finsupp.domLCongr f) = Finsupp.domLCongr f.symm

theorem Finsupp.domLCongr_single {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_7} {α₂ : Type u_8} (e : α₁ ≃ α₂) (i : α₁) (m : M) : (Finsupp.domLCongr e) (Finsupp.single i m) = Finsupp.single (e i) m

noncomputable def Finsupp.congr {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_7} (s : Set α) (t : Set α') (e : ↑s ≃ ↑t) : ↥(Finsupp.supported M R s) ≃ₗ[R] ↥(Finsupp.supported M R t)

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

Equations

• Finsupp.congr s t e = LinearEquiv.trans (Finsupp.supportedEquivFinsupp s) (LinearEquiv.trans (Finsupp.domLCongr e) (LinearEquiv.symm (Finsupp.supportedEquivFinsupp t)))

def Finsupp.mapRange.linearMap {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : (α →₀ M) →ₗ[R] α →₀ N

Finsupp.mapRange as a LinearMap.

Equations

• Finsupp.mapRange.linearMap f = let __src := Finsupp.mapRange.addMonoidHom (LinearMap.toAddMonoidHom f); { toAddHom := { toFun := Finsupp.mapRange ⇑f ⋯, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem Finsupp.mapRange.linearMap_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (g : α →₀ M) : (Finsupp.mapRange.linearMap f) g = Finsupp.mapRange ⇑f ⋯ g

@[simp]

theorem Finsupp.mapRange.linearMap_id {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [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} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : N →ₗ[R] P) (f₂ : M →ₗ[R] N) : Finsupp.mapRange.linearMap (f ∘ₗ f₂) = Finsupp.mapRange.linearMap f ∘ₗ Finsupp.mapRange.linearMap f₂

@[simp]

theorem Finsupp.mapRange.linearMap_toAddMonoidHom {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : LinearMap.toAddMonoidHom (Finsupp.mapRange.linearMap f) = Finsupp.mapRange.addMonoidHom (LinearMap.toAddMonoidHom f)

def Finsupp.mapRange.linearEquiv {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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.

@[simp]

theorem Finsupp.mapRange.linearEquiv_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (g : α →₀ M) : (Finsupp.mapRange.linearEquiv e) g = (Finsupp.mapRange.linearMap ↑e) g

@[simp]

theorem Finsupp.mapRange.linearEquiv_refl {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : Finsupp.mapRange.linearEquiv (LinearEquiv.refl R M) = LinearEquiv.refl 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} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : M ≃ₗ[R] N) (f₂ : N ≃ₗ[R] P) : Finsupp.mapRange.linearEquiv (f ≪≫ₗ f₂) = Finsupp.mapRange.linearEquiv f ≪≫ₗ Finsupp.mapRange.linearEquiv f₂

@[simp]

theorem Finsupp.mapRange.linearEquiv_symm {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M ≃ₗ[R] N) : LinearEquiv.symm (Finsupp.mapRange.linearEquiv f) = Finsupp.mapRange.linearEquiv (LinearEquiv.symm f)

@[simp]

theorem Finsupp.mapRange.linearEquiv_toAddEquiv {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M ≃ₗ[R] N) : LinearEquiv.toAddEquiv (Finsupp.mapRange.linearEquiv f) = Finsupp.mapRange.addEquiv (LinearEquiv.toAddEquiv f)

@[simp]

theorem Finsupp.mapRange.linearEquiv_toLinearMap {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M ≃ₗ[R] N) : ↑(Finsupp.mapRange.linearEquiv f) = Finsupp.mapRange.linearMap ↑f

def Finsupp.lcongr {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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

• Finsupp.lcongr e₁ e₂ = LinearEquiv.trans (Finsupp.domLCongr e₁) (Finsupp.mapRange.linearEquiv e₂)

@[simp]

theorem Finsupp.lcongr_single {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_7} {κ : Type u_8} (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] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [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} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_7} {κ : Type u_8} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (k : κ) (n : N) : (LinearEquiv.symm (Finsupp.lcongr e₁ e₂)) (Finsupp.single k n) = Finsupp.single (e₁.symm k) ((LinearEquiv.symm e₂) n)

@[simp]

theorem Finsupp.lcongr_symm {M : Type u_2} {N : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ι : Type u_7} {κ : Type u_8} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) : LinearEquiv.symm (Finsupp.lcongr e₁ e₂) = Finsupp.lcongr e₁.symm (LinearEquiv.symm e₂)

@[simp]

theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_apply {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} : ∀ (a : (α →₀ M) × (β →₀ M)), (LinearEquiv.symm (Finsupp.sumFinsuppLEquivProdFinsupp R)) a = Finsupp.sumFinsuppAddEquivProdFinsupp.invFun a

@[simp]

theorem Finsupp.sumFinsuppLEquivProdFinsupp_apply {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} : ∀ (a : α ⊕ β →₀ M), (Finsupp.sumFinsuppLEquivProdFinsupp R) a = Finsupp.sumFinsuppAddEquivProdFinsupp.toFun a

def Finsupp.sumFinsuppLEquivProdFinsupp {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [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.

theorem Finsupp.fst_sumFinsuppLEquivProdFinsupp {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} (f : α ⊕ β →₀ M) (x : α) : ((Finsupp.sumFinsuppLEquivProdFinsupp R) f).1 x = f (Sum.inl x)

theorem Finsupp.snd_sumFinsuppLEquivProdFinsupp {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} (f : α ⊕ β →₀ M) (y : β) : ((Finsupp.sumFinsuppLEquivProdFinsupp R) f).2 y = f (Sum.inr y)

theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} (fg : (α →₀ M) × (β →₀ M)) (x : α) : ((LinearEquiv.symm (Finsupp.sumFinsuppLEquivProdFinsupp R)) fg) (Sum.inl x) = fg.1 x

theorem Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} (fg : (α →₀ M) × (β →₀ M)) (y : β) : ((LinearEquiv.symm (Finsupp.sumFinsuppLEquivProdFinsupp R)) fg) (Sum.inr y) = fg.2 y

noncomputable def Finsupp.sigmaFinsuppLEquivPiFinsupp (R : Type u_5) [Semiring R] {η : Type u_7} [Fintype η] {M : Type u_9} {ιs : η → Type u_10} [AddCommMonoid 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 LinearEquiv version of Finsupp.sigmaFinsuppAddEquivPiFinsupp.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.sigmaFinsuppLEquivPiFinsupp_apply (R : Type u_5) [Semiring R] {η : Type u_7} [Fintype η] {M : Type u_9} {ιs : η → Type u_10} [AddCommMonoid M] [Module R M] (f : (j : η) × ιs j →₀ M) (j : η) (i : ιs j) : ((Finsupp.sigmaFinsuppLEquivPiFinsupp R) f j) i = f { fst := j, snd := i }

@[simp]

theorem Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply (R : Type u_5) [Semiring R] {η : Type u_7} [Fintype η] {M : Type u_9} {ιs : η → Type u_10} [AddCommMonoid M] [Module R M] (f : (j : η) → ιs j →₀ M) (ji : (j : η) × ιs j) : ((LinearEquiv.symm (Finsupp.sigmaFinsuppLEquivPiFinsupp R)) 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} [Semiring R] [AddCommMonoid M] [Module R M] : (α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M

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

This is the LinearEquiv version of Finsupp.finsuppProdEquiv.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.finsuppProdLEquiv_apply {α : Type u_7} {β : Type u_8} {R : Type u_9} {M : Type u_10} [Semiring R] [AddCommMonoid M] [Module R M] (f : α × β →₀ M) (x : α) (y : β) : (((Finsupp.finsuppProdLEquiv R) f) 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} [Semiring R] [AddCommMonoid M] [Module R M] (f : α →₀ β →₀ M) (xy : α × β) : ((LinearEquiv.symm (Finsupp.finsuppProdLEquiv R)) f) xy = (f xy.1) xy.2

instance Finsupp.instCountableSubtypeMemSubmoduleInstMembershipSetLikeSpanRange {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_7} [Countable R] [Countable ι] (v : ι → M) : Countable ↥(Submodule.span R (Set.range v))

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) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass 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

• One or more equations did not get rendered due to their size.

theorem Fintype.total_apply {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) (f : α → R) : ((Fintype.total R S) v) f = Finset.sum Finset.univ fun (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] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) [DecidableEq α] (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] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) (x : α → R) : (Finsupp.total α M R v) ((LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R α)) x) = ((Fintype.total R S) v) x

theorem Finsupp.total_eq_fintype_total {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] (S : Type u_4) [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) : Finsupp.total α M R v ∘ₗ ↑(LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R α)) = (Fintype.total R S) v

@[simp]

theorem Fintype.range_total {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_4} [Semiring S] [Module S M] [SMulCommClass R S M] (v : α → M) : LinearMap.range ((Fintype.total R S) v) = Submodule.span R (Set.range v)

theorem mem_span_range_iff_exists_fun {α : Type u_1} {M : Type u_2} (R : Type u_3) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] {v : α → M} {x : M} : x ∈ Submodule.span R (Set.range v) ↔ ∃ (c : α → R), (Finset.sum Finset.univ fun (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] [AddCommMonoid M] [Module R M] {v : α → M} : ⊤ ≤ Submodule.span R (Set.range v) ↔ ∀ (x : M), ∃ (c : α → R), (Finset.sum Finset.univ fun (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.

theorem Span.repr_def (R : Type u_4) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (w : Set M) (x : ↥(Submodule.span R w)) : Span.repr R w x = Exists.choose ⋯

@[irreducible]

def Span.repr (R : Type u_4) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (w : Set M) (x : ↥(Submodule.span R w)) : ↑w →₀ R

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

Equations

• Span.repr = wrapped✝.1

@[simp]

theorem Span.finsupp_total_repr (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {w : Set M} (x : ↥(Submodule.span R w)) : (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} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} {β : Type u_5} [Zero β] (S : Submodule R M) (f : ι →₀ β) (g : ι → β → M) (h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ S) : Finsupp.sum f g ∈ S

theorem LinearMap.map_finsupp_total {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid 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_iSup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} (p : ι → Submodule R M) {m : M} (hm : m ∈ ⨆ (i : ι), p i) : ∃ (s : Finset ι), m ∈ ⨆ i ∈ s, p i

theorem Submodule.mem_iSup_iff_exists_finset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} {p : ι → Submodule R M} {m : M} : m ∈ ⨆ (i : ι), p i ↔ ∃ (s : Finset ι), m ∈ ⨆ i ∈ s, 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} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set (Submodule R M)} {m : M} : m ∈ sSup S ↔ ∃ (s : Finset (Submodule R M)), ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i

theorem mem_span_finset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s : Finset M} {x : M} : x ∈ Submodule.span R ↑s ↔ ∃ (f : M → R), (Finset.sum s fun (i : M) => f i • i) = x

theorem mem_span_set {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {m : M} {s : Set M} : m ∈ Submodule.span R s ↔ ∃ (c : M →₀ R), ↑c.support ⊆ s ∧ (Finsupp.sum c 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} [Semiring R] [AddCommMonoid M] [Module R M] {m : M} {s : Set M} : m ∈ Submodule.span R s ↔ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → ↑s), (Finset.sum Finset.univ fun (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} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) : ↑(Submodule.span R s) = ⋃ (n : ℕ), (fun (f : Fin n → R × M) => Finset.sum Finset.univ fun (i : Fin n) => (f i).1 • (f i).2) '' {f : Fin n → R × 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_symm_apply (R : Type u_4) (M : Type u_5) (ι : Type u_6) [Semiring R] [Subsingleton R] [AddCommMonoid M] [Module R M] : ∀ (x : ι →₀ R), (LinearEquiv.symm (Module.subsingletonEquiv R M ι)) x = 0

@[simp]

theorem Module.subsingletonEquiv_apply (R : Type u_4) (M : Type u_5) (ι : Type u_6) [Semiring R] [Subsingleton R] [AddCommMonoid M] [Module R M] : ∀ (x : M), (Module.subsingletonEquiv R M ι) x = 0

def Module.subsingletonEquiv (R : Type u_4) (M : Type u_5) (ι : Type u_6) [Semiring R] [Subsingleton R] [AddCommMonoid M] [Module R M] : M ≃ₗ[R] ι →₀ R

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

Equations

• One or more equations did not get rendered due to their size.

def LinearMap.splittingOfFinsuppSurjective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid 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

• LinearMap.splittingOfFinsuppSurjective f s = (Finsupp.lift M R α) fun (x : α) => Exists.choose ⋯

theorem LinearMap.splittingOfFinsuppSurjective_splits {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : Function.Surjective ⇑f) : f ∘ₗ LinearMap.splittingOfFinsuppSurjective f s = LinearMap.id

theorem LinearMap.leftInverse_splittingOfFinsuppSurjective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : Function.Surjective ⇑f) : Function.LeftInverse ⇑f ⇑(LinearMap.splittingOfFinsuppSurjective f s)

theorem LinearMap.splittingOfFinsuppSurjective_injective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : Function.Surjective ⇑f) : Function.Injective ⇑(LinearMap.splittingOfFinsuppSurjective f s)

def LinearMap.splittingOfFunOnFintypeSurjective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Finite α] (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

• LinearMap.splittingOfFunOnFintypeSurjective f s = LinearMap.comp ((Finsupp.lift M R α) fun (x : α) => Exists.choose ⋯) ↑(LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R α))

theorem LinearMap.splittingOfFunOnFintypeSurjective_splits {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Finite α] (f : M →ₗ[R] α → R) (s : Function.Surjective ⇑f) : f ∘ₗ LinearMap.splittingOfFunOnFintypeSurjective f s = LinearMap.id

theorem LinearMap.leftInverse_splittingOfFunOnFintypeSurjective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Finite α] (f : M →ₗ[R] α → R) (s : Function.Surjective ⇑f) : Function.LeftInverse ⇑f ⇑(LinearMap.splittingOfFunOnFintypeSurjective f s)

theorem LinearMap.splittingOfFunOnFintypeSurjective_injective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Finite α] (f : M →ₗ[R] α → R) (s : Function.Surjective ⇑f) : Function.Injective ⇑(LinearMap.splittingOfFunOnFintypeSurjective f 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_9} [Zero γ] (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) : ⇑(Finsupp.sum t g) = ⇑(Finsupp.sum t 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] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_9} [Zero γ] (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) (b : M) : (Finsupp.sum t g) b = Finsupp.sum t fun (i : ι) (d : γ) => (g i d) b