# Zulip Chat Archive

## Stream: maths

### Topic: Algebraic geometry course

#### Kevin Buzzard (Jan 13 2020 at 10:39):

I'm starting my algebraic geometry course today, M4P33. Here are my notes for lecture 1. Any comments welcome. The lecture is 4-5 in London, I'll use Lean on my laptop at some point and I'll leave Zulip on so that if anyone posts in this thread it'll flash up on the screen lol

#### Kevin Buzzard (Jan 13 2020 at 10:40):

Will tidy it up later but need to do 100 other things first

#### Johan Commelin (Jan 13 2020 at 10:56):

Good luck!

#### Johan Commelin (Jan 13 2020 at 18:31):

@Kevin Buzzard How did the first lecture go?

#### Kevin Buzzard (Jan 13 2020 at 20:20):

Well I started late because something else over-ran beforehand, but it seemed to go fine. We talked about the union of two algebraic sets being an algebraic set.

#### Kevin Buzzard (Jan 14 2020 at 10:01):

I'm going to be formalising the proof of the Nullstellensatz in my course soon. Do we already have this in Lean?

#### Johan Commelin (Jan 14 2020 at 10:05):

I think @Lennard Henze was working on this

#### Johan Commelin (Jan 14 2020 at 10:05):

How are things going, Lennard?

#### Johan Commelin (Jan 14 2020 at 11:50):

@Kevin Buzzard Did you show those 4th year students Lean during the lecture? If so, how did they react?

#### Kevin Buzzard (Jan 14 2020 at 11:57):

It was a bit hectic :-) because I've got so much to do and had no real time to think about how to explain the Lean. It's in a better state now.

#### Agnishom Chattopadhyay (Jan 14 2020 at 14:03):

Naive Question: This does not begin with the definition of affine algebraic sets. If that was not taught in Lecture 1 of Algebraic Geometry, in which course was it taught?

#### Johan Commelin (Jan 14 2020 at 14:04):

Probably commutative algebra

#### Kevin Buzzard (Jan 14 2020 at 14:57):

We're following these notes by Martin Orr.

#### Kevin Buzzard (Jan 14 2020 at 14:58):

The definition is in there, except I have removed what I believe to be an unnecessary finiteness assumption.

#### Lennard Henze (Jan 14 2020 at 15:17):

Yes I was working on that, but I discontinued my work because I was overwhelmed by the task. My work so far can be found here https://github.com/Forsetes/mathlib/blob/hilberts_nullstellensatz/src/ring_theory/noether_normalization.lean

#### Kevin Buzzard (Jan 17 2020 at 10:39):

Lecture 3 of my course. Can *anyone* tell me how to get rid of those bloody `P`

s everywhere?

#### Mario Carneiro (Jan 17 2020 at 11:01):

Use parameters

#### Mario Carneiro (Jan 17 2020 at 11:02):

Alternatively, bake the application of `P`

into the notations for V and I as in Sebastian's comment

#### Kevin Buzzard (Jan 17 2020 at 11:10):

What automation does these proofs? Is there a good name for V and I? For all I know they are both `comp.left_distrib`

#### Kevin Buzzard (Jan 17 2020 at 11:11):

@Patrick Massot how close am I to getting lecture 3 into a beautiful html file?

#### Kevin Buzzard (Jan 17 2020 at 11:14):

@Mario Carneiro I thought notation didn't work with variables?

#### Mario Carneiro (Jan 17 2020 at 11:17):

I don't know any relevant automation for the last proof, but it is what I would call a one-liner

#### Mario Carneiro (Jan 17 2020 at 11:18):

You have a lot of `??`

in the proof, did you want to ask a question about it?

#### Mario Carneiro (Jan 17 2020 at 11:19):

I don't often put free variables in notations because it's confusing, but I think Sebastian's idea will work

#### Kevin Buzzard (Jan 17 2020 at 11:25):

I cut and pasted one proof and then started switching V's to I's, and then it compiled before I had finished :-)

#### Kevin Buzzard (Jan 17 2020 at 11:26):

I don't often put free variables in notations because it's confusing, but I think Sebastian's idea will work

What is Sebastian's idea?

#### Mario Carneiro (Jan 17 2020 at 11:27):

Hm, I had to mess with it a bit, but with this preamble you can replace each `π P`

with `π`

and similarly for `π`

:

variable {R : Type u} variable {W : Type v} variable (P : R β W β Prop) include P def π_ (S : set R) : set W := {x : W | β f β S, P f x} notation `π`:max := π_ (by exact P) def π_ (X : set W) : set R := {f : R | β x β X, P f x} notation `π`:max := π_ (by exact P)

#### Mario Carneiro (Jan 17 2020 at 11:30):

It also works, without the notation, if you just change all the variables to parameters

#### Mario Carneiro (Jan 17 2020 at 11:32):

Oh I see, your proof of `πππ_eq_π`

goes through because lean noticed that if it substitutes `X`

for `S`

and vice versa then `V`

becomes `I`

and vice versa... so `πππ_eq_π`

and `πππ_eq_π`

are actually the same proof

#### Mario Carneiro (Jan 17 2020 at 11:32):

See?

lemma πππ_eq_π (V : set W) : (π (π (π V))) = π V := πππ_eq_π _ _

#### Mario Carneiro (Jan 17 2020 at 11:33):

If you use parameters, this trick doesn't work

#### Patrick Massot (Jan 17 2020 at 11:55):

Patrick Massot how close am I to getting lecture 3 into a beautiful html file?

What do you want the html file to look like? Are you aiming for something as on the mathlib website or something as in my lecture notes?

#### Kevin Buzzard (Jan 17 2020 at 13:11):

Something I could slap up before the end of this lecture at 1:50pm

#### Kevin Buzzard (Jan 17 2020 at 13:11):

which I'm currently giving

#### Kevin Buzzard (Jan 17 2020 at 17:17):

do we not have nilradical in Lean?

#### Alex J. Best (Jan 17 2020 at 17:20):

Nope!

#### Alex J. Best (Jan 17 2020 at 17:22):

Or nilpotents etc. I added some bits at https://github.com/leanprover-community/mathlib/blob/ece70146a142c8b04563c21edb34c87d192b172b/src/ring_theory/dedekind_finite.lean but its almost nothing

#### Kevin Buzzard (Jan 17 2020 at 18:07):

