## Stream: maths

### Topic: integral domain timeout

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

Can others reproduce this:

import data.mv_polynomial
import ring_theory.ideal_operations

open mv_polynomial

variables {k : Type*} [comm_ring k]

variable {n : Type*}

def 𝕍 (S : set (mv_polynomial n k)) : set (n → k) :=
{x : n → k | ∀ f ∈ S, eval x f = 0} -- works BUT VARIABLES IN STUPID ORDER!

set_option profiler true

-- typechecks in under a second
theorem 𝕍_radical {k : Type*} [comm_ring k] {n : Type*}
(I : ideal (mv_polynomial n k)) :
𝕍 (I : set (mv_polynomial n k)) = 𝕍 (I.radical) := sorry

-- (deterministic) timeout
theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*}
(I : ideal (mv_polynomial n k)) :
𝕍 (I : set (mv_polynomial n k)) = 𝕍 (I.radical) := sorry


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

-- works fine
noncomputable instance {k : Type*} [integral_domain k] {n : Type*} :
has_coe (ideal (mv_polynomial n k)) (set (mv_polynomial n k)) := by apply_instance

-- times out
noncomputable theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*}
(I : ideal (mv_polynomial n k)) :
𝕍 (I : set (mv_polynomial n k)) = 𝕍 (I.radical) := sorry


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

-- times out
noncomputable theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*}
(I : ideal (mv_polynomial n k)) :
𝕍 (I : set (mv_polynomial n k)) = 𝕍 ((ideal.radical I : ideal _) : set _) := sorry


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

-- works
theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*}
(I : ideal (mv_polynomial n k)) :
𝕍 (↑I : set (mv_polynomial n k)) = 𝕍 (↑(ideal.radical I : ideal _) : set _) := sorry


So when do I need the up-arrows?

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

And why did I not need them for comm_rings?

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

theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*}
(I : ideal (mv_polynomial n k)) :
𝕍 (↑I : set _) = 𝕍 (↑(ideal.radical I) : set _) := sorry
-- don't know how to synthesize placeholder


gaargh

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

why does it look so ugly?

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

I am trying to sell this software to mathematicians

#### Johan Commelin (Jan 17 2020 at 17:47):

I guess that you can play tricks, if you want. Where you make k \^n notation for fin n → k, similar to the way that Mario made the \bbV notation. Idem dito for k[X_1, ..., X_n].

#### Johan Commelin (Jan 17 2020 at 17:47):

But such hacks will likely break down fast

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

Will Lean 4 be better in this regard?

#### Andrew Ashworth (Jan 17 2020 at 19:50):

Do you need to have the displayed content equal to the keystrokes you type in? If not, then the VSCode plugin - if it was extended appropriately - could probably render formulas to latex

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

No I definitely don't need this. @Patrick Massot can hacking VSCode give me $k^n$ instead of fin n -> k?

#### Daniel Selsam (Jan 17 2020 at 20:07):

Can others reproduce this:

-- (deterministic) timeout
theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*}
(I : ideal (mv_polynomial n k)) :
𝕍 (I : set (mv_polynomial n k)) = 𝕍 (I.radical) := sorry


Diamonds. Two searches for has_coe_to_fun traverse discrete_linear_ordered_field 14,000x times each.

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

Daniel thank you so much for these advanced debugging comments. I am just writing MSc level mathematics in a mathematically normal way and coming up with these issues in Lean 3, I am quite excited about Lean 4 now.

Last updated: May 06 2021 at 18:20 UTC