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
andAddMonoidAlgebra R M
are defined asM →₀ R
; -
polynomials and multivariate polynomials are defined as
AddMonoidAlgebra
s, hence they useFinsupp
under the hood; -
the linear combination of a family of vectors
v i
with coefficientsf i
(as used, e.g., to define linearly independent familyLinearIndependent
) is defined as a mapFinsupp.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
: TheFinsupp
which is nonzero in exactly one point.Finsupp.update
: Changes one value of aFinsupp
.Finsupp.erase
: Replaces one value of aFinsupp
by0
.Finsupp.onFinset
: The restriction of a function to aFinset
as aFinsupp
.Finsupp.mapRange
: Composition of aZeroHom
with aFinsupp
.Finsupp.embDomain
: Maps the domain of aFinsupp
by an embedding.Finsupp.zipWith
: Postcomposition of twoFinsupp
s with a functionf
such thatf 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 toFinsupp
somewhere in the statement; -
ι
: an auxiliary index type; -
M
,M'
,N
,P
: types withZero
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.
- 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
.
Instances For
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.single a b
is injective in b
. For the statement that it is injective in a
, see
Finsupp.single_left_injective
Finsupp.single a b
is injective in a
. For the statement that it is injective in b
, see
Finsupp.single_injective
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
.
Instances For
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.
Instances For
The natural Finsupp
induced by the function f
given that it has finite support.
Instances For
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
Instances For
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.
Instances For
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
.
Instances For
Additive monoid structure on α →₀ M
#
Finsupp.single
as an AddMonoidHom
.
See Finsupp.lsingle
in LinearAlgebra/Finsupp
for the stronger version as a linear map.
Instances For
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.
Instances For
Coercion from a Finsupp
to a function type is an AddMonoidHom
.
Instances For
Finsupp.erase
as an AddMonoidHom
.
Instances For
If two additive homomorphisms from α →₀ M
are equal on each single a b
,
then they are equal.
If two additive homomorphisms from α →₀ M
are equal on each single a b
,
then they are equal.
We formulate this using equality of AddMonoidHom
s 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)
.
Bundle Finsupp.embDomain f
as an additive map from α →₀ M
to β →₀ M
.