# 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 `AddMonoidAlgebra`s, 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.lean`.

Many constructions based on `α →₀ M` are `def`s rather than `abbrev`s 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 `Finsupp`s with a function `f` such that `f 0 0 = 0`.

## Notation #

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`, `N`, `O`: types with `Zero` or `(Add)(Comm)Monoid` structure;

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

## 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.

source
structure Finsupp (α : Type u_9) (M : Type u_10) [Zero M] :
Type (max u_10 u_9)

`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.

Instances For

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

Instances For

### Basic declarations about `Finsupp` #

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

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

source
theorem Finsupp.ext {α : Type u_1} {M : Type u_4} [Zero M] {f g : α →₀ M} (h : ∀ (a : α), f a = g a) :
f = g
source
theorem Finsupp.ext_iff {α : Type u_1} {M : Type u_4} [Zero M] {f g : α →₀ M} :
f = g ↔ ∀ (a : α), f a = g a
source
theorem Finsupp.ne_iff {α : Type u_1} {M : Type u_4} [Zero M] {f g : α →₀ M} :
f ≠ g ↔ ∃ (a : α), f a ≠ g a
source
@[simp]
theorem Finsupp.coe_mk {α : Type u_1} {M : Type u_4} [Zero M] (f : α → M) (s : Finset α) (h : ∀ (a : α), a ∈ s ↔ f a ≠ 0) :
⇑{ support := s, toFun := f, mem_support_toFun := h } = f
source
instance Finsupp.instZero {α : Type u_1} {M : Type u_4} [Zero M] :
Zero (α →₀ M)
Equations

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

source
@[simp]
theorem Finsupp.coe_zero {α : Type u_1} {M : Type u_4} [Zero M] :
⇑0 = 0
source
theorem Finsupp.zero_apply {α : Type u_1} {M : Type u_4} [Zero M] {a : α} :
0 a = 0
source
@[simp]
theorem Finsupp.support_zero {α : Type u_1} {M : Type u_4} [Zero M] :
support 0 = ∅
source
instance Finsupp.instInhabited {α : Type u_1} {M : Type u_4} [Zero M] :
Inhabited (α →₀ M)
Equations

- Finsupp.instInhabited = { default := 0 }

source
@[simp]
theorem Finsupp.mem_support_iff {α : Type u_1} {M : Type u_4} [Zero M] {f : α →₀ M} {a : α} :
a ∈ f.support ↔ f a ≠ 0
source
@[simp]
theorem Finsupp.fun_support_eq {α : Type u_1} {M : Type u_4} [Zero M] (f : α →₀ M) :
Function.support ⇑f = ↑f.support
source
theorem Finsupp.notMem_support_iff {α : Type u_1} {M : Type u_4} [Zero M] {f : α →₀ M} {a : α} :
a ∉ f.support ↔ f a = 0
source
@[deprecated Finsupp.notMem_support_iff (since := "2025-05-23")]
theorem Finsupp.not_mem_support_iff {α : Type u_1} {M : Type u_4} [Zero M] {f : α →₀ M} {a : α} :
a ∉ f.support ↔ f a = 0

Alias of `Finsupp.notMem_support_iff`.

source
@[simp]
theorem Finsupp.coe_eq_zero {α : Type u_1} {M : Type u_4} [Zero M] {f : α →₀ M} :
⇑f = 0 ↔ f = 0
source
theorem Finsupp.ext_iff' {α : Type u_1} {M : Type u_4} [Zero M] {f g : α →₀ M} :
f = g ↔ f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
source
@[simp]
theorem Finsupp.support_eq_empty {α : Type u_1} {M : Type u_4} [Zero M] {f : α →₀ M} :
f.support = ∅ ↔ f = 0
source
theorem Finsupp.support_nonempty_iff {α : Type u_1} {M : Type u_4} [Zero M] {f : α →₀ M} :
f.support.Nonempty ↔ f ≠ 0
source
theorem Finsupp.card_support_eq_zero {α : Type u_1} {M : Type u_4} [Zero M] {f : α →₀ M} :
f.support.card = 0 ↔ f = 0
source
instance Finsupp.instDecidableEq {α : Type u_1} {M : Type u_4} [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) ⋯

