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 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.lmapDomain: a linear map version of Finsupp.mapDomain;

Tags

function with finite support, module, linear algebra

noncomputable def Finsupp.linearEquivFunOnFinite (R : Type u_7) (M : Type u_9) (α : Type u_10) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] : (α →₀ M) ≃ₗ[R] α → M

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

Equations

• Finsupp.linearEquivFunOnFinite R M α = { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯, invFun := Finsupp.equivFunOnFinite.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Finsupp.linearEquivFunOnFinite_apply (R : Type u_7) (M : Type u_9) (α : Type u_10) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] (a✝ : α →₀ M) (a : α) : (Finsupp.linearEquivFunOnFinite R M α) a✝ a = a✝ a

@[simp]

theorem Finsupp.linearEquivFunOnFinite_single (R : Type u_7) (M : Type u_9) (α : Type u_10) [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_7) (M : Type u_9) (α : Type u_10) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] [DecidableEq α] (x : α) (m : M) : (Finsupp.linearEquivFunOnFinite R M α).symm (Pi.single x m) = Finsupp.single x m

@[simp]

theorem Finsupp.linearEquivFunOnFinite_symm_coe (R : Type u_7) (M : Type u_9) (α : Type u_10) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] (f : α →₀ M) : (Finsupp.linearEquivFunOnFinite R M α).symm ⇑f = f

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 = { toFun := (↑(Finsupp.singleAddHom a)).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⦄ (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⦄ (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 = { toFun := (↑(Finsupp.applyAddHom a)).toFun, 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 = { 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

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 = { 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

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 = { toFun := fun (l : β →₀ M) => Finsupp.comapDomain f l ⋯, map_add' := ⋯, map_smul' := ⋯ }

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 = { 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) : (Finsupp.mapRange.linearMap f).toAddMonoidHom = Finsupp.mapRange.addMonoidHom f.toAddMonoidHom

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

• Finsupp.mapRange.linearEquiv e = { toFun := Finsupp.mapRange ⇑e ⋯, map_add' := ⋯, map_smul' := ⋯, invFun := Finsupp.mapRange ⇑e.symm ⋯, left_inv := ⋯, right_inv := ⋯ }

@[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) : (Finsupp.mapRange.linearEquiv f).symm = Finsupp.mapRange.linearEquiv f.symm

@[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) : (Finsupp.mapRange.linearEquiv f).toAddEquiv = Finsupp.mapRange.addEquiv f.toAddEquiv

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

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

• Finsupp.finsuppProdLEquiv R = { toFun := Finsupp.finsuppProdEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := Finsupp.finsuppProdEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

@[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 : α × β) : ((Finsupp.finsuppProdLEquiv R).symm f) xy = (f xy.1) xy.2

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

• Module.subsingletonEquiv R M ι = { toFun := fun (x : M) => 0, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : ι →₀ R) => 0, left_inv := ⋯, right_inv := ⋯ }

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

@[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) : (Module.subsingletonEquiv R M ι).symm x✝ = 0