Today my main achievement was that I managed to reproduce the proof which I knew as a kid of something which I knew couldn't possibly be the Nullstellensatz:

I managed to abstract out all of the algebraic geometry completely :D I only import data.set.basic (although there's a joke at the top of the file)

#### Kevin Buzzard (Jan 17 2020 at 18:44):

If you use parameters, this trick doesn't work

Right, because P needs to be reversed.

#### Kevin Buzzard (Jan 17 2020 at 18:46):

def π_ (S : set R) : set W := {x : W | β f β S, P f x} notation `π`:max := π_ (by exact P)

This hack enables me to state theorems the way mathematicians would expect to see them, but when I'm working on proofs I still see the `P`

in the tactic state. Is there any way to get rid of this?

#### Kevin Buzzard (Jan 17 2020 at 21:05):

Is there a one-line tactic which solves this sort of thing:

import data.set.lattice open set example (R : Type*) (A : Type*) (P : R β A β Prop) (ΞΉ : Type*) (S : ΞΉ β set R) (x : A) : (β (f : R), (f β β (i : ΞΉ), S i) β P f x) β β (i : ΞΉ) (f : R), f β S i β P f x := begin split, intros, apply a, rw mem_Union, use i, assumption, intros h f hf, rw mem_Union at hf, cases hf with i hi, apply h i, assumption, end

I really feel like I'm following my nose at all points and so am hoping this is just the sort of thing that CS people have tacticised

#### Chris Hughes (Jan 17 2020 at 21:08):

`simp, tauto`

#### Kevin Buzzard (Jan 17 2020 at 21:47):

Do we have this:

/-- Over an infinite integral domain a polynomial f is zero iff it evaluates to zero everywhere -/ lemma mv_polynomial.eval_eq_zero {k : Type*} [integral_domain k] [infinite k] {n : Type*} {f : mv_polynomial n k} : (β x, eval x f = 0) β f = 0 := begin sorry end

? I think you can prove it in the case when n is finite, by induction on the size of n, and then for general n you write the polynomial ring as a filtered colimit of finite n's.

I would like to prove this myself, if it's not there, but I suspect there might be some quite high-powered ways to do this. For example I don't know whether I'm supposed to be reducing to the case of `n = fin m`

or `n : fintype`

or what. The reduction needs the concept of the variables which appear in f, which might be some sort of monad bind thing?

#### Kevin Buzzard (Jan 17 2020 at 21:48):

@Alexander Uhlmann isolated this property at Xena yesterday.

#### Jesse Michael Han (Jan 18 2020 at 06:33):

`simp, tauto`

i was surprised `finish`

couldn't do it alone, you have to spoon-feed it:

import data.set.lattice open set example (R : Type*) (A : Type*) (P : R β A β Prop) (ΞΉ : Type*) (S : ΞΉ β set R) (x : A) : (β (f : R), (f β β (i : ΞΉ), S i) β P f x) β β (i : ΞΉ) (f : R), f β S i β P f x := by finish[iff_iff_implies_and_implies]

#### Kevin Buzzard (Jan 18 2020 at 11:52):

Urs Schreiber pointed me to this nLab page on Twitter. Does anyone have a clue what is going on here?

#### Johan Commelin (Jan 18 2020 at 14:24):

@Kevin Buzzard I've no idea what's going on there, but I do know that it is completely useless for our purposes. We're miles away from cohesive sheaf toposes.

#### Johan Commelin (Jan 18 2020 at 21:57):

@Kevin Buzzard I want to go to bed, so I'm just dumping what I hacked together:

import data.mv_polynomial noncomputable theory open_locale classical open mv_polynomial polynomial /-- Over an infinite integral domain a polynomial f is zero if it evaluates to zero everywhere -/ lemma polynomial.eval_eq_zero {k : Type*} [integral_domain k] [infinite k] {f : polynomial k} (H : β x, eval x f = 0) : f = 0 := begin rcases infinite.exists_not_mem_finset (roots f) with β¨x, hxβ©, contrapose! hx with hf, rw mem_roots hf, apply H, end /-- Over an infinite integral domain a polynomial f is zero iff it evaluates to zero everywhere -/ lemma polynomial.eval_eq_zero_iff {k : Type*} [integral_domain k] [infinite k] {f : polynomial k} : (β x, eval x f = 0) β f = 0 := β¨polynomial.eval_eq_zero, by { rintro rfl x, exact rfl }β© def fin.equiv_empty : fin 0 β empty := { to_fun := Ξ» i, false.elim $ nat.not_lt_zero _ i.2, inv_fun := empty.elim, left_inv := Ξ» i, false.elim $ nat.not_lt_zero _ i.2, right_inv := Ξ» x, x.elim } def fin.equiv_pempty : fin 0 β pempty := { to_fun := Ξ» i, false.elim $ nat.not_lt_zero _ i.2, inv_fun := pempty.elim, left_inv := Ξ» i, false.elim $ nat.not_lt_zero _ i.2, right_inv := Ξ» x, x.elim } @[simp] lemma mv_polynomial.eval_rename {k : Type*} [comm_semiring k] {m : Type*} {n : Type*} (e : m β n) (f : mv_polynomial m k) (x) : eval x (rename e f) = eval (x β e) f := by apply f.induction_on; { intros, simp * } lemma mv_polynomial.equiv_eval_eq_zero {k : Type*} [comm_semiring k] {m : Type*} {n : Type*} (e : m β n) (H : (β f : mv_polynomial m k, (β x, eval x f = 0) β f = 0)) (f : mv_polynomial n k) (hf : β x, eval x f = 0) : f = 0 := begin let Ο := ring_equiv_of_equiv k e, suffices h : Ο.symm f = 0, { simpa using congr_arg Ο h }, apply H, intro x, show eval x (rename e.symm f) = 0, simp [hf], end universe variables u v def equiv.option {X : Type u} {Y : Type v} (e : X β Y) : option X β option Y := { to_fun := option.map e, inv_fun := option.map e.symm, left_inv := Ξ» x, by { cases x, refl, simp }, right_inv := Ξ» x, by { cases x, refl, simp } } def fin_succ_equiv_option (n : β) : fin (n+1) β option (fin n) := sorry set_option pp.universes true lemma fintype.induction {P : Ξ (X : Type*) [fintype X], Prop} (h0 : P pempty) (hs : β (X : Type*) [fintype X], P X β P (option X)) (he : β {X Y : Type*} [fintype X] [fintype Y] (e : X β Y), P X β P Y) (X : Type*) [fintype X] : P X := begin rcases fintype.exists_equiv_fin X with β¨n, β¨eβ©β©, apply he (equiv.ulift.trans e.symm), clear e, induction n with n ih, { exact he (equiv.ulift.trans fin.equiv_pempty).symm h0 }, { specialize hs _ ih, apply he _ hs, refine (equiv.ulift.trans _).symm, refine (fin_succ_equiv_option n).trans _, refine equiv.ulift.option.symm } end /-- Over an infinite integral domain a polynomial f is zero if it evaluates to zero everywhere -/ lemma mv_polynomial.fin_eval_eq_zero {k : Type*} [int : integral_domain k] [inf : infinite k] {n : Type*} [fin : fintype n] : β {f : mv_polynomial n k}, (β x, eval x f = 0) β f = 0 := begin unfreezeI, revert inf int k, revert fin n, refine fintype.induction _ _ _, { intros k int inf f H, have h : (pempty_ring_equiv k) f = 0 := H _, replace h := congr_arg (pempty_ring_equiv k).symm h, rw [ring_equiv.symm_apply_apply] at h, convert h, symmetry, exact ring_equiv.map_zero _ }, { intros n _ ih k int inf f hf, let Ο := option_equiv_right k n, suffices h : Ο f = 0, { simpa using congr_arg Ο.symm h }, apply ih, { sorry }, { resetI, sorry } }, { intros m n _ _ e H k int inf f, apply mv_polynomial.equiv_eval_eq_zero e, apply @H } end /-- Over an infinite integral domain a polynomial f is zero iff it evaluates to zero everywhere -/ lemma mv_polynomial.eval_eq_zero_iff {k : Type*} [integral_domain k] [infinite k] {n : Type*} {f : mv_polynomial n k} : (β x, eval x f = 0) β f = 0 := begin sorry end

#### Johan Commelin (Jan 18 2020 at 21:57):

Could probably use some cleaning...

#### Kevin Buzzard (Jan 18 2020 at 22:59):

Thanks!

#### Kevin Buzzard (Jan 19 2020 at 17:18):

I'm reading proofs of the Nullstellensatz. Here is something which comes up more than once. Say $k$ is a field (probably a commutative semiring would work fine) and $R$ is a finitely-generated $k$-algebra: this means that $R$ is a ring which is isomorphic to a quotient of a polynomial ring `mv_polynomial X k`

with `X`

a fintype -- alternatively it means that there's a ring map $k\to R$ and there's some `Y : finset R`

such that the induced ring hom `mv_polynomial Y k -> R`

is surjective. Mathematicians would write $R=k[x_1,x_2,\ldots,x_n]$ and note that this is not a polynomial ring -- it's "the ring generated by $k$ and the set $\{x_1,x_2,\ldots,x_n\}$", so it's a quotient of a polynomial ring.

Now every text I've read just says "after re-ordering the $x_i$ we can find some $1\leq t\leq n$ such that the $x_i$ for $1\leq t\leq n$ are independent transcendentals over $k$, and the $x_j$ for $t+1\leq j\leq n$ are algebraic over $k(x_1,\ldots,x_t)$". As a mathematician this does indeed feel like a triviality. One sets $R_0=k$ (this ring will change but it will always be equipped with a map to $R$) and simply loops through the $x_i$ and does one of two things: if the map from $R_0[X]$ to $$R$ sending $X$ to $x_i$ is injective, then add $x_i$ to the "transcendental" pile and update $R_0$ to $R_0[x_i]$. If the map isn't injective, add $x_i$ to the "algebraic" pile. Then renumber the $t$ "transcendental" $x_i$ to be the first few $x_i$ and renumber the "algebraic" $x_i$ to be the rest.

How do I do this in Lean? My algorithm above feels very natural to code in an imperative language. Because $R_0$ changes one has to think a little carefully about doing this in a functional language. I guess I'm just showing that I never learnt functional programming properly.

Of course a lot of the ring theory above is of no relevance; what is really happening, I guess, is that I have a list `[x1,x2,...,xn]`

and I want to break it into two sublists, the "in" ones and the "out" ones, but the predicate of whether you're "in" or not depends on what has happened so far. I have no doubt that this set-up is very well-understood, but not by me. I am a bit scared that if I hack my way through this then I will end up with something awful.

Reference: I am reading "A note on Zariski's Lemma" by J. McCabe (AMM Vol 83 number 7, 1976). This proof seems to me to be easiest to formalise, out of the ones I have seen.

#### Reid Barton (Jan 19 2020 at 18:13):

It might be most natural to do this by induction

#### Koundinya Vajjha (Jan 19 2020 at 18:45):

Tangential remark: @Kevin Buzzard have you also seen Munshi's proof of the Nullstellensatz?

#### Kevin Buzzard (Jan 19 2020 at 18:58):

I hadn't -- many thanks!

#### Kevin Buzzard (Jan 19 2020 at 18:59):

It might be most natural to do this by induction

Oh -- not induction on the size, but on the finset itself? Maybe!

#### Kevin Buzzard (Jan 20 2020 at 23:32):

@Johan Commelin @Yury G. Kudryashov @Chris Hughes is there some less painless way to make an interface for `mv_polynomial.iter_to_sum`

than this?

import data.mv_polynomial lemma sum.rec_comp_left (X : Type*) (Y : Type*) (Ξ² : Type*) (Ξ³ : Type*) (i : Ξ² β X) (j : Ξ³ β X) (f : X β Y) (x : Ξ² β Ξ³) : f (sum.rec i j x) = sum.rec (f β i) (f β j) x := by cases x; refl namespace mv_polynomial theorem evalβ_evalβ (R : Type*) [comm_semiring R] (Ξ² : Type*) (Ξ³ : Type*) (S : Type*) [comm_semiring S] (f : R β S) [is_semiring_hom f] (i : Ξ² β S) (j : Ξ³ β S) (p : mv_polynomial Ξ² (mv_polynomial Ξ³ R)) : evalβ (evalβ f j) i p = eval i (map (evalβ f j) p) := hom_eq_hom _ _ (by apply_instance) (by apply_instance) (Ξ» _, by rw [evalβ_C, map_C, eval_C]) (Ξ» _, by rw [evalβ_X, map_X, eval_X]) p set_option class.instance_max_depth 100 theorem map_evalβ' {R : Type*} [comm_semiring R] {Ξ² : Type*} {Ξ³ : Type*} {S : Type*} [comm_semiring S] {f : R β S} [is_semiring_hom f] {j : Ξ³ β S} {p : mv_polynomial Ξ² (mv_polynomial Ξ³ R)} : map (evalβ f j) p = evalβ (C β f) (Ξ» n, sum.rec X (C β j) n) (iter_to_sum _ _ _ p) := begin rw iter_to_sum, rw evalβ_evalβ, rw βevalβ_eq_eval_map, apply hom_eq_hom, apply_instance, apply_instance, { intro b, simp, suffices : (C (evalβ f j b) : mv_polynomial Ξ² S) = evalβ (C β f) (Ξ» n, sum.rec X (C β j) n) (evalβ C (X β sum.inr) b), simpa using this, rw βrename, rw evalβ_rename, rw [show ((Ξ» (n : Ξ² β Ξ³), sum.rec X (C β j) n) β sum.inr : Ξ³ β mv_polynomial Ξ² S) = C β j, by funext b; refl], apply evalβ_comp_left}, { intro b, simp}, end theorem evalβ_evalβ' (R : Type*) [comm_semiring R] (Ξ² : Type*) (Ξ³ : Type*) (S : Type*) [comm_semiring S] (f : R β S) [is_semiring_hom f] (i : Ξ² β S) (j : Ξ³ β S) (p : mv_polynomial Ξ² (mv_polynomial Ξ³ R)) : evalβ (evalβ f j) i p = evalβ f (Ξ» n, sum.rec i j n) (iter_to_sum _ _ _ p) := begin rw evalβ_evalβ, rw map_evalβ', generalize : iter_to_sum _ _ _ p = p', apply hom_eq_hom _ _ _ _ _ _ p', apply_instance, apply_instance, apply_instance, { intro r, rw [evalβ_C, evalβ_C, eval_C]}, { rintro (b | c), { simp}, { simp}, } end end mv_polynomial

#### Kevin Buzzard (Jan 20 2020 at 23:35):

I am trying to use multivariate polynomials to do things in MSc level commutative algebra and it's very interesting but I am also extremely slow.

#### Johan Commelin (Jan 21 2020 at 08:32):

All the different ways of composing evaluation of polynomials is quite brittle in my experience. Lean of gets stuck on elaborating concise statements, and there are many holes in the library. This is one reason why I'm in favour of @Yury G. Kudryashov proposal to ditch `eval2`

(even though I may have been the one asking to introduce it), and only have `map`

and `eval`

. Because it significantly reduces the amount of library interface that one has to develop and maintain. Nevertheless it is frustrating that many statements about plugging polynomials into polynomials that look trivial in informal math (after years of usage, I agree) become pretty unreadable in Lean. To the point that I no longer understand the code that I wrote 25 seconds ago...

(End of rant :oops:)

#### Mario Carneiro (Jan 21 2020 at 08:47):

I don't think eval2 needs to be ditched, because it can be used to define the other two, but I'm fine with having only the basic theorems about it with everything else in `map`

and `eval`

#### Johan Commelin (Jan 21 2020 at 08:52):

Does that mean that users should avoid it?

#### Johan Commelin (Jan 21 2020 at 08:53):

Also, for `eval2`

you need ring structure and a ring hom, etc. `map`

could be defined coefficient-wise which avoids some tc search that has failed me several times.

#### Patrick Massot (Jan 21 2020 at 08:54):

Johan and Mario, isn't 3am where you are?

#### Johan Commelin (Jan 21 2020 at 08:56):

In a very small neighbourhood around me, it is 09:55. But I can't globalise that property (-;

#### Johan Commelin (Jan 21 2020 at 08:56):

I will need to kill 3 more hours before I'm allowed to break my fast

#### Patrick Massot (Jan 21 2020 at 08:59):

I see.

#### Yury G. Kudryashov (Jan 21 2020 at 16:05):

My proposal was to use aeval, not just ditch eval2.

#### Chris Hughes (Jan 21 2020 at 18:51):

Do we need `bind`

for polynomials?

#### Johan Commelin (Jan 21 2020 at 20:01):

what would that look like?

#### Chris Hughes (Jan 21 2020 at 20:18):

```
bind (f : A - > polynomial B) (p : polynomial A) : polynomial B :=
p.eval2 f X
```

I think. It's the canonical map with that type.

#### Johan Commelin (Jan 21 2020 at 20:20):

Ooh right, it's one of those things that rolls out of an adjunction

#### Chris Hughes (Jan 21 2020 at 20:24):

I don't actually think it's that useful. I remember these things requiring a surprising amount of thought to prove. Stuff like with M:L:K, then if a polynomial in K has a root in L it has a root in M.

#### Johan Commelin (Jan 21 2020 at 20:26):

Right, that's exactly the kind of trivialities that are extremely hard to prove in the current library.

#### Chris Hughes (Jan 21 2020 at 20:26):

I do remember something that looked a bit like bind popping up recently.

#### Patrick Massot (Jan 21 2020 at 20:39):

I remember Cyril explaining in Amsterdam that you should always use polynomials with coefficients a priori in the biggest field that could show up, with a predicate saying it actually has coefficients in a smaller field.

#### Kevin Buzzard (Jan 21 2020 at 21:29):

I can't do that in my application, because I am doing $k[X_1,X_2,\ldots,X_n]$ with $k$ an arbitrary algebraically closed field.

#### Johan Commelin (Jan 22 2020 at 00:26):

@Sebastian Ullrich You see what Kevin did there? You added `^n`

notation to Lean 4, and now he's using $X_n$... in a subscript...

#### Kevin Buzzard (Jan 22 2020 at 00:27):

and $X_{ijk}$ right?

#### Johan Commelin (Jan 22 2020 at 01:24):

My proposal was to use aeval, not just ditch eval2.

@Yury G. Kudryashov I like that idea. We only want `eval2`

for algebras. For all the others, I guess a combo of `map`

and `eval`

is quite sufficient. And I would prefer a `map`

that doesn't depend on ring hom conditions.

#### Yury G. Kudryashov (Jan 22 2020 at 02:09):

@Johan Commelin The whole proposal is here: #1864. Comments are welcome. Volunteers to actually implement this are more than welcome.

#### Kevin Buzzard (Jan 22 2020 at 22:27):

I am finding the following "trivialities"

import data.mv_polynomial #check mv_polynomial.option_equiv_right -- mv_polynomial (option Ξ²) Ξ± β+* mv_polynomial Ξ² (polynomial Ξ±) #print mv_polynomial.option_equiv_right /- it's built from . mv_polynomial.ring_equiv_of_equiv . mv_polynomial.sum_ring_equiv . mv_polynomial.ring_equiv_congr glued together with . ring_equiv.trans -/ open mv_polynomial example (k : Type*) [comm_semiring k] (n : Type*) (g : n β polynomial k) (a : k) : polynomial.eval a (eval g ((option_equiv_right k n) (X none))) = a := sorry example (k : Type*) [comm_semiring k] (n : Type*) (g : n β polynomial k) (i : n) : eval g ((option_equiv_right k n) (X (some i))) = g i := sorry

very painful. What should I be doing here?

#### Kevin Buzzard (Jan 22 2020 at 22:40):

I think maybe this should be the first line?

example (k : Type*) [comm_semiring k] (n : Type*) (g : n β polynomial k) (a : k) : polynomial.eval a (eval g ((option_equiv_right k n) (X none))) = a := begin show polynomial.eval a (eval g ((( (@mv_polynomial.ring_equiv_congr (mv_polynomial unit k) n _ _ _ (mv_polynomial.punit_ring_equiv k)) β (mv_polynomial.sum_ring_equiv k n unit)) β (mv_polynomial.ring_equiv_of_equiv k (equiv.option_equiv_sum_punit n))) (X none))) = a, sorry end

#### Mario Carneiro (Jan 22 2020 at 22:43):

`option_equiv_right`

lacks definition lemmas

#### Kevin Buzzard (Jan 22 2020 at 22:44):

I see. So this first `show`

should be done with a `rw`

? And then after that there should be lemmas `eval_sum_ring_equiv_X`

and `eval_ring_equiv_congr_X`

and `eval_ring_equiv_of_equiv_X`

?

#### Kevin Buzzard (Jan 22 2020 at 22:46):

Should it be beta not alpha which is explicit in `mv_polynomial.ring_equiv_congr : Ξ (Ξ± : Type u_1) {Ξ² : Type u_2} {Ξ³ : Type u_1} [_inst_1 : comm_semiring Ξ±] [_inst_2 : comm_semiring Ξ³], Ξ± β+* Ξ³ β mv_polynomial Ξ² Ξ± β+* mv_polynomial Ξ² Ξ³`

?

#### Mario Carneiro (Jan 22 2020 at 22:47):

I think so

#### Mario Carneiro (Jan 22 2020 at 22:48):

I think the definitional lemmas should be stated using just application if possible, `eval`

is some derived thing (but it should probably also be available)

#### Mario Carneiro (Jan 22 2020 at 22:49):

Well, maybe not... I guess since it's a known ring hom you already have info on everything except what happens to constants and variables

#### Kevin Buzzard (Jan 22 2020 at 22:50):

there are lots of `blah_X`

and `blah_C`

lemmas

#### Kevin Buzzard (Jan 22 2020 at 22:50):

I am suggesting we add a few more ;-)