source
theorem Finsupp.finite_support {α : Type u_1} {M : Type u_4} [Zero M] (f : α →₀ M) :
(Function.support ⇑f).Finite
source
theorem Finsupp.support_subset_iff {α : Type u_1} {M : Type u_4} [Zero M] {s : Set α} {f : α →₀ M} :
↑f.support ⊆ s ↔ ∀ a ∉ s, f a = 0
source
def Finsupp.equivFunOnFinite {α : Type u_1} {M : Type u_4} [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 := ⋯ }

Instances For

source
@[simp]
theorem Finsupp.equivFunOnFinite_symm_apply_support {α : Type u_1} {M : Type u_4} [Zero M] [Finite α] (f : α → M) :
(equivFunOnFinite.symm f).support = ⋯.toFinset
source
@[simp]
theorem Finsupp.equivFunOnFinite_apply {α : Type u_1} {M : Type u_4} [Zero M] [Finite α] (a✝ : α →₀ M) (a : α) :
equivFunOnFinite a✝ a = a✝ a
source
@[simp]
theorem Finsupp.equivFunOnFinite_symm_apply_toFun {α : Type u_1} {M : Type u_4} [Zero M] [Finite α] (f : α → M) (a✝ : α) :
(equivFunOnFinite.symm f) a✝ = f a✝
source
@[simp]
theorem Finsupp.equivFunOnFinite_symm_coe {M : Type u_4} [Zero M] {α : Type u_9} [Finite α] (f : α →₀ M) :
equivFunOnFinite.symm ⇑f = f
source
@[simp]
theorem Finsupp.coe_equivFunOnFinite_symm {M : Type u_4} [Zero M] {α : Type u_9} [Finite α] (f : α → M) :
⇑(equivFunOnFinite.symm f) = f
source
noncomputable def Equiv.finsuppUnique {M : Type u_4} [Zero M] {ι : Type u_9} [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)

Instances For

source
@[simp]
theorem Equiv.finsuppUnique_symm_apply_support_val {M : Type u_4} [Zero M] {ι : Type u_9} [Unique ι] (a✝ : M) :
(finsuppUnique.symm a✝).support.val = Multiset.map Subtype.val Finset.univ.val
source
@[simp]
theorem Equiv.finsuppUnique_symm_apply_toFun {M : Type u_4} [Zero M] {ι : Type u_9} [Unique ι] (a✝ : M) (a✝¹ : ι) :
(finsuppUnique.symm a✝) a✝¹ = a✝
source
@[simp]
theorem Equiv.finsuppUnique_apply {M : Type u_4} [Zero M] {ι : Type u_9} [Unique ι] (a✝ : ι →₀ M) :
finsuppUnique a✝ = a✝ default
source
theorem Finsupp.unique_ext {α : Type u_1} {M : Type u_4} [Zero M] [Unique α] {f g : α →₀ M} (h : f default = g default) :
f = g
source
theorem Finsupp.unique_ext_iff {α : Type u_1} {M : Type u_4} [Zero M] [Unique α] {f g : α →₀ M} :
f = g ↔ f default = g default

### Declarations about `onFinset` #

source
def Finsupp.onFinset {α : Type u_1} {M : Type u_4} [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 := ⋯ }

Instances For

