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_9) (M : Type u_11) (α : Type u_12) [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 := ⋯ }

Instances For

source

@[simp]

theorem Finsupp.linearEquivFunOnFinite_apply (R : Type u_9) (M : Type u_11) (α : Type u_12) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] (a✝ : α →₀ M) (a : α) :

(linearEquivFunOnFinite R M α) a✝ a = a✝ a

source

@[simp]

theorem Finsupp.linearEquivFunOnFinite_single (R : Type u_9) (M : Type u_11) (α : Type u_12) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] [DecidableEq α] (x : α) (m : M) :

(linearEquivFunOnFinite R M α) (single x m) = Pi.single x m

source

@[simp]

theorem Finsupp.linearEquivFunOnFinite_symm_single (R : Type u_9) (M : Type u_11) (α : Type u_12) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] [DecidableEq α] (x : α) (m : M) :

(linearEquivFunOnFinite R M α).symm (Pi.single x m) = single x m

source

@[simp]

theorem Finsupp.linearEquivFunOnFinite_symm_coe (R : Type u_9) (M : Type u_11) (α : Type u_12) [Finite α] [AddCommMonoid M] [Semiring R] [Module R M] (f : α →₀ M) :

(linearEquivFunOnFinite R M α).symm ⇑f = f

source

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' := ⋯ }

Instances For

source

theorem Finsupp.lhom_ext {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ₁₂ : R →+* R₂} ⦃φ ψ : (α →₀ M) →ₛₗ[σ₁₂] N⦄ (h : ∀ (a : α) (b : M), φ (single a b) = ψ (single a b)) :

φ = ψ

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

source

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

source

theorem Finsupp.lhom_ext'_iff {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ₁₂ : R →+* R₂} {φ ψ : (α →₀ M) →ₛₗ[σ₁₂] N} :

φ = ψ ↔ ∀ (a : α), φ ∘ₛₗ lsingle a = ψ ∘ₛₗ lsingle a

source

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' := ⋯ }

Instances For

source

instance Finsupp.instFaithfulSMulOfNonempty {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Nonempty α] [FaithfulSMul R M] :

FaithfulSMul R (α →₀ M)

source

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' := ⋯ }

Instances For

source

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) :

(lsubtypeDomain s) f = subtypeDomain (fun (x : α) => x ∈ s) f

source

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

(lsingle a) b = single a b

source

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

(lapply a) f = f a

source

@[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 : α) :

lapply a ∘ₗ lsingle a = LinearMap.id

source

