Type of functions with finite support
For any type α
and a 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:
monoid_algebra R M
andadd_monoid_algebra R M
are defined asM →₀ R
;polynomials and multivariate polynomials are defined as
add_monoid_algebra
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 familylinear_independent
) 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 α ≃+ α →₀ ℕ
;free_abelian_group α ≃+ α →₀ ℤ
.
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.
Many constructions based on α →₀ M
use semireducible
type tags to avoid reusing unwanted type
instances. E.g., monoid_algebra
, add_monoid_algebra
, and types based on these two have
non-pointwise multiplication.
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 withhas_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.
TODO
This file is currently ~2K lines long, so possibly it should be splitted into smaller chunks;
Add the list of definitions and important lemmas to the module docstring.
Implementation notes
This file is a noncomputable theory
and uses classical logic throughout.
Notation
This file defines α →₀ β
as notation for finsupp α β
.
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
Equations
- finsupp.has_coe_to_fun = {F := λ (_x : α →₀ M), α → M, coe := finsupp.to_fun _inst_1}
Equations
- finsupp.has_zero = {zero := {support := ∅, to_fun := λ (_x : α), 0, mem_support_to_fun := _}}
Equations
- finsupp.inhabited = {default := 0}
Given fintype α
, equiv_fun_on_fintype
is the equiv
between α →₀ β
and α → β
.
(All functions on a finite type are finitely supported.)
Equations
- finsupp.equiv_fun_on_fintype = {to_fun := λ (f : α →₀ M) (a : α), ⇑f a, inv_fun := λ (f : α → M), {support := finset.filter (λ (a : α), f a ≠ 0) finset.univ, to_fun := f, mem_support_to_fun := _}, left_inv := _, right_inv := _}
Declarations about single
single a b
is the finitely supported function which has
value b
at a
and zero otherwise.
Declarations about on_finset
on_finset s f hf
is the finsupp function representing f
restricted to the finset s
.
The function needs to be 0
outside of s
. Use this when the set needs to be filtered anyways,
otherwise a better set representation is often available.
Equations
- finsupp.on_finset s f hf = {support := finset.filter (λ (a : α), f a ≠ 0) s, to_fun := f, mem_support_to_fun := _}
Declarations about map_range
The composition of f : M → N
and g : α →₀ M
is
map_range f hf g : α →₀ N
, well-defined when f 0 = 0
.
Equations
- finsupp.map_range f hf g = finsupp.on_finset g.support (f ∘ ⇑g) _
Declarations about emb_domain
Given f : α ↪ β
and v : α →₀ M
, emb_domain 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
- finsupp.emb_domain f v = {support := finset.map f v.support, to_fun := λ (a₂ : β), dite (a₂ ∈ finset.map f v.support) (λ (h : a₂ ∈ finset.map f v.support), ⇑v (finset.choose (λ (a₁ : α), ⇑f a₁ = a₂) v.support _)) (λ (h : a₂ ∉ finset.map f v.support), 0), mem_support_to_fun := _}
Declarations about zip_with
zip_with f hf g₁ g₂
is the finitely supported function satisfying
zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a)
, and it is well-defined when f 0 0 = 0
.
Equations
- finsupp.zip_with f hf g₁ g₂ = finsupp.on_finset (g₁.support ∪ g₂.support) (λ (a : α), f (⇑g₁ a) (⇑g₂ a)) _
Declarations about erase
erase a f
is the finitely supported function equal to f
except at a
where it is equal to
0
.
Declarations about sum
and prod
In most of this section, the domain β
is assumed to be an add_monoid
.
sum f g
is the sum of g a (f a)
over the support of f
.
prod f g
is the product of g a (f a)
over the support of f
.
A restatement of prod_ite_eq
with the equality test reversed.
A restatement of sum_ite_eq
with the equality test reversed.
If g
maps a second argument of 0 to 1, then multiplying it over the
result of on_finset
is the same as multiplying it over the original
finset
.
If g
maps a second argument of 0 to 0, summing it over the
result of on_finset
is the same as summing it over the original
finset
.
Additive monoid structure on α →₀ M
Equations
- finsupp.has_add = {add := finsupp.zip_with has_add.add finsupp.has_add._proof_1}
Equations
- finsupp.add_monoid = {add := has_add.add finsupp.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _}
finsupp.single
as an add_monoid_hom
.
See finsupp.lsingle
for the stronger version as a linear map.
Equations
- finsupp.single_add_hom a = {to_fun := finsupp.single a, map_zero' := _, map_add' := _}
Evaluation of a function f : α →₀ M
at a point as an additive monoid homomorphism.
See finsupp.lapply
for the stronger version as a linear map.
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 add_monoid_hom
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)
.
Equations
- finsupp.nat_sub = {sub := finsupp.zip_with (λ (m n : ℕ), m - n) finsupp.nat_sub._proof_1}
Equations
- finsupp.add_comm_monoid = {add := add_monoid.add finsupp.add_monoid, add_assoc := _, zero := add_monoid.zero finsupp.add_monoid, zero_add := _, add_zero := _, add_comm := _}
Equations
- finsupp.has_sub = {sub := finsupp.zip_with has_sub.sub finsupp.has_sub._proof_1}
Equations
- finsupp.add_group = {add := add_monoid.add finsupp.add_monoid, add_assoc := _, zero := add_monoid.zero finsupp.add_monoid, zero_add := _, add_zero := _, neg := finsupp.map_range has_neg.neg neg_zero, sub := has_sub.sub finsupp.has_sub, sub_eq_add_neg := _, add_left_neg := _}
Equations
- finsupp.add_comm_group = {add := add_group.add finsupp.add_group, add_assoc := _, zero := add_group.zero finsupp.add_group, zero_add := _, add_zero := _, neg := add_group.neg finsupp.add_group, sub := add_group.sub finsupp.add_group, sub_eq_add_neg := _, add_left_neg := _, add_comm := _}
The canonical isomorphism between families of additive monoid homomorphisms α → (M →+ N)
and monoid homomorphisms (α →₀ M) →+ N
.
Composition with a fixed additive homomorphism is itself an additive homomorphism on functions.
Equations
- finsupp.map_range.add_monoid_hom f = {to_fun := finsupp.map_range ⇑f _, map_zero' := _, map_add' := _}
Declarations about map_domain
Given f : α → β
and v : α →₀ M
, map_domain f v : β →₀ M
is the finitely supported function whose value at a : β
is the sum
of v x
over all x
such that f x = a
.
Equations
- finsupp.map_domain f v = v.sum (λ (a : α), finsupp.single (f a))
Declarations about comap_domain
Given f : α → β
, l : β →₀ M
and a proof hf
that f
is injective on
the preimage of l.support
, comap_domain f l hf
is the finitely supported function
from α
to M
given by composing l
with f
.
Equations
- finsupp.comap_domain f l hf = {support := l.support.preimage f hf, to_fun := λ (a : α), ⇑l (f a), mem_support_to_fun := _}
Declarations about filter
filter p f
is the function which is f a
if p a
is true and 0 otherwise.
Equations
- finsupp.filter p f = {support := finset.filter (λ (a : α), p a) f.support, to_fun := λ (a : α), ite (p a) (⇑f a) 0, mem_support_to_fun := _}
Declarations about frange
frange f
is the image of f
on the support of f
.
Equations
- f.frange = finset.image ⇑f f.support
Declarations about subtype_domain
subtype_domain p f
is the restriction of the finitely supported function
f
to the subtype p
.
Equations
- finsupp.subtype_domain p f = {support := finset.subtype p f.support, to_fun := ⇑f ∘ coe, mem_support_to_fun := _}
finsupp.filter
as an add_monoid_hom
.
Equations
- finsupp.filter_add_hom p = {to_fun := finsupp.filter p, map_zero' := _, map_add' := _}
Given f : α →₀ ℕ
, f.to_multiset
is the multiset with multiplicities given by the values of
f
on the elements of α
. We define this function as an add_equiv
.
Declarations about curry
and uncurry
Given a finitely supported function f
from a product type α × β
to γ
,
curry f
is the "curried" finitely supported function from α
to the type of
finitely supported functions from β
to γ
.
Equations
- f.curry = f.sum (λ (p : α × β) (c : M), finsupp.single p.fst (finsupp.single p.snd c))
Given a finitely supported function f
from α
to the type of
finitely supported functions from β
to M
,
uncurry f
is the "uncurried" finitely supported function from α × β
to M
.
finsupp_prod_equiv
defines the equiv
between ((α × β) →₀ M)
and (α →₀ (β →₀ M))
given by
currying and uncurrying.
Equations
- finsupp.finsupp_prod_equiv = {to_fun := finsupp.curry _inst_1, inv_fun := finsupp.uncurry _inst_1, left_inv := _, right_inv := _}
Scalar multiplication by a group element g, given by precomposition with the action of g⁻¹ on the domain.
Equations
- finsupp.comap_has_scalar = {smul := λ (g : G) (f : α →₀ M), finsupp.comap_domain (λ (a : α), g⁻¹ • a) f _}
Scalar multiplication by a group element, given by precomposition with the action of g⁻¹ on the domain, is multiplicative in g.
Equations
- finsupp.comap_mul_action = {to_has_scalar := finsupp.comap_has_scalar _inst_3, one_smul := _, mul_smul := _}
Scalar multiplication by a group element, given by precomposition with the action of g⁻¹ on the domain, is additive in the second argument.
Equations
- finsupp.comap_distrib_mul_action = {to_mul_action := finsupp.comap_mul_action _inst_3, smul_add := _, smul_zero := _}
Scalar multiplication by a group element on finitely supported functions on a group, given by precomposition with the action of g⁻¹.
Equations
- finsupp.has_scalar = {smul := λ (a : R) (v : α →₀ M), finsupp.map_range (has_scalar.smul a) _ v}
Throughout this section, some semiring
arguments are specified with {}
instead of []
.
See note [implicit instance arguments].
Equations
- finsupp.semimodule α M = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul finsupp.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
Equations
- finsupp.unique_of_right = {to_inhabited := {default := default (α →₀ R) finsupp.inhabited}, uniq := _}
Given an add_comm_monoid M
and s : set α
, restrict_support_equiv s M
is the equiv
between the subtype of finitely supported functions with support contained in s
and
the type of finitely supported functions from s
.
Equations
- finsupp.restrict_support_equiv s M = {to_fun := λ (f : {f // ↑(f.support) ⊆ s}), finsupp.subtype_domain (λ (x : α), x ∈ s) f.val, inv_fun := λ (f : ↥s →₀ M), ⟨finsupp.map_domain subtype.val f, _⟩, left_inv := _, right_inv := _}
Given add_comm_monoid M
and e : α ≃ β
, dom_congr e
is the corresponding equiv
between
α →₀ M
and β →₀ M
.
Equations
- finsupp.dom_congr e = {to_fun := finsupp.map_domain ⇑e, inv_fun := finsupp.map_domain ⇑(e.symm), left_inv := _, right_inv := _, map_add' := _}
Declarations about sigma types
Given l
, a finitely supported function from the sigma type Σ (i : ι), αs i
to M
and
an index element i : ι
, split l i
is the i
th component of l
,
a finitely supported function from as i
to M
.
Equations
- l.split i = finsupp.comap_domain (sigma.mk i) l _
Given l
, a finitely supported function from the sigma type Σ (i : ι), αs i
to β
,
split_support l
is the finset of indices in ι
that appear in the support of l
.
Equations
Given l
, a finitely supported function from the sigma type Σ i, αs i
to β
and
an ι
-indexed family g
of functions from (αs i →₀ β)
to γ
, split_comp
defines a
finitely supported function from the index type ι
to γ
given by composing g i
with
split l i
.
Equations
- l.split_comp g hg = {support := l.split_support, to_fun := λ (i : ι), g i (l.split i), mem_support_to_fun := _}
Given a multiset s
, s.to_finsupp
returns the finitely supported function on ℕ
given by
the multiplicities of the elements of s
.
Equations
Declarations about order(ed) instances on finsupp
Equations
- finsupp.partial_order = {le := preorder.le finsupp.preorder, lt := preorder.lt finsupp.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Equations
Equations
Equations
- finsupp.ordered_cancel_add_comm_monoid = {add := add_comm_monoid.add finsupp.add_comm_monoid, add_assoc := _, add_left_cancel := _, zero := add_comm_monoid.zero finsupp.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, add_right_cancel := _, le := partial_order.le finsupp.partial_order, lt := partial_order.lt finsupp.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}
finsupp.to_multiset
as an order isomorphism.
Equations
The order on σ →₀ ℕ
is well-founded.
Equations
- finsupp.decidable_le α = λ (m n : α →₀ ℕ), _.mpr finset.decidable_dforall_finset
Equations
- finsupp.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add infer_instance, add_assoc := _, zero := ordered_add_comm_monoid.zero infer_instance, zero_add := _, add_zero := _, add_comm := _, le := ordered_add_comm_monoid.le infer_instance, lt := ordered_add_comm_monoid.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := 0, bot_le := _, le_iff_exists_add := _}
The finsupp
counterpart of multiset.antidiagonal
: the antidiagonal of
s : α →₀ ℕ
consists of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)
such that t₁ + t₂ = s
.
The finitely supported function antidiagonal s
is equal to the multiplicities of these pairs.
The set {m : α →₀ ℕ | m ≤ n}
as a finset
.