Zulip Chat Archive

Stream: maths

Topic: Algebraic geometry course


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 13 2020 at 10:40):

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

view this post on Zulip Johan Commelin (Jan 13 2020 at 10:56):

Good luck!

view this post on Zulip Johan Commelin (Jan 13 2020 at 18:31):

@Kevin Buzzard How did the first lecture go?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jan 14 2020 at 10:05):

I think @Lennard Henze was working on this

view this post on Zulip Johan Commelin (Jan 14 2020 at 10:05):

How are things going, Lennard?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jan 14 2020 at 14:04):

Probably commutative algebra

view this post on Zulip Kevin Buzzard (Jan 14 2020 at 14:57):

We're following these notes by Martin Orr.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 17 2020 at 10:39):

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

view this post on Zulip Mario Carneiro (Jan 17 2020 at 11:01):

Use parameters

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 17 2020 at 11:11):

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

view this post on Zulip Kevin Buzzard (Jan 17 2020 at 11:14):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 :-)

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Jan 17 2020 at 11:30):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 17 2020 at 11:32):

See?

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

view this post on Zulip Mario Carneiro (Jan 17 2020 at 11:33):

If you use parameters, this trick doesn't work

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 17 2020 at 13:11):

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

view this post on Zulip Kevin Buzzard (Jan 17 2020 at 13:11):

which I'm currently giving

view this post on Zulip Kevin Buzzard (Jan 17 2020 at 17:17):

do we not have nilradical in Lean?

view this post on Zulip Alex J. Best (Jan 17 2020 at 17:20):

Nope!

view this post on Zulip 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

view this post on Zulip 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:

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)

view this post on Zulip Kevin Buzzard (Jan 17 2020 at 18:44):

If you use parameters, this trick doesn't work

Right, because P needs to be reversed.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Chris Hughes (Jan 17 2020 at 21:08):

simp, tauto

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 17 2020 at 21:48):

@Alexander Uhlmann isolated this property at Xena yesterday.

view this post on Zulip 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]

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 18 2020 at 21:57):

Could probably use some cleaning...

view this post on Zulip Kevin Buzzard (Jan 18 2020 at 22:59):

Thanks!

view this post on Zulip 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 kk is a field (probably a commutative semiring would work fine) and RR is a finitely-generated kk-algebra: this means that RR 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 kRk\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[x1,x2,,xn]R=k[x_1,x_2,\ldots,x_n] and note that this is not a polynomial ring -- it's "the ring generated by kk and the set {x1,x2,,xn}\{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 xix_i we can find some 1tn1\leq t\leq n such that the xix_i for 1tn1\leq t\leq n are independent transcendentals over kk, and the xjx_j for t+1jnt+1\leq j\leq n are algebraic over k(x1,,xt)k(x_1,\ldots,x_t)". As a mathematician this does indeed feel like a triviality. One sets R0=kR_0=k (this ring will change but it will always be equipped with a map to RR) and simply loops through the xix_i and does one of two things: if the map from R0[X]R_0[X] to $$R$ sending XX to xix_i is injective, then add xix_i to the "transcendental" pile and update R0R_0 to R0[xi]R_0[x_i]. If the map isn't injective, add xix_i to the "algebraic" pile. Then renumber the tt "transcendental" xix_i to be the first few xix_i and renumber the "algebraic" xix_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 R0R_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.

view this post on Zulip Reid Barton (Jan 19 2020 at 18:13):

It might be most natural to do this by induction

view this post on Zulip Koundinya Vajjha (Jan 19 2020 at 18:45):

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

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 18:58):

I hadn't -- many thanks!

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:)

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 21 2020 at 08:52):

Does that mean that users should avoid it?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 21 2020 at 08:54):

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

view this post on Zulip 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 (-;

view this post on Zulip Johan Commelin (Jan 21 2020 at 08:56):

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

view this post on Zulip Patrick Massot (Jan 21 2020 at 08:59):

I see.

view this post on Zulip Yury G. Kudryashov (Jan 21 2020 at 16:05):

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

view this post on Zulip Chris Hughes (Jan 21 2020 at 18:51):

Do we need bind for polynomials?

view this post on Zulip Johan Commelin (Jan 21 2020 at 20:01):

what would that look like?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 21 2020 at 20:20):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jan 21 2020 at 20:26):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 21 2020 at 21:29):

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

view this post on Zulip 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 XnX_n... in a subscript...

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 00:27):

and XijkX_{ijk} right?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 22 2020 at 22:43):

option_equiv_right lacks definition lemmas

view this post on Zulip 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?

view this post on Zulip 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 β γ?

view this post on Zulip Mario Carneiro (Jan 22 2020 at 22:47):

I think so

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 22:50):

there are lots of blah_X and blah_C lemmas

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 22:50):

I am suggesting we add a few more ;-)

view this post on Zulip Mario Carneiro (Jan 22 2020 at 22:50):

I think you are right

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 22:50):

I'm slowly getting the hang of this Lean malarkey

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 22:52):

I can iterate the show, rw process ;-)

view this post on Zulip Mario Carneiro (Jan 22 2020 at 22:52):

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

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 22:53):

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

view this post on Zulip Mario Carneiro (Jan 22 2020 at 22:53):

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

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 22:53):

