Type of functions with finite support

For any type α and any type M with zero, we define the type Finsupp α M (notation: α →₀ M) of finitely supported functions from α to M, i.e. the functions which are zero everywhere on α except on a finite set.

Functions with finite support are used (at least) in the following parts of the library:

• MonoidAlgebra R M and AddMonoidAlgebra R M are defined as M →₀ R;

• polynomials and multivariate polynomials are defined as AddMonoidAlgebras, hence they use Finsupp under the hood;

• the linear combination of a family of vectors v i with coefficients f i (as used, e.g., to define linearly independent family LinearIndependent) is defined as a map Finsupp.linearCombination : (ι → M) → (ι →₀ R) →ₗ[R] M.

Some other constructions are naturally equivalent to α →₀ M with some α and M but are defined in a different way in the library:

• Multiset α ≃+ α →₀ ℕ;
• FreeAbelianGroup α ≃+ α →₀ ℤ.

Most of the theory assumes that the range is a commutative additive monoid. This gives us the big sum operator as a powerful way to construct Finsupp elements, which is defined in Algebra/BigOperators/Finsupp.

-- Porting note: the semireducibility remark no longer applies in Lean 4, afaict. Many constructions based on α →₀ M use semireducible type tags to avoid reusing unwanted type instances. E.g., MonoidAlgebra, AddMonoidAlgebra, and types based on these two have non-pointwise multiplication.

Main declarations

• Finsupp: The type of finitely supported functions from α to β.
• Finsupp.onFinset: The restriction of a function to a Finset as a Finsupp.
• Finsupp.mapRange: Composition of a ZeroHom with a Finsupp.
• Finsupp.embDomain: Maps the domain of a Finsupp by an embedding.
• Finsupp.zipWith: Postcomposition of two Finsupps with a function f such that f 0 0 = 0.

Notations

This file adds α →₀ M as a global notation for Finsupp α M.

We also use the following convention for Type* variables in this file

• α, β, γ: types with no additional structure that appear as the first argument to Finsupp somewhere in the statement;

• ι : an auxiliary index type;

• M, M', N, P: types with Zero or (Add)(Comm)Monoid structure; M is also used for a (semi)module over a (semi)ring.

• G, H: groups (commutative or not, multiplicative or additive);

• R, S: (semi)rings.

Implementation notes

This file is a noncomputable theory and uses classical logic throughout.

TODO

• Expand the list of definitions and important lemmas to the module docstring.

structure Finsupp (α : Type u_13) (M : Type u_14) [Zero M] : Type (max u_13 u_14)

Finsupp α M, denoted α →₀ M, is the type of functions f : α → M such that f x = 0 for all but finitely many x.

• support : Finset α

  The support of a finitely supported function (aka Finsupp).

• toFun : α → M

  The underlying function of a bundled finitely supported function (aka Finsupp).

• mem_support_toFun (a : α) : a ∈ self.support ↔ self.toFun a ≠ 0

  The witness that the support of a Finsupp is indeed the exact locus where its underlying function is nonzero.

def «term_→₀_» : Lean.TrailingParserDescr

Finsupp α M, denoted α →₀ M, is the type of functions f : α → M such that f x = 0 for all but finitely many x.

Equations

• «term_→₀_» = Lean.ParserDescr.trailingNode `«term_→₀_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →₀ ") (Lean.ParserDescr.cat `term 25))

Basic declarations about Finsupp

instance Finsupp.instFunLike {α : Type u_1} {M : Type u_5} [Zero M] : FunLike (α →₀ M) α M

Equations