@[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') :

lapply a ∘ₗ lsingle a' = 0

source

def Finsupp.lmapDomain {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_9} (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' := ⋯ }

Instances For

source

@[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_9} (f : α → α') (l : α →₀ M) :

(lmapDomain M R f) l = mapDomain f l

source

@[simp]

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

lmapDomain M R id = LinearMap.id

source

theorem Finsupp.lmapDomain_comp {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_9} {α'' : Type u_10} (f : α → α') (g : α' → α'') :

lmapDomain M R (g ∘ f) = lmapDomain M R g ∘ₗ lmapDomain M R f

source

def Finsupp.mapDomain.linearEquiv {α : Type u_1} (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α' : Type u_9} (f : α ≃ α') :

(α →₀ M) ≃ₗ[R] α' →₀ M

Finsupp.mapDomain as a LinearEquiv.

Equations

Finsupp.mapDomain.linearEquiv M R f = { toLinearMap := Finsupp.lmapDomain M R f.toFun, invFun := Finsupp.mapDomain ⇑f.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

def Finsupp.lcomapDomain {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {β : Type u_9} (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' := ⋯ }

Instances For

source

@[simp]

theorem Finsupp.lcomapDomain_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {β : Type u_9} (f : α → β) (hf : Function.Injective f) (l : β →₀ M) :

(lcomapDomain f hf) l = comapDomain f l ⋯

source

theorem Finsupp.leftInverse_lcomapDomain_mapDomain {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {β : Type u_9} (f : α → β) (hf : Function.Injective f) :

Function.LeftInverse (⇑(lcomapDomain f hf)) (mapDomain f)

source

def Finsupp.mapRange.linearMap {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] N) :

(α →₀ M) →ₛₗ[σ₁₂] α →₀ N

Finsupp.mapRange as a LinearMap.

Equations

Finsupp.mapRange.linearMap f = { toFun := Finsupp.mapRange ⇑f ⋯, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem Finsupp.mapRange.linearMap_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] N) (g : α →₀ M) :

(linearMap f) g = mapRange ⇑f ⋯ g

source

@[simp]

theorem Finsupp.mapRange.linearMap_id {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :

linearMap LinearMap.id = LinearMap.id

source

theorem Finsupp.mapRange.linearMap_comp {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {R : Type u_5} {R₂ : Type u_6} {R₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] [AddCommMonoid P] [Module R₃ P] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : N →ₛₗ[σ₂₃] P) (f₂ : M →ₛₗ[σ₁₂] N) :

linearMap (f ∘ₛₗ f₂) = linearMap f ∘ₛₗ linearMap f₂

source

@[simp]

theorem Finsupp.mapRange.linearMap_toAddMonoidHom {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] N) :

(linearMap f).toAddMonoidHom = addMonoidHom f.toAddMonoidHom

source

def Finsupp.mapRange.linearEquiv {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M ≃ₛₗ[σ₁₂] N) :

(α →₀ M) ≃ₛₗ[σ₁₂] α →₀ 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 := ⋯ }

Instances For

source

@[simp]

theorem Finsupp.mapRange.linearEquiv_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M ≃ₛₗ[σ₁₂] N) (g : α →₀ M) :

(linearEquiv e) g = mapRange ⇑e ⋯ g

source

@[simp]

theorem Finsupp.mapRange.linearEquiv_refl {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :

linearEquiv (LinearEquiv.refl R M) = LinearEquiv.refl R (α →₀ M)

source

theorem Finsupp.mapRange.linearEquiv_trans {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {R : Type u_5} {R₂ : Type u_6} {R₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] [AddCommMonoid P] [Module R₃ P] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] (f : M ≃ₛₗ[σ₁₂] N) (f₂ : N ≃ₛₗ[σ₂₃] P) :

linearEquiv (f.trans f₂) = (linearEquiv f).trans (linearEquiv f₂)

source

@[simp]

theorem Finsupp.mapRange.linearEquiv_symm {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] N) :

(linearEquiv f).symm = linearEquiv f.symm

source

@[simp]

theorem Finsupp.mapRange.linearEquiv_toAddEquiv {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] N) :

(linearEquiv f).toAddEquiv = addEquiv f.toAddEquiv

source

@[simp]

theorem Finsupp.mapRange.linearEquiv_toLinearMap {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] N) :

↑(linearEquiv f) = linearMap ↑f

source

noncomputable def Finsupp.finsuppProdLEquiv {α : Type u_9} {β : Type u_10} (R : Type u_11) {M : Type u_12} [DecidableEq α] [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 := ⋯ }

Instances For

source

@[simp]

theorem Finsupp.finsuppProdLEquiv_symm_apply {α : Type u_9} {β : Type u_10} (R : Type u_11) {M : Type u_12} [DecidableEq α] [Semiring R] [AddCommMonoid M] [Module R M] (a✝ : α →₀ β →₀ M) :

(finsuppProdLEquiv R).symm a✝ = a✝.uncurry

source

@[simp]

theorem Finsupp.finsuppProdLEquiv_apply {α : Type u_9} {β : Type u_10} (R : Type u_11) {M : Type u_12} [DecidableEq α] [Semiring R] [AddCommMonoid M] [Module R M] (a✝ : α × β →₀ M) :

(finsuppProdLEquiv R) a✝ = a✝.curry

source

theorem Finsupp.finsuppProdLEquiv_symm_apply_apply {α : Type u_9} {β : Type u_10} {R : Type u_11} {M : Type u_12} [DecidableEq α] [Semiring R] [AddCommMonoid M] [Module R M] (f : α →₀ β →₀ M) (xy : α × β) :

((finsuppProdLEquiv R).symm f) xy = (f xy.1) xy.2

source

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 := ⋯ }

Instances For

source

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

(subsingletonEquiv R M ι).symm x✝ = 0

source

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

(subsingletonEquiv R M ι) x✝ = 0

Documentation

Mathlib.LinearAlgebra.Finsupp.Defs

Properties of the module `α →₀ M` #

Tags #

Properties of the module α →₀ M #

Tags #

Properties of the module `α →₀ M` #