# Zulip Chat Archive

## Stream: maths

### Topic: Timeout

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

#### Kenny Lau (Nov 02 2020 at 13:36):

Is it meant to succeed?

#### 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.

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

#### 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

#### Kenny Lau (Nov 02 2020 at 14:22):

If you include that line does it still time out?

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

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

#### 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 ↥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 (Nov 02 2020 at 14:35):

The `vector_space`

instance is then inferred correctly.

Last updated: May 10 2021 at 08:14 UTC