Dependent functions with finite support #
For a non-dependent version see data/finsupp.lean.
@[protected, instance]
def
dfinsupp.inhabited_pre
(ι : Type u)
(β : ι → Type v)
[Π (i : ι), has_zero (β i)] :
inhabited (dfinsupp.pre ι β)
Equations
- dfinsupp.inhabited_pre ι β = {default := {to_fun := λ (i : ι), 0, pre_support := ∅, zero := _}}
@[protected, instance]
def
dfinsupp.pre.setoid
(ι : Type u)
(β : ι → Type v)
[Π (i : ι), has_zero (β i)] :
setoid (dfinsupp.pre ι β)
Equations
- dfinsupp.pre.setoid ι β = {r := λ (x y : dfinsupp.pre ι β), ∀ (i : ι), x.to_fun i = y.to_fun i, iseqv := _}
@[protected, instance]
def
dfinsupp.has_coe_to_fun
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)] :
has_coe_to_fun (Π₀ (i : ι), β i) (λ (_x : Π₀ (i : ι), β i), Π (i : ι), β i)
Equations
- dfinsupp.has_coe_to_fun = {coe := λ (f : Π₀ (i : ι), β i), quotient.lift_on f dfinsupp.pre.to_fun dfinsupp.has_coe_to_fun._proof_1}
@[protected, instance]
def
dfinsupp.has_zero
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)] :
has_zero (Π₀ (i : ι), β i)
@[protected, instance]
def
dfinsupp.inhabited
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)] :
inhabited (Π₀ (i : ι), β i)
Equations
- dfinsupp.inhabited = {default := 0}
@[simp]
def
dfinsupp.map_range
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
(f : Π (i : ι), β₁ i → β₂ i)
(hf : ∀ (i : ι), f i 0 = 0) :
(Π₀ (i : ι), β₁ i) → (Π₀ (i : ι), β₂ i)
The composition of f : β₁ → β₂ and g : Π₀ i, β₁ i is
map_range f hf g : Π₀ i, β₂ i, well defined when f 0 = 0.
This preserves the structure on f, and exists in various bundled forms for when f is itself
bundled:
dfinsupp.map_range.add_monoid_homdfinsupp.map_range.add_equivdfinsupp.map_range.linear_mapdfinsupp.map_range.linear_equiv
Equations
- dfinsupp.map_range f hf = quotient.map (λ (x : dfinsupp.pre ι (λ (i : ι), β₁ i)), {to_fun := λ (i : ι), f i (x.to_fun i), pre_support := x.pre_support, zero := _}) _
@[simp]
theorem
dfinsupp.map_range_apply
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
(f : Π (i : ι), β₁ i → β₂ i)
(hf : ∀ (i : ι), f i 0 = 0)
(g : Π₀ (i : ι), β₁ i)
(i : ι) :
⇑(dfinsupp.map_range f hf g) i = f i (⇑g i)
@[simp]
theorem
dfinsupp.map_range_id
{ι : Type u}
{β₁ : ι → Type v₁}
[Π (i : ι), has_zero (β₁ i)]
(h : (∀ (i : ι), id 0 = 0) := _)
(g : Π₀ (i : ι), β₁ i) :
dfinsupp.map_range (λ (i : ι), id) h g = g
theorem
dfinsupp.map_range_comp
{ι : Type u}
{β : ι → Type v}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β i)]
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
(f : Π (i : ι), β₁ i → β₂ i)
(f₂ : Π (i : ι), β i → β₁ i)
(hf : ∀ (i : ι), f i 0 = 0)
(hf₂ : ∀ (i : ι), f₂ i 0 = 0)
(h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0)
(g : Π₀ (i : ι), β i) :
dfinsupp.map_range (λ (i : ι), f i ∘ f₂ i) h g = dfinsupp.map_range f hf (dfinsupp.map_range f₂ hf₂ g)
@[simp]
theorem
dfinsupp.map_range_zero
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
(f : Π (i : ι), β₁ i → β₂ i)
(hf : ∀ (i : ι), f i 0 = 0) :
dfinsupp.map_range f hf 0 = 0
def
dfinsupp.zip_with
{ι : Type u}
{β : ι → Type v}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β i)]
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
(f : Π (i : ι), β₁ i → β₂ i → β i)
(hf : ∀ (i : ι), f i 0 0 = 0) :
(Π₀ (i : ι), β₁ i) → (Π₀ (i : ι), β₂ i) → (Π₀ (i : ι), β i)
Let f i be a binary operation β₁ i → β₂ i → β i such that f i 0 0 = 0.
Then zip_with f hf is a binary operation Π₀ i, β₁ i → Π₀ i, β₂ i → Π₀ i, β i.
Equations
- dfinsupp.zip_with f hf = quotient.map₂ (λ (x : dfinsupp.pre ι (λ (i : ι), β₁ i)) (y : dfinsupp.pre ι (λ (i : ι), β₂ i)), {to_fun := λ (i : ι), f i (x.to_fun i) (y.to_fun i), pre_support := x.pre_support + y.pre_support, zero := _}) _
@[simp]
theorem
dfinsupp.zip_with_apply
{ι : Type u}
{β : ι → Type v}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β i)]
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
(f : Π (i : ι), β₁ i → β₂ i → β i)
(hf : ∀ (i : ι), f i 0 0 = 0)
(g₁ : Π₀ (i : ι), β₁ i)
(g₂ : Π₀ (i : ι), β₂ i)
(i : ι) :
⇑(dfinsupp.zip_with f hf g₁ g₂) i = f i (⇑g₁ i) (⇑g₂ i)
@[protected, instance]
def
dfinsupp.has_add
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_zero_class (β i)] :
has_add (Π₀ (i : ι), β i)
Equations
- dfinsupp.has_add = {add := dfinsupp.zip_with (λ (_x : ι), has_add.add) dfinsupp.has_add._proof_1}
theorem
dfinsupp.add_apply
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_zero_class (β i)]
(g₁ g₂ : Π₀ (i : ι), β i)
(i : ι) :
@[simp]
theorem
dfinsupp.coe_add
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_zero_class (β i)]
(g₁ g₂ : Π₀ (i : ι), β i) :
@[protected, instance]
def
dfinsupp.add_zero_class
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_zero_class (β i)] :
add_zero_class (Π₀ (i : ι), β i)
Equations
- dfinsupp.add_zero_class = {zero := 0, add := has_add.add dfinsupp.has_add, zero_add := _, add_zero := _}
@[protected, instance]
def
dfinsupp.add_monoid
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_monoid (β i)] :
add_monoid (Π₀ (i : ι), β i)
Equations
- dfinsupp.add_monoid = {add := has_add.add dfinsupp.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec (add_zero_class.to_has_add (Π₀ (i : ι), β i)), nsmul_zero' := _, nsmul_succ' := _}
def
dfinsupp.coe_fn_add_monoid_hom
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_zero_class (β i)] :
(Π₀ (i : ι), β i) →+ Π (i : ι), β i
Coercion from a dfinsupp to a pi type is an add_monoid_hom.
Equations
- dfinsupp.coe_fn_add_monoid_hom = {to_fun := coe_fn dfinsupp.has_coe_to_fun, map_zero' := _, map_add' := _}
def
dfinsupp.eval_add_monoid_hom
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_zero_class (β i)]
(i : ι) :
(Π₀ (i : ι), β i) →+ β i
Evaluation at a point is an add_monoid_hom. This is the finitely-supported version of
pi.eval_add_monoid_hom.
Equations
@[protected, instance]
def
dfinsupp.add_comm_monoid
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_comm_monoid (β i)] :
add_comm_monoid (Π₀ (i : ι), β i)
Equations
- dfinsupp.add_comm_monoid = {add := add_monoid.add dfinsupp.add_monoid, add_assoc := _, zero := add_monoid.zero dfinsupp.add_monoid, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (v : Π₀ (i : ι), β i), dfinsupp.map_range (λ (_x : ι), has_scalar.smul n) _ v, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[simp]
theorem
dfinsupp.coe_finset_sum
{ι : Type u}
{β : ι → Type v}
{α : Type u_1}
[Π (i : ι), add_comm_monoid (β i)]
(s : finset α)
(g : α → (Π₀ (i : ι), β i)) :
@[simp]
theorem
dfinsupp.finset_sum_apply
{ι : Type u}
{β : ι → Type v}
{α : Type u_1}
[Π (i : ι), add_comm_monoid (β i)]
(s : finset α)
(g : α → (Π₀ (i : ι), β i))
(i : ι) :
@[protected, instance]
def
dfinsupp.has_neg
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_group (β i)] :
has_neg (Π₀ (i : ι), β i)
Equations
- dfinsupp.has_neg = {neg := λ (f : Π₀ (i : ι), β i), dfinsupp.map_range (λ (_x : ι), has_neg.neg) dfinsupp.has_neg._proof_1 f}
@[protected, instance]
def
dfinsupp.has_sub
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_group (β i)] :
has_sub (Π₀ (i : ι), β i)
Equations
- dfinsupp.has_sub = {sub := dfinsupp.zip_with (λ (_x : ι), has_sub.sub) dfinsupp.has_sub._proof_1}
@[protected, instance]
def
dfinsupp.add_group
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_group (β i)] :
add_group (Π₀ (i : ι), β i)
Equations
- dfinsupp.add_group = {add := add_monoid.add dfinsupp.add_monoid, add_assoc := _, zero := add_monoid.zero dfinsupp.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul dfinsupp.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg dfinsupp.has_neg, sub := has_sub.sub dfinsupp.has_sub, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul._default add_monoid.add dfinsupp.add_group._proof_7 add_monoid.zero dfinsupp.add_group._proof_8 dfinsupp.add_group._proof_9 add_monoid.nsmul dfinsupp.add_group._proof_10 dfinsupp.add_group._proof_11 has_neg.neg, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
@[protected, instance]
def
dfinsupp.add_comm_group
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_comm_group (β i)] :
add_comm_group (Π₀ (i : ι), β i)
Equations
- dfinsupp.add_comm_group = {add := add_comm_monoid.add dfinsupp.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero dfinsupp.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul dfinsupp.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg dfinsupp.add_group, sub := add_group.sub dfinsupp.add_group, sub_eq_add_neg := _, zsmul := λ (n : ℤ) (v : Π₀ (i : ι), β i), dfinsupp.map_range (λ (_x : ι), has_scalar.smul n) _ v, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[protected, instance]
def
dfinsupp.has_scalar
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[monoid γ]
[Π (i : ι), add_monoid (β i)]
[Π (i : ι), distrib_mul_action γ (β i)] :
has_scalar γ (Π₀ (i : ι), β i)
Dependent functions with finite support inherit a semiring action from an action on each coordinate.
Equations
- dfinsupp.has_scalar = {smul := λ (c : γ) (v : Π₀ (i : ι), β i), dfinsupp.map_range (λ (_x : ι), has_scalar.smul c) _ v}
theorem
dfinsupp.smul_apply
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[monoid γ]
[Π (i : ι), add_monoid (β i)]
[Π (i : ι), distrib_mul_action γ (β i)]
(b : γ)
(v : Π₀ (i : ι), β i)
(i : ι) :
@[simp]
theorem
dfinsupp.coe_smul
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[monoid γ]
[Π (i : ι), add_monoid (β i)]
[Π (i : ι), distrib_mul_action γ (β i)]
(b : γ)
(v : Π₀ (i : ι), β i) :
@[protected, instance]
def
dfinsupp.smul_comm_class
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{δ : Type u_1}
[monoid γ]
[monoid δ]
[Π (i : ι), add_monoid (β i)]
[Π (i : ι), distrib_mul_action γ (β i)]
[Π (i : ι), distrib_mul_action δ (β i)]
[∀ (i : ι), smul_comm_class γ δ (β i)] :
smul_comm_class γ δ (Π₀ (i : ι), β i)
@[protected, instance]
def
dfinsupp.is_scalar_tower
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{δ : Type u_1}
[monoid γ]
[monoid δ]
[Π (i : ι), add_monoid (β i)]
[Π (i : ι), distrib_mul_action γ (β i)]
[Π (i : ι), distrib_mul_action δ (β i)]
[has_scalar γ δ]
[∀ (i : ι), is_scalar_tower γ δ (β i)] :
is_scalar_tower γ δ (Π₀ (i : ι), β i)
@[protected, instance]
def
dfinsupp.is_central_scalar
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[monoid γ]
[Π (i : ι), add_monoid (β i)]
[Π (i : ι), distrib_mul_action γ (β i)]
[Π (i : ι), distrib_mul_action γᵐᵒᵖ (β i)]
[∀ (i : ι), is_central_scalar γ (β i)] :
is_central_scalar γ (Π₀ (i : ι), β i)
@[protected, instance]
def
dfinsupp.distrib_mul_action
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[monoid γ]
[Π (i : ι), add_monoid (β i)]
[Π (i : ι), distrib_mul_action γ (β i)] :
distrib_mul_action γ (Π₀ (i : ι), β i)
Dependent functions with finite support inherit a distrib_mul_action structure from such a
structure on each coordinate.
Equations
- dfinsupp.distrib_mul_action = {to_mul_action := {to_has_scalar := {smul := has_scalar.smul dfinsupp.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
@[protected, instance]
def
dfinsupp.module
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[semiring γ]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι), module γ (β i)] :
module γ (Π₀ (i : ι), β i)
Dependent functions with finite support inherit a module structure from such a structure on each coordinate.
Equations
- dfinsupp.module = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action dfinsupp.distrib_mul_action, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
def
dfinsupp.filter
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
(p : ι → Prop)
[decidable_pred p] :
(Π₀ (i : ι), β i) → (Π₀ (i : ι), β i)
filter p f is the function which is f i if p i is true and 0 otherwise.
Equations
- dfinsupp.filter p = quotient.map (λ (x : dfinsupp.pre ι (λ (i : ι), β i)), {to_fun := λ (i : ι), ite (p i) (x.to_fun i) 0, pre_support := x.pre_support, zero := _}) _
@[simp]
theorem
dfinsupp.filter_apply
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
(p : ι → Prop)
[decidable_pred p]
(i : ι)
(f : Π₀ (i : ι), β i) :
⇑(dfinsupp.filter p f) i = ite (p i) (⇑f i) 0
theorem
dfinsupp.filter_apply_pos
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
{p : ι → Prop}
[decidable_pred p]
(f : Π₀ (i : ι), β i)
{i : ι}
(h : p i) :
⇑(dfinsupp.filter p f) i = ⇑f i
theorem
dfinsupp.filter_apply_neg
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
{p : ι → Prop}
[decidable_pred p]
(f : Π₀ (i : ι), β i)
{i : ι}
(h : ¬p i) :
⇑(dfinsupp.filter p f) i = 0
theorem
dfinsupp.filter_pos_add_filter_neg
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_zero_class (β i)]
(f : Π₀ (i : ι), β i)
(p : ι → Prop)
[decidable_pred p] :
dfinsupp.filter p f + dfinsupp.filter (λ (i : ι), ¬p i) f = f
@[simp]
theorem
dfinsupp.filter_zero
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
(p : ι → Prop)
[decidable_pred p] :
dfinsupp.filter p 0 = 0
@[simp]
theorem
dfinsupp.filter_add
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_zero_class (β i)]
(p : ι → Prop)
[decidable_pred p]
(f g : Π₀ (i : ι), β i) :
dfinsupp.filter p (f + g) = dfinsupp.filter p f + dfinsupp.filter p g
@[simp]
theorem
dfinsupp.filter_smul
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[monoid γ]
[Π (i : ι), add_monoid (β i)]
[Π (i : ι), distrib_mul_action γ (β i)]
(p : ι → Prop)
[decidable_pred p]
(r : γ)
(f : Π₀ (i : ι), β i) :
dfinsupp.filter p (r • f) = r • dfinsupp.filter p f
def
dfinsupp.filter_add_monoid_hom
{ι : Type u}
(β : ι → Type v)
[Π (i : ι), add_zero_class (β i)]
(p : ι → Prop)
[decidable_pred p] :
(Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i
dfinsupp.filter as an add_monoid_hom.
Equations
- dfinsupp.filter_add_monoid_hom β p = {to_fun := dfinsupp.filter p (λ (a : ι), _inst_2 a), map_zero' := _, map_add' := _}
@[simp]
theorem
dfinsupp.filter_add_monoid_hom_apply
{ι : Type u}
(β : ι → Type v)
[Π (i : ι), add_zero_class (β i)]
(p : ι → Prop)
[decidable_pred p]
(ᾰ : Π₀ (i : ι), (λ (i : ι), β i) i) :
⇑(dfinsupp.filter_add_monoid_hom β p) ᾰ = dfinsupp.filter p ᾰ
@[simp]
theorem
dfinsupp.filter_linear_map_apply
{ι : Type u}
(γ : Type w)
(β : ι → Type v)
[semiring γ]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι), module γ (β i)]
(p : ι → Prop)
[decidable_pred p]
(ᾰ : Π₀ (i : ι), (λ (i : ι), β i) i) :
⇑(dfinsupp.filter_linear_map γ β p) ᾰ = dfinsupp.filter p ᾰ
def
dfinsupp.filter_linear_map
{ι : Type u}
(γ : Type w)
(β : ι → Type v)
[semiring γ]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι), module γ (β i)]
(p : ι → Prop)
[decidable_pred p] :
dfinsupp.filter as a linear_map.
Equations
- dfinsupp.filter_linear_map γ β p = {to_fun := dfinsupp.filter p (λ (a : ι), _inst_4 a), map_add' := _, map_smul' := _}
@[simp]
theorem
dfinsupp.filter_neg
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_group (β i)]
(p : ι → Prop)
[decidable_pred p]
(f : Π₀ (i : ι), β i) :
dfinsupp.filter p (-f) = -dfinsupp.filter p f
@[simp]
theorem
dfinsupp.filter_sub
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_group (β i)]
(p : ι → Prop)
[decidable_pred p]
(f g : Π₀ (i : ι), β i) :
dfinsupp.filter p (f - g) = dfinsupp.filter p f - dfinsupp.filter p g
def
dfinsupp.subtype_domain
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
(p : ι → Prop)
[decidable_pred p] :
subtype_domain p f is the restriction of the finitely supported function
f to the subtype p.
Equations
- dfinsupp.subtype_domain p = quotient.map (λ (x : dfinsupp.pre ι (λ (i : ι), β i)), {to_fun := λ (i : subtype p), x.to_fun ↑i, pre_support := multiset.map (λ (j : {x_1 // x_1 ∈ multiset.filter p x.pre_support}), ⟨↑j, _⟩) (multiset.filter p x.pre_support).attach, zero := _}) _
@[simp]
theorem
dfinsupp.subtype_domain_zero
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
{p : ι → Prop}
[decidable_pred p] :
dfinsupp.subtype_domain p 0 = 0
@[simp]
theorem
dfinsupp.subtype_domain_apply
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
{p : ι → Prop}
[decidable_pred p]
{i : subtype p}
{v : Π₀ (i : ι), β i} :
⇑(dfinsupp.subtype_domain p v) i = ⇑v ↑i
@[simp]
theorem
dfinsupp.subtype_domain_add
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_zero_class (β i)]
{p : ι → Prop}
[decidable_pred p]
(v v' : Π₀ (i : ι), β i) :
dfinsupp.subtype_domain p (v + v') = dfinsupp.subtype_domain p v + dfinsupp.subtype_domain p v'
@[simp]
theorem
dfinsupp.subtype_domain_smul
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[monoid γ]
[Π (i : ι), add_monoid (β i)]
[Π (i : ι), distrib_mul_action γ (β i)]
{p : ι → Prop}
[decidable_pred p]
(r : γ)
(f : Π₀ (i : ι), β i) :
dfinsupp.subtype_domain p (r • f) = r • dfinsupp.subtype_domain p f
def
dfinsupp.subtype_domain_add_monoid_hom
{ι : Type u}
(β : ι → Type v)
[Π (i : ι), add_zero_class (β i)]
(p : ι → Prop)
[decidable_pred p] :
subtype_domain but as an add_monoid_hom.
Equations
- dfinsupp.subtype_domain_add_monoid_hom β p = {to_fun := dfinsupp.subtype_domain p (λ (a : ι), _inst_2 a), map_zero' := _, map_add' := _}
@[simp]
theorem
dfinsupp.subtype_domain_add_monoid_hom_apply
{ι : Type u}
(β : ι → Type v)
[Π (i : ι), add_zero_class (β i)]
(p : ι → Prop)
[decidable_pred p]
(ᾰ : Π₀ (i : ι), (λ (i : ι), β i) i) :
def
dfinsupp.subtype_domain_linear_map
{ι : Type u}
(γ : Type w)
(β : ι → Type v)
[semiring γ]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι), module γ (β i)]
(p : ι → Prop)
[decidable_pred p] :
dfinsupp.subtype_domain as a linear_map.
Equations
- dfinsupp.subtype_domain_linear_map γ β p = {to_fun := dfinsupp.subtype_domain p (λ (a : ι), _inst_4 a), map_add' := _, map_smul' := _}
@[simp]
theorem
dfinsupp.subtype_domain_linear_map_apply
{ι : Type u}
(γ : Type w)
(β : ι → Type v)
[semiring γ]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι), module γ (β i)]
(p : ι → Prop)
[decidable_pred p]
(ᾰ : Π₀ (i : ι), (λ (i : ι), β i) i) :
⇑(dfinsupp.subtype_domain_linear_map γ β p) ᾰ = dfinsupp.subtype_domain p ᾰ
@[simp]
theorem
dfinsupp.subtype_domain_neg
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_group (β i)]
{p : ι → Prop}
[decidable_pred p]
{v : Π₀ (i : ι), β i} :
@[simp]
theorem
dfinsupp.subtype_domain_sub
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_group (β i)]
{p : ι → Prop}
[decidable_pred p]
{v v' : Π₀ (i : ι), β i} :
dfinsupp.subtype_domain p (v - v') = dfinsupp.subtype_domain p v - dfinsupp.subtype_domain p v'
def
dfinsupp.mk
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(s : finset ι)
(x : Π (i : ↥↑s), β ↑i) :
Π₀ (i : ι), β i
Create an element of Π₀ i, β i from a finset s and a function x
defined on this finset.
theorem
dfinsupp.mk_injective
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(s : finset ι) :
def
dfinsupp.equiv_fun_on_fintype
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
[fintype ι] :
(Π₀ (i : ι), β i) ≃ Π (i : ι), β i
Given fintype ι, equiv_fun_on_fintype is the equiv between Π₀ i, β i and Π i, β i.
(All dependent functions on a finite type are finitely supported.)
Equations
- dfinsupp.equiv_fun_on_fintype = {to_fun := coe_fn dfinsupp.has_coe_to_fun, inv_fun := λ (f : Π (i : ι), β i), ⟦{to_fun := f, pre_support := finset.univ.val, zero := _}⟧, left_inv := _, right_inv := _}
@[simp]
theorem
dfinsupp.equiv_fun_on_fintype_apply
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
[fintype ι]
(x : Π₀ (i : ι), β i)
(i : ι) :
⇑dfinsupp.equiv_fun_on_fintype x i = ⇑x i
@[simp]
theorem
dfinsupp.equiv_fun_on_fintype_symm_coe
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
[fintype ι]
(f : Π₀ (i : ι), β i) :
def
dfinsupp.single
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(i : ι)
(b : β i) :
Π₀ (i : ι), β i
The function single i b : Π₀ i, β i sends i to b
and all other points to 0.
Equations
- dfinsupp.single i b = dfinsupp.mk {i} (λ (j : ↥↑{i}), _.rec_on b)
@[simp]
theorem
dfinsupp.single_apply
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i i' : ι}
{b : β i} :
theorem
dfinsupp.single_eq_pi_single
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i : ι}
{b : β i} :
⇑(dfinsupp.single i b) = pi.single i b
@[simp]
theorem
dfinsupp.single_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(i : ι) :
dfinsupp.single i 0 = 0
@[simp]
theorem
dfinsupp.single_eq_same
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i : ι}
{b : β i} :
⇑(dfinsupp.single i b) i = b
theorem
dfinsupp.single_eq_of_ne
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i i' : ι}
{b : β i}
(h : i ≠ i') :
⇑(dfinsupp.single i b) i' = 0
theorem
dfinsupp.single_injective
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i : ι} :
theorem
dfinsupp.single_eq_single_iff
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(i j : ι)
(xi : β i)
(xj : β j) :
Like finsupp.single_eq_single_iff, but with a heq due to dependent types
@[simp]
theorem
dfinsupp.single_eq_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i : ι}
{xi : β i} :
dfinsupp.single i xi = 0 ↔ xi = 0
theorem
dfinsupp.filter_single
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(p : ι → Prop)
[decidable_pred p]
(i : ι)
(x : β i) :
dfinsupp.filter p (dfinsupp.single i x) = ite (p i) (dfinsupp.single i x) 0
@[simp]
theorem
dfinsupp.filter_single_pos
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{p : ι → Prop}
[decidable_pred p]
(i : ι)
(x : β i)
(h : p i) :
dfinsupp.filter p (dfinsupp.single i x) = dfinsupp.single i x
@[simp]
theorem
dfinsupp.filter_single_neg
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{p : ι → Prop}
[decidable_pred p]
(i : ι)
(x : β i)
(h : ¬p i) :
dfinsupp.filter p (dfinsupp.single i x) = 0
theorem
dfinsupp.single_eq_of_sigma_eq
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i j : ι}
{xi : β i}
{xj : β j}
(h : ⟨i, xi⟩ = ⟨j, xj⟩) :
dfinsupp.single i xi = dfinsupp.single j xj
Equality of sigma types is sufficient (but not necessary) to show equality of dfinsupps.
@[simp]
theorem
dfinsupp.equiv_fun_on_fintype_single
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[fintype ι]
(i : ι)
(m : β i) :
@[simp]
theorem
dfinsupp.equiv_fun_on_fintype_symm_single
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[fintype ι]
(i : ι)
(m : β i) :
⇑(dfinsupp.equiv_fun_on_fintype.symm) (pi.single i m) = dfinsupp.single i m
def
dfinsupp.erase
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(i : ι) :
(Π₀ (i : ι), β i) → (Π₀ (i : ι), β i)
Redefine f i to be 0.
Equations
- dfinsupp.erase i = quotient.map (λ (x : dfinsupp.pre ι (λ (i : ι), β i)), {to_fun := λ (j : ι), ite (j = i) 0 (x.to_fun j), pre_support := x.pre_support, zero := _}) _
@[simp]
theorem
dfinsupp.erase_apply
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i j : ι}
{f : Π₀ (i : ι), β i} :
@[simp]
theorem
dfinsupp.erase_same
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i : ι}
{f : Π₀ (i : ι), β i} :
⇑(dfinsupp.erase i f) i = 0
theorem
dfinsupp.erase_ne
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i i' : ι}
{f : Π₀ (i : ι), β i}
(h : i' ≠ i) :
⇑(dfinsupp.erase i f) i' = ⇑f i'
theorem
dfinsupp.erase_eq_sub_single
{ι : Type u}
[dec : decidable_eq ι]
{β : ι → Type u_1}
[Π (i : ι), add_group (β i)]
(f : Π₀ (i : ι), β i)
(i : ι) :
dfinsupp.erase i f = f - dfinsupp.single i (⇑f i)
@[simp]
theorem
dfinsupp.erase_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(i : ι) :
dfinsupp.erase i 0 = 0
@[simp]
theorem
dfinsupp.filter_ne_eq_erase
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(f : Π₀ (i : ι), β i)
(i : ι) :
dfinsupp.filter (λ (_x : ι), _x ≠ i) f = dfinsupp.erase i f
@[simp]
theorem
dfinsupp.filter_ne_eq_erase'
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(f : Π₀ (i : ι), β i)
(i : ι) :
dfinsupp.filter (ne i) f = dfinsupp.erase i f
theorem
dfinsupp.erase_single
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(j i : ι)
(x : β i) :
dfinsupp.erase j (dfinsupp.single i x) = ite (i = j) 0 (dfinsupp.single i x)
@[simp]
theorem
dfinsupp.erase_single_same
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(i : ι)
(x : β i) :
dfinsupp.erase i (dfinsupp.single i x) = 0
@[simp]
theorem
dfinsupp.erase_single_ne
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i j : ι}
(x : β i)
(h : i ≠ j) :
dfinsupp.erase j (dfinsupp.single i x) = dfinsupp.single i x
def
dfinsupp.update
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(f : Π₀ (i : ι), β i)
(i : ι)
(b : β i)
[decidable (b = 0)] :
Π₀ (i : ι), β i
Replace the value of a Π₀ i, β i at a given point i : ι by a given value b : β i.
If b = 0, this amounts to removing i from the support.
Otherwise, i is added to it.
This is the (dependent) finitely-supported version of function.update.
Equations
- f.update i b = quotient.map (λ (x : dfinsupp.pre ι (λ (i : ι), β i)), {to_fun := function.update x.to_fun i b, pre_support := ite (b = 0) (x.pre_support.erase i) (i ::ₘ x.pre_support), zero := _}) _ f
@[simp]
theorem
dfinsupp.coe_update
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(f : Π₀ (i : ι), β i)
(i : ι)
(b : β i)
[decidable (b = 0)] :
⇑(f.update i b) = function.update ⇑f i b
@[simp]
theorem
dfinsupp.update_self
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(f : Π₀ (i : ι), β i)
(i : ι)
[decidable (⇑f i = 0)] :
@[simp]
theorem
dfinsupp.update_eq_erase
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(f : Π₀ (i : ι), β i)
(i : ι)
[decidable (0 = 0)] :
f.update i 0 = dfinsupp.erase i f
theorem
dfinsupp.update_eq_single_add_erase
{ι : Type u}
[dec : decidable_eq ι]
{β : ι → Type u_1}
[Π (i : ι), add_zero_class (β i)]
(f : Π₀ (i : ι), β i)
(i : ι)
(b : β i)
[decidable (b = 0)] :
f.update i b = dfinsupp.single i b + dfinsupp.erase i f
theorem
dfinsupp.update_eq_erase_add_single
{ι : Type u}
[dec : decidable_eq ι]
{β : ι → Type u_1}
[Π (i : ι), add_zero_class (β i)]
(f : Π₀ (i : ι), β i)
(i : ι)
(b : β i)
[decidable (b = 0)] :
f.update i b = dfinsupp.erase i f + dfinsupp.single i b
theorem
dfinsupp.update_eq_sub_add_single
{ι : Type u}
[dec : decidable_eq ι]
{β : ι → Type u_1}
[Π (i : ι), add_group (β i)]
(f : Π₀ (i : ι), β i)
(i : ι)
(b : β i)
[decidable (b = 0)] :
f.update i b = f - dfinsupp.single i (⇑f i) + dfinsupp.single i b
@[simp]
theorem
dfinsupp.single_add
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
(i : ι)
(b₁ b₂ : β i) :
dfinsupp.single i (b₁ + b₂) = dfinsupp.single i b₁ + dfinsupp.single i b₂
@[simp]
theorem
dfinsupp.erase_add
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
(i : ι)
(f₁ f₂ : Π₀ (i : ι), β i) :
dfinsupp.erase i (f₁ + f₂) = dfinsupp.erase i f₁ + dfinsupp.erase i f₂
@[simp]
theorem
dfinsupp.single_add_hom_apply
{ι : Type u}
(β : ι → Type v)
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
(i : ι)
(b : β i) :
⇑(dfinsupp.single_add_hom β i) b = dfinsupp.single i b
def
dfinsupp.single_add_hom
{ι : Type u}
(β : ι → Type v)
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
(i : ι) :
β i →+ Π₀ (i : ι), β i
dfinsupp.single as an add_monoid_hom.
Equations
- dfinsupp.single_add_hom β i = {to_fun := dfinsupp.single i, map_zero' := _, map_add' := _}
def
dfinsupp.erase_add_hom
{ι : Type u}
(β : ι → Type v)
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
(i : ι) :
(Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i
dfinsupp.erase as an add_monoid_hom.
Equations
- dfinsupp.erase_add_hom β i = {to_fun := dfinsupp.erase i, map_zero' := _, map_add' := _}
@[simp]
theorem
dfinsupp.erase_add_hom_apply
{ι : Type u}
(β : ι → Type v)
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
(i : ι)
(ᾰ : Π₀ (i : ι), (λ (i : ι), β i) i) :
⇑(dfinsupp.erase_add_hom β i) ᾰ = dfinsupp.erase i ᾰ
@[simp]
theorem
dfinsupp.single_neg
{ι : Type u}
[dec : decidable_eq ι]
{β : ι → Type v}
[Π (i : ι), add_group (β i)]
(i : ι)
(x : β i) :
dfinsupp.single i (-x) = -dfinsupp.single i x
@[simp]
theorem
dfinsupp.single_sub
{ι : Type u}
[dec : decidable_eq ι]
{β : ι → Type v}
[Π (i : ι), add_group (β i)]
(i : ι)
(x y : β i) :
dfinsupp.single i (x - y) = dfinsupp.single i x - dfinsupp.single i y
@[simp]
theorem
dfinsupp.erase_neg
{ι : Type u}
[dec : decidable_eq ι]
{β : ι → Type v}
[Π (i : ι), add_group (β i)]
(i : ι)
(f : Π₀ (i : ι), β i) :
dfinsupp.erase i (-f) = -dfinsupp.erase i f
@[simp]
theorem
dfinsupp.erase_sub
{ι : Type u}
[dec : decidable_eq ι]
{β : ι → Type v}
[Π (i : ι), add_group (β i)]
(i : ι)
(f g : Π₀ (i : ι), β i) :
dfinsupp.erase i (f - g) = dfinsupp.erase i f - dfinsupp.erase i g
theorem
dfinsupp.single_add_erase
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
(i : ι)
(f : Π₀ (i : ι), β i) :
dfinsupp.single i (⇑f i) + dfinsupp.erase i f = f
theorem
dfinsupp.erase_add_single
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
(i : ι)
(f : Π₀ (i : ι), β i) :
dfinsupp.erase i f + dfinsupp.single i (⇑f i) = f
@[protected]
theorem
dfinsupp.induction
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
{p : (Π₀ (i : ι), β i) → Prop}
(f : Π₀ (i : ι), β i)
(h0 : p 0)
(ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), ⇑f i = 0 → b ≠ 0 → p f → p (dfinsupp.single i b + f)) :
p f
theorem
dfinsupp.induction₂
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
{p : (Π₀ (i : ι), β i) → Prop}
(f : Π₀ (i : ι), β i)
(h0 : p 0)
(ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), ⇑f i = 0 → b ≠ 0 → p f → p (f + dfinsupp.single i b)) :
p f
@[simp]
theorem
dfinsupp.add_closure_Union_range_single
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)] :
add_submonoid.closure (⋃ (i : ι), set.range (dfinsupp.single i)) = ⊤
theorem
dfinsupp.add_hom_ext
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
{γ : Type w}
[add_zero_class γ]
⦃f g : (Π₀ (i : ι), β i) →+ γ⦄
(H : ∀ (i : ι) (y : β i), ⇑f (dfinsupp.single i y) = ⇑g (dfinsupp.single i y)) :
f = g
If two additive homomorphisms from Π₀ i, β i are equal on each single a b, then
they are equal.
@[ext]
theorem
dfinsupp.add_hom_ext'
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
{γ : Type w}
[add_zero_class γ]
⦃f g : (Π₀ (i : ι), β i) →+ γ⦄
(H : ∀ (x : ι), f.comp (dfinsupp.single_add_hom β x) = g.comp (dfinsupp.single_add_hom β x)) :
f = g
If two additive homomorphisms from Π₀ i, β i are equal on each single a b, then
they are equal.
@[simp]
theorem
dfinsupp.mk_add
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
{s : finset ι}
{x y : Π (i : ↥↑s), β ↑i} :
dfinsupp.mk s (x + y) = dfinsupp.mk s x + dfinsupp.mk s y
@[simp]
theorem
dfinsupp.mk_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{s : finset ι} :
dfinsupp.mk s 0 = 0
@[simp]
theorem
dfinsupp.mk_neg
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_group (β i)]
{s : finset ι}
{x : Π (i : ↥↑s), β i.val} :
dfinsupp.mk s (-x) = -dfinsupp.mk s x
@[simp]
theorem
dfinsupp.mk_sub
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_group (β i)]
{s : finset ι}
{x y : Π (i : ↥↑s), β i.val} :
dfinsupp.mk s (x - y) = dfinsupp.mk s x - dfinsupp.mk s y
def
dfinsupp.mk_add_group_hom
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_group (β i)]
(s : finset ι) :
If s is a subset of ι then mk_add_group_hom s is the canonical additive
group homomorphism from $\prod_{i\in s}\beta_i$ to $\prod_{\mathtt{i : \iota}}\beta_i.$
Equations
- dfinsupp.mk_add_group_hom s = {to_fun := dfinsupp.mk s, map_zero' := _, map_add' := _}
@[simp]
theorem
dfinsupp.mk_smul
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[monoid γ]
[Π (i : ι), add_monoid (β i)]
[Π (i : ι), distrib_mul_action γ (β i)]
{s : finset ι}
(c : γ)
(x : Π (i : ↥↑s), β ↑i) :
dfinsupp.mk s (c • x) = c • dfinsupp.mk s x
@[simp]
theorem
dfinsupp.single_smul
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[monoid γ]
[Π (i : ι), add_monoid (β i)]
[Π (i : ι), distrib_mul_action γ (β i)]
{i : ι}
(c : γ)
(x : β i) :
dfinsupp.single i (c • x) = c • dfinsupp.single i x
def
dfinsupp.support
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
(f : Π₀ (i : ι), β i) :
finset ι
Set {i | f x ≠ 0} as a finset.
Equations
- f.support = quotient.lift_on f (λ (x : dfinsupp.pre ι (λ (i : ι), β i)), finset.filter (λ (i : ι), x.to_fun i ≠ 0) x.pre_support.to_finset) dfinsupp.support._proof_1
@[simp]
theorem
dfinsupp.support_mk_subset
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{s : finset ι}
{x : Π (i : ↥↑s), β i.val} :
(dfinsupp.mk s x).support ⊆ s
theorem
dfinsupp.eq_mk_support
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
(f : Π₀ (i : ι), β i) :
@[simp]
theorem
dfinsupp.support_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)] :
@[protected, instance]
def
dfinsupp.decidable_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)] :
decidable_pred (eq 0)
Equations
- dfinsupp.decidable_zero = λ (f : Π₀ (i : ι), β i), decidable_of_iff (f.support = ∅) _
theorem
dfinsupp.support_single_ne_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{i : ι}
{b : β i}
(hb : b ≠ 0) :
(dfinsupp.single i b).support = {i}
theorem
dfinsupp.support_single_subset
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{i : ι}
{b : β i} :
(dfinsupp.single i b).support ⊆ {i}
theorem
dfinsupp.map_range_def
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
[Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]
{f : Π (i : ι), β₁ i → β₂ i}
{hf : ∀ (i : ι), f i 0 = 0}
{g : Π₀ (i : ι), β₁ i} :
dfinsupp.map_range f hf g = dfinsupp.mk g.support (λ (i : ↥↑(g.support)), f i.val (⇑g i.val))
@[simp]
theorem
dfinsupp.map_range_single
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
{f : Π (i : ι), β₁ i → β₂ i}
{hf : ∀ (i : ι), f i 0 = 0}
{i : ι}
{b : β₁ i} :
dfinsupp.map_range f hf (dfinsupp.single i b) = dfinsupp.single i (f i b)
theorem
dfinsupp.support_map_range
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
[Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι) (x : β₂ i), decidable (x ≠ 0)]
{f : Π (i : ι), β₁ i → β₂ i}
{hf : ∀ (i : ι), f i 0 = 0}
{g : Π₀ (i : ι), β₁ i} :
(dfinsupp.map_range f hf g).support ⊆ g.support
theorem
dfinsupp.zip_with_def
{ι : Type u}
{β : ι → Type v}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
[Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι) (x : β₂ i), decidable (x ≠ 0)]
{f : Π (i : ι), β₁ i → β₂ i → β i}
{hf : ∀ (i : ι), f i 0 0 = 0}
{g₁ : Π₀ (i : ι), β₁ i}
{g₂ : Π₀ (i : ι), β₂ i} :
theorem
dfinsupp.support_zip_with
{ι : Type u}
{β : ι → Type v}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
[Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι) (x : β₂ i), decidable (x ≠ 0)]
{f : Π (i : ι), β₁ i → β₂ i → β i}
{hf : ∀ (i : ι), f i 0 0 = 0}
{g₁ : Π₀ (i : ι), β₁ i}
{g₂ : Π₀ (i : ι), β₂ i} :
theorem
dfinsupp.erase_def
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
(i : ι)
(f : Π₀ (i : ι), β i) :
@[simp]
theorem
dfinsupp.support_erase
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
(i : ι)
(f : Π₀ (i : ι), β i) :
(dfinsupp.erase i f).support = f.support.erase i
theorem
dfinsupp.support_update
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
(f : Π₀ (i : ι), β i)
(i : ι)
(b : β i)
[decidable (b = 0)] :
theorem
dfinsupp.filter_def
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{p : ι → Prop}
[decidable_pred p]
(f : Π₀ (i : ι), β i) :
dfinsupp.filter p f = dfinsupp.mk (finset.filter p f.support) (λ (i : ↥↑(finset.filter p f.support)), ⇑f i.val)
@[simp]
theorem
dfinsupp.support_filter
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{p : ι → Prop}
[decidable_pred p]
(f : Π₀ (i : ι), β i) :
(dfinsupp.filter p f).support = finset.filter p f.support
theorem
dfinsupp.subtype_domain_def
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{p : ι → Prop}
[decidable_pred p]
(f : Π₀ (i : ι), β i) :
dfinsupp.subtype_domain p f = dfinsupp.mk (finset.subtype p f.support) (λ (i : ↥↑(finset.subtype p f.support)), ⇑f ↑i)
@[simp]
theorem
dfinsupp.support_subtype_domain
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{p : ι → Prop}
[decidable_pred p]
{f : Π₀ (i : ι), β i} :
(dfinsupp.subtype_domain p f).support = finset.subtype p f.support
theorem
dfinsupp.support_add
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{g₁ g₂ : Π₀ (i : ι), β i} :
@[simp]
theorem
dfinsupp.support_neg
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_group (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{f : Π₀ (i : ι), β i} :
theorem
dfinsupp.support_smul
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[semiring γ]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι), module γ (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
(b : γ)
(v : Π₀ (i : ι), β i) :
@[protected, instance]
def
dfinsupp.decidable_eq
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι), decidable_eq (β i)] :
decidable_eq (Π₀ (i : ι), β i)
def
dfinsupp.prod
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → γ) :
γ
prod f g is the product of g i (f i) over the support of f.
def
dfinsupp.sum
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → γ) :
γ
sum f g is the sum of g i (f i) over the support of f.
theorem
dfinsupp.sum_map_range_index
{ι : Type u}
{γ : Type w}
[dec : decidable_eq ι]
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
[Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι) (x : β₂ i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{f : Π (i : ι), β₁ i → β₂ i}
{hf : ∀ (i : ι), f i 0 = 0}
{g : Π₀ (i : ι), β₁ i}
{h : Π (i : ι), β₂ i → γ}
(h0 : ∀ (i : ι), h i 0 = 0) :
(dfinsupp.map_range f hf g).sum h = g.sum (λ (i : ι) (b : β₁ i), h i (f i b))
theorem
dfinsupp.prod_map_range_index
{ι : Type u}
{γ : Type w}
[dec : decidable_eq ι]
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
[Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι) (x : β₂ i), decidable (x ≠ 0)]
[comm_monoid γ]
{f : Π (i : ι), β₁ i → β₂ i}
{hf : ∀ (i : ι), f i 0 = 0}
{g : Π₀ (i : ι), β₁ i}
{h : Π (i : ι), β₂ i → γ}
(h0 : ∀ (i : ι), h i 0 = 1) :
(dfinsupp.map_range f hf g).prod h = g.prod (λ (i : ι) (b : β₁ i), h i (f i b))
theorem
dfinsupp.prod_zero_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.sum_zero_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.prod_single_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{i : ι}
{b : β i}
{h : Π (i : ι), β i → γ}
(h_zero : h i 0 = 1) :
(dfinsupp.single i b).prod h = h i b
theorem
dfinsupp.sum_single_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{i : ι}
{b : β i}
{h : Π (i : ι), β i → γ}
(h_zero : h i 0 = 0) :
(dfinsupp.single i b).sum h = h i b
theorem
dfinsupp.prod_neg_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_group (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{g : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ}
(h0 : ∀ (i : ι), h i 0 = 1) :
theorem
dfinsupp.sum_neg_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_group (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{g : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ}
(h0 : ∀ (i : ι), h i 0 = 0) :
theorem
dfinsupp.sum_comm
{γ : Type w}
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{β₁ : ι₁ → Type u_3}
{β₂ : ι₂ → Type u_4}
[decidable_eq ι₁]
[decidable_eq ι₂]
[Π (i : ι₁), has_zero (β₁ i)]
[Π (i : ι₂), has_zero (β₂ i)]
[Π (i : ι₁) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι₂) (x : β₂ i), decidable (x ≠ 0)]
[add_comm_monoid γ]
(f₁ : Π₀ (i : ι₁), β₁ i)
(f₂ : Π₀ (i : ι₂), β₂ i)
(h : Π (i : ι₁), β₁ i → Π (i : ι₂), β₂ i → γ) :
theorem
dfinsupp.prod_comm
{γ : Type w}
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{β₁ : ι₁ → Type u_3}
{β₂ : ι₂ → Type u_4}
[decidable_eq ι₁]
[decidable_eq ι₂]
[Π (i : ι₁), has_zero (β₁ i)]
[Π (i : ι₂), has_zero (β₂ i)]
[Π (i : ι₁) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι₂) (x : β₂ i), decidable (x ≠ 0)]
[comm_monoid γ]
(f₁ : Π₀ (i : ι₁), β₁ i)
(f₂ : Π₀ (i : ι₂), β₂ i)
(h : Π (i : ι₁), β₁ i → Π (i : ι₂), β₂ i → γ) :
@[simp]
theorem
dfinsupp.sum_apply
{ι : Type u}
{β : ι → Type v}
{ι₁ : Type u₁}
[decidable_eq ι₁]
{β₁ : ι₁ → Type v₁}
[Π (i₁ : ι₁), has_zero (β₁ i₁)]
[Π (i : ι₁) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι), add_comm_monoid (β i)]
{f : Π₀ (i₁ : ι₁), β₁ i₁}
{g : Π (i₁ : ι₁), β₁ i₁ → (Π₀ (i : ι), β i)}
{i₂ : ι} :
theorem
dfinsupp.support_sum
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{ι₁ : Type u₁}
[decidable_eq ι₁]
{β₁ : ι₁ → Type v₁}
[Π (i₁ : ι₁), has_zero (β₁ i₁)]
[Π (i : ι₁) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{f : Π₀ (i₁ : ι₁), β₁ i₁}
{g : Π (i₁ : ι₁), β₁ i₁ → (Π₀ (i : ι), β i)} :
@[simp]
theorem
dfinsupp.prod_one
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{f : Π₀ (i : ι), β i} :
@[simp]
theorem
dfinsupp.sum_zero
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{f : Π₀ (i : ι), β i} :
@[simp]
theorem
dfinsupp.sum_add
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{f : Π₀ (i : ι), β i}
{h₁ h₂ : Π (i : ι), β i → γ} :
@[simp]
theorem
dfinsupp.prod_mul
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{f : Π₀ (i : ι), β i}
{h₁ h₂ : Π (i : ι), β i → γ} :
@[simp]
theorem
dfinsupp.sum_neg
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_group γ]
{f : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ} :
@[simp]
theorem
dfinsupp.prod_inv
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_group γ]
{f : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.sum_add_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{f g : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ}
(h_zero : ∀ (i : ι), h i 0 = 0)
(h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂) :
theorem
dfinsupp.prod_add_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{f g : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ}
(h_zero : ∀ (i : ι), h i 0 = 1)
(h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = (h i b₁) * h i b₂) :
theorem
add_submonoid.dfinsupp_sum_mem
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
(S : add_submonoid γ)
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → γ)
(h : ∀ (c : ι), ⇑f c ≠ 0 → g c (⇑f c) ∈ S) :
theorem
submonoid.dfinsupp_prod_mem
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
(S : submonoid γ)
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → γ)
(h : ∀ (c : ι), ⇑f c ≠ 0 → g c (⇑f c) ∈ S) :
@[simp]
theorem
dfinsupp.sum_eq_sum_fintype
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[fintype ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
(v : Π₀ (i : ι), β i)
{f : Π (i : ι), β i → γ}
(hf : ∀ (i : ι), f i 0 = 0) :
v.sum f = ∑ (i : ι), f i (⇑dfinsupp.equiv_fun_on_fintype v i)
@[simp]
theorem
dfinsupp.prod_eq_prod_fintype
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[fintype ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
(v : Π₀ (i : ι), β i)
{f : Π (i : ι), β i → γ}
(hf : ∀ (i : ι), f i 0 = 1) :
v.prod f = ∏ (i : ι), f i (⇑dfinsupp.equiv_fun_on_fintype v i)
def
dfinsupp.sum_add_hom
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ]
(φ : Π (i : ι), β i →+ γ) :
(Π₀ (i : ι), β i) →+ γ
When summing over an add_monoid_hom, the decidability assumption is not needed, and the result is
also an add_monoid_hom.
Equations
- dfinsupp.sum_add_hom φ = {to_fun := λ (f : Π₀ (i : ι), β i), quotient.lift_on f (λ (x : dfinsupp.pre ι (λ (i : ι), β i)), ∑ (i : ι) in x.pre_support.to_finset, ⇑(φ i) (x.to_fun i)) _, map_zero' := _, map_add' := _}
@[simp]
theorem
dfinsupp.sum_add_hom_single
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ]
(φ : Π (i : ι), β i →+ γ)
(i : ι)
(x : β i) :
⇑(dfinsupp.sum_add_hom φ) (dfinsupp.single i x) = ⇑(φ i) x
@[simp]
theorem
dfinsupp.sum_add_hom_comp_single
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ]
(f : Π (i : ι), β i →+ γ)
(i : ι) :
(dfinsupp.sum_add_hom f).comp (dfinsupp.single_add_hom β i) = f i
theorem
dfinsupp.sum_add_hom_apply
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
(φ : Π (i : ι), β i →+ γ)
(f : Π₀ (i : ι), β i) :
⇑(dfinsupp.sum_add_hom φ) f = f.sum (λ (x : ι), ⇑(φ x))
While we didn't need decidable instances to define it, we do to reduce it to a sum
theorem
add_submonoid.dfinsupp_sum_add_hom_mem
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ]
(S : add_submonoid γ)
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i →+ γ)
(h : ∀ (c : ι), ⇑f c ≠ 0 → ⇑(g c) (⇑f c) ∈ S) :
⇑(dfinsupp.sum_add_hom g) f ∈ S
theorem
add_submonoid.supr_eq_mrange_dfinsupp_sum_add_hom
{ι : Type u}
{γ : Type w}
[dec : decidable_eq ι]
[add_comm_monoid γ]
(S : ι → add_submonoid γ) :
supr S = (dfinsupp.sum_add_hom (λ (i : ι), (S i).subtype)).mrange
The supremum of a family of commutative additive submonoids is equal to the range of
dfinsupp.sum_add_hom; that is, every element in the supr can be produced from taking a finite
number of non-zero elements of S i, coercing them to γ, and summing them.
theorem
add_submonoid.bsupr_eq_mrange_dfinsupp_sum_add_hom
{ι : Type u}
{γ : Type w}
[dec : decidable_eq ι]
(p : ι → Prop)
[decidable_pred p]
[add_comm_monoid γ]
(S : ι → add_submonoid γ) :
(⨆ (i : ι) (h : p i), S i) = ((dfinsupp.sum_add_hom (λ (i : ι), (S i).subtype)).comp (dfinsupp.filter_add_monoid_hom (λ (i : ι), ↥(S i)) p)).mrange
The bounded supremum of a family of commutative additive submonoids is equal to the range of
dfinsupp.sum_add_hom composed with dfinsupp.filter_add_monoid_hom; that is, every element in the
bounded supr can be produced from taking a finite number of non-zero elements from the S i that
satisfy p i, coercing them to γ, and summing them.
theorem
add_submonoid.mem_supr_iff_exists_dfinsupp
{ι : Type u}
{γ : Type w}
[dec : decidable_eq ι]
[add_comm_monoid γ]
(S : ι → add_submonoid γ)
(x : γ) :
theorem
add_submonoid.mem_supr_iff_exists_dfinsupp'
{ι : Type u}
{γ : Type w}
[dec : decidable_eq ι]
[add_comm_monoid γ]
(S : ι → add_submonoid γ)
[Π (i : ι) (x : ↥(S i)), decidable (x ≠ 0)]
(x : γ) :
A variant of add_submonoid.mem_supr_iff_exists_dfinsupp with the RHS fully unfolded.
theorem
add_submonoid.mem_bsupr_iff_exists_dfinsupp
{ι : Type u}
{γ : Type w}
[dec : decidable_eq ι]
(p : ι → Prop)
[decidable_pred p]
[add_comm_monoid γ]
(S : ι → add_submonoid γ)
(x : γ) :
(x ∈ ⨆ (i : ι) (h : p i), S i) ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), ⇑(dfinsupp.sum_add_hom (λ (i : ι), (S i).subtype)) (dfinsupp.filter p f) = x
theorem
dfinsupp.sum_add_hom_comm
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{β₁ : ι₁ → Type u_3}
{β₂ : ι₂ → Type u_4}
{γ : Type u_5}
[decidable_eq ι₁]
[decidable_eq ι₂]
[Π (i : ι₁), add_zero_class (β₁ i)]
[Π (i : ι₂), add_zero_class (β₂ i)]
[add_comm_monoid γ]
(f₁ : Π₀ (i : ι₁), β₁ i)
(f₂ : Π₀ (i : ι₂), β₂ i)
(h : Π (i : ι₁) (j : ι₂), β₁ i →+ β₂ j →+ γ) :
⇑(dfinsupp.sum_add_hom (λ (i₂ : ι₂), ⇑(dfinsupp.sum_add_hom (λ (i₁ : ι₁), h i₁ i₂)) f₁)) f₂ = ⇑(dfinsupp.sum_add_hom (λ (i₁ : ι₁), ⇑(dfinsupp.sum_add_hom (λ (i₂ : ι₂), (h i₁ i₂).flip)) f₂)) f₁
@[simp]
theorem
dfinsupp.lift_add_hom_apply
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ]
(φ : Π (i : ι), (λ (i : ι), β i) i →+ γ) :
@[simp]
theorem
dfinsupp.lift_add_hom_symm_apply
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ]
(F : (Π₀ (i : ι), β i) →+ γ)
(i : ι) :
⇑(dfinsupp.lift_add_hom.symm) F i = F.comp (dfinsupp.single_add_hom β i)
def
dfinsupp.lift_add_hom
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ] :
The dfinsupp version of finsupp.lift_add_hom,
Equations
- dfinsupp.lift_add_hom = {to_fun := dfinsupp.sum_add_hom _inst_2, inv_fun := λ (F : (Π₀ (i : ι), β i) →+ γ) (i : ι), F.comp (dfinsupp.single_add_hom β i), left_inv := _, right_inv := _, map_add' := _}
@[simp]
theorem
dfinsupp.lift_add_hom_single_add_hom
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)] :
⇑dfinsupp.lift_add_hom (dfinsupp.single_add_hom β) = add_monoid_hom.id (Π₀ (i : ι), β i)
The dfinsupp version of finsupp.lift_add_hom_single_add_hom,
theorem
dfinsupp.lift_add_hom_apply_single
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ]
(f : Π (i : ι), β i →+ γ)
(i : ι)
(x : β i) :
⇑(⇑dfinsupp.lift_add_hom f) (dfinsupp.single i x) = ⇑(f i) x
The dfinsupp version of finsupp.lift_add_hom_apply_single,
theorem
dfinsupp.lift_add_hom_comp_single
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ]
(f : Π (i : ι), β i →+ γ)
(i : ι) :
(⇑dfinsupp.lift_add_hom f).comp (dfinsupp.single_add_hom β i) = f i
The dfinsupp version of finsupp.lift_add_hom_comp_single,
theorem
dfinsupp.comp_lift_add_hom
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
{δ : Type u_1}
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ]
[add_comm_monoid δ]
(g : γ →+ δ)
(f : Π (i : ι), β i →+ γ) :
g.comp (⇑dfinsupp.lift_add_hom f) = ⇑dfinsupp.lift_add_hom (λ (a : ι), g.comp (f a))
The dfinsupp version of finsupp.comp_lift_add_hom,
@[simp]
theorem
dfinsupp.sum_add_hom_zero
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ] :
dfinsupp.sum_add_hom (λ (i : ι), 0) = 0
@[simp]
theorem
dfinsupp.sum_add_hom_add
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ]
(g h : Π (i : ι), β i →+ γ) :
dfinsupp.sum_add_hom (λ (i : ι), g i + h i) = dfinsupp.sum_add_hom g + dfinsupp.sum_add_hom h
@[simp]
theorem
dfinsupp.sum_add_hom_single_add_hom
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)] :
dfinsupp.sum_add_hom (dfinsupp.single_add_hom β) = add_monoid_hom.id (Π₀ (i : ι), β i)
theorem
dfinsupp.comp_sum_add_hom
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
{δ : Type u_1}
[Π (i : ι), add_zero_class (β i)]
[add_comm_monoid γ]
[add_comm_monoid δ]
(g : γ →+ δ)
(f : Π (i : ι), β i →+ γ) :
g.comp (dfinsupp.sum_add_hom f) = dfinsupp.sum_add_hom (λ (a : ι), g.comp (f a))
theorem
dfinsupp.sum_sub_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_group (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_group γ]
{f g : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ}
(h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂) :
theorem
dfinsupp.prod_finset_sum_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
{α : Type x}
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{s : finset α}
{g : α → (Π₀ (i : ι), β i)}
{h : Π (i : ι), β i → γ}
(h_zero : ∀ (i : ι), h i 0 = 1)
(h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = (h i b₁) * h i b₂) :
theorem
dfinsupp.sum_finset_sum_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
{α : Type x}
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{s : finset α}
{g : α → (Π₀ (i : ι), β i)}
{h : Π (i : ι), β i → γ}
(h_zero : ∀ (i : ι), h i 0 = 0)
(h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂) :
theorem
dfinsupp.sum_sum_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
{ι₁ : Type u₁}
[decidable_eq ι₁]
{β₁ : ι₁ → Type v₁}
[Π (i₁ : ι₁), has_zero (β₁ i₁)]
[Π (i : ι₁) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{f : Π₀ (i₁ : ι₁), β₁ i₁}
{g : Π (i₁ : ι₁), β₁ i₁ → (Π₀ (i : ι), β i)}
{h : Π (i : ι), β i → γ}
(h_zero : ∀ (i : ι), h i 0 = 0)
(h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂) :
theorem
dfinsupp.prod_sum_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
{ι₁ : Type u₁}
[decidable_eq ι₁]
{β₁ : ι₁ → Type v₁}
[Π (i₁ : ι₁), has_zero (β₁ i₁)]
[Π (i : ι₁) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{f : Π₀ (i₁ : ι₁), β₁ i₁}
{g : Π (i₁ : ι₁), β₁ i₁ → (Π₀ (i : ι), β i)}
{h : Π (i : ι), β i → γ}
(h_zero : ∀ (i : ι), h i 0 = 1)
(h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = (h i b₁) * h i b₂) :
@[simp]
theorem
dfinsupp.sum_single
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{f : Π₀ (i : ι), β i} :
f.sum dfinsupp.single = f
theorem
dfinsupp.sum_subtype_domain_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{v : Π₀ (i : ι), β i}
{p : ι → Prop}
[decidable_pred p]
{h : Π (i : ι), β i → γ}
(hp : ∀ (x : ι), x ∈ v.support → p x) :
theorem
dfinsupp.prod_subtype_domain_index
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{v : Π₀ (i : ι), β i}
{p : ι → Prop}
[decidable_pred p]
{h : Π (i : ι), β i → γ}
(hp : ∀ (x : ι), x ∈ v.support → p x) :
theorem
dfinsupp.subtype_domain_sum
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
[Π (i : ι), add_comm_monoid (β i)]
{s : finset γ}
{h : γ → (Π₀ (i : ι), β i)}
{p : ι → Prop}
[decidable_pred p] :
dfinsupp.subtype_domain p (∑ (c : γ) in s, h c) = ∑ (c : γ) in s, dfinsupp.subtype_domain p (h c)
theorem
dfinsupp.subtype_domain_finsupp_sum
{ι : Type u}
{γ : Type w}
{β : ι → Type v}
{δ : γ → Type x}
[decidable_eq γ]
[Π (c : γ), has_zero (δ c)]
[Π (c : γ) (x : δ c), decidable (x ≠ 0)]
[Π (i : ι), add_comm_monoid (β i)]
{p : ι → Prop}
[decidable_pred p]
{s : Π₀ (c : γ), δ c}
{h : Π (c : γ), δ c → (Π₀ (i : ι), β i)} :
dfinsupp.subtype_domain p (s.sum h) = s.sum (λ (c : γ) (d : δ c), dfinsupp.subtype_domain p (h c d))
Bundled versions of dfinsupp.map_range #
The names should match the equivalent bundled finsupp.map_range definitions.
theorem
dfinsupp.map_range_add
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), add_zero_class (β₁ i)]
[Π (i : ι), add_zero_class (β₂ i)]
(f : Π (i : ι), β₁ i → β₂ i)
(hf : ∀ (i : ι), f i 0 = 0)
(hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y)
(g₁ g₂ : Π₀ (i : ι), β₁ i) :
dfinsupp.map_range f hf (g₁ + g₂) = dfinsupp.map_range f hf g₁ + dfinsupp.map_range f hf g₂
@[simp]
theorem
dfinsupp.map_range.add_monoid_hom_apply
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), add_zero_class (β₁ i)]
[Π (i : ι), add_zero_class (β₂ i)]
(f : Π (i : ι), β₁ i →+ β₂ i)
(ᾰ : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :
⇑(dfinsupp.map_range.add_monoid_hom f) ᾰ = dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(f i) x) _ ᾰ
def
dfinsupp.map_range.add_monoid_hom
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), add_zero_class (β₁ i)]
[Π (i : ι), add_zero_class (β₂ i)]
(f : Π (i : ι), β₁ i →+ β₂ i) :
(Π₀ (i : ι), β₁ i) →+ Π₀ (i : ι), β₂ i
dfinsupp.map_range as an add_monoid_hom.
Equations
- dfinsupp.map_range.add_monoid_hom f = {to_fun := dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(f i) x) _, map_zero' := _, map_add' := _}
@[simp]
theorem
dfinsupp.map_range.add_monoid_hom_id
{ι : Type u}
{β₂ : ι → Type v₂}
[Π (i : ι), add_zero_class (β₂ i)] :
dfinsupp.map_range.add_monoid_hom (λ (i : ι), add_monoid_hom.id (β₂ i)) = add_monoid_hom.id (Π₀ (i : ι), β₂ i)
theorem
dfinsupp.map_range.add_monoid_hom_comp
{ι : Type u}
{β : ι → Type v}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), add_zero_class (β i)]
[Π (i : ι), add_zero_class (β₁ i)]
[Π (i : ι), add_zero_class (β₂ i)]
(f : Π (i : ι), β₁ i →+ β₂ i)
(f₂ : Π (i : ι), β i →+ β₁ i) :
dfinsupp.map_range.add_monoid_hom (λ (i : ι), (f i).comp (f₂ i)) = (dfinsupp.map_range.add_monoid_hom f).comp (dfinsupp.map_range.add_monoid_hom f₂)
def
dfinsupp.map_range.add_equiv
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), add_zero_class (β₁ i)]
[Π (i : ι), add_zero_class (β₂ i)]
(e : Π (i : ι), β₁ i ≃+ β₂ i) :
(Π₀ (i : ι), β₁ i) ≃+ Π₀ (i : ι), β₂ i
dfinsupp.map_range.add_monoid_hom as an add_equiv.
Equations
- dfinsupp.map_range.add_equiv e = {to_fun := dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(e i) x) _, inv_fun := dfinsupp.map_range (λ (i : ι) (x : β₂ i), ⇑((e i).symm) x) _, left_inv := _, right_inv := _, map_add' := _}
@[simp]
theorem
dfinsupp.map_range.add_equiv_apply
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), add_zero_class (β₁ i)]
[Π (i : ι), add_zero_class (β₂ i)]
(e : Π (i : ι), β₁ i ≃+ β₂ i)
(ᾰ : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :
⇑(dfinsupp.map_range.add_equiv e) ᾰ = dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(e i) x) _ ᾰ
@[simp]
theorem
dfinsupp.map_range.add_equiv_refl
{ι : Type u}
{β₁ : ι → Type v₁}
[Π (i : ι), add_zero_class (β₁ i)] :
dfinsupp.map_range.add_equiv (λ (i : ι), add_equiv.refl (β₁ i)) = add_equiv.refl (Π₀ (i : ι), β₁ i)
theorem
dfinsupp.map_range.add_equiv_trans
{ι : Type u}
{β : ι → Type v}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), add_zero_class (β i)]
[Π (i : ι), add_zero_class (β₁ i)]
[Π (i : ι), add_zero_class (β₂ i)]
(f : Π (i : ι), β i ≃+ β₁ i)
(f₂ : Π (i : ι), β₁ i ≃+ β₂ i) :
dfinsupp.map_range.add_equiv (λ (i : ι), (f i).trans (f₂ i)) = (dfinsupp.map_range.add_equiv f).trans (dfinsupp.map_range.add_equiv f₂)
@[simp]
theorem
dfinsupp.map_range.add_equiv_symm
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), add_zero_class (β₁ i)]
[Π (i : ι), add_zero_class (β₂ i)]
(e : Π (i : ι), β₁ i ≃+ β₂ i) :
(dfinsupp.map_range.add_equiv e).symm = dfinsupp.map_range.add_equiv (λ (i : ι), (e i).symm)
Product and sum lemmas for bundled morphisms. #
In this section, we provide analogues of add_monoid_hom.map_sum, add_monoid_hom.coe_sum, and
add_monoid_hom.sum_apply for dfinsupp.sum and dfinsupp.sum_add_hom instead of finset.sum.
We provide these for add_monoid_hom, monoid_hom, ring_hom, add_equiv, and mul_equiv.
Lemmas for linear_map and linear_equiv are in another file.
@[simp]
theorem
add_monoid_hom.map_dfinsupp_sum
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid R]
[add_comm_monoid S]
(h : R →+ S)
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → R) :
@[simp]
theorem
monoid_hom.map_dfinsupp_prod
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid R]
[comm_monoid S]
(h : R →* S)
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → R) :
theorem
add_monoid_hom.coe_dfinsupp_sum
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_monoid R]
[add_comm_monoid S]
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → R →+ S) :
theorem
monoid_hom.coe_dfinsupp_prod
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[monoid R]
[comm_monoid S]
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → R →* S) :
@[simp]
theorem
monoid_hom.dfinsupp_prod_apply
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[monoid R]
[comm_monoid S]
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → R →* S)
(r : R) :
@[simp]
theorem
add_monoid_hom.dfinsupp_sum_apply
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_monoid R]
[add_comm_monoid S]
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → R →+ S)
(r : R) :
@[simp]
theorem
ring_hom.map_dfinsupp_prod
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_semiring R]
[comm_semiring S]
(h : R →+* S)
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → R) :
@[simp]
theorem
ring_hom.map_dfinsupp_sum
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[non_assoc_semiring R]
[non_assoc_semiring S]
(h : R →+* S)
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → R) :
@[simp]
theorem
add_equiv.map_dfinsupp_sum
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid R]
[add_comm_monoid S]
(h : R ≃+ S)
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → R) :
@[simp]
theorem
mul_equiv.map_dfinsupp_prod
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid R]
[comm_monoid S]
(h : R ≃* S)
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i → R) :
The above lemmas, repeated for dfinsupp.sum_add_hom.
@[simp]
theorem
add_monoid_hom.map_dfinsupp_sum_add_hom
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[add_comm_monoid R]
[add_comm_monoid S]
[Π (i : ι), add_zero_class (β i)]
(h : R →+ S)
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i →+ R) :
⇑h (⇑(dfinsupp.sum_add_hom g) f) = ⇑(dfinsupp.sum_add_hom (λ (i : ι), h.comp (g i))) f
@[simp]
theorem
add_monoid_hom.dfinsupp_sum_add_hom_apply
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[add_zero_class R]
[add_comm_monoid S]
[Π (i : ι), add_zero_class (β i)]
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i →+ R →+ S)
(r : R) :
⇑(⇑(dfinsupp.sum_add_hom g) f) r = ⇑(dfinsupp.sum_add_hom (λ (i : ι), (⇑add_monoid_hom.eval r).comp (g i))) f
theorem
add_monoid_hom.coe_dfinsupp_sum_add_hom
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[add_zero_class R]
[add_comm_monoid S]
[Π (i : ι), add_zero_class (β i)]
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i →+ R →+ S) :
⇑(⇑(dfinsupp.sum_add_hom g) f) = ⇑(dfinsupp.sum_add_hom (λ (i : ι), (add_monoid_hom.coe_fn R S).comp (g i))) f
@[simp]
theorem
ring_hom.map_dfinsupp_sum_add_hom
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[non_assoc_semiring R]
[non_assoc_semiring S]
[Π (i : ι), add_zero_class (β i)]
(h : R →+* S)
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i →+ R) :
⇑h (⇑(dfinsupp.sum_add_hom g) f) = ⇑(dfinsupp.sum_add_hom (λ (i : ι), h.to_add_monoid_hom.comp (g i))) f
@[simp]
theorem
add_equiv.map_dfinsupp_sum_add_hom
{ι : Type u}
{β : ι → Type v}
[decidable_eq ι]
{R : Type u_1}
{S : Type u_2}
[add_comm_monoid R]
[add_comm_monoid S]
[Π (i : ι), add_zero_class (β i)]
(h : R ≃+ S)
(f : Π₀ (i : ι), β i)
(g : Π (i : ι), β i →+ R) :
⇑h (⇑(dfinsupp.sum_add_hom g) f) = ⇑(dfinsupp.sum_add_hom (λ (i : ι), h.to_add_monoid_hom.comp (g i))) f