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.total : (ι → 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.single: The Finsupp which is nonzero in exactly one point.
• Finsupp.update: Changes one value of a Finsupp.
• Finsupp.erase: Replaces one value of a Finsupp by 0.
• 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)

• 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 ∈ s.support ↔ Finsupp.toFun s a ≠ 0

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

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

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.

Basic declarations about Finsupp

instance Finsupp.funLike {α : Type u_1} {M : Type u_5} [Zero M] : FunLike (α →₀ M) α fun x => M

instance Finsupp.coeFun {α : Type u_1} {M : Type u_5} [Zero M] : CoeFun (α →₀ M) fun x => α → M

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

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

@[deprecated FunLike.ext_iff]

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

@[deprecated FunLike.coe_fn_eq]

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

@[deprecated FunLike.coe_injective]

theorem Finsupp.coeFn_injective {α : Type u_1} {M : Type u_5} [Zero M] : Function.Injective FunLike.coe

@[deprecated FunLike.congr_fun]

theorem Finsupp.congr_fun {α : Type u_1} {M : Type u_5} [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_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.zero {α : Type u_1} {M : Type u_5} [Zero M] : Zero (α →₀ M)

@[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] : 0.support = ∅

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

@[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 : α →₀ M} {g : α →₀ M} : f = g ↔ f.support = g.support ∧ ∀ (x : α), 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} : Finset.Nonempty f.support ↔ f ≠ 0

theorem Finsupp.nonzero_iff_exists {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} : f ≠ 0 ↔ ∃ a, ↑f a ≠ 0

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

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

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

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

@[simp]

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

@[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_1 : α), ↑Finsupp.equivFunOnFinite a a_1 = ↑a a_1

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

@[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 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

@[simp]

theorem Equiv.finsuppUnique_symm_apply_toFun {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] : ∀ (a : M) (a_1 : ι), ↑(↑Equiv.finsuppUnique.symm a) a_1 = ↑(Equiv.funUnique ι M).symm a a_1

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

theorem Finsupp.unique_ext {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] {f : α →₀ M} {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 : α →₀ M} {g : α →₀ M} : f = g ↔ ↑f default = ↑g default

Declarations about single

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

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

theorem Finsupp.single_apply {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} [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_5} [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_5} [Zero M] {a : α} {b : M} : ↑(Finsupp.single a b) = Set.indicator {a} fun x => b

@[simp]

theorem Finsupp.single_eq_same {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} : ↑(Finsupp.single a b) a = b

@[simp]

theorem Finsupp.single_eq_of_ne {α : Type u_1} {M : Type u_5} [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_5} [Zero M] [DecidableEq α] (a : α) (b : M) : ↑(Finsupp.single a b) = Function.update 0 a b

theorem Finsupp.single_eq_pi_single {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] (a : α) (b : M) : ↑(Finsupp.single a b) = Pi.single a b

@[simp]

theorem Finsupp.single_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) : Finsupp.single a 0 = 0

theorem Finsupp.single_of_single_apply {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (a' : α) (b : M) : Finsupp.single a (↑(Finsupp.single a' b) a) = ↑(Finsupp.single a' (Finsupp.single a' b)) a

theorem Finsupp.support_single_ne_zero {α : Type u_1} {M : Type u_5} [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_5} [Zero M] {a : α} {b : M} : (Finsupp.single a b).support ⊆ {a}

theorem Finsupp.single_apply_mem {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} (x : α) : ↑(Finsupp.single a b) x ∈ {0, b}

theorem Finsupp.range_single_subset {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} : Set.range ↑(Finsupp.single a b) ⊆ {0, b}

theorem Finsupp.single_injective {α : Type u_1} {M : Type u_5} [Zero M] (a : α) : Function.Injective (Finsupp.single 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_1} {M : Type u_5} [Zero M] {a : α} {x : α} {b : M} : ↑(Finsupp.single a b) x = 0 ↔ x = a → b = 0

theorem Finsupp.single_apply_ne_zero {α : Type u_1} {M : Type u_5} [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_5} [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_5} [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_5} [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_1} {M : Type u_5} [Zero M] {b : M} (h : b ≠ 0) : Function.Injective fun a => Finsupp.single a b

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_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} (h : b ≠ 0) : Finsupp.single a b = Finsupp.single a' b ↔ a = a'

theorem Finsupp.support_single_ne_bot {α : Type u_1} {M : Type u_5} [Zero M] {b : M} (i : α) (h : b ≠ 0) : (Finsupp.single i b).support ≠ ⊥

theorem Finsupp.support_single_disjoint {α : Type u_1} {M : Type u_5} [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_5} [Zero M] {a : α} {b : M} : Finsupp.single a b = 0 ↔ b = 0

theorem Finsupp.single_swap {α : Type u_1} {M : Type u_5} [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_5} [Zero M] [Nonempty α] [Nontrivial M] : Nontrivial (α →₀ M)

theorem Finsupp.unique_single {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] (x : α →₀ M) : x = Finsupp.single default (↑x default)

@[simp]

