Type of functions with finite support

For any type α and any type M with zero, we define the type Finsupp α M (notation: α →₀ M) of finitely supported functions from α to M, i.e. the functions which are zero everywhere on α except on a finite set.

Functions with finite support are used (at least) in the following parts of the library:

• MonoidAlgebra R M and AddMonoidAlgebra R M are defined as M →₀ R;

• polynomials and multivariate polynomials are defined as AddMonoidAlgebras, hence they use Finsupp under the hood;

• the linear combination of a family of vectors v i with coefficients f i (as used, e.g., to define linearly independent family LinearIndependent) is defined as a map Finsupp.linearCombination : (ι → M) → (ι →₀ R) →ₗ[R] M.

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

• Multiset α ≃+ α →₀ ℕ;
• FreeAbelianGroup α ≃+ α →₀ ℤ.

Most of the theory assumes that the range is a commutative additive monoid. This gives us the big sum operator as a powerful way to construct Finsupp elements, which is defined in Mathlib.Algebra.BigOperators.Finsupp.Basic.

Many constructions based on α →₀ M are defs rather than abbrevs to avoid reusing unwanted type class instances. E.g., MonoidAlgebra, AddMonoidAlgebra, and types based on these two have non-pointwise multiplication.

Main declarations

• Finsupp: The type of finitely supported functions from α to β.
• Finsupp.onFinset: The restriction of a function to a Finset as a Finsupp.
• Finsupp.mapRange: Composition of a ZeroHom with a Finsupp.
• Finsupp.embDomain: Maps the domain of a Finsupp by an embedding.
• Finsupp.zipWith: Postcomposition of two Finsupps with a function f such that f 0 0 = 0.

Notations

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

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

• α, β, γ: types with no additional structure that appear as the first argument to Finsupp somewhere in the statement;

• ι : an auxiliary index type;

• M, M', N, P: types with Zero or (Add)(Comm)Monoid structure; M is also used for a (semi)module over a (semi)ring.

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

• R, S: (semi)rings.

Implementation notes

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

TODO

• Expand the list of definitions and important lemmas to the module docstring.

structure Finsupp (α : Type u_13) (M : Type u_14) [Zero M] : Type (max u_13 u_14)

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

• support : Finset α

  The support of a finitely supported function (aka Finsupp).

• toFun : α → M

  The underlying function of a bundled finitely supported function (aka Finsupp).

• mem_support_toFun (a : α) : Iff (Membership.mem self.support a) (Ne (self.toFun a) 0)

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

def «term_→₀_» : Lean.TrailingParserDescr

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

Equations

• Eq «term_→₀_» (Lean.ParserDescr.trailingNode `«term_→₀_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →₀ ") (Lean.ParserDescr.cat `term 25)))

Basic declarations about Finsupp

def Finsupp.instFunLike {α : Type u_1} {M : Type u_5} [Zero M] : FunLike (Finsupp α M) α M

Equations

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

theorem Finsupp.ext {α : Type u_1} {M : Type u_5} [Zero M] {f g : Finsupp α M} (h : ∀ (a : α), Eq (DFunLike.coe f a) (DFunLike.coe g a)) : Eq f g

theorem Finsupp.ext_iff {α : Type u_1} {M : Type u_5} [Zero M] {f g : Finsupp α M} : Iff (Eq f g) (∀ (a : α), Eq (DFunLike.coe f a) (DFunLike.coe g a))

theorem Finsupp.ne_iff {α : Type u_1} {M : Type u_5} [Zero M] {f g : Finsupp α M} : Iff (Ne f g) (Exists fun (a : α) => Ne (DFunLike.coe f a) (DFunLike.coe g a))

theorem Finsupp.coe_mk {α : Type u_1} {M : Type u_5} [Zero M] (f : α → M) (s : Finset α) (h : ∀ (a : α), Iff (Membership.mem s a) (Ne (f a) 0)) : Eq (DFunLike.coe { support := s, toFun := f, mem_support_toFun := h }) f

