## Stream: maths

### Topic: mv_polynomial induction on variables

#### 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

#### 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)

#### Aaron Anderson (Nov 12 2020 at 17:57):

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

#### 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?

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

#### Alex J. Best (Nov 13 2020 at 08:12):

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 (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


#### Alex J. Best (Nov 13 2020 at 08:32):

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

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

#### Eric Wieser (Nov 13 2020 at 13:17):

is by resetI; exact the same as by exactI?

#### 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


#### Johan Commelin (Nov 13 2020 at 15:32):

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

#### Eric Wieser (Nov 13 2020 at 15:39):

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

#### 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)

#### Johan Commelin (Nov 13 2020 at 15:46):

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

#### 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".

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

#### Aaron Anderson (Nov 13 2020 at 17:27):

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

#### Johan Commelin (Nov 13 2020 at 18:04):

There are some highly nonconstructive steps in this induction method.

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

#### 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?

#### Mario Carneiro (Nov 22 2020 at 05:10):

why would you want to?

#### Mario Carneiro (Nov 22 2020 at 05:10):

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

#### 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