mv_polynomial induction on variables

Stream: maths

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Johan Commelin]

@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.

[Alex J. Best]

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

[Alex J. Best]

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

[Alex J. Best]

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

[Patrick Massot]

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

[Eric Wieser]

is by resetI; exact the same as by exactI?

[Eric Wieser]

#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

[Johan Commelin]

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

[Eric Wieser]

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

[Eric Wieser]

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)

[Johan Commelin]

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

[Johan Commelin]

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

[Aaron Anderson]

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.

[Aaron Anderson]

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

[Johan Commelin]

There are some highly nonconstructive steps in this induction method.

[Johan Commelin]

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.

[Aaron Anderson]

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?

[Mario Carneiro]

why would you want to?

[Mario Carneiro]

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

[Mario Carneiro]

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