## Stream: maths

### Topic: coeff_mul

#### Johan Commelin (Jul 09 2019 at 06:42):

I have just finished the proof of coeff_mul for mv_polynomial:

#### Johan Commelin (Jul 09 2019 at 06:43):

lemma coeff_mul (φ ψ : mv_polynomial σ α) (n) :
coeff n (φ * ψ) = finset.sum (finsupp.nat_downset n) (λ m, coeff m φ * coeff (n - m) ψ) :=


#### Johan Commelin (Jul 09 2019 at 06:43):

I think this would fill a little gap in the API for polynomials.

#### Johan Commelin (Jul 09 2019 at 06:44):

Question: what should finsupp.nat_downset be called? Does this somehow generalise? Is there something like "partial orders with downsets that are finsets"?

#### Johan Commelin (Jul 09 2019 at 06:44):

Also... if people want a golfing challenge... currently the proof is a whopping 120 lines...

#### Johan Commelin (Jul 09 2019 at 06:46):

Another option is to sum over a finset in the product, so that we are even closer to mimicking $\sum_{i + j = n} c_i(\phi) \cdot c_j(\psi)$.

#### Mario Carneiro (Jul 09 2019 at 07:02):

It already exists, it's called multiset.diagonal I think

#### Mario Carneiro (Jul 09 2019 at 07:03):

