Zulip Chat Archive

Stream: maths

Topic: mv_polynomial induction on variables


view this post on Zulip Aaron Anderson (Nov 12 2020 at 17:56):

There are a few proofs in ring_theory.polynomial.basic that follow the same general path through several lemmas

view this post on Zulip Aaron Anderson (Nov 12 2020 at 17:56):

Proving that a property is invariant under ring isos, and then proving that P R -> P (polynomial R)

view this post on Zulip Aaron Anderson (Nov 12 2020 at 17:57):

and then concluding that P R → P (mv_polynomial σ R) given fintype σ.

view this post on Zulip Aaron Anderson (Nov 12 2020 at 17:58):

Is there a way that we can generalize this into a single lemma, to use on the remaining properties of that sort?

view this post on Zulip Johan Commelin (Nov 13 2020 at 06:50):

@Aaron Anderson Good question, I've also been thinking about this (but not for very long). We would want some sort of mv_polynomial.induction_on_vars or something like that. I haven't tried actually implementing it.

view this post on Zulip Alex J. Best (Nov 13 2020 at 08:12):

I also thought about this once but never tried, I just had a go and ended up with

open polynomial
open mv_polynomial
lemma aa {R0 : Type} {σ : Type} [fintype σ] [comm_ring R0] (P : Π (R) [comm_ring R], Prop)
  (hp :  {R S} [comm_ring R] [comm_ring S], by resetI; exact S ≃+* R  P R  P S )
  (h :  (R) [h : comm_ring R], @P R h  P (by resetI; exact polynomial R)) (hR0 : P R0) :
  P (mv_polynomial σ R0) :=