• Finsupp.instFunLike = { coe := Finsupp.toFun, coe_injective' := ⋯ }

theorem Finsupp.ext {α : Type u_1} {M : Type u_5} [Zero M] {f g : α →₀ M} (h : ∀ (a : α), f a = g a) : f = g

theorem Finsupp.ne_iff {α : Type u_1} {M : Type u_5} [Zero M] {f g : α →₀ M} : f ≠ g ↔ ∃ (a : α), f a ≠ g a

@[simp]

theorem Finsupp.coe_mk {α : Type u_1} {M : Type u_5} [Zero M] (f : α → M) (s : Finset α) (h : ∀ (a : α), a ∈ s ↔ f a ≠ 0) : ⇑{ support := s, toFun := f, mem_support_toFun := h } = f

instance Finsupp.instZero {α : Type u_1} {M : Type u_5} [Zero M] : Zero (α →₀ M)

Equations

• Finsupp.instZero = { zero := { support := ∅, toFun := 0, mem_support_toFun := ⋯ } }

@[simp]

theorem Finsupp.coe_zero {α : Type u_1} {M : Type u_5} [Zero M] : ⇑0 = 0

theorem Finsupp.zero_apply {α : Type u_1} {M : Type u_5} [Zero M] {a : α} : 0 a = 0

@[simp]

theorem Finsupp.support_zero {α : Type u_1} {M : Type u_5} [Zero M] : Finsupp.support 0 = ∅

instance Finsupp.instInhabited {α : Type u_1} {M : Type u_5} [Zero M] : Inhabited (α →₀ M)

Equations

• Finsupp.instInhabited = { default := 0 }

@[simp]

theorem Finsupp.mem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} : a ∈ f.support ↔ f a ≠ 0

@[simp]

theorem Finsupp.fun_support_eq {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) : Function.support ⇑f = ↑f.support

theorem Finsupp.not_mem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} : a ∉ f.support ↔ f a = 0

@[simp]

theorem Finsupp.coe_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} : ⇑f = 0 ↔ f = 0

theorem Finsupp.ext_iff' {α : Type u_1} {M : Type u_5} [Zero M] {f g : α →₀ M} : f = g ↔ f.support = g.support ∧ ∀ x ∈ f.support, f x = g x

@[simp]

theorem Finsupp.support_eq_empty {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} : f.support = ∅ ↔ f = 0

theorem Finsupp.support_nonempty_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} : f.support.Nonempty ↔ f ≠ 0

theorem Finsupp.card_support_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} : f.support.card = 0 ↔ f = 0

instance Finsupp.instDecidableEq {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] [DecidableEq M] : DecidableEq (α →₀ M)

Equations

• f.instDecidableEq g = decidable_of_iff (f.support = g.support ∧ ∀ a ∈ f.support, f a = g a) ⋯

theorem Finsupp.finite_support {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) : (Function.support ⇑f).Finite

theorem Finsupp.support_subset_iff {α : Type u_1} {M : Type u_5} [Zero M] {s : Set α} {f : α →₀ M} : ↑f.support ⊆ s ↔ ∀ a ∉ s, f a = 0

def Finsupp.equivFunOnFinite {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] : (α →₀ M) ≃ (α → M)

Given Finite α, equivFunOnFinite is the Equiv between α →₀ β and α → β. (All functions on a finite type are finitely supported.)

Equations

