Zulip Chat Archive

Stream: new members

Topic: Natural embedding of quotients


Hanting Zhang (Jan 06 2021 at 23:02):

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 (Jan 06 2021 at 23:20):

Can you provide a #mwe ?

Adam Topaz (Jan 06 2021 at 23:21):

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

Hanting Zhang (Jan 06 2021 at 23:23):

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 (Jan 06 2021 at 23:25):

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 (Jan 06 2021 at 23:28):

Is this true for n = 0?

Yakov Pechersky (Jan 06 2021 at 23:28):

Doesn't seem like it.

Yakov Pechersky (Jan 06 2021 at 23:32):

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

Hanting Zhang (Jan 06 2021 at 23:42):

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

Hanting Zhang (Jan 06 2021 at 23:43):

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

Yakov Pechersky (Jan 06 2021 at 23:44):

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

Yakov Pechersky (Jan 06 2021 at 23:46):

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

Eric Wieser (Jan 06 2021 at 23:46):

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

Eric Wieser (Jan 06 2021 at 23:47):

What's the goal state at the sorry?

Yakov Pechersky (Jan 06 2021 at 23:47):

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 (Jan 06 2021 at 23:48):

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 (Jan 06 2021 at 23:49):

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 (Jan 06 2021 at 23:49):

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

Eric Wieser (Jan 06 2021 at 23:51):

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)


Last updated: Dec 20 2023 at 11:08 UTC