def Finsupp.instZero {α : Type u_1} {M : Type u_5} [Zero M] : Zero (Finsupp α M)

Equations

• Eq Finsupp.instZero { zero := { support := EmptyCollection.emptyCollection, toFun := 0, mem_support_toFun := ⋯ } }

theorem Finsupp.coe_zero {α : Type u_1} {M : Type u_5} [Zero M] : Eq (DFunLike.coe 0) 0

theorem Finsupp.zero_apply {α : Type u_1} {M : Type u_5} [Zero M] {a : α} : Eq (DFunLike.coe 0 a) 0

theorem Finsupp.support_zero {α : Type u_1} {M : Type u_5} [Zero M] : Eq (support 0) EmptyCollection.emptyCollection

def Finsupp.instInhabited {α : Type u_1} {M : Type u_5} [Zero M] : Inhabited (Finsupp α M)

Equations

• Eq Finsupp.instInhabited { default := 0 }

theorem Finsupp.mem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : Finsupp α M} {a : α} : Iff (Membership.mem f.support a) (Ne (DFunLike.coe f a) 0)

theorem Finsupp.fun_support_eq {α : Type u_1} {M : Type u_5} [Zero M] (f : Finsupp α M) : Eq (Function.support (DFunLike.coe f)) f.support.toSet

theorem Finsupp.not_mem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : Finsupp α M} {a : α} : Iff (Not (Membership.mem f.support a)) (Eq (DFunLike.coe f a) 0)

theorem Finsupp.coe_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {f : Finsupp α M} : Iff (Eq (DFunLike.coe f) 0) (Eq f 0)

theorem Finsupp.ext_iff' {α : Type u_1} {M : Type u_5} [Zero M] {f g : Finsupp α M} : Iff (Eq f g) (And (Eq f.support g.support) (∀ (x : α), Membership.mem f.support x → Eq (DFunLike.coe f x) (DFunLike.coe g x)))

theorem Finsupp.support_eq_empty {α : Type u_1} {M : Type u_5} [Zero M] {f : Finsupp α M} : Iff (Eq f.support EmptyCollection.emptyCollection) (Eq f 0)

theorem Finsupp.support_nonempty_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : Finsupp α M} : Iff f.support.Nonempty (Ne f 0)

theorem Finsupp.card_support_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {f : Finsupp α M} : Iff (Eq f.support.card 0) (Eq f 0)

def Finsupp.instDecidableEq {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] [DecidableEq M] : DecidableEq (Finsupp α M)

Equations

• Eq (f.instDecidableEq g) (decidable_of_iff (And (Eq f.support g.support) (∀ (a : α), Membership.mem f.support a → Eq (DFunLike.coe f a) (DFunLike.coe g a))) ⋯)

theorem Finsupp.finite_support {α : Type u_1} {M : Type u_5} [Zero M] (f : Finsupp α M) : (Function.support (DFunLike.coe f)).Finite

theorem Finsupp.support_subset_iff {α : Type u_1} {M : Type u_5} [Zero M] {s : Set α} {f : Finsupp α M} : Iff (HasSubset.Subset f.support.toSet s) (∀ (a : α), Not (Membership.mem s a) → Eq (DFunLike.coe f a) 0)

def Finsupp.equivFunOnFinite {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] : Equiv (Finsupp α M) (α → M)

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

Equations

• Eq Finsupp.equivFunOnFinite { toFun := DFunLike.coe, invFun := fun (f : α → M) => { support := ⋯.toFinset, toFun := f, mem_support_toFun := ⋯ }, left_inv := ⋯, right_inv := ⋯ }