source
@[simp]
theorem Finsupp.coe_onFinset {α : Type u_1} {M : Type u_4} [Zero M] (s : Finset α) (f : α → M) (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) :
⇑(onFinset s f hf) = f
source
@[simp]
theorem Finsupp.onFinset_apply {α : Type u_1} {M : Type u_4} [Zero M] {s : Finset α} {f : α → M} {hf : ∀ (a : α), f a ≠ 0 → a ∈ s} {a : α} :
(onFinset s f hf) a = f a
source
theorem Finsupp.support_onFinset {α : Type u_1} {M : Type u_4} [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}
source
@[simp]
theorem Finsupp.support_onFinset_subset {α : Type u_1} {M : Type u_4} [Zero M] {s : Finset α} {f : α → M} {hf : ∀ (a : α), f a ≠ 0 → a ∈ s} :
(onFinset s f hf).support ⊆ s
source
theorem Finsupp.mem_support_onFinset {α : Type u_1} {M : Type u_4} [Zero M] {s : Finset α} {f : α → M} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) {a : α} :
a ∈ (onFinset s f hf).support ↔ f a ≠ 0
source
noncomputable def Finsupp.ofSupportFinite {α : Type u_1} {M : Type u_4} [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 := ⋯ }

Instances For

source
theorem Finsupp.ofSupportFinite_coe {α : Type u_1} {M : Type u_4} [Zero M] {f : α → M} {hf : (Function.support f).Finite} :
⇑(ofSupportFinite f hf) = f
source
theorem Finsupp.ofSupportFinite_support {α : Type u_1} {M : Type u_4} [Zero M] {f : α → M} (hf : (Function.support f).Finite) :
(ofSupportFinite f hf).support = hf.toFinset
source
instance Finsupp.instCanLift {α : Type u_1} {M : Type u_4} [Zero M] :
CanLift (α → M) (α →₀ M) DFunLike.coe fun (f : α → M) => (Function.support f).Finite

### Declarations about `mapRange` #

source
def Finsupp.mapRange {α : Type u_1} {M : Type u_4} {N : Type u_5} [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) ⋯

Instances For

