Properties of the module α →₀ M

• Finsupp.linearEquivFunOnFinite: α →₀ β and a → β are equivalent if α is finite
• FunOnFinite.map: the map (X → M) → (Y → M) induced by a map f : X ⟶ Y when X and Y are finite.
• FunOnFinite.linearMmap: the linear map (X → M) →ₗ[R] (Y → M) induced by a map f : X ⟶ Y when X and Y are finite.

Tags

function with finite support, module, linear algebra

noncomputable def Finsupp.uniqueLinearEquiv (R : Type u_1) {α : Type u_3} (M : Type u_4) [AddCommMonoid M] [Semiring R] [Module R M] [Subsingleton α] (a : α) : (α →₀ M) ≃ₗ[R] M

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

Equations

• Finsupp.uniqueLinearEquiv R M a = { toFun := (Finsupp.uniqueAddEquiv a).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Finsupp.uniqueAddEquiv a).invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Finsupp.uniqueLinearEquiv_apply (R : Type u_1) {α : Type u_3} (M : Type u_4) [AddCommMonoid M] [Semiring R] [Module R M] [Subsingleton α] (a : α) (a✝ : α →₀ M) : (uniqueLinearEquiv R M a) a✝ = a✝ a

@[simp]

theorem Finsupp.uniqueLinearEquiv_symm_apply (R : Type u_1) {α : Type u_3} (M : Type u_4) [AddCommMonoid M] [Semiring R] [Module R M] [Subsingleton α] (a : α) (a✝ : M) : (uniqueLinearEquiv R M a).symm a✝ = single a a✝

@[simp]

theorem Finsupp.uniqueLinearEquiv_symm_apply_apply (R : Type u_1) {α : Type u_3} (M : Type u_4) [AddCommMonoid M] [Semiring R] [Module R M] (a : α) [Subsingleton α] (m : M) (b : α) : ((uniqueLinearEquiv R M a).symm m) b = m

@[deprecated Finsupp.uniqueLinearEquiv (since := "2026-05-06")]

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

@[deprecated Finsupp.uniqueLinearEquiv_apply (since := "2026-05-06")]

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

@[deprecated Finsupp.uniqueLinearEquiv_symm_apply (since := "2026-05-06")]

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

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 = { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

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

@[simp]

theorem Finsupp.lcoeFun_comp_lsingle {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [DecidableEq α] (x : α) : lcoeFun ∘ₗ lsingle x = LinearMap.single R (fun (x : α) => M) x

noncomputable def LinearMap.prodOfFinsuppNat {R : Type u_1} {M : Type u_2} {P : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] (f : P × M →ₗ[R] M) : (ℕ →₀ P) →ₗ[R] P × M

A linear map from a product module P × M to M induces a linear map from P^(ℕ) to M, where the nth component is given by P —ι₁→ P × M composed with P × M —f→ M —ι₂→ P × M n times.

Equations

• f.prodOfFinsuppNat = (Finsupp.lsum ℕ) fun (n : ℕ) => ((LinearMap.inr R P M ∘ₗ f) ^ n) ∘ₗ LinearMap.inl R P M

theorem LinearMap.fst_prodOfFinsuppNat {R : Type u_1} {M : Type u_2} {P : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] (f : P × M →ₗ[R] M) (x : ℕ →₀ P) : (f.prodOfFinsuppNat x).1 = x 0

theorem LinearMap.snd_prodOfFinsuppNat {R : Type u_1} {M : Type u_2} {P : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] (f : P × M →ₗ[R] M) (x : ℕ →₀ P) : (f.prodOfFinsuppNat x).2 = f (f.prodOfFinsuppNat ((Finsupp.comapDomain.addMonoidHom ⋯) x))

theorem LinearMap.prodOfFinsuppNat_injective {R : Type u_1} {M : Type u_2} {P : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] {f : P × M →ₗ[R] M} (inj : Function.Injective ⇑f) : Function.Injective ⇑f.prodOfFinsuppNat

theorem LinearMap.exists_finsupp_nat_of_prod_injective {R : Type u_1} {M : Type u_2} {P : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] {f : P × M →ₗ[R] M} (inj : Function.Injective ⇑f) : ∃ (g : (ℕ →₀ P) →ₗ[R] M), Function.Injective ⇑g

theorem LinearMap.exists_finsupp_nat_of_fin_fun_injective {R : Type u_1} {P : Type u_4} [Semiring R] [AddCommMonoid P] [Module R P] {n : ℕ} {f : (Fin (n + 1) → P) →ₗ[R] Fin n → P} (inj : Function.Injective ⇑f) : ∃ (g : (ℕ →₀ P) →ₗ[R] Fin n → P), Function.Injective ⇑g

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

• f.splittingOfFunOnFintypeSurjective s = ((Finsupp.lift M R α) fun (x : α) => ⋯.choose) ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R R α).symm

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

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

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

def Finsupp.submodule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_5} (S : α → Submodule R M) : Submodule R (α →₀ M)

