Typeclass for algebraic extension of fields?

Stream: Is there code for X?

[Kevin Buzzard]

If [Field K] [Field L] [Algebra K L], do we have a typeclass for "L is algebraic over K"? We have docs#Algebra.IsAlgebraic, but

attribute [instance] Algebra.IsAlgebraic
/-
cannot find synthesization order for instance Algebra.IsAlgebraic with type
  (R : Type u) → (A : Type v) → [inst : CommRing R] → [inst_1 : Ring A] → [inst : Algebra R A] → Prop
all remaining arguments have metavariables:
  CommRing ?R
  Ring ?A
  @Algebra ?R ?A CommRing.toCommSemiring Ring.toSemiring
-/

[Johan Commelin]

Ha! We should probably refactor mathlib. Idem dito for Algebra.IsIntegral

[Anne Baanen]

I think you mean attribute [class] Algebra.IsAlgebraic not instance. I was very puzzled about the error for a moment :)

[Anne Baanen]

Let me see if I can quickly turn IsIntegral and IsAlgebraic into a class.

[Eric Wieser]

Should we redefine Algebra.IsAlgebraic as Subalgebra.IsAlgebraic \top to match docs#Monoid.FG etc?

[Eric Wieser]

(the other way around seems fine too, but consistency seems valuable here)

[Anne Baanen]

Hmm, I thought the new synthesis algorithm could avoid loops...

  [] ✅ apply FiniteDimensional.finiteDimensional_self to Module.Finite K K ▶
  [resume] propagating FiniteDimensional K K to subgoal Module.Finite K K of Algebra.FiniteType K K ▶
  [resume] propagating Algebra.FiniteType K K to subgoal Algebra.FiniteType K K of Module.Finite K K ▶
  [resume] propagating Algebra.IsAlgebraic K K → Module.Finite K K to subgoal Module.Finite K K of Algebra.FiniteType K K ▶
  [resume] propagating Algebra.IsAlgebraic K K → Algebra.FiniteType K K to subgoal Algebra.FiniteType K K of Module.Finite K K ▶
  [resume] propagating Algebra.IsAlgebraic K K →
        Algebra.IsAlgebraic K K → Module.Finite K K to subgoal Module.Finite K K of Algebra.FiniteType K K ▶
  [resume] propagating Algebra.IsAlgebraic K K →
        Algebra.IsAlgebraic K K → Algebra.FiniteType K K to subgoal Algebra.FiniteType K K of Module.Finite K K ▶
  [resume] propagating Algebra.IsAlgebraic K K →
        Algebra.IsAlgebraic K K →
          Algebra.IsAlgebraic K K → Module.Finite K K to subgoal Module.Finite K K of Algebra.FiniteType K K ▶
  [resume] propagating Algebra.IsAlgebraic K K →
        Algebra.IsAlgebraic K K →
          Algebra.IsAlgebraic K K → Algebra.FiniteType K K to subgoal Algebra.FiniteType K K of Module.Finite K K ▶
  [resume] propagating Algebra.IsAlgebraic K K →
        Algebra.IsAlgebraic K K →
          Algebra.IsAlgebraic K K →
            Algebra.IsAlgebraic K K → Module.Finite K K to subgoal Module.Finite K K of Algebra.FiniteType K K ▶
  [resume] propagating Algebra.IsAlgebraic K K →
        Algebra.IsAlgebraic K K →
          Algebra.IsAlgebraic K K →
            Algebra.IsAlgebraic K K → Algebra.FiniteType K K to subgoal Algebra.FiniteType K K of Module.Finite K K ▶
  [resume] propagating Algebra.IsAlgebraic K K →
        Algebra.IsAlgebraic K K →
          Algebra.IsAlgebraic K K →
            Algebra.IsAlgebraic K K →
              Algebra.IsAlgebraic K K → Module.Finite K K to subgoal Module.Finite K K of Algebra.FiniteType K K ▶
  [] 501 more entries... ▶

[Anne Baanen]

Eric Wieser said:

Should we redefine Algebra.IsAlgebraic as Subalgebra.IsAlgebraic \top to match docs#Monoid.FG etc?

Hopefully we can do this somewhat more easily after changing it into a class, since it's no longer equal to ∀ x, IsAlgebraic R x by definition.

[Anne Baanen]

Oh right, Algebra.IsAlgebraic.isIntegral has type Algebra.IsAlgebraic K A → Algebra.IsIntegral K A, not ∀ [Algebra.IsAlgebraic K A], Algebra.IsIntegral K A and the system doesn't quite support implications correctly.

[Anne Baanen]

Should alias turn arguments that have the type of a class into instance implicits?

[Anne Baanen]

Finally done fixing everything! #12761

[Kevin Buzzard]

Merged! Thanks so much Anne!