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

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

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

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), (↑φ fun₀ | a => b) = ↑ψ fun₀ | 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 : α), LinearMap.comp φ (Finsupp.lsingle a) = LinearMap.comp ψ (Finsupp.lsingle a)) : φ = ψ

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

We formulate this fact using equality of linear maps φ.comp (lsingle a) and ψ.comp (lsingle a) so that the ext tactic can apply a type-specific extensionality lemma to prove equality of these maps. E.g., if M = R, then it suffices to verify φ (single a 1) = ψ (single a 1).

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

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

Equations

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

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

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

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

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

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 = fun₀ | 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.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 : α) (_ : a ∈ s), LinearMap.range (Finsupp.lsingle a) ≤ ⨅ (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 : α) (_ : a ∈ s), LinearMap.range (Finsupp.lsingle a)) (⨆ (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

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

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 : α), ¬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) : (fun₀ | 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 => fun₀ | 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 α) : (α →₀ M) →ₗ[R] { x // x ∈ Finsupp.supported M R s }

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

Equations

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

@[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) : ↑(↑(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 α) : LinearMap.comp (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 α) : 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 α) : { x // x ∈ 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 (_ : IsLinearMap R ↑(Finsupp.restrictSupportEquiv s M))

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 => 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) fun₀ | i => m) = ↑(f i) m

theorem Finsupp.lsum_symm_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} (S : Type u_6) [Semiring R] [Semiring S] [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 = LinearMap.comp 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 fun₀ | 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 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 fun₀ | 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

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

@[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) = LinearMap.comp (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 : α), a ∈ s → ∀ (b : α), 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

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

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 => 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) fun₀ | 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)) : LinearMap.comp (Finsupp.total α' M' R v') (Finsupp.lmapDomain R R f) = LinearMap.comp 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 : α → α') : LinearMap.comp (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, ↑(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, (Finsupp.sum c fun i a => 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, 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 α) : { x // x ∈ Finsupp.supported R R s } →ₗ[R] { x // x ∈ 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

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

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) = LinearMap.comp (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) (_ : ∀ (c : R) (x : α₁ →₀ M), ↑(Finsupp.domCongr e) (c • x) = c • ↑(Finsupp.domCongr e) x)

@[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₂ : α₂ ≃ α₃) : LinearEquiv.trans (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) fun₀ | i => m) = fun₀ | ↑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) : { x // x ∈ Finsupp.supported M R s } ≃ₗ[R] { x // x ∈ 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

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

@[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 (_ : ↑f 0 = 0) 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 (LinearMap.comp f f₂) = LinearMap.comp (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 (LinearEquiv.trans f f₂) = LinearEquiv.trans (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₂) fun₀ | i => m) = fun₀ | ↑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₂)) fun₀ | k => n) = fun₀ | ↑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_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 = Equiv.toFun Finsupp.sumFinsuppAddEquivProdFinsupp.toEquiv a

@[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 = Equiv.invFun Finsupp.sumFinsuppAddEquivProdFinsupp.toEquiv 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).fst 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).snd 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.fst 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.snd 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.fst) xy.snd

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 { x // x ∈ Submodule.span R (Set.range v) }

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

Equations

• @Finsupp.instCountableSubtypeMemSubmoduleInstMembershipSetLikeSpanRange = @Finsupp.instCountableSubtypeMemSubmoduleInstMembershipSetLikeSpanRange.proof_1

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) : LinearMap.comp (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, (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, (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 : { x // x ∈ Submodule.span R w }) : Span.repr R w x = Exists.choose (_ : ∃ l, ↑(Finsupp.total (↑w) M R Subtype.val) l = ↑x)

@[irreducible]

def Span.repr (R : Type u_4) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (w : Set M) (x : { x // 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 : { x // 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, m ∈ ⨆ (i : ι) (_ : 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, m ∈ ⨆ (i : ι) (_ : i ∈ s), p i

Submodule.exists_finset_of_mem_iSup as an iff

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, (Finset.sum s fun i => 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, ↑c.support ⊆ s ∧ (Finsupp.sum c fun mi 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 g, (Finset.sum Finset.univ fun i => 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 => Finset.sum Finset.univ fun i => (f i).fst • (f i).snd) '' {f | ∀ (i : Fin n), (f i).snd ∈ 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 (_ : ∃ a, ↑f a = fun₀ | x => 1)

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) : LinearMap.comp 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} [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

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

theorem LinearMap.splittingOfFunOnFintypeSurjective_splits {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Fintype α] (f : M →ₗ[R] α → R) (s : Function.Surjective ↑f) : LinearMap.comp 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} [Fintype α] (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} [Fintype α] (f : M →ₗ[R] α → R) (s : Function.Surjective ↑f) : Function.Injective ↑(LinearMap.splittingOfFunOnFintypeSurjective f s)