Documentation

Mathlib.Data.Finsupp.Defs

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:

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

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

Notations #

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

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

Implementation notes #

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

TODO #

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.

Instances For

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

    Equations
      Instances For

        Basic declarations about Finsupp #

        instance Finsupp.instFunLike {α : Type u_1} {M : Type u_5} [Zero M] :
        FunLike (α →₀ M) α M
        Equations
          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
            @[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] :
            instance Finsupp.instInhabited {α : Type u_1} {M : Type u_5} [Zero M] :
            Equations
              @[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) :
              theorem Finsupp.notMem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
              af.support f a = 0
              @[deprecated Finsupp.notMem_support_iff (since := "2025-05-23")]
              theorem Finsupp.not_mem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
              af.support f a = 0

              Alias of Finsupp.notMem_support_iff.

              @[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 xf.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} :
              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] :
              Equations
                theorem Finsupp.finite_support {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) :
                theorem Finsupp.support_subset_iff {α : Type u_1} {M : Type u_5} [Zero M] {s : Set α} {f : α →₀ M} :
                f.support s as, 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
                  Instances For
                    @[simp]
                    theorem Finsupp.equivFunOnFinite_symm_apply_support {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (f : αM) :
                    @[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_apply {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (a✝ : α →₀ M) (a : α) :
                    equivFunOnFinite a✝ a = a✝ a
                    @[simp]
                    theorem Finsupp.equivFunOnFinite_symm_coe {M : Type u_5} [Zero M] {α : Type u_13} [Finite α] (f : α →₀ M) :
                    @[simp]
                    theorem Finsupp.coe_equivFunOnFinite_symm {M : Type u_5} [Zero M] {α : Type u_13} [Finite α] (f : αM) :
                    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
                      Instances For
                        @[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_apply {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] (a✝ : ι →₀ M) :
                        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} :

                        Declarations about onFinset #

                        def Finsupp.onFinset {α : Type u_1} {M : Type u_5} [Zero M] (s : Finset α) (f : αM) (hf : ∀ (a : α), f a 0a 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
                          Instances For
                            @[simp]
                            theorem Finsupp.coe_onFinset {α : Type u_1} {M : Type u_5} [Zero M] (s : Finset α) (f : αM) (hf : ∀ (a : α), f a 0a 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 0a 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 0a s) :
                            (onFinset s f hf).support = {as | 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 0a 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 0a 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
                              Instances For
                                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 : MN) (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
                                  Instances For
                                    @[simp]
                                    theorem Finsupp.mapRange_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : MN} {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 : MN} {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 : NP) (hf : f 0 = 0) (f₂ : MN) (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₁ : NP) (e₂ : MN) (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 : MN} {hf : f 0 = 0} {g : α →₀ M} :
                                    theorem Finsupp.support_mapRange_of_injective {ι : Type u_4} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {e : MN} (he0 : e 0 = 0) (f : ι →₀ M) (he : Function.Injective e) :
                                    theorem Finsupp.range_mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (e : MN) (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 : MN) (he₀ : e 0 = 0) (he : Function.Injective e) :

                                    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 : MN) (he₀ : e 0 = 0) (he : Function.Surjective e) :

                                    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
                                      Instances For
                                        @[simp]
                                        theorem Finsupp.support_embDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (v : α →₀ M) :
                                        @[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 : aSet.range f) :
                                        (embDomain f v) a = 0
                                        theorem Finsupp.embDomain_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (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 : MN) (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 : MNP) (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
                                          Instances For
                                            @[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 : MNP} {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 : MNP} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} :
                                            (zipWith f hf g₁ g₂).support g₁.support g₂.support