#### Mario Carneiro (Jan 22 2020 at 22:50):

I think you are right

#### Kevin Buzzard (Jan 22 2020 at 22:50):

I'm slowly getting the hang of this Lean malarkey

#### Mario Carneiro (Jan 22 2020 at 22:51):

I really hope it's a `rfl`

proof because there are a whole bunch of definitions in the way

#### Kevin Buzzard (Jan 22 2020 at 22:52):

I can iterate the `show, rw`

process ;-)

#### Mario Carneiro (Jan 22 2020 at 22:52):

I'm still not even sure what `option_equiv_right Ξ± Ξ² (X none) = _`

should complete to

#### Kevin Buzzard (Jan 22 2020 at 22:53):

you mean `option_equiv_right R n (X none) = _`

?

#### Mario Carneiro (Jan 22 2020 at 22:53):

I'm in the same context as the definition, they were called alpha and beta there

#### Kevin Buzzard (Jan 22 2020 at 22:53):

It's `C unit`

or `C punit`

or whatever

#### Kevin Buzzard (Jan 22 2020 at 22:54):

wait

#### Mario Carneiro (Jan 22 2020 at 22:54):

I think it's `C polynomial.X`

#### Kevin Buzzard (Jan 22 2020 at 22:54):

yeah, that :-)

