## Stream: general

### Topic: why is this slow?

#### Kenny Lau (Sep 16 2018 at 09:44):

import data.polynomial
import linear_algebra.multivariate_polynomial
import ring_theory.associated

universe u

namespace algebraic_closure

variables (k : Type u) [field k] [decidable_eq k]

def irred : set (polynomial k) :=
{ p | irreducible p }

def big_ring : Type u :=
mv_polynomial (irred k) k

instance : comm_ring (big_ring k) :=
mv_polynomial.comm_ring

set_option profiler true
def big_ideal : set (big_ring k) :=


#### Kenny Lau (Sep 16 2018 at 10:46):

@Kevin Buzzard @Chris Hughes I suspect Chris's span is the wrong one, which means we will have to once again wait for the refactoring

#### Kevin Buzzard (Sep 16 2018 at 10:48):

So what exactly is being refactored? Yeah I am putting "research level" coding on hold at the minute and thinking more about organisational stuff. The question of why it's slow is still of independent interest. What is causing the hold-up? Is it type class inference?

#### Kenny Lau (Sep 16 2018 at 10:49):

if we specify that we're talking about the span as an ideal (which is this case) or that we're talking about the span as a k-module (which is not this case) then it would be more convenient

#### Kevin Buzzard (Sep 16 2018 at 11:02):

@Mario Carneiro is this another +1 for saying which ring we're talking about explicitly?

I guess there is also now the option of making the "ideal" version of things into its own little interface -- e.g. ideal.span could mean "the span of this subset of the ring R as an R-module"

#### Kevin Buzzard (Sep 16 2018 at 11:02):

I would love to be able to debug this sort of thing. Presumably the by exact insertion changes the elaboration strategy somehow. But in my mind this just raises a bunch of questions as to how it's working and how the change makes any difference.

#### Kevin Buzzard (Sep 16 2018 at 11:02):

def big_ideal' : set (big_ring k) :=


#### Kevin Buzzard (Sep 16 2018 at 11:36):

I'm hoping that submodule will as well.

#### Kevin Buzzard (Sep 16 2018 at 11:37):

In your polynomial code, module R (polynomial R) takes precedence over module (polynomial R) (polynomial R) making it really difficult to talk about ideals of polynomial rings!

#### Chris Hughes (Sep 16 2018 at 11:43):

Change it then. I didn't really think about that problem when I wrote it.

#### Kevin Buzzard (Sep 16 2018 at 11:45):

rofl

def big_ideal' : set (big_ring k) :=
span \$ ⋃ p : irred k, {@polynomial.eval₂ k _ _ (big_ring k) _ mv_polynomial.C _ (mv_polynomial.X p) p.1}


breaks it again -- apparently explictly telling Lean to use big_ring k rather than letting it work it out for itself is a bad idea. @Mario Carneiro what is going on here?

#### Kevin Buzzard (Sep 16 2018 at 11:48):

Adding instance : is_semiring_hom (mv_polynomial.C : k → big_ring k) := by apply_instance  speeds Kenny's original code up a bit.

Last updated: May 14 2021 at 13:24 UTC