source
@[simp]
theorem Finsupp.mapRange_apply {α : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] {f : M → N} {hf : f 0 = 0} {g : α →₀ M} {a : α} :
(mapRange f hf g) a = f (g a)
source
@[simp]
theorem Finsupp.mapRange_zero {α : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] {f : M → N} {hf : f 0 = 0} :
mapRange f hf 0 = 0
source
@[simp]
theorem Finsupp.mapRange_id {α : Type u_1} {M : Type u_4} [Zero M] (g : α →₀ M) :
mapRange id ⋯ g = g
source
theorem Finsupp.mapRange_comp {α : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [Zero M] [Zero N] [Zero O] (f : N → O) (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)
source
@[simp]
theorem Finsupp.mapRange_mapRange {α : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [Zero M] [Zero N] [Zero O] (e₁ : N → O) (e₂ : M → N) (he₁ : e₁ 0 = 0) (he₂ : e₂ 0 = 0) (f : α →₀ M) :
mapRange e₁ he₁ (mapRange e₂ he₂ f) = mapRange (e₁ ∘ e₂) ⋯ f
source
theorem Finsupp.support_mapRange {α : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] {f : M → N} {hf : f 0 = 0} {g : α →₀ M} :
(mapRange f hf g).support ⊆ g.support
source
theorem Finsupp.support_mapRange_of_injective {ι : Type u_3} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] {e : M → N} (he0 : e 0 = 0) (f : ι →₀ M) (he : Function.Injective e) :
(mapRange e he0 f).support = f.support
source
theorem Finsupp.range_mapRange {α : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] (e : M → N) (he₀ : e 0 = 0) :
Set.range (mapRange e he₀) = {g : α →₀ N | ∀ (i : α), g i ∈ Set.range e}
source
theorem Finsupp.mapRange_injective {α : Type u_1} {M : Type u_4} {N : Type u_5} [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.

source
theorem Finsupp.mapRange_surjective {α : Type u_1} {M : Type u_4} {N : Type u_5} [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.

source
def Finsupp.mapRange.equiv {ι : Type u_3} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] (e : M ≃ N) (hf : e 0 = 0) :
(ι →₀ M) ≃ (ι →₀ N)

`Finsupp.mapRange` as an equiv.

Equations

- Finsupp.mapRange.equiv e hf = { toFun := Finsupp.mapRange (⇑e) hf, invFun := Finsupp.mapRange ⇑e.symm ⋯, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Finsupp.mapRange.equiv_apply {ι : Type u_3} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] (e : M ≃ N) (hf : e 0 = 0) (g : ι →₀ M) :
(equiv e hf) g = mapRange (⇑e) hf g
source
@[simp]
theorem Finsupp.mapRange.equiv_refl {ι : Type u_3} {M : Type u_4} [Zero M] :
equiv (Equiv.refl M) ⋯ = Equiv.refl (ι →₀ M)
source
theorem Finsupp.mapRange.equiv_trans {ι : Type u_3} {M : Type u_4} {N : Type u_5} {O : Type u_6} [Zero M] [Zero N] [Zero O] (e : M ≃ N) (hf : e 0 = 0) (f₂ : N ≃ O) (hf₂ : f₂ 0 = 0) :
equiv (e.trans f₂) ⋯ = (equiv e hf).trans (equiv f₂ hf₂)
source
@[simp]
theorem Finsupp.mapRange.equiv_symm {ι : Type u_3} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] (e : M ≃ N) (hf : e 0 = 0) :
(equiv e hf).symm = equiv e.symm ⋯

### Declarations about `embDomain` #

source
def Finsupp.embDomain {α : Type u_1} {β : Type u_2} {M : Type u_4} [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.

Instances For

source
@[simp]
theorem Finsupp.support_embDomain {α : Type u_1} {β : Type u_2} {M : Type u_4} [Zero M] (f : α ↪ β) (v : α →₀ M) :
(embDomain f v).support = Finset.map f v.support
source
@[simp]
theorem Finsupp.embDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_4} [Zero M] (f : α ↪ β) :
embDomain f 0 = 0
source
@[simp]
theorem Finsupp.embDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_4} [Zero M] (f : α ↪ β) (v : α →₀ M) (a : α) :
(embDomain f v) (f a) = v a
source
theorem Finsupp.embDomain_notin_range {α : Type u_1} {β : Type u_2} {M : Type u_4} [Zero M] (f : α ↪ β) (v : α →₀ M) (a : β) (h : a ∉ Set.range ⇑f) :
(embDomain f v) a = 0
source
theorem Finsupp.embDomain_injective {α : Type u_1} {β : Type u_2} {M : Type u_4} [Zero M] (f : α ↪ β) :
Function.Injective (embDomain f)
source
@[simp]
theorem Finsupp.embDomain_inj {α : Type u_1} {β : Type u_2} {M : Type u_4} [Zero M] {f : α ↪ β} {l₁ l₂ : α →₀ M} :
embDomain f l₁ = embDomain f l₂ ↔ l₁ = l₂
source
@[simp]
theorem Finsupp.embDomain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_4} [Zero M] {f : α ↪ β} {l : α →₀ M} :
embDomain f l = 0 ↔ l = 0
source
theorem Finsupp.embDomain_mapRange {α : Type u_1} {β : Type u_2} {M : Type u_4} {N : Type u_5} [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` #

source
def Finsupp.zipWith {α : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [Zero M] [Zero N] [Zero O] (f : M → N → O) (hf : f 0 0 = 0) (g₁ : α →₀ M) (g₂ : α →₀ N) :
α →₀ O

Given finitely supported functions `g₁ : α →₀ M` and `g₂ : α →₀ N` and function `f : M → N → O`, `Finsupp.zipWith f hf g₁ g₂` is the finitely supported function `α →₀ O` 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)) ⋯

Instances For

source
@[simp]
theorem Finsupp.zipWith_apply {α : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [Zero M] [Zero N] [Zero O] {f : M → N → O} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} {a : α} :
(zipWith f hf g₁ g₂) a = f (g₁ a) (g₂ a)
source
theorem Finsupp.support_zipWith {α : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [Zero M] [Zero N] [Zero O] [D : DecidableEq α] {f : M → N → O} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} :
(zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support