(actually that's the subtraction free version - nat_downset is multiset.powerset)

#### Mario Carneiro (Jul 09 2019 at 07:05):

Just like with nat, I recommend avoiding subtraction here and indeed I suggest using a finset over the product as you've indicated

#### Johan Commelin (Jul 09 2019 at 07:19):

Ok, but multiset X is not defeq to finsupp X nat

#### Johan Commelin (Jul 09 2019 at 07:22):

@Mario Carneiro I think multiset.diagonal is very nice. But how should I apply it in the context of mv_polynomial? There is no obvious analogue for arbitrary finsupps. Should I use glue between multiset X and finsupp X nat?

#### Mario Carneiro (Jul 09 2019 at 07:24):

The analogue I think is to axiomatize it

#### Mario Carneiro (Jul 09 2019 at 07:25):

there are other examples, but I don't know a better way to say it than "the set of all elements below x is finite"

#### Mario Carneiro (Jul 09 2019 at 07:26):

In the case of finsupp X nat specifically, I think I would just prove it by transferring from multiset X

#### Johan Commelin (Jul 09 2019 at 07:27):

I'm still confused about what you would want the statement of coeff_mul to look like...

#### Mario Carneiro (Jul 09 2019 at 07:28):

lemma coeff_mul (φ ψ : mv_polynomial σ α) (n) :
coeff n (φ * ψ) = finset.sum (finsupp.diagonal n) (λ p, coeff p.1 φ * coeff p.2 ψ) :=


#### Mario Carneiro (Jul 09 2019 at 07:30):

here finsupp.diagonal n is something like (multiset.diagonal n.support).map (prod.map f f) where f m = \lam x, count x m

#### Mario Carneiro (Jul 09 2019 at 07:32):

and f is then shown to be one half of an order isomorphism, so that mem_diagonal holds also for finsupp

#### Johan Commelin (Jul 09 2019 at 07:33):

Aha... thanks for the suggestions!

#### Johan Commelin (Jul 09 2019 at 07:34):

@Mario Carneiro It's not a problem that finsupp.diagonal is only defined for ℕ?

#### Mario Carneiro (Jul 09 2019 at 07:35):

The generalization, like I said, is to have a typeclass for types that have a diagonal function; this is the instance for nat

#### Mario Carneiro (Jul 09 2019 at 07:38):

Another example of a type with this property (let's say "downward finite") is finsupp X A itself, when A is downward finite

#### Kenny Lau (Jul 09 2019 at 07:41):

Ok, but multiset X is not defeq to finsupp X nat

hey we have a natural isomorphism

#### Mario Carneiro (Jul 09 2019 at 07:43):

I would have thought you would be the first to point out that it's not constructively provable

which direction?

#### Mario Carneiro (Jul 09 2019 at 07:46):

finsupp -> multiset

#### Kenny Lau (Jul 09 2019 at 07:47):

but you have the support

#### Mario Carneiro (Jul 09 2019 at 07:48):

Oh you're right. As long as X is decidable both directions work

#### Kenny Lau (Jul 09 2019 at 07:48):

looks like I need to bring up my special category

#### Kenny Lau (Jul 09 2019 at 10:12):

@Mario Carneiro

-- ⟨s.to_finset, λ x, s.count x, λ x, multiset.mem_to_finset.trans $multiset.count_pos.symm.trans$ nat.pos_iff_ne_zero⟩
-- faster but less idiomatic
def Multiset_Finsupp_nat : Multiset.{u} ≅ Finsupp_nat.{u} :=
{ hom :=
{ app := λ α s, (s.map $λ x, finsupp.single x 1).sum,  #### Kenny Lau (Jul 09 2019 at 10:12): which one would you choose? #### Kenny Lau (Jul 09 2019 at 11:20): import data.multiset data.finsupp import category_theory.natural_isomorphism category_theory.types category_theory.opposites category_theory.concrete_category universe u open category_theory namespace category_theory.instances @[reducible] def DecEq := bundled decidable_eq instance (x : DecEq) : decidable_eq x := x.str instance DecEq_category : category DecEq := { hom := λ x y, x → y, id := λ x, id, comp := λ x y z f g, g ∘ f } end category_theory.instances open category_theory.instances @[reducible] def Multiset : DecEq.{u} ⥤ Type u := { obj := λ α, multiset α, map := λ α β, multiset.map, map_id' := λ α, funext multiset.map_id, map_comp' := λ α β γ f g, funext$ λ s, (multiset.map_map g f s).symm }

@[reducible] def Finsupp_nat : DecEq.{u} ⥤ Type u :=
{ obj := λ α, α →₀ ℕ,
map := λ α β, finsupp.map_domain,
map_id' := λ α, funext $λ s, finsupp.map_domain_id, map_comp' := λ α β γ f g, funext$ λ s, finsupp.map_domain_comp }

theorem multiset.map_repeat {α : Type u} {β : Type*} (f : α → β) (x : α) (n : ℕ) :
multiset.map f (multiset.repeat x n) = multiset.repeat (f x) n :=
nat.rec_on n rfl $λ n ih, by rw [multiset.repeat_succ, multiset.map_cons, ih, multiset.repeat_succ] theorem multiset.repeat_add {α : Type u} (x : α) (m n : ℕ) : multiset.repeat x (m + n) = multiset.repeat x m + multiset.repeat x n := nat.rec_on n (by rw [multiset.repeat_zero, add_zero, add_zero])$ λ n ih,

-- ⟨s.to_finset, λ x, s.count x, λ x, multiset.mem_to_finset.trans $multiset.count_pos.symm.trans$ nat.pos_iff_ne_zero⟩
-- faster but less idiomatic
def Multiset_Finsupp_nat : Multiset.{u} ≅ Finsupp_nat.{u} :=
{ hom :=
{ app := λ α s, (s.map $λ x, finsupp.single x 1).sum, naturality' := λ α β f, funext$ λ s, finsupp.ext $λ x, show ((multiset.map f s).map$ λ x, finsupp.single x 1).sum x = finsupp.map_domain f (s.map $λ x, finsupp.single x 1).sum x, from multiset.induction_on s rfl$ λ a s ih, if h : f a = x
then by rw [multiset.map_cons, multiset.map_cons, multiset.sum_cons, finsupp.add_apply, finsupp.single_apply, if_pos h,
else by rw [multiset.map_cons, multiset.map_cons, multiset.sum_cons, finsupp.add_apply, finsupp.single_apply, if_neg h,
inv :=
{ app := λ α s, s.sum multiset.repeat,
naturality' := λ α β f, funext $λ s, show (s.map_domain f).sum multiset.repeat = (s.sum multiset.repeat).map f, from finsupp.induction s rfl$ λ x n s hsx hn ih, begin
{ refl }, { intros, refl }, { intros, rw multiset.repeat_add },
{ refl }, { intros, refl }, { intros, rw multiset.repeat_add }
end },
hom_inv_id' := nat_trans.ext $λ α, funext$ λ s, by skip,
inv_hom_id' := nat_trans.ext $λ α, funext$ λ s, finsupp.ext $by skip }  #### Kenny Lau (Jul 09 2019 at 11:20): that's it for now #### Kenny Lau (Jul 09 2019 at 13:25): I think I was just aware of finsupp.of_multiset #### Kenny Lau (Jul 09 2019 at 13:31): import data.multiset data.finsupp import category_theory.natural_isomorphism category_theory.types category_theory.opposites category_theory.concrete_category universe u open category_theory namespace category_theory.instances @[reducible] def DecEq := bundled decidable_eq instance (x : DecEq) : decidable_eq x := x.str instance DecEq_category : category DecEq := { hom := λ x y, x → y, id := λ x, id, comp := λ x y z f g, g ∘ f } end category_theory.instances open category_theory.instances @[reducible] def Multiset : DecEq.{u} ⥤ Type u := { obj := λ α, multiset α, map := λ α β, multiset.map, map_id' := λ α, funext multiset.map_id, map_comp' := λ α β γ f g, funext$ λ s, (multiset.map_map g f s).symm }

@[reducible] def Finsupp_nat : DecEq.{u} ⥤ Type u :=
{ obj := λ α, α →₀ ℕ,
map := λ α β, finsupp.map_domain,
map_id' := λ α, funext $λ s, finsupp.map_domain_id, map_comp' := λ α β γ f g, funext$ λ s, finsupp.map_domain_comp }

theorem multiset.map_repeat {α : Type u} {β : Type*} (f : α → β) (x : α) (n : ℕ) :
multiset.map f (multiset.repeat x n) = multiset.repeat (f x) n :=
nat.rec_on n rfl $λ n ih, by rw [multiset.repeat_succ, multiset.map_cons, ih, multiset.repeat_succ] theorem multiset.repeat_add {α : Type u} (x : α) (m n : ℕ) : multiset.repeat x (m + n) = multiset.repeat x m + multiset.repeat x n := nat.rec_on n (by rw [multiset.repeat_zero, add_zero, add_zero])$ λ n ih,

-- ⟨s.to_finset, λ x, s.count x, λ x, multiset.mem_to_finset.trans $multiset.count_pos.symm.trans$ nat.pos_iff_ne_zero⟩
-- faster but less idiomatic
def Multiset_Finsupp_nat : Multiset.{u} ≅ Finsupp_nat.{u} :=
{ hom :=
{ app := λ α s, (s.map $λ x, finsupp.single x 1).sum, naturality' := λ α β f, funext$ λ s, finsupp.ext $λ x, show ((multiset.map f s).map$ λ x, finsupp.single x 1).sum x = finsupp.map_domain f (s.map $λ x, finsupp.single x 1).sum x, from multiset.induction_on s rfl$ λ a s ih, if h : f a = x
then by rw [multiset.map_cons, multiset.map_cons, multiset.sum_cons, finsupp.add_apply, finsupp.single_apply, if_pos h,
else by rw [multiset.map_cons, multiset.map_cons, multiset.sum_cons, finsupp.add_apply, finsupp.single_apply, if_neg h,
inv :=
{ app := λ α s, s.sum multiset.repeat,
naturality' := λ α β f, funext $λ s, show (s.map_domain f).sum multiset.repeat = (s.sum multiset.repeat).map f, from finsupp.induction s rfl$ λ x n s hsx hn ih, begin
{ refl }, { intros, refl }, { intros, rw multiset.repeat_add },
{ refl }, { intros, refl }, { intros, rw multiset.repeat_add }
end },
hom_inv_id' := nat_trans.ext $λ α, funext$ λ s,
show (s.map $λ x, finsupp.single x 1).sum.sum multiset.repeat = s, from multiset.induction_on s rfl$ λ a s ih, begin
{ refl }, { intros, refl }, { intros, rw multiset.repeat_add }
end,
inv_hom_id' := nat_trans.ext $λ α, funext$ λ s,
show ((s.sum multiset.repeat).map $λ x, finsupp.single x 1).sum = s, from finsupp.induction s rfl$ λ y n s hsy hn ih, begin
{ congr' 1, clear hn, induction n with n ih,
{ rw [finsupp.single_zero, multiset.repeat_zero, multiset.sum_zero] },
{ refl }, { intros, refl }, { intros, rw multiset.repeat_add }
end }


#### Johan Commelin (Jul 09 2019 at 14:20):

Stuff got 90 lines shorter after @Mario Carneiro's suggestions: https://gist.github.com/jcommelin/add8c8df8b3479c435d3f5ac34cdb1f7

#### Johan Commelin (Jul 09 2019 at 14:20):

Still using - to subtract single s 1 but I think that can't be avoided.

#### Patrick Massot (Jul 09 2019 at 14:23):

This is still pretty frightening. It's really baffling to think the definition of multiplication does not make this lemma obvious...

#### Johan Commelin (Jul 09 2019 at 14:23):

Of course people shouldn't be discouraged to golf this down to a 5 line proof

#### Johan Commelin (Jul 09 2019 at 14:46):

I really feel like making this the definition of multiplication.

#### Johan Commelin (Jul 09 2019 at 14:46):

But I guess mv_polynomial inherits multiplication in a crazy way from ℕ being a add_monoid.

#### Chris Hughes (Jul 09 2019 at 14:56):

I'm surprised you didn't use multiset.count anywhere.

#### Johan Commelin (Jul 09 2019 at 14:57):

Maybe I should not have proven it by induction on the polynomials...

I don't know.

#### Johan Commelin (Jul 09 2019 at 14:57):

It seemed like an obvious thing to do. Maybe it is obviously bad.

#### Johan Commelin (Jul 11 2019 at 09:19):

lemma coeff_mul (φ ψ : mv_polynomial σ α) (n : σ →₀ ℕ) :
coeff n (φ * ψ) = finset.sum (diagonal n) (λ p, coeff p.1 φ * coeff p.2 ψ) :=
begin
rw mul_def,
have := @finset.sum_sigma (σ →₀ ℕ) α _ _ φ.support (λ _, ψ.support)
(λ x, if (x.1 + x.2 = n) then coeff x.1 φ * coeff x.2 ψ else 0),
convert this.symm using 1; clear this,
{ rw [coeff],
repeat {rw sum_apply, apply finset.sum_congr rfl, intros, dsimp only},
exact single_apply },
{ have : (diagonal n).filter (λ x, x.1 ∈ φ.support ∧ x.2 ∈ ψ.support) ⊆ (diagonal n) :=
finset.filter_subset _,
rw [← finset.sum_sdiff this, finset.sum_eq_zero, zero_add], swap,
{ intros x hx, rw [finset.mem_sdiff, not_iff_not_of_iff (finset.mem_filter),
not_and, not_and, not_mem_support_iff] at hx,
by_cases H : x.1 ∈ φ.support,
{ rw [coeff, coeff, hx.2 hx.1 H, mul_zero] },
{ rw not_mem_support_iff at H, rw [coeff, H, zero_mul] } },
symmetry,
rw [← finset.sum_sdiff (finset.filter_subset _), finset.sum_eq_zero, zero_add], swap,
{ intros x hx, rw [finset.mem_sdiff, not_iff_not_of_iff (finset.mem_filter), not_and] at hx,
replace hx := hx.2 hx.1, rw if_neg, exact hx },
{ apply finset.sum_bij, swap 5, { intros x hx, exact (x.1, x.2) },
{ intros x hx, rw [finset.mem_filter, finset.mem_sigma] at hx,
rw [finset.mem_filter, mem_diagonal],
dsimp, exact hx.symm },
{ intros x hx, rw finset.mem_filter at hx, rw if_pos hx.2 },
{ rintros ⟨i,j⟩ ⟨k,l⟩ hij hkl, simpa using and.intro },
{ rintros ⟨i,j⟩ hij, refine ⟨⟨i,j⟩, _, _⟩, { apply_instance },
{ rw [finset.mem_filter, mem_diagonal] at hij, rw [finset.mem_filter, finset.mem_sigma],
exact hij.symm },
{ refl } } },
all_goals { apply_instance } }
end
`

#### Johan Commelin (Jul 11 2019 at 09:19):

I hope this is a more reasonable length.

Last updated: May 10 2021 at 06:13 UTC