#### Mario Carneiro (Jan 22 2020 at 22:54):

but lean times out when I write that

#### Mario Carneiro (Jan 22 2020 at 22:55):

oh, nvm

#### Mario Carneiro (Jan 22 2020 at 23:03):

theorem option_equiv_right_CX {Ξ± Ξ²} [comm_semiring Ξ±] : option_equiv_right Ξ± Ξ² (X none) = C polynomial.X := show map (evalβ polynomial.C (Ξ»u:punit, polynomial.X)) (sum_to_iter Ξ± Ξ² unit (rename (equiv.option_equiv_sum_punit._match_1 Ξ²) (X none))) = C polynomial.X, by simp [sum_to_iter_Xr]

`sum_to_iter_Xr`

should be a simp lemma

#### Kevin Buzzard (Jan 22 2020 at 23:04):

oh nice!

#### Mario Carneiro (Jan 22 2020 at 23:04):

also `punit_ring_equiv`

and like all the other involved functions should have definitional lemmas so I don't have to manually unfold them like this

#### Kevin Buzzard (Jan 22 2020 at 23:06):

To people not reading the details: what is happening here is that Lean has four(!) different ways of storing $R[X][n]$ where $X$ is one variable and $n$ is a set of variables; it's polynomials with coefficients in `option n`