theorem Finsupp.equivFunOnFinite_apply {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (a✝ : Finsupp α M) (a : α) : Eq (DFunLike.coe equivFunOnFinite a✝ a) (DFunLike.coe a✝ a)

theorem Finsupp.equivFunOnFinite_symm_apply_support {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (f : α → M) : Eq (DFunLike.coe equivFunOnFinite.symm f).support ⋯.toFinset

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

theorem Finsupp.equivFunOnFinite_symm_coe {M : Type u_5} [Zero M] {α : Type u_13} [Finite α] (f : Finsupp α M) : Eq (DFunLike.coe equivFunOnFinite.symm (DFunLike.coe f)) f

theorem Finsupp.coe_equivFunOnFinite_symm {M : Type u_5} [Zero M] {α : Type u_13} [Finite α] (f : α → M) : Eq (DFunLike.coe (DFunLike.coe equivFunOnFinite.symm f)) f

noncomputable def Equiv.finsuppUnique {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] : Equiv (Finsupp ι M) M

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

Equations

• Eq Equiv.finsuppUnique (Finsupp.equivFunOnFinite.trans (Equiv.funUnique ι M))

theorem Equiv.finsuppUnique_symm_apply_toFun {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] (a✝ : M) (a✝¹ : ι) : Eq (DFunLike.coe (DFunLike.coe finsuppUnique.symm a✝) a✝¹) a✝

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

theorem Equiv.finsuppUnique_apply {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] (a✝ : Finsupp ι M) : Eq (DFunLike.coe finsuppUnique a✝) (DFunLike.coe a✝ Inhabited.default)

theorem Finsupp.unique_ext {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] {f g : Finsupp α M} (h : Eq (DFunLike.coe f Inhabited.default) (DFunLike.coe g Inhabited.default)) : Eq f g

theorem Finsupp.unique_ext_iff {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] {f g : Finsupp α M} : Iff (Eq f g) (Eq (DFunLike.coe f Inhabited.default) (DFunLike.coe g Inhabited.default))

Declarations about onFinset

def Finsupp.onFinset {α : Type u_1} {M : Type u_5} [Zero M] (s : Finset α) (f : α → M) (hf : ∀ (a : α), Ne (f a) 0 → Membership.mem s a) : Finsupp α 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

• Eq (Finsupp.onFinset s f hf) { support := Finset.filter (fun (a : α) => Ne (f a) 0) s, toFun := f, mem_support_toFun := ⋯ }

theorem Finsupp.coe_onFinset {α : Type u_1} {M : Type u_5} [Zero M] (s : Finset α) (f : α → M) (hf : ∀ (a : α), Ne (f a) 0 → Membership.mem s a) : Eq (DFunLike.coe (onFinset s f hf)) f

theorem Finsupp.onFinset_apply {α : Type u_1} {M : Type u_5} [Zero M] {s : Finset α} {f : α → M} {hf : ∀ (a : α), Ne (f a) 0 → Membership.mem s a} {a : α} : Eq (DFunLike.coe (onFinset s f hf) a) (f a)

theorem Finsupp.support_onFinset_subset {α : Type u_1} {M : Type u_5} [Zero M] {s : Finset α} {f : α → M} {hf : ∀ (a : α), Ne (f a) 0 → Membership.mem s a} : HasSubset.Subset (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 : α), Ne (f a) 0 → Membership.mem s a) {a : α} : Iff (Membership.mem (onFinset s f hf).support a) (Ne (f a) 0)

theorem Finsupp.support_onFinset {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq M] {s : Finset α} {f : α → M} (hf : ∀ (a : α), Ne (f a) 0 → Membership.mem s a) : Eq (onFinset s f hf).support (Finset.filter (fun (a : α) => Ne (f a) 0) s)

noncomputable def Finsupp.ofSupportFinite {α : Type u_1} {M : Type u_5} [Zero M] (f : α → M) (hf : (Function.support f).Finite) : Finsupp α M

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

Equations

• Eq (Finsupp.ofSupportFinite f hf) { support := hf.toFinset, toFun := f, mem_support_toFun := ⋯ }

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

theorem Finsupp.instCanLift {α : Type u_1} {M : Type u_5} [Zero M] : CanLift (α → M) (Finsupp α M) DFunLike.coe fun (f : α → M) => (Function.support f).Finite

Declarations about mapRange

def Finsupp.mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : M → N) (hf : Eq (f 0) 0) (g : Finsupp α M) : Finsupp α 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