• Finsupp.equivFunOnFinite = { toFun := DFunLike.coe, invFun := fun (f : α → M) => { support := ⋯.toFinset, toFun := f, mem_support_toFun := ⋯ }, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Finsupp.equivFunOnFinite_symm_apply_support {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (f : α → M) : (Finsupp.equivFunOnFinite.symm f).support = ⋯.toFinset

@[simp]

theorem Finsupp.equivFunOnFinite_symm_apply_toFun {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (f : α → M) (a✝ : α) : (Finsupp.equivFunOnFinite.symm f) a✝ = f a✝

@[simp]

theorem Finsupp.equivFunOnFinite_apply {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (a✝ : α →₀ M) (a : α) : Finsupp.equivFunOnFinite a✝ a = a✝ a

@[simp]

theorem Finsupp.equivFunOnFinite_symm_coe {M : Type u_5} [Zero M] {α : Type u_13} [Finite α] (f : α →₀ M) : Finsupp.equivFunOnFinite.symm ⇑f = f

@[simp]

theorem Finsupp.coe_equivFunOnFinite_symm {M : Type u_5} [Zero M] {α : Type u_13} [Finite α] (f : α → M) : ⇑(Finsupp.equivFunOnFinite.symm f) = f

noncomputable def Equiv.finsuppUnique {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] : (ι →₀ M) ≃ M

If α has a unique term, the type of finitely supported functions α →₀ β is equivalent to β.

Equations

• Equiv.finsuppUnique = Finsupp.equivFunOnFinite.trans (Equiv.funUnique ι M)

@[simp]

theorem Equiv.finsuppUnique_symm_apply_toFun {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] (a✝ : M) (a✝¹ : ι) : (Equiv.finsuppUnique.symm a✝) a✝¹ = a✝

@[simp]

theorem Equiv.finsuppUnique_apply {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] (a✝ : ι →₀ M) : Equiv.finsuppUnique a✝ = a✝ default

@[simp]

theorem Equiv.finsuppUnique_symm_apply_support_val {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] (a✝ : M) : (Equiv.finsuppUnique.symm a✝).support.val = Multiset.map Subtype.val Finset.univ.val

theorem Finsupp.unique_ext {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] {f g : α →₀ M} (h : f default = g default) : f = g

Declarations about onFinset

def Finsupp.onFinset {α : Type u_1} {M : Type u_5} [Zero M] (s : Finset α) (f : α → M) (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) : α →₀ M

Finsupp.onFinset s f hf is the finsupp function representing f restricted to the finset s. The function must be 0 outside of s. Use this when the set needs to be filtered anyways, otherwise a better set representation is often available.

Equations

• Finsupp.onFinset s f hf = { support := Finset.filter (fun (a : α) => f a ≠ 0) s, toFun := f, mem_support_toFun := ⋯ }

@[simp]

theorem Finsupp.coe_onFinset {α : Type u_1} {M : Type u_5} [Zero M] (s : Finset α) (f : α → M) (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) : ⇑(Finsupp.onFinset s f hf) = f

@[simp]

theorem Finsupp.onFinset_apply {α : Type u_1} {M : Type u_5} [Zero M] {s : Finset α} {f : α → M} {hf : ∀ (a : α), f a ≠ 0 → a ∈ s} {a : α} : (Finsupp.onFinset s f hf) a = f a

@[simp]

theorem Finsupp.support_onFinset_subset {α : Type u_1} {M : Type u_5} [Zero M] {s : Finset α} {f : α → M} {hf : ∀ (a : α), f a ≠ 0 → a ∈ s} : (Finsupp.onFinset s f hf).support ⊆ s

theorem Finsupp.mem_support_onFinset {α : Type u_1} {M : Type u_5} [Zero M] {s : Finset α} {f : α → M} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) {a : α} : a ∈ (Finsupp.onFinset s f hf).support ↔ f a ≠ 0

theorem Finsupp.support_onFinset {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq M] {s : Finset α} {f : α → M} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) : (Finsupp.onFinset s f hf).support = Finset.filter (fun (a : α) => f a ≠ 0) s

noncomputable def Finsupp.ofSupportFinite {α : Type u_1} {M : Type u_5} [Zero M] (f : α → M) (hf : (Function.support f).Finite) : α →₀ M

The natural Finsupp induced by the function f given that it has finite support.

Equations

• Finsupp.ofSupportFinite f hf = { support := hf.toFinset, toFun := f, mem_support_toFun := ⋯ }

theorem Finsupp.ofSupportFinite_coe {α : Type u_1} {M : Type u_5} [Zero M] {f : α → M} {hf : (Function.support f).Finite} : ⇑(Finsupp.ofSupportFinite f hf) = f

instance Finsupp.instCanLift {α : Type u_1} {M : Type u_5} [Zero M] : CanLift (α → M) (α →₀ M) DFunLike.coe fun (f : α → M) => (Function.support f).Finite

Declarations about mapRange

def Finsupp.mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : M → N) (hf : f 0 = 0) (g : α →₀ M) : α →₀ N

The composition of f : M → N and g : α →₀ M is mapRange f hf g : α →₀ N, which is well-defined when f 0 = 0.

This preserves the structure on f, and exists in various bundled forms for when f is itself bundled (defined in Data/Finsupp/Basic):

• Finsupp.mapRange.equiv
• Finsupp.mapRange.zeroHom
• Finsupp.mapRange.addMonoidHom
• Finsupp.mapRange.addEquiv
• Finsupp.mapRange.linearMap
• Finsupp.mapRange.linearEquiv

Equations

• Finsupp.mapRange f hf g = Finsupp.onFinset g.support (f ∘ ⇑g) ⋯

@[simp]

theorem Finsupp.mapRange_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : M → N} {hf : f 0 = 0} {g : α →₀ M} {a : α} : (Finsupp.mapRange f hf g) a = f (g a)

