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 Mandadd_monoid_algebra R Mare defined asM →₀ R; -
polynomials and multivariate polynomials are defined as
add_monoid_algebras, hence they usefinsuppunder the hood; -
the linear combination of a family of vectors
v iwith 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: Thefinsuppwhich is nonzero in exactly one point.finsupp.update: Changes one value of afinsupp.finsupp.erase: Replaces one value of afinsuppby0.finsupp.on_finset: The restriction of a function to afinsetas afinsupp.finsupp.map_range: Composition of azero_homwith afinsupp.finsupp.emb_domain: Maps the domain of afinsuppby an embedding.finsupp.map_domain: Maps the domain of afinsuppby a function and by summing.finsupp.comap_domain: Postcomposition of afinsuppwith a function injective on the preimage of its support.finsupp.zip_with: Postcomposition of twofinsupps with a functionfsuch 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 tofinsuppsomewhere in the statement; -
ι: an auxiliary index type; -
M,M',N,P: types withhas_zeroor(add_)(comm_)monoidstructure;Mis 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.finsuppand 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
@[protected, instance]
Equations
- finsupp.fun_like = {coe := finsupp.to_fun _inst_1, coe_injective' := _}
@[protected, instance]
def
finsupp.has_coe_to_fun
{α : Type u_1}
{M : Type u_5}
[has_zero M] :
has_coe_to_fun (α →₀ M) (λ (_x : α →₀ M), α → M)
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.
theorem
finsupp.congr_fun
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f g : α →₀ M}
(h : f = g)
(a : α) :
Deprecated. Use fun_like.congr_fun instead.
@[protected, instance]
Equations
- finsupp.has_zero = {zero := {support := ∅, to_fun := 0, mem_support_to_fun := _}}
@[protected, instance]
Equations
- finsupp.inhabited = {default := 0}
@[simp, norm_cast]
theorem
finsupp.fun_support_eq
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(f : α →₀ M) :
function.support ⇑f = ↑(f.support)
@[protected, instance]
def
finsupp.decidable_eq
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[decidable_eq α]
[decidable_eq M] :
decidable_eq (α →₀ M)
@[simp]
theorem
finsupp.equiv_fun_on_fintype_symm_apply_to_fun
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[fintype α]
(f : α → M)
(ᾰ : α) :
⇑(⇑(finsupp.equiv_fun_on_fintype.symm) f) ᾰ = f ᾰ
@[simp]
theorem
finsupp.equiv_fun_on_fintype_apply
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[fintype α]
(f : α →₀ M)
(a : α) :
⇑finsupp.equiv_fun_on_fintype f a = ⇑f a
@[simp]
theorem
finsupp.equiv_fun_on_fintype_symm_apply_support
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[fintype α]
(f : α → M) :
(⇑(finsupp.equiv_fun_on_fintype.symm) f).support = finset.filter (λ (a : α), f a ≠ 0) finset.univ
noncomputable
def
finsupp.equiv_fun_on_fintype
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[fintype α] :
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 := _}
@[simp]
theorem
finsupp.equiv_fun_on_fintype_symm_coe
{M : Type u_5}
[has_zero M]
{α : Type u_1}
[fintype α]
(f : α →₀ M) :
@[simp]
theorem
equiv.finsupp_unique_symm_apply_to_fun
{M : Type u_5}
[has_zero M]
{ι : Type u_1}
[unique ι]
(ᾰ : M)
(ᾰ_1 : ι) :
⇑(⇑(equiv.finsupp_unique.symm) ᾰ) ᾰ_1 = ᾰ
If α has a unique term,
then the type of finitely supported functions α →₀ β is equivalent to β.
Equations
@[simp]
theorem
equiv.finsupp_unique_symm_apply_support_val
{M : Type u_5}
[has_zero M]
{ι : Type u_1}
[unique ι]
(ᾰ : M) :
(⇑(equiv.finsupp_unique.symm) ᾰ).support.val = multiset.filter (λ (a : ι), ¬ᾰ = 0) {inhabited.default}
@[simp]
theorem
equiv.finsupp_unique_apply
{M : Type u_5}
[has_zero M]
{ι : Type u_1}
[unique ι]
(ᾰ : ι →₀ M) :
Declarations about single #
noncomputable
def
finsupp.single
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(a : α)
(b : M) :
α →₀ M
single a b is the finitely supported function which has
value b at a and zero otherwise.
theorem
finsupp.single_apply
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a a' : α}
{b : M}
[decidable (a = a')] :
⇑(finsupp.single a b) a' = ite (a = a') b 0
theorem
finsupp.single_eq_indicator
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a : α}
{b : M} :
⇑(finsupp.single a b) = {a}.indicator (λ (_x : α), b)
@[simp]
theorem
finsupp.single_eq_same
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a : α}
{b : M} :
⇑(finsupp.single a b) a = b
@[simp]
theorem
finsupp.single_eq_of_ne
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a a' : α}
{b : M}
(h : a ≠ a') :
⇑(finsupp.single a b) a' = 0
theorem
finsupp.single_eq_update
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[decidable_eq α]
(a : α)
(b : M) :
⇑(finsupp.single a b) = function.update 0 a b
theorem
finsupp.single_eq_pi_single
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[decidable_eq α]
(a : α)
(b : M) :
⇑(finsupp.single a b) = pi.single a b
@[simp]
theorem
finsupp.single_zero
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(a : α) :
finsupp.single a 0 = 0
theorem
finsupp.single_of_single_apply
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(a a' : α)
(b : M) :
finsupp.single a (⇑(finsupp.single a' b) a) = ⇑(finsupp.single a' (finsupp.single a' b)) a
theorem
finsupp.support_single_ne_zero
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{b : M}
(a : α)
(hb : b ≠ 0) :
(finsupp.single a b).support = {a}
theorem
finsupp.support_single_subset
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a : α}
{b : M} :
(finsupp.single a b).support ⊆ {a}
theorem
finsupp.single_apply_mem
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a : α}
{b : M}
(x : α) :
⇑(finsupp.single a b) x ∈ {0, b}
theorem
finsupp.range_single_subset
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a : α}
{b : M} :
set.range ⇑(finsupp.single a b) ⊆ {0, b}
finsupp.single a b is injective in b. For the statement that it is injective in a, see
finsupp.single_left_injective
theorem
finsupp.single_eq_single_iff
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(a₁ a₂ : α)
(b₁ b₂ : M) :
theorem
finsupp.single_left_injective
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{b : M}
(h : b ≠ 0) :
function.injective (λ (a : α), finsupp.single a b)
finsupp.single a b is injective in a. For the statement that it is injective in b, see
finsupp.single_injective
theorem
finsupp.single_left_inj
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a a' : α}
{b : M}
(h : b ≠ 0) :
finsupp.single a b = finsupp.single a' b ↔ a = a'
theorem
finsupp.support_single_ne_bot
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{b : M}
(i : α)
(h : b ≠ 0) :
(finsupp.single i b).support ≠ ⊥
theorem
finsupp.support_single_disjoint
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{b : M}
[decidable_eq α]
{b' : M}
(hb : b ≠ 0)
(hb' : b' ≠ 0)
{i j : α} :
disjoint (finsupp.single i b).support (finsupp.single j b').support ↔ i ≠ j
@[simp]
theorem
finsupp.single_eq_zero
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a : α}
{b : M} :
finsupp.single a b = 0 ↔ b = 0
theorem
finsupp.single_swap
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(a₁ a₂ : α)
(b : M) :
⇑(finsupp.single a₁ b) a₂ = ⇑(finsupp.single a₂ b) a₁
@[protected, instance]
def
finsupp.nontrivial
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[nonempty α]
[nontrivial M] :
nontrivial (α →₀ M)
@[ext]
theorem
finsupp.unique_ext
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[unique α]
{f g : α →₀ M}
(h : ⇑f inhabited.default = ⇑g inhabited.default) :
f = g
theorem
finsupp.unique_ext_iff
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[unique α]
{f g : α →₀ M} :
f = g ↔ ⇑f inhabited.default = ⇑g inhabited.default
@[simp]
theorem
finsupp.unique_single_eq_iff
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a a' : α}
{b : M}
[unique α]
{b' : M} :
finsupp.single a b = finsupp.single a' b' ↔ b = b'
theorem
finsupp.support_eq_singleton'
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α →₀ M}
{a : α} :
theorem
finsupp.support_subset_singleton
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α →₀ M}
{a : α} :
theorem
finsupp.support_subset_singleton'
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α →₀ M}
{a : α} :
f.support ⊆ {a} ↔ ∃ (b : M), f = finsupp.single a b
@[simp]
theorem
finsupp.equiv_fun_on_fintype_single
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[decidable_eq α]
[fintype α]
(x : α)
(m : M) :
@[simp]
theorem
finsupp.equiv_fun_on_fintype_symm_single
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[decidable_eq α]
[fintype α]
(x : α)
(m : M) :
⇑(finsupp.equiv_fun_on_fintype.symm) (pi.single x m) = finsupp.single x m
Declarations about update #
noncomputable
def
finsupp.update
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(f : α →₀ M)
(a : α)
(b : M) :
α →₀ M
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 := _}
@[simp]
theorem
finsupp.coe_update
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(f : α →₀ M)
(a : α)
(b : M)
[decidable_eq α] :
⇑(f.update a b) = function.update ⇑f a b
theorem
finsupp.support_update
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(f : α →₀ M)
(a : α)
(b : M)
[decidable_eq α] :
@[simp]
theorem
finsupp.support_update_zero
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(f : α →₀ M)
(a : α)
[decidable_eq α] :
theorem
finsupp.support_update_ne_zero
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(f : α →₀ M)
(a : α)
{b : M}
[decidable_eq α]
(h : b ≠ 0) :
(f.update a b).support = has_insert.insert a f.support
Declarations about on_finset #
noncomputable
def
finsupp.on_finset
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(s : finset α)
(f : α → M)
(hf : ∀ (a : α), f a ≠ 0 → a ∈ s) :
α →₀ M
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 := _}
@[simp]
theorem
finsupp.on_finset_apply
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{s : finset α}
{f : α → M}
{hf : ∀ (a : α), f a ≠ 0 → a ∈ s}
{a : α} :
⇑(finsupp.on_finset s f hf) a = f a
@[simp]
theorem
finsupp.support_on_finset_subset
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{s : finset α}
{f : α → M}
{hf : ∀ (a : α), f a ≠ 0 → a ∈ s} :
(finsupp.on_finset s f hf).support ⊆ s
theorem
finsupp.support_on_finset
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{s : finset α}
{f : α → M}
(hf : ∀ (a : α), f a ≠ 0 → a ∈ s) :
(finsupp.on_finset s f hf).support = finset.filter (λ (a : α), f a ≠ 0) s
noncomputable
def
finsupp.of_support_finite
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(f : α → M)
(hf : (function.support f).finite) :
α →₀ M
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 := _}
theorem
finsupp.of_support_finite_coe
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α → M}
{hf : (function.support f).finite} :
⇑(finsupp.of_support_finite f hf) = f
@[protected, instance]
Equations
- finsupp.can_lift = {coe := coe_fn finsupp.has_coe_to_fun, cond := λ (f : α → M), (function.support f).finite, prf := _}
Declarations about map_range #
noncomputable
def
finsupp.map_range
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[has_zero N]
(f : M → N)
(hf : f 0 = 0)
(g : α →₀ M) :
α →₀ N
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.equivfinsupp.map_range.zero_homfinsupp.map_range.add_monoid_homfinsupp.map_range.add_equivfinsupp.map_range.linear_mapfinsupp.map_range.linear_equiv
Equations
- finsupp.map_range f hf g = finsupp.on_finset g.support (f ∘ ⇑g) _
@[simp]
theorem
finsupp.map_range_apply
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[has_zero N]
{f : M → N}
{hf : f 0 = 0}
{g : α →₀ M}
{a : α} :
⇑(finsupp.map_range f hf g) a = f (⇑g a)
@[simp]
theorem
finsupp.map_range_zero
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[has_zero N]
{f : M → N}
{hf : f 0 = 0} :
finsupp.map_range f hf 0 = 0
@[simp]
theorem
finsupp.map_range_id
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(g : α →₀ M) :
finsupp.map_range id rfl g = g
theorem
finsupp.map_range_comp
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[has_zero M]
[has_zero N]
[has_zero P]
(f : N → P)
(hf : f 0 = 0)
(f₂ : M → N)
(hf₂ : f₂ 0 = 0)
(h : (f ∘ f₂) 0 = 0)
(g : α →₀ M) :
finsupp.map_range (f ∘ f₂) h g = finsupp.map_range f hf (finsupp.map_range f₂ hf₂ g)
theorem
finsupp.support_map_range
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[has_zero N]
{f : M → N}
{hf : f 0 = 0}
{g : α →₀ M} :
(finsupp.map_range f hf g).support ⊆ g.support
@[simp]
theorem
finsupp.map_range_single
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[has_zero N]
{f : M → N}
{hf : f 0 = 0}
{a : α}
{b : M} :
finsupp.map_range f hf (finsupp.single a b) = finsupp.single a (f b)
theorem
finsupp.support_map_range_of_injective
{ι : Type u_4}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[has_zero N]
{e : M → N}
(he0 : e 0 = 0)
(f : ι →₀ M)
(he : function.injective e) :
(finsupp.map_range e he0 f).support = f.support
Declarations about emb_domain #
noncomputable
def
finsupp.emb_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α ↪ β)
(v : α →₀ M) :
β →₀ M
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 := _}
@[simp]
theorem
finsupp.support_emb_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α ↪ β)
(v : α →₀ M) :
(finsupp.emb_domain f v).support = finset.map f v.support
@[simp]
theorem
finsupp.emb_domain_zero
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α ↪ β) :
finsupp.emb_domain f 0 = 0
@[simp]
theorem
finsupp.emb_domain_apply
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α ↪ β)
(v : α →₀ M)
(a : α) :
⇑(finsupp.emb_domain f v) (⇑f a) = ⇑v a
theorem
finsupp.emb_domain_injective
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α ↪ β) :
@[simp]
theorem
finsupp.emb_domain_inj
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
{f : α ↪ β}
{l₁ l₂ : α →₀ M} :
finsupp.emb_domain f l₁ = finsupp.emb_domain f l₂ ↔ l₁ = l₂
@[simp]
theorem
finsupp.emb_domain_eq_zero
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
{f : α ↪ β}
{l : α →₀ M} :
finsupp.emb_domain f l = 0 ↔ l = 0
theorem
finsupp.emb_domain_map_range
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[has_zero N]
(f : α ↪ β)
(g : M → N)
(p : α →₀ M)
(hg : g 0 = 0) :
finsupp.emb_domain f (finsupp.map_range g hg p) = finsupp.map_range g hg (finsupp.emb_domain f p)
theorem
finsupp.single_of_emb_domain_single
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(l : α →₀ M)
(f : α ↪ β)
(a : β)
(b : M)
(hb : b ≠ 0)
(h : finsupp.emb_domain f l = finsupp.single a b) :
∃ (x : α), l = finsupp.single x b ∧ ⇑f x = a
@[simp]
theorem
finsupp.emb_domain_single
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α ↪ β)
(a : α)
(m : M) :
finsupp.emb_domain f (finsupp.single a m) = finsupp.single (⇑f a) m
Declarations about zip_with #
noncomputable
def
finsupp.zip_with
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[has_zero M]
[has_zero N]
[has_zero P]
(f : M → N → P)
(hf : f 0 0 = 0)
(g₁ : α →₀ M)
(g₂ : α →₀ N) :
α →₀ P
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)) _
theorem
finsupp.support_zip_with
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[has_zero M]
[has_zero N]
[has_zero P]
[D : decidable_eq α]
{f : M → N → P}
{hf : f 0 0 = 0}
{g₁ : α →₀ M}
{g₂ : α →₀ N} :
Declarations about erase #
noncomputable
def
finsupp.erase
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(a : α)
(f : α →₀ M) :
α →₀ M
erase a f is the finitely supported function equal to f except at a where it is equal to
0.
@[simp]
theorem
finsupp.support_erase
{α : Type u_1}
{M : Type u_5}
[has_zero M]
[decidable_eq α]
{a : α}
{f : α →₀ M} :
(finsupp.erase a f).support = f.support.erase a
@[simp]
theorem
finsupp.erase_same
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a : α}
{f : α →₀ M} :
⇑(finsupp.erase a f) a = 0
@[simp]
theorem
finsupp.erase_ne
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a a' : α}
{f : α →₀ M}
(h : a' ≠ a) :
⇑(finsupp.erase a f) a' = ⇑f a'
@[simp]
theorem
finsupp.erase_single
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a : α}
{b : M} :
finsupp.erase a (finsupp.single a b) = 0
theorem
finsupp.erase_single_ne
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{a a' : α}
{b : M}
(h : a ≠ a') :
finsupp.erase a (finsupp.single a' b) = finsupp.single a' b
@[simp]
theorem
finsupp.erase_of_not_mem_support
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{f : α →₀ M}
{a : α}
(haf : a ∉ f.support) :
finsupp.erase a f = f
@[simp]
theorem
finsupp.erase_zero
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(a : α) :
finsupp.erase a 0 = 0
Declarations about sum and prod #
In most of this section, the domain β is assumed to be an add_monoid.
theorem
finsupp.prod_fintype
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[comm_monoid N]
[fintype α]
(f : α →₀ M)
(g : α → M → N)
(h : ∀ (i : α), g i 0 = 1) :
f.prod g = finset.univ.prod (λ (i : α), g i (⇑f i))
theorem
finsupp.sum_fintype
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
[fintype α]
(f : α →₀ M)
(g : α → M → N)
(h : ∀ (i : α), g i 0 = 0) :
f.sum g = finset.univ.sum (λ (i : α), g i (⇑f i))
@[simp]
theorem
finsupp.prod_single_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[comm_monoid N]
{a : α}
{b : M}
{h : α → M → N}
(h_zero : h a 0 = 1) :
(finsupp.single a b).prod h = h a b
@[simp]
theorem
finsupp.sum_single_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
{a : α}
{b : M}
{h : α → M → N}
(h_zero : h a 0 = 0) :
(finsupp.single a b).sum h = h a b
theorem
finsupp.sum_map_range_index
{α : Type u_1}
{M : Type u_5}
{M' : Type u_6}
{N : Type u_7}
[has_zero M]
[has_zero M']
[add_comm_monoid N]
{f : M → M'}
{hf : f 0 = 0}
{g : α →₀ M}
{h : α → M' → N}
(h0 : ∀ (a : α), h a 0 = 0) :
(finsupp.map_range f hf g).sum h = g.sum (λ (a : α) (b : M), h a (f b))
theorem
finsupp.prod_map_range_index
{α : Type u_1}
{M : Type u_5}
{M' : Type u_6}
{N : Type u_7}
[has_zero M]
[has_zero M']
[comm_monoid N]
{f : M → M'}
{hf : f 0 = 0}
{g : α →₀ M}
{h : α → M' → N}
(h0 : ∀ (a : α), h a 0 = 1) :
(finsupp.map_range f hf g).prod h = g.prod (λ (a : α) (b : M), h a (f b))
@[simp]
theorem
finsupp.prod_zero_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[comm_monoid N]
{h : α → M → N} :
@[simp]
theorem
finsupp.sum_zero_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
{h : α → M → N} :
theorem
finsupp.prod_comm
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{M' : Type u_6}
{N : Type u_7}
[has_zero M]
[has_zero M']
[comm_monoid N]
(f : α →₀ M)
(g : β →₀ M')
(h : α → M → β → M' → N) :
theorem
finsupp.sum_comm
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{M' : Type u_6}
{N : Type u_7}
[has_zero M]
[has_zero M']
[add_comm_monoid N]
(f : α →₀ M)
(g : β →₀ M')
(h : α → M → β → M' → N) :
@[simp]
theorem
finsupp.prod_ite_eq
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[comm_monoid N]
[decidable_eq α]
(f : α →₀ M)
(a : α)
(b : α → M → N) :
@[simp]
theorem
finsupp.sum_ite_eq
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
[decidable_eq α]
(f : α →₀ M)
(a : α)
(b : α → M → N) :
@[simp]
theorem
finsupp.sum_ite_self_eq
{α : Type u_1}
[decidable_eq α]
{N : Type u_2}
[add_comm_monoid N]
(f : α →₀ N)
(a : α) :
@[simp]
theorem
finsupp.prod_ite_eq'
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[comm_monoid N]
[decidable_eq α]
(f : α →₀ M)
(a : α)
(b : α → M → N) :
A restatement of prod_ite_eq with the equality test reversed.
@[simp]
theorem
finsupp.sum_ite_eq'
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
[decidable_eq α]
(f : α →₀ M)
(a : α)
(b : α → M → N) :
A restatement of sum_ite_eq with the equality test reversed.
@[simp]
theorem
finsupp.sum_ite_self_eq'
{α : Type u_1}
[decidable_eq α]
{N : Type u_2}
[add_comm_monoid N]
(f : α →₀ N)
(a : α) :
@[simp]
theorem
finsupp.prod_pow
{α : Type u_1}
{N : Type u_7}
[comm_monoid N]
[fintype α]
(f : α →₀ ℕ)
(g : α → N) :
theorem
finsupp.on_finset_prod
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[comm_monoid N]
{s : finset α}
{f : α → M}
{g : α → M → N}
(hf : ∀ (a : α), f a ≠ 0 → a ∈ s)
(hg : ∀ (a : α), g a 0 = 1) :
(finsupp.on_finset s f hf).prod g = s.prod (λ (a : α), g a (f a))
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.
theorem
finsupp.on_finset_sum
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
{s : finset α}
{f : α → M}
{g : α → M → N}
(hf : ∀ (a : α), f a ≠ 0 → a ∈ s)
(hg : ∀ (a : α), g a 0 = 0) :
(finsupp.on_finset s f hf).sum g = s.sum (λ (a : α), g a (f a))
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.
theorem
finsupp.mul_prod_erase
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[comm_monoid N]
(f : α →₀ M)
(y : α)
(g : α → M → N)
(hyf : y ∈ f.support) :
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.
theorem
finsupp.add_sum_erase
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
(f : α →₀ M)
(y : α)
(g : α → M → N)
(hyf : y ∈ f.support) :
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.
theorem
finsupp.mul_prod_erase'
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[comm_monoid N]
(f : α →₀ M)
(y : α)
(g : α → M → N)
(hg : ∀ (i : α), g i 0 = 1) :
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.
theorem
finsupp.add_sum_erase'
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
(f : α →₀ M)
(y : α)
(g : α → M → N)
(hg : ∀ (i : α), g i 0 = 0) :
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.
theorem
add_submonoid_class.finsupp_sum_mem
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
{S : Type u_2}
[set_like S N]
[add_submonoid_class S N]
(s : S)
(f : α →₀ M)
(g : α → M → N)
(h : ∀ (c : α), ⇑f c ≠ 0 → g c (⇑f c) ∈ s) :
theorem
submonoid_class.finsupp_prod_mem
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[comm_monoid N]
{S : Type u_2}
[set_like S N]
[submonoid_class S N]
(s : S)
(f : α →₀ M)
(g : α → M → N)
(h : ∀ (c : α), ⇑f c ≠ 0 → g c (⇑f c) ∈ s) :
Additive monoid structure on α →₀ M #
@[protected, instance]
Equations
- finsupp.has_add = {add := finsupp.zip_with has_add.add finsupp.has_add._proof_1}
@[simp]
theorem
finsupp.add_apply
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(g₁ g₂ : α →₀ M)
(a : α) :
theorem
finsupp.support_add
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
[decidable_eq α]
{g₁ g₂ : α →₀ M} :
theorem
finsupp.support_add_eq
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
[decidable_eq α]
{g₁ g₂ : α →₀ M}
(h : disjoint g₁.support g₂.support) :
@[simp]
theorem
finsupp.single_add
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(a : α)
(b₁ b₂ : M) :
finsupp.single a (b₁ + b₂) = finsupp.single a b₁ + finsupp.single a b₂
@[protected, instance]
noncomputable
def
finsupp.add_zero_class
{α : Type u_1}
{M : Type u_5}
[add_zero_class M] :
add_zero_class (α →₀ M)
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' := _}
@[simp]
theorem
finsupp.single_add_hom_apply
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(a : α)
(b : M) :
⇑(finsupp.single_add_hom a) b = finsupp.single a b
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.
@[simp]
theorem
finsupp.apply_add_hom_apply
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(a : α)
(g : α →₀ M) :
⇑(finsupp.apply_add_hom a) g = ⇑g a
@[simp]
theorem
finsupp.coe_fn_add_hom_apply
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(x : α →₀ M)
(ᾰ : α) :
⇑finsupp.coe_fn_add_hom x ᾰ = ⇑x ᾰ
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' := _}
theorem
finsupp.update_eq_single_add_erase
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(f : α →₀ M)
(a : α)
(b : M) :
f.update a b = finsupp.single a b + finsupp.erase a f
theorem
finsupp.update_eq_erase_add_single
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(f : α →₀ M)
(a : α)
(b : M) :
f.update a b = finsupp.erase a f + finsupp.single a b
theorem
finsupp.single_add_erase
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(a : α)
(f : α →₀ M) :
finsupp.single a (⇑f a) + finsupp.erase a f = f
theorem
finsupp.erase_add_single
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(a : α)
(f : α →₀ M) :
finsupp.erase a f + finsupp.single a (⇑f a) = f
@[simp]
theorem
finsupp.erase_add
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(a : α)
(f f' : α →₀ M) :
finsupp.erase a (f + f') = finsupp.erase a f + finsupp.erase a f'
@[simp]
theorem
finsupp.erase_add_hom_apply
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(a : α)
(f : α →₀ M) :
⇑(finsupp.erase_add_hom a) f = finsupp.erase a f
finsupp.erase as an add_monoid_hom.
Equations
- finsupp.erase_add_hom a = {to_fun := finsupp.erase a, map_zero' := _, map_add' := _}
@[protected]
theorem
finsupp.induction
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
{p : (α →₀ M) → Prop}
(f : α →₀ M)
(h0 : p 0)
(ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (finsupp.single a b + f)) :
p f
theorem
finsupp.induction₂
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
{p : (α →₀ M) → Prop}
(f : α →₀ M)
(h0 : p 0)
(ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + finsupp.single a b)) :
p f
theorem
finsupp.induction_linear
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
{p : (α →₀ M) → Prop}
(f : α →₀ M)
(h0 : p 0)
(hadd : ∀ (f g : α →₀ M), p f → p g → p (f + g))
(hsingle : ∀ (a : α) (b : M), p (finsupp.single a b)) :
p f
@[simp]
theorem
finsupp.add_closure_set_of_eq_single
{α : Type u_1}
{M : Type u_5}
[add_zero_class M] :
add_submonoid.closure {f : α →₀ M | ∃ (a : α) (b : M), f = finsupp.single a b} = ⊤
theorem
finsupp.add_hom_ext
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_zero_class M]
[add_zero_class N]
⦃f g : (α →₀ M) →+ N⦄
(H : ∀ (x : α) (y : M), ⇑f (finsupp.single x y) = ⇑g (finsupp.single x y)) :
f = g
If two additive homomorphisms from α →₀ M are equal on each single a b, then
they are equal.
@[ext]
theorem
finsupp.add_hom_ext'
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_zero_class M]
[add_zero_class N]
⦃f g : (α →₀ M) →+ N⦄
(H : ∀ (x : α), f.comp (finsupp.single_add_hom x) = g.comp (finsupp.single_add_hom x)) :
f = g
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_homs 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).
theorem
finsupp.mul_hom_ext
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_zero_class M]
[mul_one_class N]
⦃f g : multiplicative (α →₀ M) →* N⦄
(H : ∀ (x : α) (y : M), ⇑f (⇑multiplicative.of_add (finsupp.single x y)) = ⇑g (⇑multiplicative.of_add (finsupp.single x y))) :
f = g
@[ext]
theorem
finsupp.mul_hom_ext'
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_zero_class M]
[mul_one_class N]
{f g : multiplicative (α →₀ M) →* N}
(H : ∀ (x : α), f.comp (⇑add_monoid_hom.to_multiplicative (finsupp.single_add_hom x)) = g.comp (⇑add_monoid_hom.to_multiplicative (finsupp.single_add_hom x))) :
f = g
theorem
finsupp.map_range_add
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_zero_class M]
[add_zero_class N]
{f : M → N}
{hf : f 0 = 0}
(hf' : ∀ (x y : M), f (x + y) = f x + f y)
(v₁ v₂ : α →₀ M) :
finsupp.map_range f hf (v₁ + v₂) = finsupp.map_range f hf v₁ + finsupp.map_range f hf v₂
@[simp]
theorem
finsupp.emb_domain.add_monoid_hom_apply
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_zero_class M]
(f : α ↪ β)
(v : α →₀ M) :
noncomputable
def
finsupp.emb_domain.add_monoid_hom
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_zero_class M]
(f : α ↪ β) :
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' := _}
@[simp]
theorem
finsupp.emb_domain_add
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_zero_class M]
(f : α ↪ β)
(v w : α →₀ M) :
finsupp.emb_domain f (v + w) = finsupp.emb_domain f v + finsupp.emb_domain f w
@[protected, instance]
noncomputable
def
finsupp.has_nat_scalar
{α : Type u_1}
{M : Type u_5}
[add_monoid M] :
has_scalar ℕ (α →₀ M)
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}
@[protected, instance]
noncomputable
def
finsupp.add_monoid
{α : Type u_1}
{M : Type u_5}
[add_monoid M] :
add_monoid (α →₀ M)
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
theorem
map_finsupp_sum
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[has_zero M]
[add_comm_monoid N]
[add_comm_monoid P]
{H : Type u_2}
[add_monoid_hom_class H N P]
(h : H)
(f : α →₀ M)
(g : α → M → N) :
theorem
map_finsupp_prod
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[has_zero M]
[comm_monoid N]
[comm_monoid P]
{H : Type u_2}
[monoid_hom_class H N P]
(h : H)
(f : α →₀ M)
(g : α → M → N) :
@[protected]
theorem
mul_equiv.map_finsupp_prod
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[has_zero M]
[comm_monoid N]
[comm_monoid P]
(h : N ≃* P)
(f : α →₀ M)
(g : α → M → N) :
Deprecated, use _root_.map_finsupp_prod instead.
@[protected]
theorem
add_equiv.map_finsupp_sum
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[has_zero M]
[add_comm_monoid N]
[add_comm_monoid P]
(h : N ≃+ P)
(f : α →₀ M)
(g : α → M → N) :
Deprecated, use _root_.map_finsupp_sum instead.
@[protected]
theorem
add_monoid_hom.map_finsupp_sum
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[has_zero M]
[add_comm_monoid N]
[add_comm_monoid P]
(h : N →+ P)
(f : α →₀ M)
(g : α → M → N) :
Deprecated, use _root_.map_finsupp_sum instead.
@[protected]
theorem
monoid_hom.map_finsupp_prod
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[has_zero M]
[comm_monoid N]
[comm_monoid P]
(h : N →* P)
(f : α →₀ M)
(g : α → M → N) :
Deprecated, use _root_.map_finsupp_prod instead.
@[protected]
theorem
ring_hom.map_finsupp_prod
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
{S : Type u_12}
[has_zero M]
[comm_semiring R]
[comm_semiring S]
(h : R →+* S)
(f : α →₀ M)
(g : α → M → R) :
Deprecated, use _root_.map_finsupp_prod instead.
theorem
add_monoid_hom.coe_finsupp_sum
{α : Type u_1}
{β : Type u_2}
{N : Type u_7}
{P : Type u_8}
[has_zero β]
[add_monoid N]
[add_comm_monoid P]
(f : α →₀ β)
(g : α → β → N →+ P) :
@[simp]
theorem
add_monoid_hom.finsupp_sum_apply
{α : Type u_1}
{β : Type u_2}
{N : Type u_7}
{P : Type u_8}
[has_zero β]
[add_monoid N]
[add_comm_monoid P]
(f : α →₀ β)
(g : α → β → N →+ P)
(x : N) :
@[protected, instance]
noncomputable
def
finsupp.add_comm_monoid
{α : Type u_1}
{M : Type u_5}
[add_comm_monoid M] :
add_comm_monoid (α →₀ M)
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
@[protected, instance]
Equations
- finsupp.has_neg = {neg := finsupp.map_range has_neg.neg finsupp.has_neg._proof_1}
@[protected, instance]
Equations
- finsupp.has_sub = {sub := finsupp.zip_with has_sub.sub finsupp.has_sub._proof_1}
@[protected, instance]
noncomputable
def
finsupp.has_int_scalar
{α : Type u_1}
{G : Type u_9}
[add_group G] :
has_scalar ℤ (α →₀ G)
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}
@[protected, instance]
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
@[protected, instance]
noncomputable
def
finsupp.add_comm_group
{α : Type u_1}
{G : Type u_9}
[add_comm_group G] :
add_comm_group (α →₀ G)
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
theorem
finsupp.single_add_single_eq_single_add_single
{α : Type u_1}
{M : Type u_5}
[add_comm_monoid M]
{k l m n : α}
{u v : M}
(hu : u ≠ 0)
(hv : v ≠ 0) :
theorem
finsupp.single_multiset_sum
{α : Type u_1}
{M : Type u_5}
[add_comm_monoid M]
(s : multiset M)
(a : α) :
finsupp.single a s.sum = (multiset.map (finsupp.single a) s).sum
theorem
finsupp.single_finset_sum
{α : Type u_1}
{ι : Type u_4}
{M : Type u_5}
[add_comm_monoid M]
(s : finset ι)
(f : ι → M)
(a : α) :
finsupp.single a (s.sum (λ (b : ι), f b)) = s.sum (λ (b : ι), finsupp.single a (f b))
theorem
finsupp.single_sum
{α : Type u_1}
{ι : Type u_4}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
(s : ι →₀ M)
(f : ι → M → N)
(a : α) :
finsupp.single a (s.sum f) = s.sum (λ (d : ι) (c : M), finsupp.single a (f d c))
theorem
finsupp.erase_eq_sub_single
{α : Type u_1}
{G : Type u_9}
[add_group G]
(f : α →₀ G)
(a : α) :
finsupp.erase a f = f - finsupp.single a (⇑f a)
theorem
finsupp.update_eq_sub_add_single
{α : Type u_1}
{G : Type u_9}
[add_group G]
(f : α →₀ G)
(a : α)
(b : G) :
f.update a b = f - finsupp.single a (⇑f a) + finsupp.single a b
theorem
finsupp.finset_sum_apply
{α : Type u_1}
{ι : Type u_4}
{N : Type u_7}
[add_comm_monoid N]
(S : finset ι)
(f : ι → α →₀ N)
(a : α) :
theorem
finsupp.coe_finset_sum
{α : Type u_1}
{ι : Type u_4}
{N : Type u_7}
[add_comm_monoid N]
(S : finset ι)
(f : ι → α →₀ N) :
theorem
finsupp.support_sum
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[decidable_eq β]
[has_zero M]
[add_comm_monoid N]
{f : α →₀ M}
{g : α → M → β →₀ N} :
theorem
finsupp.support_finset_sum
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[decidable_eq β]
[add_comm_monoid M]
{s : finset α}
{f : α → β →₀ M} :
@[simp]
theorem
finsupp.sum_zero
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
{f : α →₀ M} :
@[simp]
theorem
finsupp.prod_inv
{α : Type u_1}
{M : Type u_5}
{G : Type u_9}
[has_zero M]
[comm_group G]
{f : α →₀ M}
{h : α → M → G} :
@[simp]
theorem
finsupp.sum_neg
{α : Type u_1}
{M : Type u_5}
{G : Type u_9}
[has_zero M]
[add_comm_group G]
{f : α →₀ M}
{h : α → M → G} :
theorem
finsupp.sum_add_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_zero_class M]
[add_comm_monoid N]
{f g : α →₀ M}
{h : α → M → N}
(h_zero : ∀ (a : α), a ∈ f.support ∪ g.support → h a 0 = 0)
(h_add : ∀ (a : α), a ∈ f.support ∪ g.support → ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) :
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.
theorem
finsupp.prod_add_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_zero_class M]
[comm_monoid N]
{f g : α →₀ M}
{h : α → M → N}
(h_zero : ∀ (a : α), a ∈ f.support ∪ g.support → h a 0 = 1)
(h_add : ∀ (a : α), a ∈ f.support ∪ g.support → ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) :
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.
theorem
finsupp.sum_add_index'
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_zero_class M]
[add_comm_monoid N]
{f g : α →₀ M}
{h : α → M → N}
(h_zero : ∀ (a : α), h a 0 = 0)
(h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) :
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.
theorem
finsupp.prod_add_index'
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_zero_class M]
[comm_monoid N]
{f g : α →₀ M}
{h : α → M → N}
(h_zero : ∀ (a : α), h a 0 = 1)
(h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) :
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.
@[simp]
theorem
finsupp.sum_hom_add_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_zero_class M]
[add_comm_monoid N]
{f g : α →₀ M}
(h : α → M →+ N) :
@[simp]
theorem
finsupp.prod_hom_add_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_zero_class M]
[comm_monoid N]
{f g : α →₀ M}
(h : α → multiplicative M →* N) :
(f + g).prod (λ (a : α) (b : M), ⇑(h a) (⇑multiplicative.of_add b)) = f.prod (λ (a : α) (b : M), ⇑(h a) (⇑multiplicative.of_add b)) * g.prod (λ (a : α) (b : M), ⇑(h a) (⇑multiplicative.of_add b))
noncomputable
def
finsupp.lift_add_hom
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_zero_class M]
[add_comm_monoid N] :
The canonical isomorphism between families of additive monoid homomorphisms α → (M →+ N)
and monoid homomorphisms (α →₀ M) →+ N.
@[simp]
theorem
finsupp.lift_add_hom_apply
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(F : α → M →+ N)
(f : α →₀ M) :
@[simp]
theorem
finsupp.lift_add_hom_symm_apply
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(F : (α →₀ M) →+ N)
(x : α) :
⇑(finsupp.lift_add_hom.symm) F x = F.comp (finsupp.single_add_hom x)
theorem
finsupp.lift_add_hom_symm_apply_apply
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(F : (α →₀ M) →+ N)
(x : α)
(y : M) :
⇑(⇑(finsupp.lift_add_hom.symm) F x) y = ⇑F (finsupp.single x y)
@[simp]
@[simp]
theorem
finsupp.sum_single
{α : Type u_1}
{M : Type u_5}
[add_comm_monoid M]
(f : α →₀ M) :
f.sum finsupp.single = f
@[simp]
theorem
finsupp.sum_univ_single
{α : Type u_1}
{M : Type u_5}
[add_comm_monoid M]
[fintype α]
(i : α)
(m : M) :
finset.univ.sum (λ (j : α), ⇑(finsupp.single i m) j) = m
@[simp]
theorem
finsupp.sum_univ_single'
{α : Type u_1}
{M : Type u_5}
[add_comm_monoid M]
[fintype α]
(i : α)
(m : M) :
finset.univ.sum (λ (j : α), ⇑(finsupp.single j m) i) = m
@[simp]
theorem
finsupp.lift_add_hom_apply_single
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : α → M →+ N)
(a : α)
(b : M) :
⇑(⇑finsupp.lift_add_hom f) (finsupp.single a b) = ⇑(f a) b
@[simp]
theorem
finsupp.lift_add_hom_comp_single
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : α → M →+ N)
(a : α) :
(⇑finsupp.lift_add_hom f).comp (finsupp.single_add_hom a) = f a
theorem
finsupp.comp_lift_add_hom
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
(g : N →+ P)
(f : α → M →+ N) :
g.comp (⇑finsupp.lift_add_hom f) = ⇑finsupp.lift_add_hom (λ (a : α), g.comp (f a))
theorem
finsupp.sum_sub_index
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_group β]
[add_comm_group γ]
{f g : α →₀ β}
{h : α → β → γ}
(h_sub : ∀ (a : α) (b₁ b₂ : β), h a (b₁ - b₂) = h a b₁ - h a b₂) :
theorem
finsupp.sum_emb_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
{v : α →₀ M}
{f : α ↪ β}
{g : β → M → N} :
(finsupp.emb_domain f v).sum g = v.sum (λ (a : α) (b : M), g (⇑f a) b)
theorem
finsupp.prod_emb_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[comm_monoid N]
{v : α →₀ M}
{f : α ↪ β}
{g : β → M → N} :
(finsupp.emb_domain f v).prod g = v.prod (λ (a : α) (b : M), g (⇑f a) b)
theorem
finsupp.prod_finset_sum_index
{α : Type u_1}
{ι : Type u_4}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[comm_monoid N]
{s : finset ι}
{g : ι → α →₀ M}
{h : α → M → N}
(h_zero : ∀ (a : α), h a 0 = 1)
(h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) :
theorem
finsupp.sum_finset_sum_index
{α : Type u_1}
{ι : Type u_4}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
{s : finset ι}
{g : ι → α →₀ M}
{h : α → M → N}
(h_zero : ∀ (a : α), h a 0 = 0)
(h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) :
theorem
finsupp.sum_sum_index
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
{f : α →₀ M}
{g : α → M → β →₀ N}
{h : β → N → P}
(h_zero : ∀ (a : β), h a 0 = 0)
(h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂) :
theorem
finsupp.prod_sum_index
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_monoid P]
{f : α →₀ M}
{g : α → M → β →₀ N}
{h : β → N → P}
(h_zero : ∀ (a : β), h a 0 = 1)
(h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ * h a b₂) :
theorem
finsupp.multiset_sum_sum_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : multiset (α →₀ M))
(h : α → M → N)
(h₀ : ∀ (a : α), h a 0 = 0)
(h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) :
theorem
finsupp.multiset_map_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{M : Type u_5}
[has_zero M]
{f : α →₀ M}
{m : β → γ}
{h : α → M → multiset β} :
multiset.map m (f.sum h) = f.sum (λ (a : α) (b : M), multiset.map m (h a b))
theorem
finsupp.sum_add_index_of_disjoint
{α : Type u_1}
{M : Type u_5}
[add_comm_monoid M]
{f1 f2 : α →₀ M}
(hd : disjoint f1.support f2.support)
{β : Type u_2}
[add_comm_monoid β]
(g : α → M → β) :
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
theorem
finsupp.prod_add_index_of_disjoint
{α : Type u_1}
{M : Type u_5}
[add_comm_monoid M]
{f1 f2 : α →₀ M}
(hd : disjoint f1.support f2.support)
{β : Type u_2}
[comm_monoid β]
(g : α → M → β) :
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
noncomputable
def
finsupp.map_range.equiv
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[has_zero N]
(f : M ≃ N)
(hf : ⇑f 0 = 0)
(hf' : ⇑(f.symm) 0 = 0) :
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 := _}
@[simp]
theorem
finsupp.map_range.equiv_refl
{α : Type u_1}
{M : Type u_5}
[has_zero M] :
finsupp.map_range.equiv (equiv.refl M) rfl rfl = equiv.refl (α →₀ M)
theorem
finsupp.map_range.equiv_trans
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[has_zero M]
[has_zero N]
[has_zero P]
(f : M ≃ N)
(hf : ⇑f 0 = 0)
(hf' : ⇑(f.symm) 0 = 0)
(f₂ : N ≃ P)
(hf₂ : ⇑f₂ 0 = 0)
(hf₂' : ⇑(f₂.symm) 0 = 0) :
finsupp.map_range.equiv (f.trans f₂) _ _ = (finsupp.map_range.equiv f hf hf').trans (finsupp.map_range.equiv f₂ hf₂ hf₂')
@[simp]
theorem
finsupp.map_range.equiv_symm
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[has_zero N]
(f : M ≃ N)
(hf : ⇑f 0 = 0)
(hf' : ⇑(f.symm) 0 = 0) :
(finsupp.map_range.equiv f hf hf').symm = finsupp.map_range.equiv f.symm hf' hf
noncomputable
def
finsupp.map_range.zero_hom
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[has_zero N]
(f : zero_hom M N) :
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' := _}
@[simp]
theorem
finsupp.map_range.zero_hom_apply
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[has_zero N]
(f : zero_hom M N)
(g : α →₀ M) :
⇑(finsupp.map_range.zero_hom f) g = finsupp.map_range ⇑f _ g
@[simp]
theorem
finsupp.map_range.zero_hom_id
{α : Type u_1}
{M : Type u_5}
[has_zero M] :
finsupp.map_range.zero_hom (zero_hom.id M) = zero_hom.id (α →₀ M)
noncomputable
def
finsupp.map_range.add_monoid_hom
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : 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' := _}
@[simp]
theorem
finsupp.map_range.add_monoid_hom_apply
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : M →+ N)
(g : α →₀ M) :
⇑(finsupp.map_range.add_monoid_hom f) g = finsupp.map_range ⇑f _ g
@[simp]
theorem
finsupp.map_range.add_monoid_hom_comp
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
(f : N →+ P)
(f₂ : M →+ N) :
@[simp]
theorem
finsupp.map_range.add_monoid_hom_to_zero_hom
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : M →+ N) :
theorem
finsupp.map_range_multiset_sum
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : M →+ N)
(m : multiset (α →₀ M)) :
finsupp.map_range ⇑f _ m.sum = (multiset.map (λ (x : α →₀ M), finsupp.map_range ⇑f _ x) m).sum
theorem
finsupp.map_range_finset_sum
{α : Type u_1}
{ι : Type u_4}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : M →+ N)
(s : finset ι)
(g : ι → α →₀ M) :
finsupp.map_range ⇑f _ (s.sum (λ (x : ι), g x)) = s.sum (λ (x : ι), finsupp.map_range ⇑f _ (g x))
noncomputable
def
finsupp.map_range.add_equiv
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : M ≃+ N) :
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' := _}
@[simp]
theorem
finsupp.map_range.add_equiv_apply
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : M ≃+ N)
(g : α →₀ M) :
⇑(finsupp.map_range.add_equiv f) g = finsupp.map_range ⇑f _ g
@[simp]
theorem
finsupp.map_range.add_equiv_trans
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{P : Type u_8}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
(f : M ≃+ N)
(f₂ : N ≃+ P) :
@[simp]
theorem
finsupp.map_range.add_equiv_symm
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : M ≃+ N) :
@[simp]
theorem
finsupp.map_range.add_equiv_to_add_monoid_hom
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : M ≃+ N) :
@[simp]
theorem
finsupp.map_range.add_equiv_to_equiv
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : M ≃+ N) :
Declarations about map_domain #
noncomputable
def
finsupp.map_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(f : α → β)
(v : α →₀ M) :
β →₀ M
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))
theorem
finsupp.map_domain_apply
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
{f : α → β}
(hf : function.injective f)
(x : α →₀ M)
(a : α) :
⇑(finsupp.map_domain f x) (f a) = ⇑x a
theorem
finsupp.map_domain_notin_range
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
{f : α → β}
(x : α →₀ M)
(a : β)
(h : a ∉ set.range f) :
⇑(finsupp.map_domain f x) a = 0
@[simp]
theorem
finsupp.map_domain_id
{α : Type u_1}
{M : Type u_5}
[add_comm_monoid M]
{v : α →₀ M} :
finsupp.map_domain id v = v
theorem
finsupp.map_domain_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{M : Type u_5}
[add_comm_monoid M]
{v : α →₀ M}
{f : α → β}
{g : β → γ} :
finsupp.map_domain (g ∘ f) v = finsupp.map_domain g (finsupp.map_domain f v)
@[simp]
theorem
finsupp.map_domain_single
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
{f : α → β}
{a : α}
{b : M} :
finsupp.map_domain f (finsupp.single a b) = finsupp.single (f a) b
@[simp]
theorem
finsupp.map_domain_zero
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
{f : α → β} :
finsupp.map_domain f 0 = 0
theorem
finsupp.map_domain_congr
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
{v : α →₀ M}
{f g : α → β}
(h : ∀ (x : α), x ∈ v.support → f x = g x) :
finsupp.map_domain f v = finsupp.map_domain g v
theorem
finsupp.map_domain_add
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
{v₁ v₂ : α →₀ M}
{f : α → β} :
finsupp.map_domain f (v₁ + v₂) = finsupp.map_domain f v₁ + finsupp.map_domain f v₂
@[simp]
theorem
finsupp.map_domain_equiv_apply
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
{f : α ≃ β}
(x : α →₀ M)
(a : β) :
@[simp]
theorem
finsupp.map_domain.add_monoid_hom_apply
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(f : α → β)
(v : α →₀ M) :
noncomputable
def
finsupp.map_domain.add_monoid_hom
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(f : α → β) :
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' := _}
@[simp]
theorem
finsupp.map_domain.add_monoid_hom_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{M : Type u_5}
[add_comm_monoid M]
(f : β → γ)
(g : α → β) :
theorem
finsupp.map_domain_finset_sum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
{M : Type u_5}
[add_comm_monoid M]
{f : α → β}
{s : finset ι}
{v : ι → α →₀ M} :
finsupp.map_domain f (s.sum (λ (i : ι), v i)) = s.sum (λ (i : ι), finsupp.map_domain f (v i))
theorem
finsupp.map_domain_sum
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[has_zero N]
{f : α → β}
{s : α →₀ N}
{v : α → N → α →₀ M} :
finsupp.map_domain f (s.sum v) = s.sum (λ (a : α) (b : N), finsupp.map_domain f (v a b))
theorem
finsupp.map_domain_support
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
[decidable_eq β]
{f : α → β}
{s : α →₀ M} :
(finsupp.map_domain f s).support ⊆ finset.image f s.support
theorem
finsupp.map_domain_apply'
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(S : set α)
{f : α → β}
(x : α →₀ M)
(hS : ↑(x.support) ⊆ S)
(hf : set.inj_on f S)
{a : α}
(ha : a ∈ S) :
⇑(finsupp.map_domain f x) (f a) = ⇑x a
theorem
finsupp.map_domain_support_of_inj_on
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
[decidable_eq β]
{f : α → β}
(s : α →₀ M)
(hf : set.inj_on f ↑(s.support)) :
(finsupp.map_domain f s).support = finset.image f s.support
theorem
finsupp.map_domain_support_of_injective
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
[decidable_eq β]
{f : α → β}
(hf : function.injective f)
(s : α →₀ M) :
(finsupp.map_domain f s).support = finset.image f s.support
theorem
finsupp.sum_map_domain_index
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
{f : α → β}
{s : α →₀ M}
{h : β → M → N}
(h_zero : ∀ (b : β), h b 0 = 0)
(h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ + h b m₂) :
(finsupp.map_domain f s).sum h = s.sum (λ (a : α) (m : M), h (f a) m)
theorem
finsupp.prod_map_domain_index
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[comm_monoid N]
{f : α → β}
{s : α →₀ M}
{h : β → M → N}
(h_zero : ∀ (b : β), h b 0 = 1)
(h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ * h b m₂) :
(finsupp.map_domain f s).prod h = s.prod (λ (a : α) (m : M), h (f a) m)
@[simp]
theorem
finsupp.sum_map_domain_index_add_monoid_hom
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
{f : α → β}
{s : α →₀ M}
(h : β → M →+ N) :
A version of sum_map_domain_index that takes a bundled add_monoid_hom,
rather than separate linearity hypotheses.
theorem
finsupp.emb_domain_eq_map_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(f : α ↪ β)
(v : α →₀ M) :
finsupp.emb_domain f v = finsupp.map_domain ⇑f v
theorem
finsupp.prod_map_domain_index_inj
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[comm_monoid N]
{f : α → β}
{s : α →₀ M}
{h : β → M → N}
(hf : function.injective f) :
(finsupp.map_domain f s).prod h = s.prod (λ (a : α) (b : M), h (f a) b)
theorem
finsupp.sum_map_domain_index_inj
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
{f : α → β}
{s : α →₀ M}
{h : β → M → N}
(hf : function.injective f) :
(finsupp.map_domain f s).sum h = s.sum (λ (a : α) (b : M), h (f a) b)
theorem
finsupp.map_domain_injective
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
{f : α → β}
(hf : function.injective f) :
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' := _}
@[simp]
theorem
finsupp.map_domain.add_monoid_hom_comp_map_range
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : α → β)
(g : M →+ N) :
theorem
finsupp.map_domain_map_range
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : α → β)
(v : α →₀ M)
(g : M → N)
(h0 : g 0 = 0)
(hadd : ∀ (x y : M), g (x + y) = g x + g y) :
finsupp.map_domain f (finsupp.map_range g h0 v) = finsupp.map_range g h0 (finsupp.map_domain f v)
When g preserves addition, map_range and map_domain commute.
theorem
finsupp.sum_update_add
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[add_comm_monoid α]
[add_comm_monoid β]
(f : ι →₀ α)
(i : ι)
(a : α)
(g : ι → α → β)
(hg : ∀ (i : ι), g i 0 = 0)
(hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂) :
theorem
finsupp.map_domain_inj_on
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(S : set α)
{f : α → β}
(hf : set.inj_on f S) :
set.inj_on (finsupp.map_domain f) {w : α →₀ M | ↑(w.support) ⊆ S}
Declarations about comap_domain #
@[simp]
theorem
finsupp.comap_domain_support
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α → β)
(l : β →₀ M)
(hf : set.inj_on f (f ⁻¹' ↑(l.support))) :
(finsupp.comap_domain f l hf).support = l.support.preimage f hf
noncomputable
def
finsupp.comap_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α → β)
(l : β →₀ M)
(hf : set.inj_on f (f ⁻¹' ↑(l.support))) :
α →₀ M
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 := _}
@[simp]
theorem
finsupp.comap_domain_apply
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α → β)
(l : β →₀ M)
(hf : set.inj_on f (f ⁻¹' ↑(l.support)))
(a : α) :
⇑(finsupp.comap_domain f l hf) a = ⇑l (f a)
theorem
finsupp.sum_comap_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
[add_comm_monoid N]
(f : α → β)
(l : β →₀ M)
(g : β → M → N)
(hf : set.bij_on f (f ⁻¹' ↑(l.support)) ↑(l.support)) :
(finsupp.comap_domain f l _).sum (g ∘ f) = l.sum g
theorem
finsupp.eq_zero_of_comap_domain_eq_zero
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(f : α → β)
(l : β →₀ M)
(hf : set.bij_on f (f ⁻¹' ↑(l.support)) ↑(l.support)) :
finsupp.comap_domain f l _ = 0 → l = 0
@[simp]
theorem
finsupp.comap_domain_zero
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α → β)
(hif : set.inj_on f (f ⁻¹' ↑(0.support)) := _) :
finsupp.comap_domain f 0 hif = 0
Note the hif argument is needed for this to work in rw.
@[simp]
theorem
finsupp.comap_domain_single
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α → β)
(a : α)
(m : M)
(hif : set.inj_on f (f ⁻¹' ↑((finsupp.single (f a) m).support))) :
finsupp.comap_domain f (finsupp.single (f a) m) hif = finsupp.single a m
theorem
finsupp.comap_domain_add
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_zero_class M]
{f : α → β}
(v₁ v₂ : β →₀ M)
(hv₁ : set.inj_on f (f ⁻¹' ↑(v₁.support)))
(hv₂ : set.inj_on f (f ⁻¹' ↑(v₂.support)))
(hv₁₂ : set.inj_on f (f ⁻¹' ↑((v₁ + v₂).support))) :
finsupp.comap_domain f (v₁ + v₂) hv₁₂ = finsupp.comap_domain f v₁ hv₁ + finsupp.comap_domain f v₂ hv₂
theorem
finsupp.comap_domain_add_of_injective
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_zero_class M]
{f : α → β}
(hf : function.injective f)
(v₁ v₂ : β →₀ M) :
finsupp.comap_domain f (v₁ + v₂) _ = finsupp.comap_domain f v₁ _ + finsupp.comap_domain f v₂ _
A version of finsupp.comap_domain_add that's easier to use.
noncomputable
def
finsupp.comap_domain.add_monoid_hom
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_zero_class M]
{f : α → β}
(hf : function.injective f) :
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' := _}
@[simp]
theorem
finsupp.comap_domain.add_monoid_hom_apply
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_zero_class M]
{f : α → β}
(hf : function.injective f)
(x : β →₀ M) :
⇑(finsupp.comap_domain.add_monoid_hom hf) x = finsupp.comap_domain f x _
theorem
finsupp.map_domain_comap_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(f : α → β)
(hf : function.injective f)
(l : β →₀ M)
(hl : ↑(l.support) ⊆ set.range f) :
finsupp.map_domain f (finsupp.comap_domain f l _) = l
noncomputable
def
finsupp.some
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(f : option α →₀ M) :
α →₀ M
Restrict a finitely supported function on option α to a finitely supported function on α.
Equations
- f.some = finsupp.comap_domain option.some f _
@[simp]
theorem
finsupp.some_apply
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(f : option α →₀ M)
(a : α) :
⇑(f.some) a = ⇑f (option.some a)
@[simp]
theorem
finsupp.some_single_none
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(m : M) :
(finsupp.single option.none m).some = 0
@[simp]
theorem
finsupp.some_single_some
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(a : α)
(m : M) :
(finsupp.single (option.some a) m).some = finsupp.single a m
theorem
finsupp.prod_option_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[comm_monoid N]
(f : option α →₀ M)
(b : option α → M → N)
(h_zero : ∀ (o : option α), b o 0 = 1)
(h_add : ∀ (o : option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂) :
f.prod b = b option.none (⇑f option.none) * f.some.prod (λ (a : α), b (option.some a))
theorem
finsupp.sum_option_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : option α →₀ M)
(b : option α → M → N)
(h_zero : ∀ (o : option α), b o 0 = 0)
(h_add : ∀ (o : option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ + b o m₂) :
f.sum b = b option.none (⇑f option.none) + f.some.sum (λ (a : α), b (option.some a))
theorem
finsupp.sum_option_index_smul
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
[semiring R]
[add_comm_monoid M]
[module R M]
(f : option α →₀ R)
(b : option α → M) :
f.sum (λ (o : option α) (r : R), r • b o) = ⇑f option.none • b option.none + f.some.sum (λ (a : α) (r : R), r • b (option.some a))
Declarations about equiv_congr_left #
def
finsupp.equiv_map_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α ≃ β)
(l : α →₀ M) :
β →₀ M
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 := _}
@[simp]
theorem
finsupp.equiv_map_domain_refl
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(l : α →₀ M) :
finsupp.equiv_map_domain (equiv.refl α) l = l
theorem
finsupp.equiv_map_domain_trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{M : Type u_5}
[has_zero M]
(f : α ≃ β)
(g : β ≃ γ)
(l : α →₀ M) :
finsupp.equiv_map_domain (f.trans g) l = finsupp.equiv_map_domain g (finsupp.equiv_map_domain f l)
theorem
finsupp.equiv_map_domain_trans'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{M : Type u_5}
[has_zero M]
(f : α ≃ β)
(g : β ≃ γ) :
@[simp]