# Zulip Chat Archive

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

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