@[simp]

theorem Finsupp.mapRange_zero {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : M → N} {hf : f 0 = 0} : Finsupp.mapRange f hf 0 = 0

@[simp]

theorem Finsupp.mapRange_id {α : Type u_1} {M : Type u_5} [Zero M] (g : α →₀ M) : Finsupp.mapRange id ⋯ g = g

theorem Finsupp.mapRange_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : N → P) (hf : f 0 = 0) (f₂ : M → N) (hf₂ : f₂ 0 = 0) (h : (f ∘ f₂) 0 = 0) (g : α →₀ M) : Finsupp.mapRange (f ∘ f₂) h g = Finsupp.mapRange f hf (Finsupp.mapRange f₂ hf₂ g)

@[simp]

theorem Finsupp.mapRange_mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (e₁ : N → P) (e₂ : M → N) (he₁ : e₁ 0 = 0) (he₂ : e₂ 0 = 0) (f : α →₀ M) : Finsupp.mapRange e₁ he₁ (Finsupp.mapRange e₂ he₂ f) = Finsupp.mapRange (e₁ ∘ e₂) ⋯ f

theorem Finsupp.support_mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : M → N} {hf : f 0 = 0} {g : α →₀ M} : (Finsupp.mapRange f hf g).support ⊆ g.support

theorem Finsupp.support_mapRange_of_injective {ι : Type u_4} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {e : M → N} (he0 : e 0 = 0) (f : ι →₀ M) (he : Function.Injective e) : (Finsupp.mapRange e he0 f).support = f.support

theorem Finsupp.range_mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (e : M → N) (he₀ : e 0 = 0) : Set.range (Finsupp.mapRange e he₀) = {g : α →₀ N | ∀ (i : α), g i ∈ Set.range e}

theorem Finsupp.mapRange_injective {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (e : M → N) (he₀ : e 0 = 0) (he : Function.Injective e) : Function.Injective (Finsupp.mapRange e he₀)

Finsupp.mapRange of a injective function is injective.

theorem Finsupp.mapRange_surjective {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (e : M → N) (he₀ : e 0 = 0) (he : Function.Surjective e) : Function.Surjective (Finsupp.mapRange e he₀)

Finsupp.mapRange of a surjective function is surjective.

Declarations about embDomain

def Finsupp.embDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) (v : α →₀ M) : β →₀ M

Given f : α ↪ β and v : α →₀ M, Finsupp.embDomain f v : β →₀ M is the finitely supported function whose value at f a : β is v a. For a b : β outside the range of f, it is zero.

Equations

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

@[simp]

theorem Finsupp.support_embDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) (v : α →₀ M) : (Finsupp.embDomain f v).support = Finset.map f v.support

@[simp]

theorem Finsupp.embDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) : Finsupp.embDomain f 0 = 0

@[simp]

theorem Finsupp.embDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) (v : α →₀ M) (a : α) : (Finsupp.embDomain f v) (f a) = v a

