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.
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.on_finset
: The restriction of a function to afinset
as afinsupp
.finsupp.map_range
: Composition of azero_hom
with afinsupp
.finsupp.emb_domain
: Maps the domain of afinsupp
by an embedding.finsupp.map_domain
: Maps the domain of afinsupp
by a function and by summing.finsupp.comap_domain
: Postcomposition of afinsupp
with a function injective on the preimage of its support.finsupp.zip_with
: Postcomposition of twofinsupp
s with a functionf
such thatf 0 0 = 0
.finsupp.sum
: Sum of the values of afinsupp
.finsupp.prod
: Product of the nonzero values of afinsupp
.
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.
Implementation notes #
This file is a noncomputable theory
and uses classical logic throughout.
TODO #
-
This file is currently ~2.7K lines long, so it should be splitted into smaller chunks. One option would be to move all the sum and product stuff to
algebra.big_operators.finsupp
and move the definitions that depend on it to new files underdata.finsupp.
. -
Expand the list of definitions and important lemmas to the module docstring.
- support : finset α
- to_fun : α → M
- mem_support_to_fun : ∀ (a : α), a ∈ self.support ↔ self.to_fun 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
- finsupp.has_sizeof_inst
- finsupp.fun_like
- finsupp.has_coe_to_fun
- finsupp.has_zero
- finsupp.inhabited
- finsupp.nontrivial
- finsupp.can_lift
- finsupp.has_add
- finsupp.add_zero_class
- finsupp.has_nat_scalar
- finsupp.add_monoid
- finsupp.add_comm_monoid
- finsupp.has_neg
- finsupp.has_sub
- finsupp.has_int_scalar
- finsupp.add_group
- finsupp.add_comm_group
- finsupp.has_scalar
- finsupp.has_faithful_smul
- finsupp.distrib_mul_action
- finsupp.is_scalar_tower
- finsupp.smul_comm_class
- finsupp.is_central_scalar
- finsupp.module
- finsupp.no_zero_smul_divisors
- finsupp.unique_of_right
- finsupp.unique_of_left
- finsupp.has_le
- finsupp.preorder
- finsupp.partial_order
- finsupp.semilattice_inf
- finsupp.semilattice_sup
- finsupp.lattice
- finsupp.ordered_add_comm_monoid
- finsupp.ordered_cancel_add_comm_monoid
- finsupp.has_le.le.contravariant_class
- finsupp.order_bot
- finsupp.tsub
- finsupp.has_ordered_sub
- finsupp.canonically_ordered_add_monoid
- finite_dimensional_finsupp
- module.free.finsupp.free
- finsupp.locally_finite_order
- finsupp.has_mul
- finsupp.mul_zero_class
- finsupp.semigroup_with_zero
- finsupp.non_unital_non_assoc_semiring
- finsupp.non_unital_semiring
- finsupp.non_unital_comm_semiring
- finsupp.non_unital_non_assoc_ring
- finsupp.non_unital_ring
- finsupp.non_unital_comm_ring
- finsupp.pointwise_scalar
- finsupp.pointwise_module
- slim_check.total_function.finsupp.sampleable_ext
Equations
- finsupp.fun_like = {coe := finsupp.to_fun _inst_1, coe_injective' := _}
Helper instance for when there are too many metavariables to apply fun_like.has_coe_to_fun
directly.
Equations
Deprecated. Use fun_like.ext_iff
instead.
Deprecated. Use fun_like.coe_fn_eq
instead.
Deprecated. Use fun_like.coe_injective
instead.
Deprecated. Use fun_like.congr_fun
instead.
Equations
- finsupp.has_zero = {zero := {support := ∅, to_fun := 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 := _}
If α
has a unique term,
then the type of finitely supported functions α →₀ β
is equivalent to β
.
Equations
Declarations about single
#
single a b
is the finitely supported function which has
value b
at a
and zero otherwise.
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
Declarations about update
#
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
- f.update a b = {support := ite (b = 0) (f.support.erase a) (has_insert.insert a f.support), to_fun := function.update ⇑f a b, mem_support_to_fun := _}
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 := _}
The natural finsupp
induced by the function f
given that it has finite support.
Equations
- finsupp.of_support_finite f hf = {support := hf.to_finset, to_fun := f, mem_support_to_fun := _}
Equations
- finsupp.can_lift = {coe := coe_fn finsupp.has_coe_to_fun, cond := λ (f : α → M), (function.support f).finite, prf := _}
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
.
This preserves the structure on f
, and exists in various bundled forms for when f
is itself
bundled:
finsupp.map_range.equiv
finsupp.map_range.zero_hom
finsupp.map_range.add_monoid_hom
finsupp.map_range.add_equiv
finsupp.map_range.linear_map
finsupp.map_range.linear_equiv
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
.
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
.
Taking a product over f : α →₀ M
is the same as multiplying the value on a single element
y ∈ f.support
by the product over erase y f
.
Taking a sum over over f : α →₀ M
is the same as adding the value on a
single element y ∈ f.support
to the sum over erase y f
.
Generalization of finsupp.mul_prod_erase
: if g
maps a second argument of 0 to 1,
then its product over f : α →₀ M
is the same as multiplying the value on any element
y : α
by the product over erase y f
.
Generalization of finsupp.add_sum_erase
: if g
maps a second argument of 0
to 0, then its sum over f : α →₀ M
is the same as adding the value on any element
y : α
to the sum over erase y f
.
Additive monoid structure on α →₀ M
#
Equations
- finsupp.has_add = {add := finsupp.zip_with has_add.add finsupp.has_add._proof_1}
Equations
- finsupp.add_zero_class = function.injective.add_zero_class coe_fn finsupp.add_zero_class._proof_1 finsupp.add_zero_class._proof_2 finsupp.coe_add
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.
Coercion from a finsupp
to a function type is an add_monoid_hom
.
Equations
- finsupp.coe_fn_add_hom = {to_fun := coe_fn finsupp.has_coe_to_fun, map_zero' := _, map_add' := _}
finsupp.erase
as an add_monoid_hom
.
Equations
- finsupp.erase_add_hom a = {to_fun := finsupp.erase a, map_zero' := _, map_add' := _}
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)
.
Bundle emb_domain f
as an additive map from α →₀ M
to β →₀ M
.
Equations
- finsupp.emb_domain.add_monoid_hom f = {to_fun := λ (v : α →₀ M), finsupp.emb_domain f v, map_zero' := _, map_add' := _}
Note the general finsupp.has_scalar
instance doesn't apply as ℕ
is not distributive
unless β i
's addition is commutative.
Equations
- finsupp.has_nat_scalar = {smul := λ (n : ℕ) (v : α →₀ M), finsupp.map_range (has_scalar.smul n) _ v}
Equations
- finsupp.add_monoid = function.injective.add_monoid coe_fn finsupp.add_monoid._proof_1 finsupp.add_monoid._proof_2 finsupp.add_monoid._proof_3 finsupp.add_monoid._proof_4
Deprecated, use _root_.map_finsupp_prod
instead.
Deprecated, use _root_.map_finsupp_sum
instead.
Deprecated, use _root_.map_finsupp_sum
instead.
Deprecated, use _root_.map_finsupp_prod
instead.
Deprecated, use _root_.map_finsupp_prod
instead.
Equations
- finsupp.add_comm_monoid = function.injective.add_comm_monoid coe_fn finsupp.add_comm_monoid._proof_1 finsupp.add_comm_monoid._proof_2 finsupp.add_comm_monoid._proof_3 finsupp.add_comm_monoid._proof_4
Equations
- finsupp.has_neg = {neg := finsupp.map_range has_neg.neg finsupp.has_neg._proof_1}
Equations
- finsupp.has_sub = {sub := finsupp.zip_with has_sub.sub finsupp.has_sub._proof_1}
Note the general finsupp.has_scalar
instance doesn't apply as ℤ
is not distributive
unless β i
's addition is commutative.
Equations
- finsupp.has_int_scalar = {smul := λ (n : ℤ) (v : α →₀ G), finsupp.map_range (has_scalar.smul n) _ v}
Equations
- finsupp.add_group = function.injective.add_group coe_fn finsupp.add_group._proof_1 finsupp.add_group._proof_2 finsupp.add_group._proof_3 finsupp.coe_neg finsupp.coe_sub finsupp.add_group._proof_4 finsupp.add_group._proof_5
Equations
- finsupp.add_comm_group = function.injective.add_comm_group coe_fn finsupp.add_comm_group._proof_1 finsupp.add_comm_group._proof_2 finsupp.add_comm_group._proof_3 finsupp.add_comm_group._proof_4 finsupp.add_comm_group._proof_5 finsupp.add_comm_group._proof_6 finsupp.add_comm_group._proof_7
Taking the product under h
is an additive homomorphism of finsupps,
if h
is an additive homomorphism on the support.
This is a more general version of finsupp.sum_add_index'
; the latter has simpler hypotheses.
Taking the product under h
is an additive-to-multiplicative homomorphism of finsupps,
if h
is an additive-to-multiplicative homomorphism on the support.
This is a more general version of finsupp.prod_add_index'
; the latter has simpler hypotheses.
Taking the sum under h
is an additive homomorphism of finsupps,
if h
is an additive homomorphism.
This is a more specific version of finsupp.sum_add_index
with simpler hypotheses.
Taking the product under h
is an additive-to-multiplicative homomorphism of finsupps,
if h
is an additive-to-multiplicative homomorphism.
This is a more specialized version of finsupp.prod_add_index
with simpler hypotheses.
The canonical isomorphism between families of additive monoid homomorphisms α → (M →+ N)
and monoid homomorphisms (α →₀ M) →+ N
.
For disjoint f1
and f2
, and function g
, the sum of the sums of g
over f1
and f2
equals the sum of g
over f1 + f2
For disjoint f1
and f2
, and function g
, the product of the products of g
over f1
and f2
equals the product of g
over f1 + f2
finsupp.map_range
as an equiv.
Equations
- finsupp.map_range.equiv f hf hf' = {to_fun := finsupp.map_range ⇑f hf, inv_fun := finsupp.map_range ⇑(f.symm) hf', left_inv := _, right_inv := _}
Composition with a fixed zero-preserving homomorphism is itself an zero-preserving homomorphism on functions.
Equations
- finsupp.map_range.zero_hom f = {to_fun := finsupp.map_range ⇑f _, map_zero' := _}
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' := _}
finsupp.map_range.add_monoid_hom
as an equiv.
Equations
- finsupp.map_range.add_equiv f = {to_fun := finsupp.map_range ⇑f _, inv_fun := finsupp.map_range ⇑(f.symm) _, left_inv := _, right_inv := _, 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))
finsupp.map_domain
is an add_monoid_hom
.
Equations
- finsupp.map_domain.add_monoid_hom f = {to_fun := finsupp.map_domain f, map_zero' := _, map_add' := _}
A version of sum_map_domain_index
that takes a bundled add_monoid_hom
,
rather than separate linearity hypotheses.
When f
is an embedding we have an embedding (α →₀ ℕ) ↪ (β →₀ ℕ)
given by map_domain
.
Equations
- finsupp.map_domain_embedding f = {to_fun := finsupp.map_domain ⇑f, inj' := _}
When g
preserves addition, map_range
and map_domain
commute.
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 := _}
Note the hif
argument is needed for this to work in rw
.
A version of finsupp.comap_domain_add
that's easier to use.
finsupp.comap_domain
is an add_monoid_hom
.
Equations
- finsupp.comap_domain.add_monoid_hom hf = {to_fun := λ (x : β →₀ M), finsupp.comap_domain f x _, map_zero' := _, map_add' := _}
Restrict a finitely supported function on option α
to a finitely supported function on α
.
Equations
- f.some = finsupp.comap_domain option.some f _
Declarations about equiv_congr_left
#
Given f : α ≃ β
, we can map l : α →₀ M
to equiv_map_domain f l : β →₀ M
(computably)
by mapping the support forwards and the function backwards.
Equations
- finsupp.equiv_map_domain f l = {support := finset.map f.to_embedding l.support, to_fun := λ (a : β), ⇑l (⇑(f.symm) a), mem_support_to_fun := _}