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 Ps 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:

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 (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 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 kβ†’Rk\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 1≀t≀n1\leq t\leq n such that the xix_i for 1≀t≀n1\leq t\leq n are independent transcendentals over kk, and the xjx_j for t+1≀j≀nt+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.

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[X1,X2,…,Xn]k[X_1,X_2,\ldots,X_n] with kk 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 XnX_n... in a subscript...

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

and XijkX_{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]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

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

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

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:

  1. Reduce code duplication between polynomial and mv_polynomial.
  2. 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 xΛ™=Ax+eatv\dot x=Ax+e^{at}v where aa is an eigenvalue of AA.

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 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 xi∈Kx_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 j=ΜΈij\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)

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: Dec 20 2023 at 11:08 UTC