theorem Finsupp.embDomain_notin_range {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) (v : α →₀ M) (a : β) (h : a ∉ Set.range ⇑f) : (Finsupp.embDomain f v) a = 0

theorem Finsupp.embDomain_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) : Function.Injective (Finsupp.embDomain f)

@[simp]

theorem Finsupp.embDomain_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α ↪ β} {l₁ l₂ : α →₀ M} : Finsupp.embDomain f l₁ = Finsupp.embDomain f l₂ ↔ l₁ = l₂

@[simp]

theorem Finsupp.embDomain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α ↪ β} {l : α →₀ M} : Finsupp.embDomain f l = 0 ↔ l = 0

theorem Finsupp.embDomain_mapRange {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : α ↪ β) (g : M → N) (p : α →₀ M) (hg : g 0 = 0) : Finsupp.embDomain f (Finsupp.mapRange g hg p) = Finsupp.mapRange g hg (Finsupp.embDomain f p)

Declarations about zipWith

def Finsupp.zipWith {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : M → N → P) (hf : f 0 0 = 0) (g₁ : α →₀ M) (g₂ : α →₀ N) : α →₀ P

Given finitely supported functions g₁ : α →₀ M and g₂ : α →₀ N and function f : M → N → P, Finsupp.zipWith f hf g₁ g₂ is the finitely supported function α →₀ P satisfying zipWith f hf g₁ g₂ a = f (g₁ a) (g₂ a), which is well-defined when f 0 0 = 0.

Equations

• Finsupp.zipWith f hf g₁ g₂ = Finsupp.onFinset (g₁.support ∪ g₂.support) (fun (a : α) => f (g₁ a) (g₂ a)) ⋯

@[simp]

theorem Finsupp.zipWith_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] {f : M → N → P} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} {a : α} : (Finsupp.zipWith f hf g₁ g₂) a = f (g₁ a) (g₂ a)

theorem Finsupp.support_zipWith {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] [D : DecidableEq α] {f : M → N → P} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} : (Finsupp.zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support

Additive monoid structure on α →₀ M

instance Finsupp.instAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] : Add (α →₀ M)

Equations

• Finsupp.instAdd = { add := Finsupp.zipWith (fun (x1 x2 : M) => x1 + x2) ⋯ }

@[simp]

theorem Finsupp.coe_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f g : α →₀ M) : ⇑(f + g) = ⇑f + ⇑g

theorem Finsupp.add_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (g₁ g₂ : α →₀ M) (a : α) : (g₁ + g₂) a = g₁ a + g₂ a

theorem Finsupp.support_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] [DecidableEq α] {g₁ g₂ : α →₀ M} : (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support

theorem Finsupp.support_add_eq {α : Type u_1} {M : Type u_5} [AddZeroClass M] [DecidableEq α] {g₁ g₂ : α →₀ M} (h : Disjoint g₁.support g₂.support) : (g₁ + g₂).support = g₁.support ∪ g₂.support

instance Finsupp.instAddZeroClass {α : Type u_1} {M : Type u_5} [AddZeroClass M] : AddZeroClass (α →₀ M)

Equations

• Finsupp.instAddZeroClass = Function.Injective.addZeroClass (fun (f : α →₀ M) => ⇑f) ⋯ ⋯ ⋯

instance Finsupp.instIsLeftCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsLeftCancelAdd M] : IsLeftCancelAdd (α →₀ M)

noncomputable def Finsupp.addEquivFunOnFinite {M : Type u_5} [AddZeroClass M] {ι : Type u_13} [Finite ι] : (ι →₀ M) ≃+ (ι → M)

When ι is finite and M is an AddMonoid, then Finsupp.equivFunOnFinite gives an AddEquiv

Equations