Given a family Sᵢ of R-submodules of M indexed by a type α, this is the R-submodule of α →₀ M of functions f such that f i ∈ Sᵢ for all i : α.

Equations

• Finsupp.submodule S = { carrier := {x : α →₀ M | ∀ (i : α), x i ∈ S i}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Finsupp.mem_submodule_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_5} (S : α → Submodule R M) (x : α →₀ M) : x ∈ submodule S ↔ ∀ (i : α), x i ∈ S i

theorem Finsupp.ker_mapRange {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) (I : Type u_6) : (mapRange.linearMap f).ker = submodule fun (x : I) => f.ker

theorem Finsupp.range_mapRange_linearMap {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) (hf : f.ker = ⊥) (I : Type u_6) : (mapRange.linearMap f).range = submodule fun (x : I) => f.range

noncomputable def FunOnFinite.map {M : Type u_5} [AddCommMonoid M] {X : Type u_6} {Y : Type u_7} [Finite X] [Finite Y] (f : X → Y) (s : X → M) : Y → M

The map (X → M) → (Y → M) induced by a map X → Y between finite types.

Equations

• FunOnFinite.map f s = Finsupp.equivFunOnFinite (Finsupp.mapDomain f (Finsupp.equivFunOnFinite.symm s))

theorem FunOnFinite.map_apply_apply {M : Type u_5} [AddCommMonoid M] {X : Type u_6} {Y : Type u_7} [Fintype X] [Finite Y] [DecidableEq Y] (f : X → Y) (s : X → M) (y : Y) : map f s y = ∑ x : X with f x = y, s x

@[simp]

theorem FunOnFinite.map_piSingle {M : Type u_5} [AddCommMonoid M] {X : Type u_6} {Y : Type u_7} [Finite X] [Finite Y] [DecidableEq X] [DecidableEq Y] (f : X → Y) (x : X) (m : M) : map f (Pi.single x m) = Pi.single (f x) m

theorem FunOnFinite.map_id (M : Type u_5) [AddCommMonoid M] {X : Type u_6} [Finite X] : map id = id

theorem FunOnFinite.map_comp {M : Type u_5} [AddCommMonoid M] {X : Type u_6} {Y : Type u_7} {Z : Type u_8} [Finite X] [Finite Y] [Finite Z] (g : Y → Z) (f : X → Y) : map (g ∘ f) = map g ∘ map f

noncomputable def FunOnFinite.linearMap (R : Type u_5) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_7} {Y : Type u_8} [Finite X] [Finite Y] (f : X → Y) : (X → M) →ₗ[R] Y → M

The linear map (X → M) →ₗ[R] (Y → M) induced by a map X → Y between finite types.

Equations

• FunOnFinite.linearMap R M f = (↑(Finsupp.linearEquivFunOnFinite R M Y) ∘ₗ Finsupp.lmapDomain M R f) ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R M X).symm

theorem FunOnFinite.linearMap_apply_apply (R : Type u_5) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_7} {Y : Type u_8} [Fintype X] [Finite Y] [DecidableEq Y] (f : X → Y) (s : X → M) (y : Y) : (linearMap R M f) s y = {x : X | f x = y}.sum s

@[simp]

theorem FunOnFinite.linearMap_piSingle (R : Type u_5) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_7} {Y : Type u_8} [Finite X] [Finite Y] [DecidableEq X] [DecidableEq Y] (f : X → Y) (x : X) (m : M) : (linearMap R M f) (Pi.single x m) = Pi.single (f x) m

@[simp]

theorem FunOnFinite.linearMap_id (R : Type u_5) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] (X : Type u_7) [Finite X] : linearMap R M id = LinearMap.id

theorem FunOnFinite.linearMap_comp (R : Type u_5) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_7} {Y : Type u_8} {Z : Type u_9} [Finite X] [Finite Y] [Finite Z] (f : X → Y) (g : Y → Z) : linearMap R M (g ∘ f) = linearMap R M g ∘ₗ linearMap R M f