Miscellaneous definitions, lemmas, and constructions using finsupp #
Main declarations #
finsupp.graph: the finset of input and output pairs with non-zero outputs.alist.lookup_finsupp: converts an association list into a finitely supported function viaalist.lookup, sending absent keys to zero.finsupp.map_range.equiv:finsupp.map_rangeas an equiv.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.some: restrict a finitely supported function onoption αto a finitely supported function onα.finsupp.filter:filter p fis the finitely supported function that isf aifp ais true and 0 otherwise.finsupp.frange: the image of a finitely supported function on its support.finsupp.subtype_domain: the restriction of a finitely supported functionfto a subtype.
Implementation notes #
This file is a noncomputable theory and uses classical logic throughout.
TODO #
-
This file is currently ~1600 lines long and is quite a miscellany of definitions and lemmas, so it should be divided into smaller pieces.
-
Expand the list of definitions and important lemmas to the module docstring.
Declarations about graph #
The graph of a finitely supported function over its support, i.e. the finset of input and output pairs with non-zero outputs.
@[simp]
Declarations about alist.lookup_finsupp #
@[simp]
theorem
alist.lookup_finsupp_to_fun
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(l : alist (λ (x : α), M))
(a : α) :
⇑(l.lookup_finsupp) a = (alist.lookup a l).get_or_else 0
noncomputable
def
alist.lookup_finsupp
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(l : alist (λ (x : α), M)) :
α →₀ M
Converts an association list into a finitely supported function via alist.lookup, sending
absent keys to zero.
Equations
- l.lookup_finsupp = {support := (list.filter (λ (x : Σ (x : α), M), x.snd ≠ 0) l.entries).keys.to_finset, to_fun := λ (a : α), (alist.lookup a l).get_or_else 0, mem_support_to_fun := _}
@[simp]
theorem
alist.lookup_finsupp_support
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(l : alist (λ (x : α), M)) :
l.lookup_finsupp.support = (list.filter (λ (x : Σ (x : α), M), x.snd ≠ 0) l.entries).keys.to_finset
theorem
alist.lookup_finsupp_apply
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(l : alist (λ (x : α), M))
(a : α) :
⇑(l.lookup_finsupp) a = (alist.lookup a l).get_or_else 0
Alias of alist.lookup_finsupp_to_fun.
theorem
alist.lookup_finsupp_eq_iff_of_ne_zero
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{l : alist (λ (x : α), M)}
{a : α}
{x : M}
(hx : x ≠ 0) :
⇑(l.lookup_finsupp) a = x ↔ x ∈ alist.lookup a l
theorem
alist.lookup_finsupp_eq_zero_iff
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{l : alist (λ (x : α), M)}
{a : α} :
⇑(l.lookup_finsupp) a = 0 ↔ a ∉ l ∨ 0 ∈ alist.lookup a l
@[simp]
theorem
alist.empty_lookup_finsupp
{α : Type u_1}
{M : Type u_5}
[has_zero M] :
∅.lookup_finsupp = 0
@[simp]
theorem
alist.insert_lookup_finsupp
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(l : alist (λ (x : α), M))
(a : α)
(m : M) :
(alist.insert a m l).lookup_finsupp = l.lookup_finsupp.update a m
@[simp]
theorem
alist.singleton_lookup_finsupp
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(a : α)
(m : M) :
(alist.singleton a m).lookup_finsupp = finsupp.single a m
@[simp]
theorem
finsupp.to_alist_lookup_finsupp
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(f : α →₀ M) :
f.to_alist.lookup_finsupp = f
Declarations about map_range #
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 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]
theorem
finsupp.equiv_map_domain_single
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α ≃ β)
(a : α)
(b : M) :
finsupp.equiv_map_domain f (finsupp.single a b) = finsupp.single (⇑f a) b
@[simp]
theorem
finsupp.equiv_map_domain_zero
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
{f : α ≃ β} :
finsupp.equiv_map_domain f 0 = 0
def
finsupp.equiv_congr_left
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α ≃ β) :
Given f : α ≃ β, the finitely supported function spaces are also in bijection:
(α →₀ M) ≃ (β →₀ M).
This is the finitely-supported version of equiv.Pi_congr_left.
Equations
- finsupp.equiv_congr_left f = {to_fun := finsupp.equiv_map_domain f, inv_fun := finsupp.equiv_map_domain f.symm, left_inv := _, right_inv := _}
@[simp]
theorem
finsupp.equiv_congr_left_apply
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α ≃ β)
(l : α →₀ M) :
@[simp]
theorem
finsupp.equiv_congr_left_symm
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[has_zero M]
(f : α ≃ β) :
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}
theorem
finsupp.equiv_map_domain_eq_map_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[add_comm_monoid M]
(f : α ≃ β)
(l : α →₀ M) :
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))
noncomputable
def
finsupp.filter
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(p : α → Prop)
(f : α →₀ M) :
α →₀ M
filter p f is the finitely supported function that is f a if p a is true and 0 otherwise.
Equations
- finsupp.filter p f = {support := finset.filter (λ (a : α), p a) f.support, to_fun := λ (a : α), ite (p a) (⇑f a) 0, mem_support_to_fun := _}
theorem
finsupp.filter_apply
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(p : α → Prop)
(f : α →₀ M)
(a : α)
[D : decidable (p a)] :
⇑(finsupp.filter p f) a = ite (p a) (⇑f a) 0
theorem
finsupp.filter_eq_indicator
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(p : α → Prop)
(f : α →₀ M) :
⇑(finsupp.filter p f) = {x : α | p x}.indicator ⇑f
theorem
finsupp.filter_eq_zero_iff
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(p : α → Prop)
(f : α →₀ M) :
finsupp.filter p f = 0 ↔ ∀ (x : α), p x → ⇑f x = 0
theorem
finsupp.filter_eq_self_iff
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(p : α → Prop)
(f : α →₀ M) :
finsupp.filter p f = f ↔ ∀ (x : α), ⇑f x ≠ 0 → p x
@[simp]
theorem
finsupp.filter_apply_pos
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(p : α → Prop)
(f : α →₀ M)
{a : α}
(h : p a) :
⇑(finsupp.filter p f) a = ⇑f a
@[simp]
theorem
finsupp.filter_apply_neg
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(p : α → Prop)
(f : α →₀ M)
{a : α}
(h : ¬p a) :
⇑(finsupp.filter p f) a = 0
@[simp]
theorem
finsupp.support_filter
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(p : α → Prop)
(f : α →₀ M)
[D : decidable_pred p] :
(finsupp.filter p f).support = finset.filter p f.support
theorem
finsupp.filter_zero
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(p : α → Prop) :
finsupp.filter p 0 = 0
@[simp]
theorem
finsupp.filter_single_of_pos
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(p : α → Prop)
{a : α}
{b : M}
(h : p a) :
finsupp.filter p (finsupp.single a b) = finsupp.single a b
@[simp]
theorem
finsupp.filter_single_of_neg
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(p : α → Prop)
{a : α}
{b : M}
(h : ¬p a) :
finsupp.filter p (finsupp.single a b) = 0
theorem
finsupp.prod_filter_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
(p : α → Prop)
(f : α →₀ M)
[comm_monoid N]
(g : α → M → N) :
(finsupp.filter p f).prod g = (finsupp.filter p f).support.prod (λ (x : α), g x (⇑f x))
theorem
finsupp.sum_filter_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
(p : α → Prop)
(f : α →₀ M)
[add_comm_monoid N]
(g : α → M → N) :
(finsupp.filter p f).sum g = (finsupp.filter p f).support.sum (λ (x : α), g x (⇑f x))
@[simp]
theorem
finsupp.sum_filter_add_sum_filter_not
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
(p : α → Prop)
(f : α →₀ M)
[add_comm_monoid N]
(g : α → M → N) :
(finsupp.filter p f).sum g + (finsupp.filter (λ (a : α), ¬p a) f).sum g = f.sum g
@[simp]
theorem
finsupp.prod_filter_mul_prod_filter_not
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
(p : α → Prop)
(f : α →₀ M)
[comm_monoid N]
(g : α → M → N) :
(finsupp.filter p f).prod g * (finsupp.filter (λ (a : α), ¬p a) f).prod g = f.prod g
@[simp]
theorem
finsupp.sum_sub_sum_filter
{α : Type u_1}
{M : Type u_5}
{G : Type u_9}
[has_zero M]
(p : α → Prop)
(f : α →₀ M)
[add_comm_group G]
(g : α → M → G) :
f.sum g - (finsupp.filter p f).sum g = (finsupp.filter (λ (a : α), ¬p a) f).sum g
@[simp]
theorem
finsupp.prod_div_prod_filter
{α : Type u_1}
{M : Type u_5}
{G : Type u_9}
[has_zero M]
(p : α → Prop)
(f : α →₀ M)
[comm_group G]
(g : α → M → G) :
f.prod g / (finsupp.filter p f).prod g = (finsupp.filter (λ (a : α), ¬p a) f).prod g
theorem
finsupp.filter_pos_add_filter_neg
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(f : α →₀ M)
(p : α → Prop) :
finsupp.filter p f + finsupp.filter (λ (a : α), ¬p a) f = f
Declarations about frange #
frange f is the image of f on the support of f.
Equations
- f.frange = finset.image ⇑f f.support
theorem
finsupp.frange_single
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{x : α}
{y : M} :
(finsupp.single x y).frange ⊆ {y}
Declarations about subtype_domain #
noncomputable
def
finsupp.subtype_domain
{α : Type u_1}
{M : Type u_5}
[has_zero M]
(p : α → Prop)
(f : α →₀ M) :
subtype_domain p f is the restriction of the finitely supported function f to subtype p.
Equations
- finsupp.subtype_domain p f = {support := finset.subtype p f.support, to_fun := ⇑f ∘ coe, mem_support_to_fun := _}
@[simp]
theorem
finsupp.support_subtype_domain
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{p : α → Prop}
[D : decidable_pred p]
{f : α →₀ M} :
(finsupp.subtype_domain p f).support = finset.subtype p f.support
@[simp]
theorem
finsupp.subtype_domain_apply
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{p : α → Prop}
{a : subtype p}
{v : α →₀ M} :
⇑(finsupp.subtype_domain p v) a = ⇑v a.val
@[simp]
theorem
finsupp.subtype_domain_zero
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{p : α → Prop} :
finsupp.subtype_domain p 0 = 0
theorem
finsupp.subtype_domain_eq_zero_iff'
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{p : α → Prop}
{f : α →₀ M} :
finsupp.subtype_domain p f = 0 ↔ ∀ (x : α), p x → ⇑f x = 0
theorem
finsupp.subtype_domain_eq_zero_iff
{α : Type u_1}
{M : Type u_5}
[has_zero M]
{p : α → Prop}
{f : α →₀ M}
(hf : ∀ (x : α), x ∈ f.support → p x) :
finsupp.subtype_domain p f = 0 ↔ f = 0
theorem
finsupp.sum_subtype_domain_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
{p : α → Prop}
[add_comm_monoid N]
{v : α →₀ M}
{h : α → M → N}
(hp : ∀ (x : α), x ∈ v.support → p x) :
theorem
finsupp.prod_subtype_domain_index
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
[has_zero M]
{p : α → Prop}
[comm_monoid N]
{v : α →₀ M}
{h : α → M → N}
(hp : ∀ (x : α), x ∈ v.support → p x) :
@[simp]
theorem
finsupp.subtype_domain_add
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
{p : α → Prop}
{v v' : α →₀ M} :
finsupp.subtype_domain p (v + v') = finsupp.subtype_domain p v + finsupp.subtype_domain p v'
noncomputable
def
finsupp.subtype_domain_add_monoid_hom
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
{p : α → Prop} :
subtype_domain but as an add_monoid_hom.
Equations
- finsupp.subtype_domain_add_monoid_hom = {to_fun := finsupp.subtype_domain p, map_zero' := _, map_add' := _}
noncomputable
def
finsupp.filter_add_hom
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
(p : α → Prop) :
finsupp.filter as an add_monoid_hom.
Equations
- finsupp.filter_add_hom p = {to_fun := finsupp.filter p, map_zero' := _, map_add' := _}
@[simp]
theorem
finsupp.filter_add
{α : Type u_1}
{M : Type u_5}
[add_zero_class M]
{p : α → Prop}
{v v' : α →₀ M} :
finsupp.filter p (v + v') = finsupp.filter p v + finsupp.filter p v'
theorem
finsupp.subtype_domain_sum
{α : Type u_1}
{ι : Type u_4}
{M : Type u_5}
[add_comm_monoid M]
{p : α → Prop}
{s : finset ι}
{h : ι → α →₀ M} :
finsupp.subtype_domain p (s.sum (λ (c : ι), h c)) = s.sum (λ (c : ι), finsupp.subtype_domain p (h c))
theorem
finsupp.subtype_domain_finsupp_sum
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
{p : α → Prop}
[has_zero N]
{s : β →₀ N}
{h : β → N → α →₀ M} :
finsupp.subtype_domain p (s.sum h) = s.sum (λ (c : β) (d : N), finsupp.subtype_domain p (h c d))
theorem
finsupp.filter_sum
{α : Type u_1}
{ι : Type u_4}
{M : Type u_5}
[add_comm_monoid M]
{p : α → Prop}
(s : finset ι)
(f : ι → α →₀ M) :
finsupp.filter p (s.sum (λ (a : ι), f a)) = s.sum (λ (a : ι), finsupp.filter p (f a))
theorem
finsupp.filter_eq_sum
{α : Type u_1}
{M : Type u_5}
[add_comm_monoid M]
(p : α → Prop)
[D : decidable_pred p]
(f : α →₀ M) :
finsupp.filter p f = (finset.filter p f.support).sum (λ (i : α), finsupp.single i (⇑f i))
@[simp]
theorem
finsupp.subtype_domain_neg
{α : Type u_1}
{G : Type u_9}
[add_group G]
{p : α → Prop}
{v : α →₀ G} :
finsupp.subtype_domain p (-v) = -finsupp.subtype_domain p v
@[simp]
theorem
finsupp.subtype_domain_sub
{α : Type u_1}
{G : Type u_9}
[add_group G]
{p : α → Prop}
{v v' : α →₀ G} :
finsupp.subtype_domain p (v - v') = finsupp.subtype_domain p v - finsupp.subtype_domain p v'
@[simp]
theorem
finsupp.single_neg
{α : Type u_1}
{G : Type u_9}
[add_group G]
(a : α)
(b : G) :
finsupp.single a (-b) = -finsupp.single a b
@[simp]
theorem
finsupp.single_sub
{α : Type u_1}
{G : Type u_9}
[add_group G]
(a : α)
(b₁ b₂ : G) :
finsupp.single a (b₁ - b₂) = finsupp.single a b₁ - finsupp.single a b₂
@[simp]
theorem
finsupp.erase_neg
{α : Type u_1}
{G : Type u_9}
[add_group G]
(a : α)
(f : α →₀ G) :
finsupp.erase a (-f) = -finsupp.erase a f
@[simp]
theorem
finsupp.erase_sub
{α : Type u_1}
{G : Type u_9}
[add_group G]
(a : α)
(f₁ f₂ : α →₀ G) :
finsupp.erase a (f₁ - f₂) = finsupp.erase a f₁ - finsupp.erase a f₂
@[simp]
theorem
finsupp.filter_neg
{α : Type u_1}
{G : Type u_9}
[add_group G]
(p : α → Prop)
(f : α →₀ G) :
finsupp.filter p (-f) = -finsupp.filter p f
@[simp]
theorem
finsupp.filter_sub
{α : Type u_1}
{G : Type u_9}
[add_group G]
(p : α → Prop)
(f₁ f₂ : α →₀ G) :
finsupp.filter p (f₁ - f₂) = finsupp.filter p f₁ - finsupp.filter p f₂
Declarations about curry and uncurry #
@[protected]
noncomputable
def
finsupp.curry
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(f : α × β →₀ M) :
Given a finitely supported function f from a product type α × β to γ,
curry f is the "curried" finitely supported function from α to the type of
finitely supported functions from β to γ.
Equations
- f.curry = f.sum (λ (p : α × β) (c : M), finsupp.single p.fst (finsupp.single p.snd c))
@[simp]
theorem
finsupp.curry_apply
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(f : α × β →₀ M)
(x : α)
(y : β) :
theorem
finsupp.sum_curry_index
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{N : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
(f : α × β →₀ M)
(g : α → β → M → N)
(hg₀ : ∀ (a : α) (b : β), g a b 0 = 0)
(hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁) :
@[protected]
noncomputable
def
finsupp.uncurry
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(f : α →₀ β →₀ M) :
Given a finitely supported function f from α to the type of
finitely supported functions from β to M,
uncurry f is the "uncurried" finitely supported function from α × β to M.
noncomputable
def
finsupp.finsupp_prod_equiv
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M] :
finsupp_prod_equiv defines the equiv between ((α × β) →₀ M) and (α →₀ (β →₀ M)) given by
currying and uncurrying.
Equations
- finsupp.finsupp_prod_equiv = {to_fun := finsupp.curry _inst_1, inv_fun := finsupp.uncurry _inst_1, left_inv := _, right_inv := _}
theorem
finsupp.filter_curry
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(f : α × β →₀ M)
(p : α → Prop) :
(finsupp.filter (λ (a : α × β), p a.fst) f).curry = finsupp.filter p f.curry
theorem
finsupp.support_curry
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
[decidable_eq α]
(f : α × β →₀ M) :
noncomputable
def
finsupp.sum_elim
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_zero γ]
(f : α →₀ γ)
(g : β →₀ γ) :
finsupp.sum_elim f g maps inl x to f x and inr y to g y.
noncomputable
def
finsupp.sum_finsupp_equiv_prod_finsupp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_zero γ] :
The equivalence between (α ⊕ β) →₀ γ and (α →₀ γ) × (β →₀ γ).
This is the finsupp version of equiv.sum_arrow_equiv_prod_arrow.
@[simp]
theorem
finsupp.sum_finsupp_equiv_prod_finsupp_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_zero γ]
(f : α ⊕ β →₀ γ) :
@[simp]
theorem
finsupp.sum_finsupp_add_equiv_prod_finsupp_symm_apply
{M : Type u_5}
[add_monoid M]
{α : Type u_1}
{β : Type u_2}
(ᾰ : (α →₀ M) × (β →₀ M)) :
@[simp]
theorem
finsupp.sum_finsupp_add_equiv_prod_finsupp_apply
{M : Type u_5}
[add_monoid M]
{α : Type u_1}
{β : Type u_2}
(ᾰ : α ⊕ β →₀ M) :
noncomputable
def
finsupp.sum_finsupp_add_equiv_prod_finsupp
{M : Type u_5}
[add_monoid M]
{α : Type u_1}
{β : Type u_2} :
The additive equivalence between (α ⊕ β) →₀ M and (α →₀ M) × (β →₀ M).
This is the finsupp version of equiv.sum_arrow_equiv_prod_arrow.
Equations
theorem
finsupp.fst_sum_finsupp_add_equiv_prod_finsupp
{M : Type u_5}
[add_monoid M]
{α : Type u_1}
{β : Type u_2}
(f : α ⊕ β →₀ M)
(x : α) :
theorem
finsupp.snd_sum_finsupp_add_equiv_prod_finsupp
{M : Type u_5}
[add_monoid M]
{α : Type u_1}
{β : Type u_2}
(f : α ⊕ β →₀ M)
(y : β) :
theorem
finsupp.sum_finsupp_add_equiv_prod_finsupp_symm_inl
{M : Type u_5}
[add_monoid M]
{α : Type u_1}
{β : Type u_2}
(fg : (α →₀ M) × (β →₀ M))
(x : α) :
theorem
finsupp.sum_finsupp_add_equiv_prod_finsupp_symm_inr
{M : Type u_5}
[add_monoid M]
{α : Type u_1}
{β : Type u_2}
(fg : (α →₀ M) × (β →₀ M))
(y : β) :
Declarations about scalar multiplication #
@[simp]
theorem
finsupp.single_smul
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
[has_zero M]
[monoid_with_zero R]
[mul_action_with_zero R M]
(a b : α)
(f : α → M)
(r : R) :
⇑(finsupp.single a r) b • f a = ⇑(finsupp.single a (r • f b)) b
noncomputable
def
finsupp.comap_has_smul
{α : Type u_1}
{M : Type u_5}
{G : Type u_9}
[monoid G]
[mul_action G α]
[add_comm_monoid M] :
Scalar multiplication acting on the domain.
This is not an instance as it would conflict with the action on the range.
See the instance_diamonds test for examples of such conflicts.
Equations
- finsupp.comap_has_smul = {smul := λ (g : G), finsupp.map_domain (has_smul.smul g)}
theorem
finsupp.comap_smul_def
{α : Type u_1}
{M : Type u_5}
{G : Type u_9}
[monoid G]
[mul_action G α]
[add_comm_monoid M]
(g : G)
(f : α →₀ M) :
g • f = finsupp.map_domain (has_smul.smul g) f
@[simp]
theorem
finsupp.comap_smul_single
{α : Type u_1}
{M : Type u_5}
{G : Type u_9}
[monoid G]
[mul_action G α]
[add_comm_monoid M]
(g : G)
(a : α)
(b : M) :
g • finsupp.single a b = finsupp.single (g • a) b
noncomputable
def
finsupp.comap_mul_action
{α : Type u_1}
{M : Type u_5}
{G : Type u_9}
[monoid G]
[mul_action G α]
[add_comm_monoid M] :
mul_action G (α →₀ M)
finsupp.comap_has_smul is multiplicative
Equations
- finsupp.comap_mul_action = {to_has_smul := finsupp.comap_has_smul _inst_3, one_smul := _, mul_smul := _}
noncomputable
def
finsupp.comap_distrib_mul_action
{α : Type u_1}
{M : Type u_5}
{G : Type u_9}
[monoid G]
[mul_action G α]
[add_comm_monoid M] :
distrib_mul_action G (α →₀ M)
finsupp.comap_has_smul is distributive
Equations
- finsupp.comap_distrib_mul_action = {to_mul_action := finsupp.comap_mul_action _inst_3, smul_zero := _, smul_add := _}
@[simp]
theorem
finsupp.comap_smul_apply
{α : Type u_1}
{M : Type u_5}
{G : Type u_9}
[group G]
[mul_action G α]
[add_comm_monoid M]
(g : G)
(f : α →₀ M)
(a : α) :
When G is a group, finsupp.comap_has_smul acts by precomposition with the action of g⁻¹.
@[protected, instance]
noncomputable
def
finsupp.has_smul
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
[monoid R]
[add_monoid M]
[distrib_mul_action R M] :
Equations
- finsupp.has_smul = {smul := λ (a : R) (v : α →₀ M), finsupp.map_range (has_smul.smul a) _ v}
Throughout this section, some monoid and semiring arguments are specified with {} instead of
[]. See note [implicit instance arguments].
@[simp]
theorem
finsupp.coe_smul
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
{_x : monoid R}
[add_monoid M]
[distrib_mul_action R M]
(b : R)
(v : α →₀ M) :
theorem
finsupp.smul_apply
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
{_x : monoid R}
[add_monoid M]
[distrib_mul_action R M]
(b : R)
(v : α →₀ M)
(a : α) :
theorem
is_smul_regular.finsupp
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
{_x : monoid R}
[add_monoid M]
[distrib_mul_action R M]
{k : R}
(hk : is_smul_regular M k) :
is_smul_regular (α →₀ M) k
@[protected, instance]
def
finsupp.has_faithful_smul
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
[monoid R]
[nonempty α]
[add_monoid M]
[distrib_mul_action R M]
[has_faithful_smul R M] :
has_faithful_smul R (α →₀ M)
@[protected, instance]
noncomputable
def
finsupp.distrib_mul_action
(α : Type u_1)
(M : Type u_5)
{R : Type u_11}
[monoid R]
[add_monoid M]
[distrib_mul_action R M] :
distrib_mul_action R (α →₀ M)
Equations
- finsupp.distrib_mul_action α M = {to_mul_action := {to_has_smul := {smul := has_smul.smul finsupp.has_smul}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}
@[protected, instance]
def
finsupp.is_scalar_tower
(α : Type u_1)
(M : Type u_5)
{R : Type u_11}
{S : Type u_12}
[monoid R]
[monoid S]
[add_monoid M]
[distrib_mul_action R M]
[distrib_mul_action S M]
[has_smul R S]
[is_scalar_tower R S M] :
is_scalar_tower R S (α →₀ M)
@[protected, instance]
def
finsupp.smul_comm_class
(α : Type u_1)
(M : Type u_5)
{R : Type u_11}
{S : Type u_12}
[monoid R]
[monoid S]
[add_monoid M]
[distrib_mul_action R M]
[distrib_mul_action S M]
[smul_comm_class R S M] :
smul_comm_class R S (α →₀ M)
@[protected, instance]
def
finsupp.is_central_scalar
(α : Type u_1)
(M : Type u_5)
{R : Type u_11}
[monoid R]
[add_monoid M]
[distrib_mul_action R M]
[distrib_mul_action Rᵐᵒᵖ M]
[is_central_scalar R M] :
is_central_scalar R (α →₀ M)
@[protected, instance]
noncomputable
def
finsupp.module
(α : Type u_1)
(M : Type u_5)
{R : Type u_11}
[semiring R]
[add_comm_monoid M]
[module R M] :
Equations
- finsupp.module α M = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul finsupp.has_smul}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}
theorem
finsupp.support_smul
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
{_x : monoid R}
[add_monoid M]
[distrib_mul_action R M]
{b : R}
{g : α →₀ M} :
@[simp]
theorem
finsupp.support_smul_eq
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
[semiring R]
[add_comm_monoid M]
[module R M]
[no_zero_smul_divisors R M]
{b : R}
(hb : b ≠ 0)
{g : α →₀ M} :
@[simp]
theorem
finsupp.filter_smul
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
{p : α → Prop}
{_x : monoid R}
[add_monoid M]
[distrib_mul_action R M]
{b : R}
{v : α →₀ M} :
finsupp.filter p (b • v) = b • finsupp.filter p v
theorem
finsupp.map_domain_smul
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{R : Type u_11}
{_x : monoid R}
[add_comm_monoid M]
[distrib_mul_action R M]
{f : α → β}
(b : R)
(v : α →₀ M) :
finsupp.map_domain f (b • v) = b • finsupp.map_domain f v
@[simp]
theorem
finsupp.smul_single
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
{_x : monoid R}
[add_monoid M]
[distrib_mul_action R M]
(c : R)
(a : α)
(b : M) :
c • finsupp.single a b = finsupp.single a (c • b)
@[simp]
theorem
finsupp.smul_single'
{α : Type u_1}
{R : Type u_11}
{_x : semiring R}
(c : R)
(a : α)
(b : R) :
c • finsupp.single a b = finsupp.single a (c * b)
theorem
finsupp.map_range_smul
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{R : Type u_11}
{_x : monoid R}
[add_monoid M]
[distrib_mul_action R M]
[add_monoid N]
[distrib_mul_action R N]
{f : M → N}
{hf : f 0 = 0}
(c : R)
(v : α →₀ M)
(hsmul : ∀ (x : M), f (c • x) = c • f x) :
finsupp.map_range f hf (c • v) = c • finsupp.map_range f hf v
theorem
finsupp.smul_single_one
{α : Type u_1}
{R : Type u_11}
[semiring R]
(a : α)
(b : R) :
b • finsupp.single a 1 = finsupp.single a b
theorem
finsupp.comap_domain_smul
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{R : Type u_11}
[add_monoid M]
[monoid R]
[distrib_mul_action R M]
{f : α → β}
(r : R)
(v : β →₀ M)
(hfv : set.inj_on f (f ⁻¹' ↑(v.support)))
(hfrv : set.inj_on f (f ⁻¹' ↑((r • v).support)) := _) :
finsupp.comap_domain f (r • v) hfrv = r • finsupp.comap_domain f v hfv
theorem
finsupp.comap_domain_smul_of_injective
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
{R : Type u_11}
[add_monoid M]
[monoid R]
[distrib_mul_action R M]
{f : α → β}
(hf : function.injective f)
(r : R)
(v : β →₀ M) :
finsupp.comap_domain f (r • v) _ = r • finsupp.comap_domain f v _
A version of finsupp.comap_domain_smul that's easier to use.
theorem
finsupp.sum_smul_index'
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{R : Type u_11}
[monoid R]
[add_monoid M]
[distrib_mul_action R M]
[add_comm_monoid N]
{g : α →₀ M}
{b : R}
{h : α → M → N}
(h0 : ∀ (i : α), h i 0 = 0) :
theorem
finsupp.sum_smul_index_add_monoid_hom
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{R : Type u_11}
[monoid R]
[add_monoid M]
[add_comm_monoid N]
[distrib_mul_action R M]
{g : α →₀ M}
{b : R}
{h : α → M →+ N} :
A version of finsupp.sum_smul_index' for bundled additive maps.
@[protected, instance]
def
finsupp.no_zero_smul_divisors
{M : Type u_5}
{R : Type u_11}
[semiring R]
[add_comm_monoid M]
[module R M]
{ι : Type u_1}
[no_zero_smul_divisors R M] :
no_zero_smul_divisors R (ι →₀ M)
noncomputable
def
finsupp.distrib_mul_action_hom.single
{α : Type u_1}
{M : Type u_5}
{R : Type u_11}
[semiring R]
[add_comm_monoid M]
[distrib_mul_action R M]
(a : α) :
finsupp.single as a distrib_mul_action_hom.
See also finsupp.lsingle for the version as a linear map.
Equations
- finsupp.distrib_mul_action_hom.single a = {to_fun := (finsupp.single_add_hom a).to_fun, map_smul' := _, map_zero' := _, map_add' := _}
theorem
finsupp.distrib_mul_action_hom_ext
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{R : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[distrib_mul_action R M]
[distrib_mul_action R N]
{f g : (α →₀ M) →+[R] N}
(h : ∀ (a : α) (m : M), ⇑f (finsupp.single a m) = ⇑g (finsupp.single a m)) :
f = g
@[ext]
theorem
finsupp.distrib_mul_action_hom_ext'
{α : Type u_1}
{M : Type u_5}
{N : Type u_7}
{R : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[distrib_mul_action R M]
[distrib_mul_action R N]
{f g : (α →₀ M) →+[R] N}
(h : ∀ (a : α), f.comp (finsupp.distrib_mul_action_hom.single a) = g.comp (finsupp.distrib_mul_action_hom.single a)) :
f = g
@[protected, instance]
The finsupp version of pi.unique.
Equations
- finsupp.unique_of_right = finsupp.unique_of_right._proof_2.unique
@[protected, instance]
The finsupp version of pi.unique_of_is_empty.
Equations
- finsupp.unique_of_left = finsupp.unique_of_left._proof_2.unique
noncomputable
def
finsupp.restrict_support_equiv
{α : Type u_1}
(s : set α)
(M : Type u_2)
[add_comm_monoid M] :
Given an add_comm_monoid M and s : set α, restrict_support_equiv s M is the equiv
between the subtype of finitely supported functions with support contained in s and
the type of finitely supported functions from s.
Equations
- finsupp.restrict_support_equiv s M = {to_fun := λ (f : {f // ↑(f.support) ⊆ s}), finsupp.subtype_domain (λ (x : α), x ∈ s) f.val, inv_fun := λ (f : ↥s →₀ M), ⟨finsupp.map_domain subtype.val f, _⟩, left_inv := _, right_inv := _}
@[simp]
theorem
finsupp.dom_congr_apply
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(e : α ≃ β)
(l : α →₀ M) :
⇑(finsupp.dom_congr e) l = finsupp.equiv_map_domain e l
@[protected]
def
finsupp.dom_congr
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(e : α ≃ β) :
Given add_comm_monoid M and e : α ≃ β, dom_congr e is the corresponding equiv between
α →₀ M and β →₀ M.
This is finsupp.equiv_congr_left as an add_equiv.
Equations
- finsupp.dom_congr e = {to_fun := finsupp.equiv_map_domain e, inv_fun := finsupp.equiv_map_domain e.symm, left_inv := _, right_inv := _, map_add' := _}
@[simp]
theorem
finsupp.dom_congr_refl
{α : Type u_1}
{M : Type u_5}
[add_comm_monoid M] :
finsupp.dom_congr (equiv.refl α) = add_equiv.refl (α →₀ M)
@[simp]
theorem
finsupp.dom_congr_symm
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[add_comm_monoid M]
(e : α ≃ β) :
@[simp]
theorem
finsupp.dom_congr_trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{M : Type u_5}
[add_comm_monoid M]
(e : α ≃ β)
(f : β ≃ γ) :
(finsupp.dom_congr e).trans (finsupp.dom_congr f) = finsupp.dom_congr (e.trans f)
Declarations about sigma types #
noncomputable
def
finsupp.split
{ι : Type u_4}
{M : Type u_5}
{αs : ι → Type u_13}
[has_zero M]
(l : (Σ (i : ι), αs i) →₀ M)
(i : ι) :
αs i →₀ M
Given l, a finitely supported function from the sigma type Σ (i : ι), αs i to M and
an index element i : ι, split l i is the ith component of l,
a finitely supported function from as i to M.
This is the finsupp version of sigma.curry.
Equations
- l.split i = finsupp.comap_domain (sigma.mk i) l _
noncomputable
def
finsupp.split_support
{ι : Type u_4}
{M : Type u_5}
{αs : ι → Type u_13}
[has_zero M]
(l : (Σ (i : ι), αs i) →₀ M) :
finset ι
Given l, a finitely supported function from the sigma type Σ (i : ι), αs i to β,
split_support l is the finset of indices in ι that appear in the support of l.
Equations
theorem
finsupp.mem_split_support_iff_nonzero
{ι : Type u_4}
{M : Type u_5}
{αs : ι → Type u_13}
[has_zero M]
(l : (Σ (i : ι), αs i) →₀ M)
(i : ι) :
i ∈ l.split_support ↔ l.split i ≠ 0
noncomputable
def
finsupp.split_comp
{ι : Type u_4}
{M : Type u_5}
{N : Type u_7}
{αs : ι → Type u_13}
[has_zero M]
(l : (Σ (i : ι), αs i) →₀ M)
[has_zero N]
(g : Π (i : ι), (αs i →₀ M) → N)
(hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0) :
ι →₀ N
Given l, a finitely supported function from the sigma type Σ i, αs i to β and
an ι-indexed family g of functions from (αs i →₀ β) to γ, split_comp defines a
finitely supported function from the index type ι to γ given by composing g i with
split l i.
Equations
- l.split_comp g hg = {support := l.split_support, to_fun := λ (i : ι), g i (l.split i), mem_support_to_fun := _}
theorem
finsupp.sigma_support
{ι : Type u_4}
{M : Type u_5}
{αs : ι → Type u_13}
[has_zero M]
(l : (Σ (i : ι), αs i) →₀ M) :
theorem
finsupp.sigma_sum
{ι : Type u_4}
{M : Type u_5}
{N : Type u_7}
{αs : ι → Type u_13}
[has_zero M]
(l : (Σ (i : ι), αs i) →₀ M)
[add_comm_monoid N]
(f : (Σ (i : ι), αs i) → M → N) :
noncomputable
def
finsupp.sigma_finsupp_equiv_pi_finsupp
{α : Type u_1}
{η : Type u_14}
[fintype η]
{ιs : η → Type u_15}
[has_zero α] :
On a fintype η, finsupp.split is an equivalence between (Σ (j : η), ιs j) →₀ α
and Π j, (ιs j →₀ α).
This is the finsupp version of equiv.Pi_curry.
Equations
- finsupp.sigma_finsupp_equiv_pi_finsupp = {to_fun := finsupp.split _inst_3, inv_fun := λ (f : Π (j : η), ιs j →₀ α), finsupp.on_finset (finset.univ.sigma (λ (j : η), (f j).support)) (λ (ji : Σ (j : η), ιs j), ⇑(f ji.fst) ji.snd) _, left_inv := _, right_inv := _}
noncomputable
def
finsupp.sigma_finsupp_add_equiv_pi_finsupp
{η : Type u_14}
[fintype η]
{α : Type u_1}
{ιs : η → Type u_2}
[add_monoid α] :
On a fintype η, finsupp.split is an additive equivalence between
(Σ (j : η), ιs j) →₀ α and Π j, (ιs j →₀ α).
This is the add_equiv version of finsupp.sigma_finsupp_equiv_pi_finsupp.
Equations
@[simp]
theorem
finsupp.sigma_finsupp_add_equiv_pi_finsupp_apply
{η : Type u_14}
[fintype η]
{α : Type u_1}
{ιs : η → Type u_2}
[add_monoid α]
(f : (Σ (j : η), ιs j) →₀ α)
(j : η)
(i : ιs j) :