• Finsupp.addEquivFunOnFinite = { toEquiv := Finsupp.equivFunOnFinite, map_add' := ⋯ }

noncomputable def AddEquiv.finsuppUnique {M : Type u_5} [AddZeroClass M] {ι : Type u_13} [Unique ι] : (ι →₀ M) ≃+ M

AddEquiv between (ι →₀ M) and M, when ι has a unique element

Equations

• AddEquiv.finsuppUnique = { toEquiv := Equiv.finsuppUnique, map_add' := ⋯ }

instance Finsupp.instIsRightCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsRightCancelAdd M] : IsRightCancelAdd (α →₀ M)

instance Finsupp.instIsCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsCancelAdd M] : IsCancelAdd (α →₀ M)

def Finsupp.applyAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) : (α →₀ M) →+ M

Evaluation of a function f : α →₀ M at a point as an additive monoid homomorphism.

See Finsupp.lapply in LinearAlgebra/Finsupp for the stronger version as a linear map.

Equations

• Finsupp.applyAddHom a = { toFun := fun (g : α →₀ M) => g a, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.applyAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (g : α →₀ M) : (Finsupp.applyAddHom a) g = g a

noncomputable def Finsupp.coeFnAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] : (α →₀ M) →+ α → M

Coercion from a Finsupp to a function type is an AddMonoidHom.

Equations

• Finsupp.coeFnAddHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.coeFnAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a✝ : α →₀ M) (a : α) : Finsupp.coeFnAddHom a✝ a = a✝ a

theorem Finsupp.mapRange_add {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] {f : M → N} {hf : f 0 = 0} (hf' : ∀ (x y : M), f (x + y) = f x + f y) (v₁ v₂ : α →₀ M) : Finsupp.mapRange f hf (v₁ + v₂) = Finsupp.mapRange f hf v₁ + Finsupp.mapRange f hf v₂

theorem Finsupp.mapRange_add' {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] [FunLike β M N] [AddMonoidHomClass β M N] {f : β} (v₁ v₂ : α →₀ M) : Finsupp.mapRange ⇑f ⋯ (v₁ + v₂) = Finsupp.mapRange ⇑f ⋯ v₁ + Finsupp.mapRange ⇑f ⋯ v₂

def Finsupp.embDomain.addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : α ↪ β) : (α →₀ M) →+ β →₀ M

Bundle Finsupp.embDomain f as an additive map from α →₀ M to β →₀ M.

Equations

• Finsupp.embDomain.addMonoidHom f = { toFun := fun (v : α →₀ M) => Finsupp.embDomain f v, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.embDomain.addMonoidHom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : α ↪ β) (v : α →₀ M) : (Finsupp.embDomain.addMonoidHom f) v = Finsupp.embDomain f v

@[simp]

theorem Finsupp.embDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : α ↪ β) (v w : α →₀ M) : Finsupp.embDomain f (v + w) = Finsupp.embDomain f v + Finsupp.embDomain f w

instance Finsupp.instNatSMul {α : Type u_1} {M : Type u_5} [AddMonoid M] : SMul ℕ (α →₀ M)

Note the general SMul instance for Finsupp doesn't apply as ℕ is not distributive unless β i's addition is commutative.

Equations

• Finsupp.instNatSMul = { smul := fun (n : ℕ) (v : α →₀ M) => Finsupp.mapRange (fun (x : M) => n • x) ⋯ v }

instance Finsupp.instAddMonoid {α : Type u_1} {M : Type u_5} [AddMonoid M] : AddMonoid (α →₀ M)

Equations

• Finsupp.instAddMonoid = Function.Injective.addMonoid (fun (f : α →₀ M) => ⇑f) ⋯ ⋯ ⋯ ⋯

instance Finsupp.instAddCommMonoid {α : Type u_1} {M : Type u_5} [AddCommMonoid M] : AddCommMonoid (α →₀ M)

Equations

• Finsupp.instAddCommMonoid = AddCommMonoid.mk ⋯

instance Finsupp.instNeg {α : Type u_1} {G : Type u_9} [NegZeroClass G] : Neg (α →₀ G)

Equations

