Natural embedding of quotients

Stream: new members

[Hanting Zhang]

Given f : α → β and the induced quotient setoid.ker f, how can I extend the map α → quotient (setoid.ker f) ↪ β? I haven't found anything in mathlib yet.

[Adam Topaz]

Can you provide a #mwe ?

[Adam Topaz]

I'm not sure what you mean by extend the map.

[Hanting Zhang]

I'm trying to prove Vieta's formulas:

import ring_theory.polynomial.basic

universes u v
open_locale big_operators
open polynomial finset

namespace vieta

variables {α β : Type u} [integral_domain α]
variables {n : ℕ} {r : ℕ → α} {f : polynomial α}

noncomputable instance has_coe_poly : has_coe α (polynomial α) := ⟨λ a, monomial 0 a⟩

lemma coeff_poly_from_roots :
  (∏ i in range n, (X - (r i : polynomial α)))
  = ∑ k in range n, (∑ A in (powerset_len (n - k) (range n)), (∏ j in A, r j)) * X ^ k :=
begin
  have h : ∏ i in range n, (X - (r i : polynomial α)) = ∏ i in range n, ((- r i : polynomial α) + (λ i, X) i) :=
  begin congr, ext, rw sub_eq_add_neg, rw add_comm end,
  rw h,
  rw prod_add,
  rw sum_partition (setoid.ker card),
  sorry
end
end vieta

[Hanting Zhang]

At sorry I've managed turn the product into a double sum, first over equivalence classes of powerset (range n) of cardinality 0..n, then over all the subsets of cardinality k.

[Yakov Pechersky]

Is this true for n = 0?

[Yakov Pechersky]

Doesn't seem like it.

[Yakov Pechersky]

And if I change it to over n + 1, then for n = 0, one has to prove X - ↑(r 0) = ↑(r 0)

[Hanting Zhang]

I think I've stated the problem wrong. The ranges on the sum should be range (n + 1).

[Hanting Zhang]

That's a minor off by one error though, I'm more stuck on how to translate between the sum indices correctly.

[Yakov Pechersky]

You should be able to induct on the sums or on n

[Yakov Pechersky]

Then there are lemmas that will undo the sums over range (n + 1) like docs#finset.sum_range_succ

[Eric Wieser]

Although you might not need to if the lemmas doing the induction already exist

[Eric Wieser]

What's the goal state at the sorry?

[Yakov Pechersky]

Except here it's the equality of a product with a sum, which I don't think is covered by those lemmas, which usually expect both sides to be sums (or products).

[Hanting Zhang]

It's basically a huge mess:

∑ (xbar : quotient (setoid.ker card)) in image quotient.mk (range n).powerset,
∑ (y : finset ℕ) in filter (λ (y : finset ℕ), ⟦y⟧ = xbar) (range n).powerset,
(∏ (a : ℕ) in y, -↑(r a)) * ∏ (a : ℕ) in range n \ y, (λ (i : ℕ), X) a =
∑ (k : ℕ) in range (n + 1), (∑ (A : finset ℕ) in powerset_len (n - k) (range (n + 1)), ∏ (j : ℕ) in A, ↑(r j)) * X ^ k

[Yakov Pechersky]

I would make sure the statement is in a form that is true for the base case first, and show you can prove that.

[Yakov Pechersky]

The correct statement should be provable with something very close to simp [powerset_len]

[Eric Wieser]

I did some stuff with sums over quotients in #5269, although I think the trick required me to massage both sides to the same summand (and is still a massive mess)