, or in `n + punit`

, or polynomials in variables `n`

over base ring `R[X]`

, or polynomials in variables `n`

over polynomials in variables `punit`

#### Kevin Buzzard (Jan 22 2020 at 23:06):

Of course, all of these are the same, and humans find it extremely easy to switch between representations at the drop of a hat

#### Mario Carneiro (Jan 22 2020 at 23:09):

the other case is similar, luckily:

@[simp] theorem option_equiv_right_X_none {Ξ± Ξ²} [comm_semiring Ξ±] : option_equiv_right Ξ± Ξ² (X none) = C polynomial.X := show map (evalβ polynomial.C (Ξ»u:punit, polynomial.X)) (sum_to_iter Ξ± Ξ² unit (rename (equiv.option_equiv_sum_punit._match_1 Ξ²) (X none))) = C polynomial.X, by simp [sum_to_iter_Xr] @[simp] theorem option_equiv_right_X_some {Ξ± Ξ²} [comm_semiring Ξ±] (b : Ξ²) : option_equiv_right Ξ± Ξ² (X (some b)) = X b := show map (evalβ polynomial.C (Ξ»u:punit, polynomial.X)) (sum_to_iter Ξ± Ξ² unit (rename (equiv.option_equiv_sum_punit._match_1 Ξ²) (X (some b)))) = X b, by simp [sum_to_iter_Xl]