• Finsupp.instNeg = { neg := Finsupp.mapRange Neg.neg ⋯ }

@[simp]

theorem Finsupp.coe_neg {α : Type u_1} {G : Type u_9} [NegZeroClass G] (g : α →₀ G) : ⇑(-g) = -⇑g

theorem Finsupp.neg_apply {α : Type u_1} {G : Type u_9} [NegZeroClass G] (g : α →₀ G) (a : α) : (-g) a = -g a

theorem Finsupp.mapRange_neg {α : Type u_1} {G : Type u_9} {H : Type u_10} [NegZeroClass G] [NegZeroClass H] {f : G → H} {hf : f 0 = 0} (hf' : ∀ (x : G), f (-x) = -f x) (v : α →₀ G) : Finsupp.mapRange f hf (-v) = -Finsupp.mapRange f hf v

theorem Finsupp.mapRange_neg' {α : Type u_1} {β : Type u_2} {G : Type u_9} {H : Type u_10} [AddGroup G] [SubtractionMonoid H] [FunLike β G H] [AddMonoidHomClass β G H] {f : β} (v : α →₀ G) : Finsupp.mapRange ⇑f ⋯ (-v) = -Finsupp.mapRange ⇑f ⋯ v

instance Finsupp.instSub {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] : Sub (α →₀ G)

Equations

• Finsupp.instSub = { sub := Finsupp.zipWith Sub.sub ⋯ }

@[simp]

theorem Finsupp.coe_sub {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] (g₁ g₂ : α →₀ G) : ⇑(g₁ - g₂) = ⇑g₁ - ⇑g₂

theorem Finsupp.sub_apply {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] (g₁ g₂ : α →₀ G) (a : α) : (g₁ - g₂) a = g₁ a - g₂ a

theorem Finsupp.mapRange_sub {α : Type u_1} {G : Type u_9} {H : Type u_10} [SubNegZeroMonoid G] [SubNegZeroMonoid H] {f : G → H} {hf : f 0 = 0} (hf' : ∀ (x y : G), f (x - y) = f x - f y) (v₁ v₂ : α →₀ G) : Finsupp.mapRange f hf (v₁ - v₂) = Finsupp.mapRange f hf v₁ - Finsupp.mapRange f hf v₂

theorem Finsupp.mapRange_sub' {α : Type u_1} {β : Type u_2} {G : Type u_9} {H : Type u_10} [AddGroup G] [SubtractionMonoid H] [FunLike β G H] [AddMonoidHomClass β G H] {f : β} (v₁ v₂ : α →₀ G) : Finsupp.mapRange ⇑f ⋯ (v₁ - v₂) = Finsupp.mapRange ⇑f ⋯ v₁ - Finsupp.mapRange ⇑f ⋯ v₂

instance Finsupp.instIntSMul {α : Type u_1} {G : Type u_9} [AddGroup G] : SMul ℤ (α →₀ G)

Note the general SMul instance for Finsupp doesn't apply as ℤ is not distributive unless β i's addition is commutative.

Equations

• Finsupp.instIntSMul = { smul := fun (n : ℤ) (v : α →₀ G) => Finsupp.mapRange (fun (x : G) => n • x) ⋯ v }

instance Finsupp.instAddGroup {α : Type u_1} {G : Type u_9} [AddGroup G] : AddGroup (α →₀ G)

Equations

• Finsupp.instAddGroup = AddGroup.mk ⋯

instance Finsupp.instAddCommGroup {α : Type u_1} {G : Type u_9} [AddCommGroup G] : AddCommGroup (α →₀ G)

Equations

• Finsupp.instAddCommGroup = AddCommGroup.mk ⋯

@[simp]

theorem Finsupp.support_neg {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) : (-f).support = f.support

theorem Finsupp.support_sub {α : Type u_1} {G : Type u_9} [DecidableEq α] [AddGroup G] {f g : α →₀ G} : (f - g).support ⊆ f.support ∪ g.support