• Eq (Finsupp.mapRange f hf g) (Finsupp.onFinset g.support (Function.comp f (DFunLike.coe g)) ⋯)

theorem Finsupp.mapRange_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : M → N} {hf : Eq (f 0) 0} {g : Finsupp α M} {a : α} : Eq (DFunLike.coe (mapRange f hf g) a) (f (DFunLike.coe g a))

theorem Finsupp.mapRange_zero {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : M → N} {hf : Eq (f 0) 0} : Eq (mapRange f hf 0) 0

theorem Finsupp.mapRange_id {α : Type u_1} {M : Type u_5} [Zero M] (g : Finsupp α M) : Eq (mapRange id ⋯ g) g

theorem Finsupp.mapRange_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : N → P) (hf : Eq (f 0) 0) (f₂ : M → N) (hf₂ : Eq (f₂ 0) 0) (h : Eq (Function.comp f f₂ 0) 0) (g : Finsupp α M) : Eq (mapRange (Function.comp f f₂) h g) (mapRange f hf (mapRange f₂ hf₂ g))

theorem Finsupp.mapRange_mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (e₁ : N → P) (e₂ : M → N) (he₁ : Eq (e₁ 0) 0) (he₂ : Eq (e₂ 0) 0) (f : Finsupp α M) : Eq (mapRange e₁ he₁ (mapRange e₂ he₂ f)) (mapRange (Function.comp e₁ e₂) ⋯ f)

theorem Finsupp.support_mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : M → N} {hf : Eq (f 0) 0} {g : Finsupp α M} : HasSubset.Subset (mapRange f hf g).support g.support

theorem Finsupp.support_mapRange_of_injective {ι : Type u_4} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {e : M → N} (he0 : Eq (e 0) 0) (f : Finsupp ι M) (he : Function.Injective e) : Eq (mapRange e he0 f).support f.support

theorem Finsupp.range_mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (e : M → N) (he₀ : Eq (e 0) 0) : Eq (Set.range (mapRange e he₀)) (setOf fun (g : Finsupp α N) => ∀ (i : α), Membership.mem (Set.range e) (DFunLike.coe g i))

theorem Finsupp.mapRange_injective {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (e : M → N) (he₀ : Eq (e 0) 0) (he : Function.Injective e) : Function.Injective (mapRange e he₀)

Finsupp.mapRange of a injective function is injective.

theorem Finsupp.mapRange_surjective {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (e : M → N) (he₀ : Eq (e 0) 0) (he : Function.Surjective e) : Function.Surjective (mapRange e he₀)

Finsupp.mapRange of a surjective function is surjective.

Declarations about embDomain

def Finsupp.embDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : Function.Embedding α β) (v : Finsupp α M) : Finsupp β 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.

theorem Finsupp.support_embDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : Function.Embedding α β) (v : Finsupp α M) : Eq (embDomain f v).support (Finset.map f v.support)

theorem Finsupp.embDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : Function.Embedding α β) : Eq (embDomain f 0) 0

theorem Finsupp.embDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : Function.Embedding α β) (v : Finsupp α M) (a : α) : Eq (DFunLike.coe (embDomain f v) (DFunLike.coe f a)) (DFunLike.coe v a)

theorem Finsupp.embDomain_notin_range {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : Function.Embedding α β) (v : Finsupp α M) (a : β) (h : Not (Membership.mem (Set.range (DFunLike.coe f)) a)) : Eq (DFunLike.coe (embDomain f v) a) 0

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