#### Mario Carneiro (Jan 22 2020 at 23:10):

@[simp] theorem option_equiv_right_C {Ξ± Ξ²} [comm_semiring Ξ±] (a : Ξ±) : option_equiv_right Ξ± Ξ² (C a) = C (polynomial.C a) := show map (evalβ polynomial.C (Ξ»u:punit, polynomial.X)) (sum_to_iter Ξ± Ξ² unit (rename (equiv.option_equiv_sum_punit._match_1 Ξ²) (C a))) = C (polynomial.C a), by simp [sum_to_iter_C]

#### Kevin Buzzard (Jan 22 2020 at 23:12):

So all three of the `sum_to_iter_?`

things should be simp lemmas?

#### Mario Carneiro (Jan 22 2020 at 23:12):

yes

#### Kevin Buzzard (Jan 22 2020 at 23:13):

Many thanks! And we can perhaps get rid of the `show`

lines by coming up with some other simp lemmas?

#### Kevin Buzzard (Jan 22 2020 at 23:13):

Or is this overoptimistic?

#### Mario Carneiro (Jan 22 2020 at 23:13):

I also brute forced my way through several other definitions here, that should have definitional lemmas: `ring_equiv_of_equiv`

, `option_equiv_sum_punit`

(the definition should not be simp), `sum_comm`

(ditto), `sum_ring_equiv`

, `punit_ring_equiv`

#### Mario Carneiro (Jan 22 2020 at 23:14):

Ideally this proof should be `dunfold option_equiv_right; simp`

#### Johan Commelin (Jan 23 2020 at 08:31):

Johan Commelin The whole proposal is here: #1864. Comments are welcome. Volunteers to actually implement this are more than welcome.

@Yury G. Kudryashov I didn't mean to imply that you and Mario should do all the work. (Sorry if it came across like that.) What I meant was that you seemed to have a pretty clear view of what you wanted as an end result. So I was inviting you and Mario to lead the discussion. Once it's clear what we want, I'm willing to write a bunch of code.

#### Kevin Buzzard (Jan 23 2020 at 14:35):

Do we not have this?

import data.mv_polynomial open mv_polynomial -- two evaluations of one mv_polynomial coincide, if the evaluation functions -- agree on the variables occurring in the polynomial example {R : Type*} [comm_semiring R] {S : Type*} [comm_semiring S] {n : Type*} (f g : n β S) (Ο : R β S) (p : mv_polynomial n R) (h : β i β vars p, f i = g i) : evalβ Ο f p = evalβ Ο g p := sorry

Johan -- I'm on a train, but thanks to Mario's heroic `simp`

efforts yesterday and your efforts from a few days ago, I now have a proof in the finite variable case.

#### Kevin Buzzard (Jan 23 2020 at 14:36):

The annoying thing about the example above is that so far I have never needed to penetrate the interface for `mv_polynomial`

, but now I am maybe going to have to think about how the type is implemented?

#### Johan Commelin (Jan 23 2020 at 14:39):

@Kevin Buzzard I guess we don't have this. Try

begin apply p.induction_on, all_goals {sorry} end

#### Kevin Buzzard (Jan 23 2020 at 14:40):

Nice idea!

#### Kevin Buzzard (Jan 23 2020 at 14:40):

I had just started with `unfold eval_2`

:-) That looked much worse :-)

#### Kevin Buzzard (Jan 23 2020 at 14:41):

So apparently I am crazy trying to prove this without assuming that $\phi$ is a ring hom? I'm not sure we need it...

#### Kevin Buzzard (Jan 23 2020 at 14:44):

aargh one of the goals is not true :-/

#### Johan Commelin (Jan 23 2020 at 14:46):

@Kevin Buzzard I'm quite sure that you need `Ο`

to be a ring hom

#### Johan Commelin (Jan 23 2020 at 14:47):

Ooh, no, you're right. You shouldn't (in theory).

#### Johan Commelin (Jan 23 2020 at 14:47):

@Kevin Buzzard Which goal is false?

#### Kevin Buzzard (Jan 23 2020 at 14:47):

Why? Not that it matters.

Induction fails because one of the goals is

p0 : mv_polynomial n R, i : n, hp : evalβ Ο f p0 = evalβ Ο g p0 β’ evalβ Ο f (p0 * X i) = evalβ Ο g (p0 * X i)

and my hypothesis is that f and g agree on the variables mentioned in p, but here p0 is arbitrary.

#### Kevin Buzzard (Jan 23 2020 at 14:48):

[sorry, on a train with sporadic connection]

#### Kevin Buzzard (Jan 23 2020 at 14:50):

In the library there is

lemma hom_eq_hom [semiring Ξ³] (f g : mv_polynomial Ο Ξ± β Ξ³) (hf : is_semiring_hom f) (hg : is_semiring_hom g) (hC : βa:Ξ±, f (C a) = g (C a)) (hX : βn:Ο, f (X n) = g (X n)) (p : mv_polynomial Ο Ξ±) : f p = g p := ...

but if the `p`

were before the `hX`

one could weaken `hX`

and only ask that the equality held for variables in the support (in the obvious sense) of p

#### Kevin Buzzard (Jan 23 2020 at 14:50):

I think I might have to modify the proof of `induction_on`

