Dependent functions with finite support #
For a non-dependent version see data/finsupp.lean
.
Notation #
This file introduces the notation Π₀ a, β a
as notation for DFinsupp β
, mirroring the α →₀ β
notation used for Finsupp
. This works for nested binders too, with Π₀ a b, γ a b
as notation
for DFinsupp (fun a ↦ DFinsupp (γ a))
.
Implementation notes #
The support is internally represented (in the primed DFinsupp.support'
) as a Multiset
that
represents a superset of the true support of the function, quotiented by the always-true relation so
that this does not impact equality. This approach has computational benefits over storing a
Finset
; it allows us to add together two finitely-supported functions without
having to evaluate the resulting function to recompute its support (which would required
decidability of b = 0
for b : β i
).
The true support of the function can still be recovered with DFinsupp.support
; but these
decidability obligations are now postponed to when the support is actually needed. As a consequence,
there are two ways to sum a DFinsupp
: with DFinsupp.sum
which works over an arbitrary function
but requires recomputation of the support and therefore a Decidable
argument; and with
DFinsupp.sumAddHom
which requires an additive morphism, using its properties to show that
summing over a superset of the support is sufficient.
Finsupp
takes an altogether different approach here; it uses Classical.Decidable
and declares
the Add
instance as noncomputable. This design difference is independent of the fact that
DFinsupp
is dependently-typed and Finsupp
is not; in future, we may want to align these two
definitions, or introduce two more definitions for the other combinations of decisions.
- mk' :: (
- toFun : (i : ι) → β i
The underlying function of a dependent function with finite support (aka
DFinsupp
). - support' : Trunc { s_1 // ∀ (i : ι), i ∈ s_1 ∨ DFinsupp.toFun s i = 0 }
The support of a dependent function with finite support (aka
DFinsupp
). - )
A dependent function Π i, β i
with finite support, with notation Π₀ i, β i
.
Note that DFinsupp.support
is the preferred API for accessing the support of the function,
DFinsupp.support'
is an implementation detail that aids computability; see the implementation
notes in this file for more information.
Instances For
Π₀ i, β i
denotes the type of dependent functions with finite support DFinsupp β
.
Instances For
A dependent function Π i, β i
with finite support, with notation Π₀ i, β i
.
Note that DFinsupp.support
is the preferred API for accessing the support of the function,
DFinsupp.support'
is an implementation detail that aids computability; see the implementation
notes in this file for more information.
Instances For
The composition of f : β₁ → β₂
and g : Π₀ i, β₁ i
is
mapRange f hf g : Π₀ i, β₂ i
, well defined when f 0 = 0
.
This preserves the structure on f
, and exists in various bundled forms for when f
is itself
bundled:
DFinsupp.mapRange.addMonoidHom
DFinsupp.mapRange.addEquiv
dfinsupp.mapRange.linearMap
dfinsupp.mapRange.linearEquiv
Instances For
Let f i
be a binary operation β₁ i → β₂ i → β i
such that f i 0 0 = 0
.
Then zipWith f hf
is a binary operation Π₀ i, β₁ i → Π₀ i, β₂ i → Π₀ i, β i
.
Instances For
Coercion from a DFinsupp
to a pi type is an AddMonoidHom
.
Instances For
Evaluation at a point is an AddMonoidHom
. This is the finitely-supported version of
Pi.evalAddMonoidHom
.
Instances For
Dependent functions with finite support inherit a semiring action from an action on each coordinate.
Dependent functions with finite support inherit a DistribMulAction
structure from such a
structure on each coordinate.
Dependent functions with finite support inherit a module structure from such a structure on each coordinate.
Filter p f
is the function which is f i
if p i
is true and 0 otherwise.
Instances For
DFinsupp.filter
as an AddMonoidHom
.
Instances For
DFinsupp.filter
as a LinearMap
.
Instances For
subtypeDomain p f
is the restriction of the finitely supported function
f
to the subtype p
.
Instances For
subtypeDomain
but as an AddMonoidHom
.
Instances For
DFinsupp.subtypeDomain
as a LinearMap
.
Instances For
Create an element of Π₀ i, β i
from a finset s
and a function x
defined on this Finset
.
Instances For
Given Fintype ι
, equivFunOnFintype
is the Equiv
between Π₀ i, β i
and Π i, β i
.
(All dependent functions on a finite type are finitely supported.)
Instances For
The function single i b : Π₀ i, β i
sends i
to b
and all other points to 0
.
Instances For
Like Finsupp.single_eq_single_iff
, but with a HEq
due to dependent types
DFinsupp.single a b
is injective in a
. For the statement that it is injective in b
, see
DFinsupp.single_injective
Equality of sigma types is sufficient (but not necessary) to show equality of DFinsupp
s.
Redefine f i
to be 0
.
Instances For
Replace the value of a Π₀ i, β i
at a given point i : ι
by a given value b : β i
.
If b = 0
, this amounts to removing i
from the support.
Otherwise, i
is added to it.
This is the (dependent) finitely-supported version of Function.update
.
Instances For
DFinsupp.single
as an AddMonoidHom
.
Instances For
DFinsupp.erase
as an AddMonoidHom
.
Instances For
If two additive homomorphisms from Π₀ i, β i
are equal on each single a b
, then
they are equal.
If two additive homomorphisms from Π₀ i, β i
are equal on each single a b
, then
they are equal.
See note [partially-applied ext lemmas].
If s
is a subset of ι
then mk_addGroupHom s
is the canonical additive
group homomorphism from $\prod_{i\in s}\beta_i$ to $\prod_{\mathtt{i : \iota}}\beta_i.$
Instances For
Set {i | f x ≠ 0}
as a Finset
.
Instances For
Equivalence between dependent functions with finite support s : Finset ι
and functions
∀ i, {x : β i // x ≠ 0}
.
Instances For
Equivalence between all dependent finitely supported functions f : Π₀ i, β i
and type
of pairs ⟨s : Finset ι, f : ∀ i : s, {x : β i // x ≠ 0}⟩
.
Instances For
Reindexing (and possibly removing) terms of a dfinsupp.
Instances For
A computable version of comap_domain when an explicit left inverse is provided.
Instances For
Reindexing terms of a dfinsupp.
This is the dfinsupp version of Equiv.piCongrLeft'
.
Instances For
The natural map between Π₀ (i : Σ i, α i), δ i.1 i.2
and Π₀ i (j : α i), δ i j
.
Instances For
The natural map between Π₀ i (j : α i), δ i j
and Π₀ (i : Σ i, α i), δ i.1 i.2
, inverse of
curry
.
Instances For
The natural bijection between Π₀ (i : Σ i, α i), δ i.1 i.2
and Π₀ i (j : α i), δ i j
.
This is the dfinsupp version of Equiv.piCurry
.
Instances For
Bijection obtained by separating the term of index none
of a dfinsupp over Option ι
.
This is the dfinsupp version of Equiv.piOptionEquivProd
.
Instances For
sum f g
is the sum of g i (f i)
over the support of f
.
Instances For
DFinsupp.prod f g
is the product of g i (f i)
over the support of f
.
Instances For
When summing over an AddMonoidHom
, the decidability assumption is not needed, and the result is
also an AddMonoidHom
.
Instances For
While we didn't need decidable instances to define it, we do to reduce it to a sum
The supremum of a family of commutative additive submonoids is equal to the range of
DFinsupp.sumAddHom
; that is, every element in the iSup
can be produced from taking a finite
number of non-zero elements of S i
, coercing them to γ
, and summing them.
The bounded supremum of a family of commutative additive submonoids is equal to the range of
DFinsupp.sumAddHom
composed with DFinsupp.filterAddMonoidHom
; that is, every element in the
bounded iSup
can be produced from taking a finite number of non-zero elements from the S i
that
satisfy p i
, coercing them to γ
, and summing them.
A variant of AddSubmonoid.mem_iSup_iff_exists_dfinsupp
with the RHS fully unfolded.
The DFinsupp
version of Finsupp.liftAddHom
,
Instances For
The DFinsupp
version of Finsupp.liftAddHom_singleAddHom
,
The DFinsupp
version of Finsupp.liftAddHom_apply_single
,
The DFinsupp
version of Finsupp.liftAddHom_comp_single
,
The DFinsupp
version of Finsupp.comp_liftAddHom
,
Bundled versions of DFinsupp.mapRange
#
The names should match the equivalent bundled Finsupp.mapRange
definitions.
DFinsupp.mapRange
as an AddMonoidHom
.
Instances For
DFinsupp.mapRange.addMonoidHom
as an AddEquiv
.
Instances For
Product and sum lemmas for bundled morphisms. #
In this section, we provide analogues of AddMonoidHom.map_sum
, AddMonoidHom.coe_finset_sum
,
and AddMonoidHom.finset_sum_apply
for DFinsupp.sum
and DFinsupp.sumAddHom
instead of
Finset.sum
.
We provide these for AddMonoidHom
, MonoidHom
, RingHom
, AddEquiv
, and MulEquiv
.
Lemmas for LinearMap
and LinearEquiv
are in another file.
The above lemmas, repeated for DFinsupp.sumAddHom
.
See DFinsupp.infinite_of_right
for this in instance form, with the drawback that
it needs all π i
to be infinite.
See DFinsupp.infinite_of_exists_right
for the case that only one π ι
is infinite.