theorem Finsupp.embDomain_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : Function.Embedding α β} {l₁ l₂ : Finsupp α M} : Iff (Eq (embDomain f l₁) (embDomain f l₂)) (Eq l₁ l₂)

theorem Finsupp.embDomain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : Function.Embedding α β} {l : Finsupp α M} : Iff (Eq (embDomain f l) 0) (Eq 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 : Function.Embedding α β) (g : M → N) (p : Finsupp α M) (hg : Eq (g 0) 0) : Eq (embDomain f (mapRange g hg p)) (mapRange g hg (embDomain f p))

Declarations about zipWith

def Finsupp.zipWith {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : M → N → P) (hf : Eq (f 0 0) 0) (g₁ : Finsupp α M) (g₂ : Finsupp α N) : Finsupp α 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

• Eq (Finsupp.zipWith f hf g₁ g₂) (Finsupp.onFinset (Union.union g₁.support g₂.support) (fun (a : α) => f (DFunLike.coe g₁ a) (DFunLike.coe g₂ a)) ⋯)

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 : Eq (f 0 0) 0} {g₁ : Finsupp α M} {g₂ : Finsupp α N} {a : α} : Eq (DFunLike.coe (zipWith f hf g₁ g₂) a) (f (DFunLike.coe g₁ a) (DFunLike.coe 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 : Eq (f 0 0) 0} {g₁ : Finsupp α M} {g₂ : Finsupp α N} : HasSubset.Subset (zipWith f hf g₁ g₂).support (Union.union g₁.support g₂.support)

Additive monoid structure on α →₀ M

def Finsupp.instAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] : Add (Finsupp α M)

Equations

• Eq Finsupp.instAdd { add := Finsupp.zipWith (fun (x1 x2 : M) => HAdd.hAdd x1 x2) ⋯ }

theorem Finsupp.coe_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f g : Finsupp α M) : Eq (DFunLike.coe (HAdd.hAdd f g)) (HAdd.hAdd (DFunLike.coe f) (DFunLike.coe g))

theorem Finsupp.add_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (g₁ g₂ : Finsupp α M) (a : α) : Eq (DFunLike.coe (HAdd.hAdd g₁ g₂) a) (HAdd.hAdd (DFunLike.coe g₁ a) (DFunLike.coe g₂ a))

theorem Finsupp.support_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] [DecidableEq α] {g₁ g₂ : Finsupp α M} : HasSubset.Subset (HAdd.hAdd g₁ g₂).support (Union.union g₁.support g₂.support)

theorem Finsupp.support_add_eq {α : Type u_1} {M : Type u_5} [AddZeroClass M] [DecidableEq α] {g₁ g₂ : Finsupp α M} (h : Disjoint g₁.support g₂.support) : Eq (HAdd.hAdd g₁ g₂).support (Union.union g₁.support g₂.support)

def Finsupp.instAddZeroClass {α : Type u_1} {M : Type u_5} [AddZeroClass M] : AddZeroClass (Finsupp α M)

Equations

• Eq Finsupp.instAddZeroClass { toZero := Finsupp.instZero, toAdd := Finsupp.instAdd, zero_add := ⋯, add_zero := ⋯ }

theorem Finsupp.instIsLeftCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsLeftCancelAdd M] : IsLeftCancelAdd (Finsupp α M)

noncomputable def Finsupp.addEquivFunOnFinite {M : Type u_5} [AddZeroClass M] {ι : Type u_13} [Finite ι] : AddEquiv (Finsupp ι M) (ι → M)

When ι is finite and M is an AddMonoid, then Finsupp.equivFunOnFinite gives an AddEquiv

Equations