#### Johan Commelin (Jan 23 2020 at 14:52):

Aaah, I see.

#### Johan Commelin (Jan 23 2020 at 14:52):

Annoying

#### Kevin Buzzard (Jan 23 2020 at 14:52):

I'm going in...

#### Kevin Buzzard (Jan 23 2020 at 15:01):

aargh we don't even have this as far as I can see:

lemma vars_map {R : Type*} [comm_semiring R] {S : Type*} [comm_semiring S] {Ο : Type*} (Ο : R β S) [is_semiring_hom Ο] (p : mv_polynomial Ο R) : vars (map Ο p) β vars p :=

#### Kevin Buzzard (Jan 23 2020 at 15:33):

or this?

lemma mem_rename_range {R : Type*} [comm_semiring R] {Ο Ο : Type*} {g : Ο β Ο} (p : mv_polynomial Ο R) (h : (vars p).to_set β set.range g) : β q : mv_polynomial Ο R, rename g q = p := sorry

#### Kevin Buzzard (Jan 23 2020 at 16:01):

/me hopes @Chris Hughes is coming to Xena...

#### Kevin Buzzard (Jan 23 2020 at 18:39):

He was!

lemma evalβ_eq_of_eq_on_vars {R : Type*} [comm_semiring R] {S : Type*} [comm_semiring S] {Ο : Type*} (f g : Ο β S) (Ο : R β S) (p : mv_polynomial Ο R) [is_semiring_hom Ο] -- do we need this?? (h : β i β (p.support.bind finsupp.support), f i = g i) : evalβ Ο f p = evalβ Ο g p := begin unfold evalβ, unfold finsupp.sum finsupp.prod, refine finset.sum_congr rfl _, intros x hx, congr' 1, refine finset.prod_congr rfl _, intros i hi, simp only [finset.mem_bind, exists_imp_distrib] at h, have := h i x hx hi, rw this, end

#### Johan Commelin (Jan 23 2020 at 18:40):

Doesn't that mean you can remove those first two lines with `unfold`

s?

#### Kevin Buzzard (Jan 23 2020 at 18:41):

However he also says that the definition of `vars`

in `mv_polynomial`

should be what he wants it to be :P

#### Kevin Buzzard (Jan 23 2020 at 18:41):

oh we only just did it :-)

#### Kevin Buzzard (Jan 25 2020 at 14:56):

@Johan Commelin I finally did it. It's not mathlib-ready ;-)

#### Johan Commelin (Jan 25 2020 at 15:09):

Nice!

#### Yury G. Kudryashov (Jan 25 2020 at 18:42):

There are two steps mixed together in `mv_polynomial`

. Currently both are done using `finsupp`

but I think that this should be `mv_polynomial R Ξ± := monoid_algebra R (multiplicative $ free_comm_monoid Ξ±)`

. Here `free_comm_monoid Ξ±`

could be either `finsupp Ξ± nat`

or `multiset Ξ±`

. I think that we should have both `monoid_algebra`

and `free_comm_monoid`

, and most definitions / lemmas about polynomials should combine lemmas about these two. A big advantage of this approach is that it will make much easier to define, e.g., `R[x, y, xβ»ΒΉ, yβ»ΒΉ]`

as `monoid_algebra (free_comm_group Ξ±)`

, or quasipolynomials as the `monoid_algebra`

of the monoid `multiplicative (complex Γ nat)`

interpreted as $e^{at}t^n$. It might make sense to have `free_comm_monoid`

and `free_add_comm_monoid`

with one being `multiplicative`

