Zulip Chat Archive

Stream: maths

Topic: Timeout


view this post on Zulip Anne Baanen (Nov 02 2020 at 13:05):

The following code causes a timeout and I can't figure out where (explicitly instantating type classes doesn't help, nor does set_option trace.type_context.is_def_eq true give a lot of output). Is it something in the kernel?

import field_theory.adjoin
import field_theory.splitting_field

instance foo {K L : Type*} [field K] [field L] [algebra K L]
  {x : L} (hx : is_integral K x) :
  vector_space Kx (minimal_polynomial hx).splitting_field :=
sorry

view this post on Zulip Kenny Lau (Nov 02 2020 at 13:36):

Is it meant to succeed?

view this post on Zulip Anne Baanen (Nov 02 2020 at 13:51):

I mean, ↥K⟮x⟯ is a field and (minimal_polynomial hx).splitting_field is a field, hence an add_comm_group, so I wouldn't expect vector_space ↥K⟮x⟯ (minimal_polynomial hx).splitting_field to be impossible to write.

view this post on Zulip Anne Baanen (Nov 02 2020 at 13:52):

(And the implementation should be ring_hom.to_algebra.to_semimodule on the map sending x to one of the roots and K along algebra_map K (splitting_field _), no?)

view this post on Zulip Kenny Lau (Nov 02 2020 at 14:22):

But ring_hom.to_algebra is not (and should not be) an instance because it relies on a ring hom

view this post on Zulip Kenny Lau (Nov 02 2020 at 14:22):

If you include that line does it still time out?

view this post on Zulip Anne Baanen (Nov 02 2020 at 14:32):

Kenny Lau said:

But ring_hom.to_algebra is not (and should not be) an instance because it relies on a ring hom

Indeed! My question was not "why do I need to declare this instance" :) Only "how should I understand this timeout, so I can debug similar ones in the future?"

view this post on Zulip Anne Baanen (Nov 02 2020 at 14:32):

Kenny Lau said:

If you include that line does it still time out?

If I replace the sorry, it works indeed:

noncomputable instance foo {K L : Type*} [field K] [field L] [algebra K L]
  {x : L} (hx : is_integral K x) :
  vector_space Kx (minimal_polynomial hx).splitting_field :=
@algebra.to_semimodule _ _ _ _ (ring_hom.to_algebra sorry)

view this post on Zulip Anne Baanen (Nov 02 2020 at 14:35):

Of course in my actual code, I only define an algebra, using a more general form:

def algebra_of_splits {F : Type*} [field F] [algebra K F]
  {x : L} (hx : is_integral K x) (hF : (minimal_polynomial hx).splits (algebra_map K F)) :
  algebra Kx F := _

noncomputable instance algebra_adjoin_splitting_field {x : L} (hx : is_integral K x) :=
algebra_of_splits hx (splitting_field.splits _)

view this post on Zulip Anne Baanen (Nov 02 2020 at 14:35):

The vector_space instance is then inferred correctly.


Last updated: May 10 2021 at 08:14 UTC