• Eq Finsupp.addEquivFunOnFinite { toEquiv := Finsupp.equivFunOnFinite, map_add' := ⋯ }

noncomputable def AddEquiv.finsuppUnique {M : Type u_5} [AddZeroClass M] {ι : Type u_13} [Unique ι] : AddEquiv (Finsupp ι M) M

AddEquiv between (ι →₀ M) and M, when ι has a unique element

Equations

• Eq AddEquiv.finsuppUnique { toEquiv := Equiv.finsuppUnique, map_add' := ⋯ }

theorem Finsupp.instIsRightCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsRightCancelAdd M] : IsRightCancelAdd (Finsupp α M)

theorem Finsupp.instIsCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsCancelAdd M] : IsCancelAdd (Finsupp α M)

def Finsupp.applyAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) : AddMonoidHom (Finsupp α 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

• Eq (Finsupp.applyAddHom a) { toFun := fun (g : Finsupp α M) => DFunLike.coe g a, map_zero' := ⋯, map_add' := ⋯ }

theorem Finsupp.applyAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (g : Finsupp α M) : Eq (DFunLike.coe (applyAddHom a) g) (DFunLike.coe g a)

noncomputable def Finsupp.coeFnAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] : AddMonoidHom (Finsupp α M) (α → M)

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

Equations

• Eq Finsupp.coeFnAddHom { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

theorem Finsupp.coeFnAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a✝ : Finsupp α M) (a : α) : Eq (DFunLike.coe coeFnAddHom a✝ a) (DFunLike.coe a✝ a)

theorem Finsupp.mapRange_add {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] {f : M → N} {hf : Eq (f 0) 0} (hf' : ∀ (x y : M), Eq (f (HAdd.hAdd x y)) (HAdd.hAdd (f x) (f y))) (v₁ v₂ : Finsupp α M) : Eq (mapRange f hf (HAdd.hAdd v₁ v₂)) (HAdd.hAdd (mapRange f hf v₁) (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] [FunLike β M N] [AddMonoidHomClass β M N] {f : β} (v₁ v₂ : Finsupp α M) : Eq (mapRange (DFunLike.coe f) ⋯ (HAdd.hAdd v₁ v₂)) (HAdd.hAdd (mapRange (DFunLike.coe f) ⋯ v₁) (mapRange (DFunLike.coe f) ⋯ v₂))

def Finsupp.embDomain.addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : Function.Embedding α β) : AddMonoidHom (Finsupp α M) (Finsupp β M)

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

Equations

• Eq (Finsupp.embDomain.addMonoidHom f) { toFun := fun (v : Finsupp α M) => Finsupp.embDomain f v, map_zero' := ⋯, map_add' := ⋯ }

theorem Finsupp.embDomain.addMonoidHom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : Function.Embedding α β) (v : Finsupp α M) : Eq (DFunLike.coe (addMonoidHom f) v) (embDomain f v)

theorem Finsupp.embDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : Function.Embedding α β) (v w : Finsupp α M) : Eq (embDomain f (HAdd.hAdd v w)) (HAdd.hAdd (embDomain f v) (embDomain f w))

def Finsupp.instNatSMul {α : Type u_1} {M : Type u_5} [AddMonoid M] : SMul Nat (Finsupp α M)

Note the general SMul instance for Finsupp doesn't apply as ℕ is not distributive unless β i's addition is commutative.

Equations

• Eq Finsupp.instNatSMul { smul := fun (n : Nat) (v : Finsupp α M) => Finsupp.mapRange (fun (x : M) => HSMul.hSMul n x) ⋯ v }

def Finsupp.instAddMonoid {α : Type u_1} {M : Type u_5} [AddMonoid M] : AddMonoid (Finsupp α M)

Equations

• One or more equations did not get rendered due to their size.

def Finsupp.instAddCommMonoid {α : Type u_1} {M : Type u_5} [AddCommMonoid M] : AddCommMonoid (Finsupp α M)

Equations

• Eq Finsupp.instAddCommMonoid { toAddMonoid := Finsupp.instAddMonoid, add_comm := ⋯ }

def Finsupp.instNeg {α : Type u_1} {G : Type u_9} [NegZeroClass G] : Neg (Finsupp α G)