or `additive of another.

#### Johan Commelin (Jan 25 2020 at 19:16):

Didn't Kenny already define `free_comm_monoid`

?

#### Yury G. Kudryashov (Jan 25 2020 at 19:26):

@Johan Commelin `git grep`

doesn't find it. Are you talking about some PR/WIP?

#### Chris Hughes (Jan 25 2020 at 19:28):

`free_comm_monoid`

is multiset.

#### Chris Hughes (Jan 25 2020 at 19:28):

Kenny did define `free_comm_group`

#### Johan Commelin (Jan 25 2020 at 19:40):

Aah, right

#### Kevin Buzzard (Jan 25 2020 at 20:58):

I am so confused by all of this. I thought the other day @Yury G. Kudryashov was saying "use dfinsupp not finsupp" and Chris was agreeing, and now he's saying "use monoid-algebra" and Chris is agreeing.

What is going on here? Is the idea that people are suggesting that the definition of `mv_polynomial`

be changed -- and are possibly suggesting more than one change? If this change is made, then someone has to rewrite the 1000+ line `mv_polynomial.lean`

with the new definition, I guess. I think that this would be an interesting exercise for someone like me. However I cannot begin to do it until someone formalises the definitions because I cannot see the difference between any of the definitions that people are suggesting -- they're all the same mathematically.

#### Chris Hughes (Jan 25 2020 at 20:59):

monoid algebra should be defined to be dfinsupp I think.

#### Kevin Buzzard (Jan 25 2020 at 21:04):

So currently it starts like this:

import algebra.ring import data.finsupp data.polynomial data.equiv.algebra noncomputable theory local attribute [instance, priority 100] classical.prop_decidable open set function finsupp lattice universes u v w x variables {Ξ± : Type u} {Ξ² : Type v} {Ξ³ : Type w} {Ξ΄ : Type x} /-- Multivariate polynomial, where `Ο` is the index set of the variables and `Ξ±` is the coefficient ring -/ def mv_polynomial (Ο : Type*) (Ξ± : Type*) [comm_semiring Ξ±] := (Ο ββ β) ββ Ξ±

How do you think it should start? Same imports?

#### Chris Hughes (Jan 25 2020 at 21:06):

I think change `ββ`

to `Ξ β`

and `β`

to an arbitrary monoid.

#### Chris Hughes (Jan 25 2020 at 21:13):

I also think `dfinsupp`

should just be called `direct_sum`

, since there are no applications I can think of where we don't want it to be this.

#### Yury G. Kudryashov (Jan 25 2020 at 22:41):

For me `monoid_algebra`

and `free_comm_monoid`

represent algebraic interface of what we need while `finsupp`

/ `dfinsupp`

are specific types that can be used to fulfill this interface.

#### Yury G. Kudryashov (Jan 25 2020 at 22:49):

Currently `mv_polynomial`

uses `Ο ββ β`

as an implementation of `free_comm_monoid Ο`

and `M ββ Ξ±`

as an implementation of `monoid_algebra Ξ± M`

, `M = Ο ββ β`

. The definitions and theorems heavily rely on using these specific types. I think that we should define `monoid_algebra`

separately from polynomials, prove universal property etc, then have `mv_polynomial Ξ± R := monoid_algebra R (multiplicative $ free_comm_monoid Ξ±)`

, where `free_comm_monoid Ξ±`

can be either `Ξ± ββ β`

or `multiset Ξ±`

.

#### Kevin Buzzard (Jan 25 2020 at 22:50):

Only the definitions and theorems in `mv_polynomial.lean`

rely on these, right? Everything else should just use the 1000-line interface made there. So why does it matter? I'm not saying it doesn't, I'm just trying to understand this way of thinking.

#### Yury G. Kudryashov (Jan 25 2020 at 22:51):

We can implement `monoid_algebra`

either on top of `finsupp`

, or on top of `dfinsupp`

β I don't care too much. We may also want to reimplement `finsupp`

on top of `dfinsupp`

to reduce code duplication.

#### Kevin Buzzard (Jan 25 2020 at 22:51):

so here is a case where you think the implementation details don't matter.

#### Yury G. Kudryashov (Jan 25 2020 at 22:52):

Few reasons:

- Reduce code duplication between
`polynomial`

and`mv_polynomial`

. - Make it easier to add other kinds of polynomial-like objects.

#### Kevin Buzzard (Jan 25 2020 at 22:53):

I see.

#### Kevin Buzzard (Jan 25 2020 at 22:53):

Yes, you can imagine that people will want variants at some point

#### Yury G. Kudryashov (Jan 25 2020 at 22:53):

**I** will want quasipolynomials.

#### Yury G. Kudryashov (Jan 25 2020 at 22:55):

E.g., to write solutions of $\dot x=Ax+e^{at}v$ where $a$ is an eigenvalue of $A$.

#### Yury G. Kudryashov (Jan 25 2020 at 22:55):

Or to deal with some local normal forms of differential equations.

#### Kevin Buzzard (Jan 26 2020 at 16:31):

OK so I know a direct proof of Zariski's Lemma which does not go via Noether normalisation. I am not sure of the best way to formalise it though.

Statement: say $k$ is a field, $\sigma$ is a finite set, and $J$ is a maximal ideal of the polynomial ring $R:=k[\sigma]$. Then the quotient field $K:=R/J$ is a finite extension of $k$ (we know the quotient is finitely-generated as a ring, the conclusion is that it is finitely-generated as a vector space).

The beginning of the proof looks like this. Induction on size of $\sigma$. If it's empty, no problem. For the inductive step, there are two cases. The easy case is when the image in $K$ of every element of $\sigma$ is algebraic over $k$, because then $K$ is finite by some tower law argument. In the other case, we choose some $i\in\sigma$ for which the corresponding element $x_i\in K$ is not algebraic over $k$ (i.e. the subring $k[x_i]$ of $K$ is isomorphic to a polynomial ring); we can then replace $k$ by the subfield $k(x_i)$ of $K$ (field of fractions computed within $K$) and now the induction hypothesis kicks in to give $K/k(x_i)$ finite and the proof goes on from there.

I am staring at this part of the proof and am not entirely sure of how to set things up so that they should in theory go smoothly. I need finitely-generated $k$-algebras, I need to set up the statement so that the induction procedure is not awful, I need to take a field of fractions within a bigger field, and so on. Does anyone dare to offer some suggestions as to how to formalise the relevant definitions? Once I am in a begin-end block I am a much happier person.

It is not relevant to this post, but the end of the proof is then this: each $x_j$ for $j\not=i$ is integral over $k(x_i)$ and hence over $k[x_i][1/D]$ for $D$ some non-zero polynomial which is a multiple of all the denominators that show up in all the min polys of all the $x_j$. So $K$ is a field integral over $k[x_i][1/D]$ and hence $k[x_i][1/D]$ is a field (this is Prop 5.7 in Atiyah--Macdonald), and it is slightly fiddly but not too hard to verify that this can't happen (one can check, for example, that $D$ must be in every maximal ideal of $k$ and hence that $1+D$ is a constant, contradiction)

#### Johan Commelin (Jan 27 2020 at 09:11):

If we are going to refactor `mv_polynomial`

β which sounds like a good idea β shall we also make `polynomial R`

defeq to `mv_polynomial unit R`

, and rebuild the current API around that?

#### Mario Carneiro (Jan 27 2020 at 09:12):

I'm... surprised that's not the case

#### Mario Carneiro (Jan 27 2020 at 09:13):

It seems like we are converging to a noncomputable representation anyway, so this seems like the best way to reduce on proof work

#### Mario Carneiro (Jan 27 2020 at 09:13):

@Chris Hughes thoughts?

#### Johan Commelin (Jan 27 2020 at 09:14):

Could it even be an `abbreviation`

?

#### Mario Carneiro (Jan 27 2020 at 09:15):

no, I don't think so. Given the issues we have had with typeclasses in this area I don't want to make anything harder than it needs to be

#### Mario Carneiro (Jan 27 2020 at 09:15):

I'm thinking just restate all the theorems and prove by direct reference to the multivariate version

#### Kevin Buzzard (Jan 27 2020 at 10:58):

I'm... surprised that's not the case

`mv_polynomial`

imports `polynomial`

!

#### Mario Carneiro (Jan 27 2020 at 10:58):

why?

#### Mario Carneiro (Jan 27 2020 at 10:59):

it's possible the import is just there for conjunction theorems, in which case either one can come first and the conjunction theorems can just go to whichever file comes second

#### Chris Hughes (Jan 27 2020 at 11:31):

Chris Hughes thoughts?

I think making `polynomial`

into `mv_polynomial unit`

would be sensible. One part of the interface that's currently missing is to make a `polynomial`

into `mv_polynomial`

by providing a name. I guess this is just a special case of the more general theorem that a map between monoids induces a map between monoid algebras.

#### Johan Commelin (Jan 27 2020 at 12:21):

I'm continuing this discussion in a new thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Refactoring.20polynomials/near/186676397

Last updated: May 09 2021 at 09:11 UTC