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

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_1) (M : Type u_2) [inst : Zero M] :
Type (maxu_1u_2)
  • The support of a finitely supported function (aka Finsupp).

    support : Finset α
  • The underlying function of a bundled finitely supported function (aka Finsupp).

    toFun : αM
  • The witness that the support of a Finsupp is indeed the exact locus where its underlying function is nonzero.

    mem_support_toFun : ∀ (a : α), a support toFun a 0

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

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

    Basic declarations about Finsupp #

    instance Finsupp.funLike {α : Type u_1} {M : Type u_2} [inst : Zero M] :
    FunLike (α →₀ M) α fun x => M
    Equations
    • Finsupp.funLike = { coe := Finsupp.toFun, coe_injective' := (_ : ∀ ⦃a₁ a₂ : α →₀ M⦄, a₁.toFun = a₂.toFuna₁ = a₂) }
    instance Finsupp.coeFun {α : Type u_1} {M : Type u_2} [inst : Zero M] :
    CoeFun (α →₀ M) fun x => αM

    Helper instance for when there are too many metavariables to apply the FunLike instance directly.

    Equations
    • Finsupp.coeFun = inferInstance
    theorem Finsupp.ext {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {g : α →₀ M} (h : ∀ (a : α), f a = g a) :
    f = g
    theorem Finsupp.ext_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {g : α →₀ M} :
    f = g ∀ (a : α), f a = g a
    theorem Finsupp.coeFn_inj {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {g : α →₀ M} :
    f = g f = g
    theorem Finsupp.coeFn_injective {α : Type u_2} {M : Type u_1} [inst : Zero M] :
    Function.Injective FunLike.coe
    theorem Finsupp.congr_fun {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {g : α →₀ M} (h : f = g) (a : α) :
    f a = g a
    @[simp]
    theorem Finsupp.coe_mk {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : αM) (s : Finset α) (h : ∀ (a : α), a s f a 0) :
    { support := s, toFun := f, mem_support_toFun := h } = f
    instance Finsupp.zero {α : Type u_1} {M : Type u_2} [inst : Zero M] :
    Zero (α →₀ M)
    Equations
    • Finsupp.zero = { zero := { support := , toFun := 0, mem_support_toFun := (_ : ∀ (x : α), x OfNat.ofNat (αM) 0 Zero.toOfNat0 x 0) } }
    @[simp]
    theorem Finsupp.coe_zero {α : Type u_1} {M : Type u_2} [inst : Zero M] :
    0 = 0
    theorem Finsupp.zero_apply {α : Type u_2} {M : Type u_1} [inst : Zero M] {a : α} :
    0 a = 0
    @[simp]
    theorem Finsupp.support_zero {α : Type u_1} {M : Type u_2} [inst : Zero M] :
    0.support =
    instance Finsupp.inhabited {α : Type u_1} {M : Type u_2} [inst : Zero M] :
    Equations
    • Finsupp.inhabited = { default := 0 }
    @[simp]
    theorem Finsupp.mem_support_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {a : α} :
    a f.support f a 0
    @[simp]
    theorem Finsupp.fun_support_eq {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M) :
    Function.support f = f.support
    theorem Finsupp.not_mem_support_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {a : α} :
    ¬a f.support f a = 0
    @[simp]
    theorem Finsupp.coe_eq_zero {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} :
    f = 0 f = 0
    theorem Finsupp.ext_iff' {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {g : α →₀ M} :
    f = g f.support = g.support ∀ (x : α), x f.supportf x = g x
    @[simp]
    theorem Finsupp.support_eq_empty {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} :
    f.support = f = 0
    theorem Finsupp.support_nonempty_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} :
    Finset.Nonempty f.support f 0
    theorem Finsupp.nonzero_iff_exists {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} :
    f 0 a, f a 0
    theorem Finsupp.card_support_eq_zero {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} :
    Finset.card f.support = 0 f = 0
    instance Finsupp.decidableEq {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : DecidableEq α] [inst : DecidableEq M] :
    Equations
    theorem Finsupp.finite_support {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M) :
    theorem Finsupp.support_subset_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : α →₀ M} :
    f.support s ∀ (a : α), ¬a sf a = 0
    @[simp]
    theorem Finsupp.equivFunOnFinite_symm_apply_support {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : Finite α] (f : αM) :
    (↑(Equiv.symm Finsupp.equivFunOnFinite) f).support = Set.Finite.toFinset (_ : Set.Finite (Function.support f))
    @[simp]
    theorem Finsupp.equivFunOnFinite_symm_apply_toFun {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : Finite α] (f : αM) :
    ∀ (a : α), ↑(↑(Equiv.symm Finsupp.equivFunOnFinite) f) a = f a
    @[simp]
    theorem Finsupp.equivFunOnFinite_apply {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : Finite α] :
    ∀ (a : α →₀ M) (a_1 : α), Finsupp.equivFunOnFinite a a_1 = a a_1
    def Finsupp.equivFunOnFinite {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : Finite α] :
    (α →₀ M) (αM)

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

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Finsupp.equivFunOnFinite_symm_coe {M : Type u_2} [inst : Zero M] {α : Type u_1} [inst : Finite α] (f : α →₀ M) :
    ↑(Equiv.symm Finsupp.equivFunOnFinite) f = f
    @[simp]
    theorem Equiv.finsuppUnique_apply {M : Type u_1} [inst : Zero M] {ι : Type u_2} [inst : Unique ι] :
    ∀ (a : ι →₀ M), Equiv.finsuppUnique a = a default
    @[simp]
    theorem Equiv.finsuppUnique_symm_apply_support_val {M : Type u_1} [inst : Zero M] {ι : Type u_2} [inst : Unique ι] :
    ∀ (a : M), (↑(Equiv.symm Equiv.finsuppUnique) a).support.val = Multiset.map Subtype.val Finset.univ.val
    @[simp]
    theorem Equiv.finsuppUnique_symm_apply_toFun {M : Type u_1} [inst : Zero M] {ι : Type u_2} [inst : Unique ι] :
    ∀ (a : M) (a_1 : ι), ↑(↑(Equiv.symm Equiv.finsuppUnique) a) a_1 = ↑(Equiv.symm (Equiv.funUnique ι M)) a a_1
    noncomputable def Equiv.finsuppUnique {M : Type u_1} [inst : Zero M] {ι : Type u_2} [inst : Unique ι] :
    (ι →₀ M) M

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

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

    Declarations about single #

    def Finsupp.single {α : Type u_1} {M : Type u_2} [inst : Zero M] (a : α) (b : M) :
    α →₀ M

    single a b is the finitely supported function with value b at a and zero otherwise.

    Equations
    theorem Finsupp.single_apply {α : Type u_1} {M : Type u_2} [inst : Zero M] {a : α} {a' : α} {b : M} [inst : Decidable (a = a')] :
    ↑(Finsupp.single a b) a' = if a = a' then b else 0
    theorem Finsupp.single_apply_left {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] {f : αβ} (hf : Function.Injective f) (x : α) (z : α) (y : M) :
    ↑(Finsupp.single (f x) y) (f z) = ↑(Finsupp.single x y) z
    theorem Finsupp.single_eq_set_indicator {α : Type u_1} {M : Type u_2} [inst : Zero M] {a : α} {b : M} :
    ↑(Finsupp.single a b) = Set.indicator {a} fun x => b
    @[simp]
    theorem Finsupp.single_eq_same {α : Type u_2} {M : Type u_1} [inst : Zero M] {a : α} {b : M} :
    ↑(Finsupp.single a b) a = b
    @[simp]
    theorem Finsupp.single_eq_of_ne {α : Type u_1} {M : Type u_2} [inst : Zero M] {a : α} {a' : α} {b : M} (h : a a') :
    ↑(Finsupp.single a b) a' = 0
    theorem Finsupp.single_eq_update {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : DecidableEq α] (a : α) (b : M) :
    theorem Finsupp.single_eq_pi_single {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : DecidableEq α] (a : α) (b : M) :
    @[simp]
    theorem Finsupp.single_zero {α : Type u_1} {M : Type u_2} [inst : Zero M] (a : α) :
    theorem Finsupp.single_of_single_apply {α : Type u_1} {M : Type u_2} [inst : Zero M] (a : α) (a' : α) (b : M) :
    theorem Finsupp.support_single_ne_zero {α : Type u_2} {M : Type u_1} [inst : Zero M] {b : M} (a : α) (hb : b 0) :
    (Finsupp.single a b).support = {a}
    theorem Finsupp.support_single_subset {α : Type u_1} {M : Type u_2} [inst : Zero M] {a : α} {b : M} :
    (Finsupp.single a b).support {a}
    theorem Finsupp.single_apply_mem {α : Type u_2} {M : Type u_1} [inst : Zero M] {a : α} {b : M} (x : α) :
    ↑(Finsupp.single a b) x {0, b}
    theorem Finsupp.range_single_subset {α : Type u_2} {M : Type u_1} [inst : Zero M] {a : α} {b : M} :
    Set.range ↑(Finsupp.single a b) {0, b}
    theorem Finsupp.single_injective {α : Type u_2} {M : Type u_1} [inst : Zero M] (a : α) :

    Finsupp.single a b is injective in b. For the statement that it is injective in a, see Finsupp.single_left_injective

    theorem Finsupp.single_apply_eq_zero {α : Type u_2} {M : Type u_1} [inst : Zero M] {a : α} {x : α} {b : M} :
    ↑(Finsupp.single a b) x = 0 x = ab = 0
    theorem Finsupp.single_apply_ne_zero {α : Type u_2} {M : Type u_1} [inst : Zero M] {a : α} {x : α} {b : M} :
    ↑(Finsupp.single a b) x 0 x = a b 0
    theorem Finsupp.mem_support_single {α : Type u_1} {M : Type u_2} [inst : Zero M] (a : α) (a' : α) (b : M) :
    a (Finsupp.single a' b).support a = a' b 0
    theorem Finsupp.eq_single_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {a : α} {b : M} :
    f = Finsupp.single a b f.support {a} f a = b
    theorem Finsupp.single_eq_single_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] (a₁ : α) (a₂ : α) (b₁ : M) (b₂ : M) :
    Finsupp.single a₁ b₁ = Finsupp.single a₂ b₂ a₁ = a₂ b₁ = b₂ b₁ = 0 b₂ = 0
    theorem Finsupp.single_left_injective {α : Type u_2} {M : Type u_1} [inst : Zero M] {b : M} (h : b 0) :

    Finsupp.single a b is injective in a. For the statement that it is injective in b, see Finsupp.single_injective

    theorem Finsupp.single_left_inj {α : Type u_2} {M : Type u_1} [inst : Zero M] {a : α} {a' : α} {b : M} (h : b 0) :
    theorem Finsupp.support_single_ne_bot {α : Type u_2} {M : Type u_1} [inst : Zero M] {b : M} (i : α) (h : b 0) :
    (Finsupp.single i b).support
    theorem Finsupp.support_single_disjoint {α : Type u_2} {M : Type u_1} [inst : Zero M] {b : M} {b' : M} (hb : b 0) (hb' : b' 0) {i : α} {j : α} :
    Disjoint (Finsupp.single i b).support (Finsupp.single j b').support i j
    @[simp]
    theorem Finsupp.single_eq_zero {α : Type u_1} {M : Type u_2} [inst : Zero M] {a : α} {b : M} :
    Finsupp.single a b = 0 b = 0
    theorem Finsupp.single_swap {α : Type u_2} {M : Type u_1} [inst : Zero M] (a₁ : α) (a₂ : α) (b : M) :
    ↑(Finsupp.single a₁ b) a₂ = ↑(Finsupp.single a₂ b) a₁
    instance Finsupp.nontrivial {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : Nonempty α] [inst : Nontrivial M] :
    Equations
    theorem Finsupp.unique_single {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : Unique α] (x : α →₀ M) :
    x = Finsupp.single default (x default)
    @[simp]
    theorem Finsupp.unique_single_eq_iff {α : Type u_1} {M : Type u_2} [inst : Zero M] {a : α} {a' : α} {b : M} [inst : Unique α] {b' : M} :
    theorem Finsupp.support_eq_singleton {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {a : α} :
    f.support = {a} f a 0 f = Finsupp.single a (f a)
    theorem Finsupp.support_eq_singleton' {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {a : α} :
    f.support = {a} b x, f = Finsupp.single a b
    theorem Finsupp.card_support_eq_one {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} :
    Finset.card f.support = 1 a, f a 0 f = Finsupp.single a (f a)
    theorem Finsupp.card_support_eq_one' {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} :
    Finset.card f.support = 1 a b x, f = Finsupp.single a b
    theorem Finsupp.support_subset_singleton {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {a : α} :
    f.support {a} f = Finsupp.single a (f a)
    theorem Finsupp.support_subset_singleton' {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {a : α} :
    f.support {a} b, f = Finsupp.single a b
    theorem Finsupp.card_support_le_one {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : Nonempty α] {f : α →₀ M} :
    Finset.card f.support 1 a, f = Finsupp.single a (f a)
    theorem Finsupp.card_support_le_one' {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : Nonempty α] {f : α →₀ M} :
    Finset.card f.support 1 a b, f = Finsupp.single a b
    @[simp]
    theorem Finsupp.equivFunOnFinite_single {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : DecidableEq α] [inst : Finite α] (x : α) (m : M) :
    Finsupp.equivFunOnFinite (Finsupp.single x m) = Pi.single x m
    @[simp]
    theorem Finsupp.equivFunOnFinite_symm_single {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : DecidableEq α] [inst : Finite α] (x : α) (m : M) :
    ↑(Equiv.symm Finsupp.equivFunOnFinite) (Pi.single x m) = Finsupp.single x m

    Declarations about update #

    def Finsupp.update {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M) (a : α) (b : M) :
    α →₀ M

    Replace the value of a α →₀ M at a given point a : α by a given value b : M. If b = 0, this amounts to removing a from the Finsupp.support. Otherwise, if a was not in the Finsupp.support, it is added to it.

    This is the finitely-supported version of Function.update.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Finsupp.coe_update {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M) (a : α) (b : M) [inst : DecidableEq α] :
    ↑(Finsupp.update f a b) = Function.update (f) a b
    @[simp]
    theorem Finsupp.update_self {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M) (a : α) :
    Finsupp.update f a (f a) = f
    @[simp]
    theorem Finsupp.zero_update {α : Type u_1} {M : Type u_2} [inst : Zero M] (a : α) (b : M) :
    theorem Finsupp.support_update {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M) (a : α) (b : M) [inst : DecidableEq α] [inst : DecidableEq M] :
    (Finsupp.update f a b).support = if b = 0 then Finset.erase f.support a else insert a f.support
    @[simp]
    theorem Finsupp.support_update_zero {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M) (a : α) [inst : DecidableEq α] :
    (Finsupp.update f a 0).support = Finset.erase f.support a
    theorem Finsupp.support_update_ne_zero {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M) (a : α) {b : M} [inst : DecidableEq α] (h : b 0) :
    (Finsupp.update f a b).support = insert a f.support

    Declarations about erase #

    def Finsupp.erase {α : Type u_1} {M : Type u_2} [inst : Zero M] (a : α) (f : α →₀ M) :
    α →₀ M

    erase a f is the finitely supported function equal to f except at a where it is equal to 0. If a is not in the support of f then erase a f = f.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Finsupp.support_erase {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst : DecidableEq α] {a : α} {f : α →₀ M} :
    (Finsupp.erase a f).support = Finset.erase f.support a
    @[simp]
    theorem Finsupp.erase_same {α : Type u_1} {M : Type u_2} [inst : Zero M] {a : α} {f : α →₀ M} :
    ↑(Finsupp.erase a f) a = 0
    @[simp]
    theorem Finsupp.erase_ne {α : Type u_1} {M : Type u_2} [inst : Zero M] {a : α} {a' : α} {f : α →₀ M} (h : a' a) :
    ↑(Finsupp.erase a f) a' = f a'
    @[simp]
    theorem Finsupp.erase_single {α : Type u_1} {M : Type u_2} [inst : Zero M] {a : α} {b : M} :
    theorem Finsupp.erase_single_ne {α : Type u_1} {M : Type u_2} [inst : Zero M] {a : α} {a' : α} {b : M} (h : a a') :
    @[simp]
    theorem Finsupp.erase_of_not_mem_support {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : α →₀ M} {a : α} (haf : ¬a f.support) :
    @[simp]
    theorem Finsupp.erase_zero {α : Type u_1} {M : Type u_2} [inst : Zero M] (a : α) :

    Declarations about onFinset #

    def Finsupp.onFinset {α : Type u_1} {M : Type u_2} [inst : 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
    @[simp]
    theorem Finsupp.onFinset_apply {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Finset α} {f : αM} {hf : ∀ (a : α), f a 0a s} {a : α} :
    ↑(Finsupp.onFinset s f hf) a = f a
    @[simp]
    theorem Finsupp.support_onFinset_subset {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Finset α} {f : αM} {hf : ∀ (a : α), f a 0a s} :
    (Finsupp.onFinset s f hf).support s
    theorem Finsupp.mem_support_onFinset {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Finset α} {f : αM} (hf : ∀ (a : α), f a 0a s) {a : α} :
    a (Finsupp.onFinset s f hf).support f a 0
    theorem Finsupp.support_onFinset {α : Type u_2} {M : Type u_1} [inst : Zero M] [inst : DecidableEq M] {s : Finset α} {f : αM} (hf : ∀ (a : α), f a 0a 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_2} [inst : Zero M] (f : αM) (hf : Set.Finite (Function.support f)) :
    α →₀ M

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

    Equations
    theorem Finsupp.ofSupportFinite_coe {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : αM} {hf : Set.Finite (Function.support f)} :
    instance Finsupp.canLift {α : Type u_1} {M : Type u_2} [inst : Zero M] :
    CanLift (αM) (α →₀ M) FunLike.coe fun f => Set.Finite (Function.support f)
    Equations

    Declarations about mapRange #

    def Finsupp.mapRange {α : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Zero M] [inst : 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 Data/Finsupp/Basic):

    • Finsupp.mapRange.equiv
    • Finsupp.mapRange.zeroHom
    • Finsupp.mapRange.addMonoidHom
    • Finsupp.mapRange.addEquiv
    • Finsupp.mapRange.linearMap
    • Finsupp.mapRange.linearEquiv
    Equations
    @[simp]
    theorem Finsupp.mapRange_apply {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst : Zero N] {f : MN} {hf : f 0 = 0} {g : α →₀ M} {a : α} :
    ↑(Finsupp.mapRange f hf g) a = f (g a)
    @[simp]
    theorem Finsupp.mapRange_zero {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst : Zero N] {f : MN} {hf : f 0 = 0} :
    @[simp]
    theorem Finsupp.mapRange_id {α : Type u_1} {M : Type u_2} [inst : Zero M] (g : α →₀ M) :
    Finsupp.mapRange id (_ : id 0 = id 0) g = g
    theorem Finsupp.mapRange_comp {α : Type u_4} {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : Zero M] [inst : Zero N] [inst : Zero P] (f : NP) (hf : f 0 = 0) (f₂ : MN) (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)
    theorem Finsupp.support_mapRange {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst : Zero N] {f : MN} {hf : f 0 = 0} {g : α →₀ M} :
    (Finsupp.mapRange f hf g).support g.support
    @[simp]
    theorem Finsupp.mapRange_single {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst : Zero N] {f : MN} {hf : f 0 = 0} {a : α} {b : M} :
    theorem Finsupp.support_mapRange_of_injective {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst : Zero N] {e : MN} (he0 : e 0 = 0) (f : ι →₀ M) (he : Function.Injective e) :
    (Finsupp.mapRange e he0 f).support = f.support

    Declarations about embDomain #

    def Finsupp.embDomain {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : 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_3} [inst : 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_3} [inst : Zero M] (f : α β) :
    @[simp]
    theorem Finsupp.embDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : 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_3} [inst : 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_3} [inst : Zero M] (f : α β) :
    @[simp]
    theorem Finsupp.embDomain_inj {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] {f : α β} {l₁ : α →₀ M} {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_3} [inst : Zero M] {f : α β} {l : α →₀ M} :
    theorem Finsupp.embDomain_mapRange {α : Type u_1} {β : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst : Zero N] (f : α β) (g : MN) (p : α →₀ M) (hg : g 0 = 0) :
    theorem Finsupp.single_of_embDomain_single {α : Type u_1} {β : Type u_3} {M : Type u_2} [inst : Zero M] (l : α →₀ M) (f : α β) (a : β) (b : M) (hb : b 0) (h : Finsupp.embDomain f l = Finsupp.single a b) :
    x, l = Finsupp.single x b f x = a
    @[simp]
    theorem Finsupp.embDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] (f : α β) (a : α) (m : M) :

    Declarations about zipWith #

    def Finsupp.zipWith {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : Zero M] [inst : Zero N] [inst : 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
    @[simp]
    theorem Finsupp.zipWith_apply {α : Type u_4} {M : Type u_2} {N : Type u_3} {P : Type u_1} [inst : Zero M] [inst : Zero N] [inst : Zero P] {f : MNP} {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_3} {N : Type u_4} {P : Type u_2} [inst : Zero M] [inst : Zero N] [inst : Zero P] [D : DecidableEq α] {f : MNP} {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.add {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] :
    Add (α →₀ M)
    Equations
    @[simp]
    theorem Finsupp.coe_add {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (f : α →₀ M) (g : α →₀ M) :
    ↑(f + g) = f + g
    theorem Finsupp.add_apply {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (g₁ : α →₀ M) (g₂ : α →₀ M) (a : α) :
    ↑(g₁ + g₂) a = g₁ a + g₂ a
    theorem Finsupp.support_add {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] [inst : DecidableEq α] {g₁ : α →₀ M} {g₂ : α →₀ M} :
    (g₁ + g₂).support g₁.support g₂.support
    theorem Finsupp.support_add_eq {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] [inst : DecidableEq α] {g₁ : α →₀ M} {g₂ : α →₀ M} (h : Disjoint g₁.support g₂.support) :
    (g₁ + g₂).support = g₁.support g₂.support
    @[simp]
    theorem Finsupp.single_add {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (a : α) (b₁ : M) (b₂ : M) :
    Finsupp.single a (b₁ + b₂) = Finsupp.single a b₁ + Finsupp.single a b₂
    instance Finsupp.addZeroClass {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] :
    Equations
    @[simp]
    theorem Finsupp.singleAddHom_apply {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (a : α) (b : M) :
    def Finsupp.singleAddHom {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (a : α) :
    M →+ α →₀ M

    Finsupp.single as an AddMonoidHom.

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

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Finsupp.applyAddHom_apply {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (a : α) (g : α →₀ M) :
    ↑(Finsupp.applyAddHom a) g = g a
    def Finsupp.applyAddHom {α : Type u_1} {M : Type u_2} [inst : 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 = { toZeroHom := { toFun := fun g => g a, map_zero' := (_ : 0 a = 0) }, map_add' := (_ : ∀ (x x_1 : α →₀ M), ↑(x + x_1) a = x a + x_1 a) }
    @[simp]
    theorem Finsupp.coeFnAddHom_apply {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] :
    ∀ (a : α →₀ M) (a_1 : α), Finsupp.coeFnAddHom a a_1 = a a_1
    noncomputable def Finsupp.coeFnAddHom {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] :
    (α →₀ M) →+ αM

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

    Equations
    • Finsupp.coeFnAddHom = { toZeroHom := { toFun := FunLike.coe, map_zero' := (_ : 0 = 0) }, map_add' := (_ : ∀ (f g : α →₀ M), ↑(f + g) = f + g) }
    theorem Finsupp.update_eq_single_add_erase {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (f : α →₀ M) (a : α) (b : M) :
    theorem Finsupp.update_eq_erase_add_single {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (f : α →₀ M) (a : α) (b : M) :
    theorem Finsupp.single_add_erase {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (a : α) (f : α →₀ M) :
    Finsupp.single a (f a) + Finsupp.erase a f = f
    theorem Finsupp.erase_add_single {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (a : α) (f : α →₀ M) :
    Finsupp.erase a f + Finsupp.single a (f a) = f
    @[simp]
    theorem Finsupp.erase_add {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (a : α) (f : α →₀ M) (f' : α →₀ M) :
    @[simp]
    theorem Finsupp.eraseAddHom_apply {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (a : α) (f : α →₀ M) :
    def Finsupp.eraseAddHom {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (a : α) :
    (α →₀ M) →+ α →₀ M

    Finsupp.erase as an AddMonoidHom.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem Finsupp.induction {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : (a : α) → (b : M) → (f : α →₀ M) → ¬a f.supportb 0p fp (Finsupp.single a b + f)) :
    p f
    theorem Finsupp.induction₂ {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : (a : α) → (b : M) → (f : α →₀ M) → ¬a f.supportb 0p fp (f + Finsupp.single a b)) :
    p f
    theorem Finsupp.induction_linear {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (hadd : (f g : α →₀ M) → p fp gp (f + g)) (hsingle : (a : α) → (b : M) → p (Finsupp.single a b)) :
    p f
    @[simp]
    theorem Finsupp.add_closure_setOf_eq_single {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] :
    AddSubmonoid.closure { f | a b, f = Finsupp.single a b } =
    theorem Finsupp.addHom_ext {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] ⦃f : (α →₀ M) →+ N ⦃g : (α →₀ M) →+ N (H : ∀ (x : α) (y : M), f (Finsupp.single x y) = g (Finsupp.single x y)) :
    f = g

    If two additive homomorphisms from α →₀ M are equal on each single a b, then they are equal.

    theorem Finsupp.addHom_ext' {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] ⦃f : (α →₀ M) →+ N ⦃g : (α →₀ M) →+ N (H : ∀ (x : α), AddMonoidHom.comp f (Finsupp.singleAddHom x) = AddMonoidHom.comp g (Finsupp.singleAddHom x)) :
    f = g

    If two additive homomorphisms from α →₀ M are equal on each single a b, then they are equal.

    We formulate this using equality of AddMonoidHoms so that ext tactic can apply a type-specific extensionality lemma after this one. E.g., if the fiber M is or , then it suffices to verify f (single a 1) = g (single a 1).

    theorem Finsupp.mulHom_ext {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : MulOneClass N] ⦃f : Multiplicative (α →₀ M) →* N ⦃g : Multiplicative (α →₀ M) →* N (H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (Finsupp.single x y)) = g (Multiplicative.ofAdd (Finsupp.single x y))) :
    f = g
    theorem Finsupp.mulHom_ext' {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : MulOneClass N] {f : Multiplicative (α →₀ M) →* N} {g : Multiplicative (α →₀ M) →* N} (H : ∀ (x : α), MonoidHom.comp f (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) = MonoidHom.comp g (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))) :
    f = g
    theorem Finsupp.mapRange_add {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {f : MN} {hf : f 0 = 0} (hf' : ∀ (x y : M), f (x + y) = f x + f y) (v₁ : α →₀ M) (v₂ : α →₀ M) :
    Finsupp.mapRange f hf (v₁ + v₂) = Finsupp.mapRange f hf v₁ + Finsupp.mapRange f hf v₂
    theorem Finsupp.mapRange_add' {α : Type u_4} {β : Type u_2} {M : Type u_3} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddMonoidHomClass β M N] {f : β} (v₁ : α →₀ M) (v₂ : α →₀ M) :
    Finsupp.mapRange f (_ : f 0 = 0) (v₁ + v₂) = Finsupp.mapRange f (_ : f 0 = 0) v₁ + Finsupp.mapRange f (_ : f 0 = 0) v₂
    @[simp]
    theorem Finsupp.embDomain.addMonoidHom_apply {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : AddZeroClass M] (f : α β) (v : α →₀ M) :
    def Finsupp.embDomain.addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : AddZeroClass M] (f : α β) :
    (α →₀ M) →+ β →₀ M

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

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Finsupp.embDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : AddZeroClass M] (f : α β) (v : α →₀ M) (w : α →₀ M) :
    instance Finsupp.hasNatScalar {α : Type u_1} {M : Type u_2} [inst : 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
    instance Finsupp.addMonoid {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] :
    Equations
    • One or more equations did not get rendered due to their size.
    instance Finsupp.addCommMonoid {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] :
    Equations
    • One or more equations did not get rendered due to their size.
    instance Finsupp.neg {α : Type u_1} {G : Type u_2} [inst : NegZeroClass G] :
    Neg (α →₀ G)
    Equations
    @[simp]
    theorem Finsupp.coe_neg {α : Type u_2} {G : Type u_1} [inst : NegZeroClass G] (g : α →₀ G) :
    ↑(-g) = -g
    theorem Finsupp.neg_apply {α : Type u_2} {G : Type u_1} [inst : NegZeroClass G] (g : α →₀ G) (a : α) :
    ↑(-g) a = -g a
    theorem Finsupp.mapRange_neg {α : Type u_3} {G : Type u_1} {H : Type u_2} [inst : NegZeroClass G] [inst : NegZeroClass H] {f : GH} {hf : f 0 = 0} (hf' : ∀ (x : G), f (-x) = -f x) (v : α →₀ G) :
    theorem Finsupp.mapRange_neg' {α : Type u_4} {β : Type u_3} {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst : SubtractionMonoid H] [inst : AddMonoidHomClass β G H] {f : β} (v : α →₀ G) :
    Finsupp.mapRange f (_ : f 0 = 0) (-v) = -Finsupp.mapRange f (_ : f 0 = 0) v
    instance Finsupp.sub {α : Type u_1} {G : Type u_2} [inst : SubNegZeroMonoid G] :
    Sub (α →₀ G)
    Equations
    @[simp]
    theorem Finsupp.coe_sub {α : Type u_2} {G : Type u_1} [inst : SubNegZeroMonoid G] (g₁ : α →₀ G) (g₂ : α →₀ G) :
    ↑(g₁ - g₂) = g₁ - g₂
    theorem Finsupp.sub_apply {α : Type u_2} {G : Type u_1} [inst : SubNegZeroMonoid G] (g₁ : α →₀ G) (g₂ : α →₀ G) (a : α) :
    ↑(g₁ - g₂) a = g₁ a - g₂ a
    theorem Finsupp.mapRange_sub {α : Type u_3} {G : Type u_1} {H : Type u_2} [inst : SubNegZeroMonoid G] [inst : SubNegZeroMonoid H] {f : GH} {hf : f 0 = 0} (hf' : ∀ (x y : G), f (x - y) = f x - f y) (v₁ : α →₀ G) (v₂ : α →₀ G) :
    Finsupp.mapRange f hf (v₁ - v₂) = Finsupp.mapRange f hf v₁ - Finsupp.mapRange f hf v₂
    theorem Finsupp.mapRange_sub' {α : Type u_4} {β : Type u_3} {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst : SubtractionMonoid H] [inst : AddMonoidHomClass β G H] {f : β} (v₁ : α →₀ G) (v₂ : α →₀ G) :
    Finsupp.mapRange f (_ : f 0 = 0) (v₁ - v₂) = Finsupp.mapRange f (_ : f 0 = 0) v₁ - Finsupp.mapRange f (_ : f 0 = 0) v₂
    instance Finsupp.hasIntScalar {α : Type u_1} {G : Type u_2} [inst : 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
    instance Finsupp.addGroup {α : Type u_1} {G : Type u_2} [inst : AddGroup G] :
    Equations
    • One or more equations did not get rendered due to their size.
    instance Finsupp.addCommGroup {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] :
    Equations
    • One or more equations did not get rendered due to their size.
    theorem Finsupp.single_add_single_eq_single_add_single {α : Type u_2} {M : Type u_1} [inst : AddCommMonoid M] {k : α} {l : α} {m : α} {n : α} {u : M} {v : M} (hu : u 0) (hv : v 0) :
    Finsupp.single k u + Finsupp.single l v = Finsupp.single m u + Finsupp.single n v k = m l = n u = v k = n l = m u + v = 0 k = l m = n
    @[simp]
    theorem Finsupp.support_neg {α : Type u_2} {G : Type u_1} [inst : AddGroup G] (f : α →₀ G) :
    (-f).support = f.support
    theorem Finsupp.support_sub {α : Type u_1} {G : Type u_2} [inst : DecidableEq α] [inst : AddGroup G] {f : α →₀ G} {g : α →₀ G} :
    (f - g).support f.support g.support
    theorem Finsupp.erase_eq_sub_single {α : Type u_2} {G : Type u_1} [inst : AddGroup G] (f : α →₀ G) (a : α) :
    Finsupp.erase a f = f - Finsupp.single a (f a)
    theorem Finsupp.update_eq_sub_add_single {α : Type u_2} {G : Type u_1} [inst : AddGroup G] (f : α →₀ G) (a : α) (b : G) :