Equations

• Eq Finsupp.instNeg { neg := Finsupp.mapRange Neg.neg ⋯ }

theorem Finsupp.coe_neg {α : Type u_1} {G : Type u_9} [NegZeroClass G] (g : Finsupp α G) : Eq (DFunLike.coe (Neg.neg g)) (Neg.neg (DFunLike.coe g))

theorem Finsupp.neg_apply {α : Type u_1} {G : Type u_9} [NegZeroClass G] (g : Finsupp α G) (a : α) : Eq (DFunLike.coe (Neg.neg g) a) (Neg.neg (DFunLike.coe 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 : Eq (f 0) 0} (hf' : ∀ (x : G), Eq (f (Neg.neg x)) (Neg.neg (f x))) (v : Finsupp α G) : Eq (mapRange f hf (Neg.neg v)) (Neg.neg (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] [FunLike β G H] [AddMonoidHomClass β G H] {f : β} (v : Finsupp α G) : Eq (mapRange (DFunLike.coe f) ⋯ (Neg.neg v)) (Neg.neg (mapRange (DFunLike.coe f) ⋯ v))

def Finsupp.instSub {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] : Sub (Finsupp α G)

Equations

• Eq Finsupp.instSub { sub := Finsupp.zipWith Sub.sub ⋯ }

theorem Finsupp.coe_sub {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] (g₁ g₂ : Finsupp α G) : Eq (DFunLike.coe (HSub.hSub g₁ g₂)) (HSub.hSub (DFunLike.coe g₁) (DFunLike.coe g₂))

theorem Finsupp.sub_apply {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] (g₁ g₂ : Finsupp α G) (a : α) : Eq (DFunLike.coe (HSub.hSub g₁ g₂) a) (HSub.hSub (DFunLike.coe g₁ a) (DFunLike.coe 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 : Eq (f 0) 0} (hf' : ∀ (x y : G), Eq (f (HSub.hSub x y)) (HSub.hSub (f x) (f y))) (v₁ v₂ : Finsupp α G) : Eq (mapRange f hf (HSub.hSub v₁ v₂)) (HSub.hSub (mapRange f hf v₁) (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] [FunLike β G H] [AddMonoidHomClass β G H] {f : β} (v₁ v₂ : Finsupp α G) : Eq (mapRange (DFunLike.coe f) ⋯ (HSub.hSub v₁ v₂)) (HSub.hSub (mapRange (DFunLike.coe f) ⋯ v₁) (mapRange (DFunLike.coe f) ⋯ v₂))

def Finsupp.instIntSMul {α : Type u_1} {G : Type u_9} [AddGroup G] : SMul Int (Finsupp α G)

Note the general SMul instance for Finsupp doesn't apply as ℤ is not distributive unless β i's addition is commutative.

Equations

• Eq Finsupp.instIntSMul { smul := fun (n : Int) (v : Finsupp α G) => Finsupp.mapRange (fun (x : G) => HSMul.hSMul n x) ⋯ v }

def Finsupp.instAddGroup {α : Type u_1} {G : Type u_9} [AddGroup G] : AddGroup (Finsupp α G)

Equations

• One or more equations did not get rendered due to their size.

def Finsupp.instAddCommGroup {α : Type u_1} {G : Type u_9} [AddCommGroup G] : AddCommGroup (Finsupp α G)

Equations

• Eq Finsupp.instAddCommGroup { toAddGroup := Finsupp.instAddGroup, add_comm := ⋯ }

theorem Finsupp.support_neg {α : Type u_1} {G : Type u_9} [AddGroup G] (f : Finsupp α G) : Eq (Neg.neg f).support f.support

theorem Finsupp.support_sub {α : Type u_1} {G : Type u_9} [DecidableEq α] [AddGroup G] {f g : Finsupp α G} : HasSubset.Subset (HSub.hSub f g).support (Union.union f.support g.support)