Dependent functions with finite support #
For a non-dependent version see Mathlib.Data.Finsupp.Defs
.
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.
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.
- mk' :: (
- toFun : (i : ι) → β i
The underlying function of a dependent function with finite support (aka
DFinsupp
). The support of a dependent function with finite support (aka
DFinsupp
).- )
Instances For
Π₀ i, β i
denotes the type of dependent functions with finite support DFinsupp β
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
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
Equations
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
x.piecewise y s
is the finitely supported function equal to x
on the set s
,
and to y
on its complement.
Equations
- x.piecewise y s = DFinsupp.zipWith (fun (i : ι) (x y : β i) => if i ∈ s then x else y) ⋯ x y
Instances For
Equations
- DFinsupp.instAdd = { add := DFinsupp.zipWith (fun (x : ι) (x1 x2 : β x) => x1 + x2) ⋯ }
Equations
- DFinsupp.addZeroClass = Function.Injective.addZeroClass (fun (f : Π₀ (i : ι), β i) => ⇑f) ⋯ ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Note the general SMul
instance doesn't apply as ℕ
is not distributive
unless β i
's addition is commutative.
Equations
- DFinsupp.hasNatScalar = { smul := fun (c : ℕ) (v : Π₀ (i : ι), β i) => DFinsupp.mapRange (fun (x : ι) (x_1 : β x) => c • x_1) ⋯ v }
Equations
- DFinsupp.instAddMonoid = Function.Injective.addMonoid (fun (f : Π₀ (i : ι), β i) => ⇑f) ⋯ ⋯ ⋯ ⋯
Coercion from a DFinsupp
to a pi type is an AddMonoidHom
.
Equations
- DFinsupp.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- DFinsupp.addCommMonoid = Function.Injective.addCommMonoid (fun (f : Π₀ (i : ι), β i) => ⇑f) ⋯ ⋯ ⋯ ⋯
Equations
- DFinsupp.instNeg = { neg := fun (f : Π₀ (i : ι), β i) => DFinsupp.mapRange (fun (x : ι) => Neg.neg) ⋯ f }
Equations
- DFinsupp.instSub = { sub := DFinsupp.zipWith (fun (x : ι) => Sub.sub) ⋯ }
Note the general SMul
instance doesn't apply as ℤ
is not distributive
unless β i
's addition is commutative.
Equations
- DFinsupp.hasIntScalar = { smul := fun (c : ℤ) (v : Π₀ (i : ι), β i) => DFinsupp.mapRange (fun (x : ι) (x_1 : β x) => c • x_1) ⋯ v }
Equations
- DFinsupp.instAddGroup = Function.Injective.addGroup (fun (f : Π₀ (i : ι), β i) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- DFinsupp.addCommGroup = Function.Injective.addCommGroup (fun (f : Π₀ (i : ι), β i) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Filter p f
is the function which is f i
if p i
is true and 0 otherwise.
Equations
Instances For
DFinsupp.filter
as an AddMonoidHom
.
Equations
- DFinsupp.filterAddMonoidHom β p = { toFun := DFinsupp.filter p, map_zero' := ⋯, map_add' := ⋯ }
Instances For
subtypeDomain p f
is the restriction of the finitely supported function
f
to the subtype p
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
subtypeDomain
but as an AddMonoidHom
.
Equations
- DFinsupp.subtypeDomainAddMonoidHom β p = { toFun := DFinsupp.subtypeDomain p, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Create an element of Π₀ i, β i
from a finset s
and a function x
defined on this Finset
.
Equations
- DFinsupp.mk s x = { toFun := fun (i : ι) => if H : i ∈ s then x ⟨i, H⟩ else 0, support' := Trunc.mk ⟨s.val, ⋯⟩ }
Instances For
Equations
- DFinsupp.unique = ⋯.unique
Given Fintype ι
, equivFunOnFintype
is the Equiv
between Π₀ i, β i
and Π i, β i
.
(All dependent functions on a finite type are finitely supported.)
Equations
Instances For
The function single i b : Π₀ i, β i
sends i
to b
and all other points to 0
.
Equations
- DFinsupp.single i b = { toFun := Pi.single i b, support' := Trunc.mk ⟨{i}, ⋯⟩ }
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
.
Equations
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
.
Equations
Instances For
DFinsupp.single
as an AddMonoidHom
.
Equations
- DFinsupp.singleAddHom β i = { toFun := DFinsupp.single i, map_zero' := ⋯, map_add' := ⋯ }
Instances For
DFinsupp.erase
as an AddMonoidHom
.
Equations
- DFinsupp.eraseAddHom β i = { toFun := DFinsupp.erase i, map_zero' := ⋯, map_add' := ⋯ }
Instances For
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.$
Equations
- DFinsupp.mkAddGroupHom s = { toFun := DFinsupp.mk s, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Set {i | f x ≠ 0}
as a Finset
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equivalence between dependent functions with finite support s : Finset ι
and functions
∀ i, {x : β i // x ≠ 0}
.
Equations
- One or more equations did not get rendered due to their size.
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}⟩
.
Equations
- DFinsupp.sigmaFinsetFunEquiv = (Equiv.sigmaFiberEquiv DFinsupp.support).symm.trans (Equiv.sigmaCongrRight DFinsupp.subtypeSupportEqEquiv)
Instances For
Equations
- f.instDecidableEq g = decidable_of_iff (f.support = g.support ∧ ∀ i ∈ f.support, f i = g i) ⋯
Reindexing (and possibly removing) terms of a dfinsupp.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A computable version of comap_domain when an explicit left inverse is provided.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reindexing terms of a dfinsupp.
This is the dfinsupp version of Equiv.piCongrLeft'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- DFinsupp.hasAdd₂ = inferInstance
Equations
- DFinsupp.addZeroClass₂ = inferInstance
Adds a term to a dfinsupp, making a dfinsupp indexed by an Option
.
This is the dfinsupp version of Option.rec
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Bijection obtained by separating the term of index none
of a dfinsupp over Option ι
.
This is the dfinsupp version of Equiv.piOptionEquivProd
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Bundled versions of DFinsupp.mapRange
#
The names should match the equivalent bundled Finsupp.mapRange
definitions.
DFinsupp.mapRange
as an AddMonoidHom
.
Equations
- DFinsupp.mapRange.addMonoidHom f = { toFun := DFinsupp.mapRange (fun (i : ι) (x : β₁ i) => (f i) x) ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
DFinsupp.mapRange.addMonoidHom
as an AddEquiv
.
Equations
- One or more equations did not get rendered due to their size.