Algebraic geometry course

Stream: maths

[Kevin Buzzard]

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]

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

[Johan Commelin]

Good luck!

[Johan Commelin]

@Kevin Buzzard How did the first lecture go?

[Kevin Buzzard]

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]

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

[Johan Commelin]

I think @Lennard Henze was working on this

[Johan Commelin]

How are things going, Lennard?

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

Probably commutative algebra

[Kevin Buzzard]

We're following these notes by Martin Orr.

[Kevin Buzzard]

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

[Lennard Henze]

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]

Lecture 3 of my course. Can anyone tell me how to get rid of those bloody Ps everywhere?

[Mario Carneiro]

Use parameters

[Mario Carneiro]

Alternatively, bake the application of P into the notations for V and I as in Sebastian's comment

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

You have a lot of ?? in the proof, did you want to ask a question about it?

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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]

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

[Mario Carneiro]

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]

See?

lemma 𝕀𝕍𝕀_eq_𝕀 (V : set W) : (𝕀 (𝕍 (𝕀 V))) = 𝕀 V :=
𝕍𝕀𝕍_eq_𝕍 _ _

[Mario Carneiro]

If you use parameters, this trick doesn't work

[Patrick Massot]

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]

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

[Kevin Buzzard]

which I'm currently giving

[Kevin Buzzard]

do we not have nilradical in Lean?

[Alex J. Best]

Nope!

[Alex J. Best]

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]

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:

https://github.com/ImperialCollegeLondon/M4P33/blob/ac0a28f19936a7f861ff3c6c0dc57d9b6093e8e6/src/abstract_V_and_I.lean#L151

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]

If you use parameters, this trick doesn't work

Right, because P needs to be reversed.

[Kevin Buzzard]

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]

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]

simp, tauto

[Kevin Buzzard]

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]

@Alexander Uhlmann isolated this property at Xena yesterday.

[Jesse Michael Han]

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]

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

[Johan Commelin]

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

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

Could probably use some cleaning...

[Kevin Buzzard]

Thanks!

[Kevin Buzzard]

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]

It might be most natural to do this by induction

[Koundinya Vajjha]

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

[Kevin Buzzard]

I hadn't -- many thanks!

[Kevin Buzzard]

It might be most natural to do this by induction

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

[Kevin Buzzard]

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

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]

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]

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]

Does that mean that users should avoid it?

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

I see.

[Yury G. Kudryashov]

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

[Chris Hughes]

Do we need bind for polynomials?

[Johan Commelin]

what would that look like?

[Chris Hughes]

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]

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

[Chris Hughes]

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]

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

[Chris Hughes]

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

[Patrick Massot]

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]

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]

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

and $X_{ijk}$ right?

[Johan Commelin]

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]

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

[Kevin Buzzard]

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]

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]

option_equiv_right lacks definition lemmas

[Kevin Buzzard]

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]

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]

I think so

[Mario Carneiro]

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]

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]

there are lots of blah_X and blah_C lemmas

[Kevin Buzzard]

I am suggesting we add a few more ;-)

[Mario Carneiro]

I think you are right

[Kevin Buzzard]

I'm slowly getting the hang of this Lean malarkey

[Mario Carneiro]

I really hope it's a rfl proof because there are a whole bunch of definitions in the way

[Kevin Buzzard]

I can iterate the show, rw process ;-)

[Mario Carneiro]

I'm still not even sure what option_equiv_right α β (X none) = _ should complete to

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

It's C unit or C punit or whatever

[Kevin Buzzard]

wait

[Mario Carneiro]

I think it's C polynomial.X

[Kevin Buzzard]

yeah, that :-)

[Mario Carneiro]

but lean times out when I write that

[Mario Carneiro]

oh, nvm

[Mario Carneiro]

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]

oh nice!

[Mario Carneiro]

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]

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]

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]

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]

@[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]

So all three of the sum_to_iter_? things should be simp lemmas?

[Mario Carneiro]

yes

[Kevin Buzzard]

Many thanks! And we can perhaps get rid of the show lines by coming up with some other simp lemmas?

[Kevin Buzzard]

Or is this overoptimistic?

[Mario Carneiro]

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]

Ideally this proof should be dunfold option_equiv_right; simp

[Johan Commelin]

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]

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]

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]

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

begin
  apply p.induction_on,
  all_goals {sorry}
end

[Kevin Buzzard]

Nice idea!

[Kevin Buzzard]

I had just started with unfold eval_2 :-) That looked much worse :-)

[Kevin Buzzard]

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]

aargh one of the goals is not true :-/

[Johan Commelin]

@Kevin Buzzard I'm quite sure that you need φ to be a ring hom

[Johan Commelin]

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

[Johan Commelin]

@Kevin Buzzard Which goal is false?

[Kevin Buzzard]

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]

[sorry, on a train with sporadic connection]

[Kevin Buzzard]

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]

I think I might have to modify the proof of induction_on

[Johan Commelin]

Aaah, I see.

[Johan Commelin]

Annoying

[Kevin Buzzard]

I'm going in...

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

Doesn't that mean you can remove those first two lines with unfolds?

[Kevin Buzzard]

However he also says that the definition of vars in mv_polynomial should be what he wants it to be :P

[Kevin Buzzard]

oh we only just did it :-)

[Kevin Buzzard]

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

[Johan Commelin]

Nice!

[Yury G. Kudryashov]

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]

Didn't Kenny already define free_comm_monoid?

[Yury G. Kudryashov]

@Johan Commelin git grep doesn't find it. Are you talking about some PR/WIP?

[Chris Hughes]

free_comm_monoid is multiset.

[Chris Hughes]

Kenny did define free_comm_group

[Johan Commelin]

Aah, right

[Kevin Buzzard]

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]

monoid algebra should be defined to be dfinsupp I think.

[Kevin Buzzard]

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]

I think change →₀ to Π₀ and ℕ to an arbitrary monoid.

[Chris Hughes]

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]

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]

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]

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]

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]

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

[Yury G. Kudryashov]

Few reasons:

1. Reduce code duplication between polynomial and mv_polynomial.
2. Make it easier to add other kinds of polynomial-like objects.

[Kevin Buzzard]

I see.

[Kevin Buzzard]

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

[Yury G. Kudryashov]

I will want quasipolynomials.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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]

@Chris Hughes thoughts?

[Johan Commelin]

Could it even be an abbreviation?

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

mv_polynomial imports polynomial!

[Mario Carneiro]

why?

[Mario Carneiro]

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]

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]

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