Timeout

Stream: maths

[Anne Baanen]

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 ↥K⟮x⟯ (minimal_polynomial hx).splitting_field :=
sorry

[Kenny Lau]

Is it meant to succeed?

[Anne Baanen]

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.

[Anne Baanen]

(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?)

[Kenny Lau]

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

[Kenny Lau]

If you include that line does it still time out?

[Anne Baanen]

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

[Anne Baanen]

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 ↥K⟮x⟯ (minimal_polynomial hx).splitting_field :=
@algebra.to_semimodule _ _ _ _ (ring_hom.to_algebra sorry)

[Anne Baanen]

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 ↥K⟮x⟯ F := _

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

[Anne Baanen]

The vector_space instance is then inferred correctly.