theorem Finsupp.unique_single_eq_iff {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} [Unique α] {b' : M} : Finsupp.single a b = Finsupp.single a' b' ↔ b = b'

theorem Finsupp.support_eq_singleton {α : Type u_1} {M : Type u_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [Zero M] [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_5} [Zero M] [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_5} [Zero M] [DecidableEq α] [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_5} [Zero M] [DecidableEq α] [Finite α] (x : α) (m : M) : ↑Finsupp.equivFunOnFinite.symm (Pi.single x m) = Finsupp.single x m

Declarations about update

def Finsupp.update {α : Type u_1} {M : Type u_5} [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.

@[simp]

theorem Finsupp.coe_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) [DecidableEq α] : ↑(Finsupp.update f a b) = Function.update (↑f) a b

@[simp]

theorem Finsupp.update_self {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) : Finsupp.update f a (↑f a) = f

@[simp]

theorem Finsupp.zero_update {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (b : M) : Finsupp.update 0 a b = Finsupp.single a b

theorem Finsupp.support_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) [DecidableEq α] [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_5} [Zero M] (f : α →₀ M) (a : α) [DecidableEq α] : (Finsupp.update f a 0).support = Finset.erase f.support a

theorem Finsupp.support_update_ne_zero {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) {b : M} [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_5} [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.

@[simp]

theorem Finsupp.support_erase {α : Type u_1} {M : Type u_5} [Zero M] [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_5} [Zero M] {a : α} {f : α →₀ M} : ↑(Finsupp.erase a f) a = 0

@[simp]

theorem Finsupp.erase_ne {α : Type u_1} {M : Type u_5} [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_5} [Zero M] {a : α} {b : M} : Finsupp.erase a (Finsupp.single a b) = 0

theorem Finsupp.erase_single_ne {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} (h : a ≠ a') : Finsupp.erase a (Finsupp.single a' b) = Finsupp.single a' b

@[simp]

theorem Finsupp.erase_of_not_mem_support {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} (haf : ¬a ∈ f.support) : Finsupp.erase a f = f

@[simp]

theorem Finsupp.erase_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) : Finsupp.erase a 0 = 0

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.

@[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 : Set.Finite (Function.support f)) : α →₀ M

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

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

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

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

@[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 (_ : id 0 = id 0) 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)

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

@[simp]

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

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

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.

@[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₁ : α →₀ 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_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)

theorem Finsupp.single_of_embDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [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_5} [Zero M] (f : α ↪ β) (a : α) (m : M) : Finsupp.embDomain f (Finsupp.single a m) = Finsupp.single (↑f a) m

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.

@[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.add {α : Type u_1} {M : Type u_5} [AddZeroClass M] : Add (α →₀ M)

@[simp]

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

theorem Finsupp.add_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (g₁ : α →₀ M) (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₁ : α →₀ M} {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₁ : α →₀ 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_5} [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_5} [AddZeroClass M] : AddZeroClass (α →₀ M)

@[simp]

theorem Finsupp.singleAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (b : M) : ↑(Finsupp.singleAddHom a) b = Finsupp.single a b

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

Finsupp.single as an AddMonoidHom.

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

@[simp]

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

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.

@[simp]

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

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.

theorem Finsupp.update_eq_single_add_erase {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (a : α) (b : M) : Finsupp.update f a b = Finsupp.single a b + Finsupp.erase a f

theorem Finsupp.update_eq_erase_add_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (a : α) (b : M) : Finsupp.update f a b = Finsupp.erase a f + Finsupp.single a b

theorem Finsupp.single_add_erase {α : Type u_1} {M : Type u_5} [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_5} [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_5} [AddZeroClass M] (a : α) (f : α →₀ M) (f' : α →₀ M) : Finsupp.erase a (f + f') = Finsupp.erase a f + Finsupp.erase a f'

@[simp]

theorem Finsupp.eraseAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) : ↑(Finsupp.eraseAddHom a) f = Finsupp.erase a f

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

Finsupp.erase as an AddMonoidHom.

theorem Finsupp.induction {α : Type u_1} {M : Type u_5} [AddZeroClass M] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : (a : α) → (b : M) → (f : α →₀ M) → ¬a ∈ f.support → b ≠ 0 → p f → p (Finsupp.single a b + f)) : p f

theorem Finsupp.induction₂ {α : Type u_1} {M : Type u_5} [AddZeroClass M] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : (a : α) → (b : M) → (f : α →₀ M) → ¬a ∈ f.support → b ≠ 0 → p f → p (f + Finsupp.single a b)) : p f

theorem Finsupp.induction_linear {α : Type u_1} {M : Type u_5} [AddZeroClass M] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (hadd : (f g : α →₀ M) → p f → p g → p (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_5} [AddZeroClass M] : AddSubmonoid.closure {f | ∃ a b, f = Finsupp.single a b} = ⊤

theorem Finsupp.addHom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [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_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [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_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [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_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [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_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₁ : α →₀ 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_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] [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_5} [AddZeroClass M] (f : α ↪ β) (v : α →₀ M) : ↑(Finsupp.embDomain.addMonoidHom f) v = Finsupp.embDomain 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.

@[simp]

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

instance Finsupp.hasNatScalar {α : 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.

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

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

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

@[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] [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_9} [SubNegZeroMonoid G] : Sub (α →₀ G)

@[simp]

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

theorem Finsupp.sub_apply {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] (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₁ : α →₀ 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_1} {β : Type u_2} {G : Type u_9} {H : Type u_10} [AddGroup G] [SubtractionMonoid H] [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_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.

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

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

theorem Finsupp.single_add_single_eq_single_add_single {α : Type u_1} {M : Type u_5} [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_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 : α →₀ G} : (f - g).support ⊆ f.support ∪ g.support

theorem Finsupp.erase_eq_sub_single {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) (a : α) : Finsupp.erase a f = f - Finsupp.single a (↑f a)

theorem Finsupp.update_eq_sub_add_single {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) (a : α) (b : G) : Finsupp.update f a b = f - Finsupp.single a (↑f a) + Finsupp.single a b