synthesized type class instance is not definitionally equal

Stream: new members

[Xavier Roblot]

Can somebody please explains to me what is happening with the code below. I get an error when I try to use finite_dimensional.of_finset_basis.

I don't understand what the error message means: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized algebra.to_module inferred algebra.to_module

Here is the code:

import number_theory.number_field
import algebra.char_p.algebra
import data.complex.basic

variables {K : Type*} [field K] [number_field K]

example (x : K) : ∀ φ : K →+* ℂ, (polynomial.map (algebra_map ℚ ℂ) (minpoly ℚ x)).is_root (φ x) :=
begin
  let Qx := adjoin_root (minpoly ℚ x),
  have hx : is_integral ℚ x, { exact is_separable.is_integral ℚ x },
  letI : irreducible (minpoly ℚ x), { exact minpoly.irreducible hx },
  letI : field Qx, { exact adjoin_root.field },
  letI : number_field Qx := {
    to_char_zero :=
    begin
      exact char_zero_of_injective_algebra_map (algebra_map ℚ Qx).injective,
    end,
    to_finite_dimensional :=
    begin
      refine finite_dimensional.of_finset_basis _,
      sorry,
    end, },
end

[Eric Wieser]

set_option pp.implicit true will give you a better error message

[Alex J. Best]

Ouch, this looks pretty nasty, you are running into a longstanding problem we have with algebras that while we have plans to fix, we haven't been able to yet.

[Alex J. Best]

It might be better to rethink the strategy a bit to proceed, is it possible to work with the docs#subfield generated by x instead?

[Alex J. Best]

One other thing, irreducible (minpoly ℚ x) and number_field Qx should both be haveI rather than letI as they are Props and don't carry any extra data, I don't think it helps fix the problem though

[Xavier Roblot]

Well, I will have to rethink my proof then. Note that I would also be very happy with any other way to prove that Qx is finite_dimensional. It is the only bit missing in the proof...

[Alex J. Best]

Okay maybe we can find a workaround if you already have a full proof with only one missing piece then, I'll have another look later this evening

[Xavier Roblot]

Thanks, Alex. That would be great since adjoin_root is very well-suited to work with number field, I found.