begin
  apply hp (ring_equiv_of_equiv R0 (fintype.equiv_fin σ).out),
  induction fintype.card σ,
  { apply hp (ring_equiv_of_equiv R0 fin_zero_equiv'),
    apply hp (pempty_ring_equiv R0),
    exact hR0, },
  { apply hp (mv_polynomial.fin_succ_equiv R0 n),
    apply h,
    exact ih, }
end

view this post on Zulip Alex J. Best (Nov 13 2020 at 08:28):

yeah its kinda janky with the universe levels and typeclasses lol but it semi works

instance is_noetherian_ring' (R :Type) [comm_ring R] {σ : Type} [fintype σ] [h : is_noetherian_ring R] :
  is_noetherian_ring (mv_polynomial σ R) :=
begin
  convert aa _ _ _ _,
  swap,
  { intros, resetI,
    exact is_noetherian_ring R_1, },
  swap,
  exact σ,
  swap,
  exact R,
  simp,
  apply_instance,
  exact h,
  { simp,
  intros _  _ _ _ f hh, resetI, exact is_noetherian_ring_of_ring_equiv _ f.symm, },
  simp,
  intros,
  resetI,
  exact polynomial.is_noetherian_ring,
end

view this post on Zulip Alex J. Best (Nov 13 2020 at 08:32):

It gets a bit nicer if I leave R0 and sigma explicit

view this post on Zulip Patrick Massot (Nov 13 2020 at 11:11):

These by resetI; exact S ≃+* R → P R → P S really don't look nice. We should at least encapsulate them into some definition.

view this post on Zulip Eric Wieser (Nov 13 2020 at 13:17):

is by resetI; exact the same as by exactI?

view this post on Zulip Eric Wieser (Nov 13 2020 at 14:06):

#mwe version of @Alex J. Best's lemma (complete with exactI:

import data.mv_polynomial.equiv
import data.mv_polynomial

open polynomial
open mv_polynomial

open_locale classical

lemma aa {R0 : Type} {σ : Type} [fintype σ] [comm_ring R0] (P : Π (R) [comm_ring R], Prop)
  (hp :  {R S} [comm_ring R] [comm_ring S], by exactI S ≃+* R  P R  P S)
  (h :  (R) [comm_ring R], by exactI P R  P (polynomial R)) (hR0 : P R0) :
  P (mv_polynomial σ R0) :=
begin
  apply hp (ring_equiv_of_equiv R0 (fintype.equiv_fin σ).out),
  induction fintype.card σ,
  { apply hp (ring_equiv_of_equiv R0 fin_zero_equiv'),
    apply hp (pempty_ring_equiv R0),
    exact hR0, },
  { apply hp (mv_polynomial.fin_succ_equiv R0 n),
    apply h,
    exact ih, }
end

view this post on Zulip Johan Commelin (Nov 13 2020 at 15:32):

I think we should refactor some of the proofs in mathlib to use this lemma.

view this post on Zulip Eric Wieser (Nov 13 2020 at 15:39):

It seems to me that the input hypotheses to the lemma are overly general

view this post on Zulip Eric Wieser (Nov 13 2020 at 15:43):

Using (hp : ∀ {R S} [comm_ring R], by exactI mv_polynomial S R0 ≃+* R → P R → P (mv_polynomial S R0)) is a little more constrained (replacing S with mv_polynomial S R0)

view this post on Zulip Johan Commelin (Nov 13 2020 at 15:46):

True, but I can't think of an application where this difference matters.

view this post on Zulip Johan Commelin (Nov 13 2020 at 15:47):

We want to apply it to P that are isom-invariant. And proving the isom-invariance is usually "trivial".

view this post on Zulip Aaron Anderson (Nov 13 2020 at 17:24):

FWIW, this should be able to refactor the proofs for is_integral_domain, is_noetherian_ring, and is_jacobson, and then quickly provide proofs for unique_factorization_monoid, and given a version with data, gcd_monoid.

view this post on Zulip Aaron Anderson (Nov 13 2020 at 17:27):

I don't think the version with data will be very simple or necessarily similar...

view this post on Zulip Johan Commelin (Nov 13 2020 at 18:04):

There are some highly nonconstructive steps in this induction method.

view this post on Zulip Johan Commelin (Nov 13 2020 at 18:05):

But if there were a gcd_monoid.copy, then we could at least use this method to get all the proofs. Might still be useful.

view this post on Zulip Aaron Anderson (Nov 22 2020 at 04:54):

Eric Wieser said:

#mwe version of Alex J. Best's lemma (complete with exactI:

import data.mv_polynomial.equiv
import data.mv_polynomial

open polynomial
open mv_polynomial

open_locale classical

lemma aa {R0 : Type} {σ : Type} [fintype σ] [comm_ring R0] (P : Π (R) [comm_ring R], Prop)
  (hp :  {R S} [comm_ring R] [comm_ring S], by exactI S ≃+* R  P R  P S)
  (h :  (R) [comm_ring R], by exactI P R  P (polynomial R)) (hR0 : P R0) :
  P (mv_polynomial σ R0) :=
begin
  apply hp (ring_equiv_of_equiv R0 (fintype.equiv_fin σ).out),
  induction fintype.card σ,
  { apply hp (ring_equiv_of_equiv R0 fin_zero_equiv'),
    apply hp (pempty_ring_equiv R0),
    exact hR0, },
  { apply hp (mv_polynomial.fin_succ_equiv R0 n),
    apply h,
    exact ih, }
end

Is there any way to make this work for different universes?

view this post on Zulip Mario Carneiro (Nov 22 2020 at 05:10):

why would you want to?

view this post on Zulip Mario Carneiro (Nov 22 2020 at 05:10):

all the hypotheses can be in the same universe as the inputs

view this post on Zulip Mario Carneiro (Nov 22 2020 at 05:38):

lemma aa {R0 : Type u} {σ : Type v} [fintype σ] [comm_ring R0]
  (P : Π (R : Type u) [comm_ring R], Prop)
  (Q : Π (R : Type (max u v)) [comm_ring R], Prop)
  (hp :  {R S} [comm_ring R] [comm_ring S], by exactI S ≃+* R  P R  P S)
  (hq :  {R S} [comm_ring R] [comm_ring S], by exactI S ≃+* R  P R  Q S)
  (h :  (R : Type u) [comm_ring R], by exactI P R  P (polynomial R)) (hR0 : P R0) :
  Q (mv_polynomial σ R0) :=
begin
  apply hq (ring_equiv_of_equiv R0 (fintype.equiv_fin σ).out),
  induction fintype.card σ,
  { apply hp ((ring_equiv_of_equiv R0 fin_zero_equiv').trans (pempty_ring_equiv R0)),
    exact hR0, },
  { apply hp (mv_polynomial.fin_succ_equiv R0 n),
    apply h,
    exact ih, }
end

Last updated: May 14 2021 at 19:21 UTC