It's C unit or C punit or whatever

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 22:54):

wait

view this post on Zulip Mario Carneiro (Jan 22 2020 at 22:54):

I think it's C polynomial.X

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 22:54):

yeah, that :-)

view this post on Zulip Mario Carneiro (Jan 22 2020 at 22:54):

but lean times out when I write that

view this post on Zulip Mario Carneiro (Jan 22 2020 at 22:55):

oh, nvm

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 23:04):

oh nice!

view this post on Zulip 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

view this post on Zulip 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]R[X][n] where XX is one variable and nn 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

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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]

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 23:12):

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

view this post on Zulip Mario Carneiro (Jan 22 2020 at 23:12):

yes

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 22 2020 at 23:13):

Or is this overoptimistic?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 22 2020 at 23:14):

Ideally this proof should be dunfold option_equiv_right; simp

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 23 2020 at 14:40):

Nice idea!

view this post on Zulip Kevin Buzzard (Jan 23 2020 at 14:40):

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

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Jan 23 2020 at 14:44):

aargh one of the goals is not true :-/

view this post on Zulip Johan Commelin (Jan 23 2020 at 14:46):

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

view this post on Zulip Johan Commelin (Jan 23 2020 at 14:47):

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

view this post on Zulip Johan Commelin (Jan 23 2020 at 14:47):

@Kevin Buzzard Which goal is false?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 23 2020 at 14:48):

[sorry, on a train with sporadic connection]

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 23 2020 at 14:50):

I think I might have to modify the proof of induction_on

view this post on Zulip Johan Commelin (Jan 23 2020 at 14:52):

Aaah, I see.

view this post on Zulip Johan Commelin (Jan 23 2020 at 14:52):

Annoying

view this post on Zulip Kevin Buzzard (Jan 23 2020 at 14:52):

I'm going in...

view this post on Zulip 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 :=

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 23 2020 at 16:01):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 23 2020 at 18:40):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 23 2020 at 18:41):

oh we only just did it :-)

view this post on Zulip Kevin Buzzard (Jan 25 2020 at 14:56):

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

view this post on Zulip Johan Commelin (Jan 25 2020 at 15:09):

Nice!

view this post on Zulip 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 eattne^{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.

view this post on Zulip Johan Commelin (Jan 25 2020 at 19:16):

Didn't Kenny already define free_comm_monoid?

view this post on Zulip Yury G. Kudryashov (Jan 25 2020 at 19:26):

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

view this post on Zulip Chris Hughes (Jan 25 2020 at 19:28):

free_comm_monoid is multiset.

view this post on Zulip Chris Hughes (Jan 25 2020 at 19:28):

Kenny did define free_comm_group

view this post on Zulip Johan Commelin (Jan 25 2020 at 19:40):

Aah, right

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jan 25 2020 at 20:59):

monoid algebra should be defined to be dfinsupp I think.

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Jan 25 2020 at 21:06):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 α.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 25 2020 at 22:51):

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

view this post on Zulip Yury G. Kudryashov (Jan 25 2020 at 22:52):

Few reasons:

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

view this post on Zulip Kevin Buzzard (Jan 25 2020 at 22:53):

I see.

view this post on Zulip Kevin Buzzard (Jan 25 2020 at 22:53):

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

view this post on Zulip Yury G. Kudryashov (Jan 25 2020 at 22:53):

I will want quasipolynomials.

view this post on Zulip Yury G. Kudryashov (Jan 25 2020 at 22:55):

E.g., to write solutions of x˙=Ax+eatv\dot x=Ax+e^{at}v where aa is an eigenvalue of AA.

view this post on Zulip Yury G. Kudryashov (Jan 25 2020 at 22:55):

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

view this post on Zulip 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 kk is a field, σ\sigma is a finite set, and $J$ is a maximal ideal of the polynomial ring R:=k[σ]R:=k[\sigma]. Then the quotient field K:=R/JK:=R/J is a finite extension of kk (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 KK of every element of σ\sigma is algebraic over kk, because then KK is finite by some tower law argument. In the other case, we choose some iσi\in\sigma for which the corresponding element xiKx_i\in K is not algebraic over kk (i.e. the subring k[xi]k[x_i] of KK is isomorphic to a polynomial ring); we can then replace kk by the subfield k(xi)k(x_i) of KK (field of fractions computed within KK) and now the induction hypothesis kicks in to give K/k(xi)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 kk-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 xjx_j for jij\not=i is integral over k(xi)k(x_i) and hence over k[xi][1/D]k[x_i][1/D] for DD some non-zero polynomial which is a multiple of all the denominators that show up in all the min polys of all the xjx_j. So KK is a field integral over k[xi][1/D]k[x_i][1/D] and hence k[xi][1/D]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 DD must be in every maximal ideal of kk and hence that 1+D1+D is a constant, contradiction)

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 27 2020 at 09:12):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 27 2020 at 09:13):

@Chris Hughes thoughts?

view this post on Zulip Johan Commelin (Jan 27 2020 at 09:14):

Could it even be an abbreviation?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 27 2020 at 10:58):

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

mv_polynomial imports polynomial!

view this post on Zulip Mario Carneiro (Jan 27 2020 at 10:58):

why?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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