# Zulip Chat Archive

## 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) := span $ ⋃ p : irred k, { polynomial.eval₂ mv_polynomial.C (mv_polynomial.X p) p.1 } /- parsing took 0.154ms elaboration of big_ideal took 7.53s type checking of big_ideal took 9.17ms decl post-processing of big_ideal took 11.1ms compilation of algebraic_closure.big_ideal took 0.205ms -/ end algebraic_closure

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

is there any way to make this faster?

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

@Chris Hughes

#### Chris Hughes (Sep 16 2018 at 10:01):

This compiles in no time. I don't know the solution though.

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

#### 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) := by exact (span $ ⋃ p : irred k, { polynomial.eval₂ mv_polynomial.C (mv_polynomial.X p) p.1 })

is much quicker for me and seems to give the same answer.

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

Stupid `#print notation ⋃`

gives me a useless answer. I had to grep through the source code to find it's `set.Union`

.

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

So in future presumably `span`

will take the ring as an explicit argument?

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

hopefully. Hey I got Kenny's version working quickly:

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

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