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 Mathlib.Algebra.BigOperators.Finsupp.Basic.

Many constructions based on α →₀ M are defs rather than abbrevs to avoid reusing unwanted type class 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.ext_iff {α : Type u_1} {M : Type u_5} [Zero M] {f g : α →₀ M} : f = g ↔ ∀ (a : α), f a = g a

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] : 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) : (equivFunOnFinite.symm f).support = ⋯.toFinset

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Finsupp.coe_equivFunOnFinite_symm {M : Type u_5} [Zero M] {α : Type u_13} [Finite α] (f : α → M) : ⇑(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✝¹ : ι) : (finsuppUnique.symm a✝) a✝¹ = a✝

@[simp]

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

@[simp]

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

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

theorem Finsupp.unique_ext_iff {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] {f g : α →₀ M} : f = g ↔ f default = g default

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 := Finsupp.onFinset_support✝ s f, 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) : ⇑(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 : α} : (onFinset s f hf) a = f a

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) : (onFinset s f hf).support = {a ∈ s | f a ≠ 0}

@[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} : (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 ∈ (onFinset s f hf).support ↔ f a ≠ 0

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} : ⇑(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 Mathlib/Data/Finsupp/Basic.lean):

• 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 : α} : (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} : mapRange f hf 0 = 0

@[simp]

theorem Finsupp.mapRange_id {α : Type u_1} {M : Type u_5} [Zero M] (g : α →₀ M) : 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) : mapRange (f ∘ f₂) h g = mapRange f hf (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) : mapRange e₁ he₁ (mapRange e₂ he₂ f) = 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} : (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) : (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 (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 (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 (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) : (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 : α ↪ β) : 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 : α) : (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) : (embDomain f v) a = 0

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

@[simp]

theorem Finsupp.embDomain_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α ↪ β} {l₁ l₂ : α →₀ M} : embDomain f l₁ = 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} : 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) : embDomain f (mapRange g hg p) = mapRange g hg (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 : α} : (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} : (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support