about metavariables in typeclass

Stream: new members

[Hbz]

import Mathlib

open Polynomial

open scoped Classical Polynomial

noncomputable section

variable (𝕜 : Type) [Field 𝕜]

def RationalFunctionField := FractionRing (Polynomial 𝕜)

namespace RationalFunctionField

variable {𝕜}

instance : CommRing (RationalFunctionField 𝕜) := by
  unfold RationalFunctionField
  exact OreLocalization.instCommRing

instance : Field (RationalFunctionField 𝕜) := by
  unfold RationalFunctionField
  exact FractionRing.field (Polynomial 𝕜)

instance : IsDomain (Polynomial 𝕜) := by
  exact instIsDomain

instance : Algebra 𝕜 (RationalFunctionField 𝕜) := by
  unfold RationalFunctionField
  exact OreLocalization.instAlgebra

instance : Algebra (Polynomial 𝕜) (RationalFunctionField 𝕜) := by
  unfold RationalFunctionField
  exact OreLocalization.instAlgebra

instance : IsFractionRing (Polynomial 𝕜) (RationalFunctionField 𝕜) := by
  unfold RationalFunctionField
  exact Localization.isLocalization

def ofPolynomial : Polynomial 𝕜 →ₐ[𝕜] RationalFunctionField 𝕜 :=
  { toFun := algebraMap (Polynomial 𝕜) (RationalFunctionField 𝕜)
    map_one' := by simp [algebraMap]
    map_mul' := fun x y => by simp [algebraMap]
    map_zero' := by simp [algebraMap]
    map_add' := fun x y => by simp [algebraMap]
    commutes' := fun k => by exact rfl}

def x : RationalFunctionField 𝕜 := ofPolynomial Polynomial.X

def baseSubfield : Subfield (RationalFunctionField 𝕜) :=
  Subfield.closure (Set.range (algebraMap 𝕜 _) ∪ {x ^ 2})

#check Module

instance : CommRing (↥(baseSubfield)) :=
  Subfield.instCommRing baseSubfield

and i just want to ask why lean tell me
typeclass instance problem is stuck, it is often due to metavariables
Field ?m.32792
and how can i solve it. :slight_smile:

[Aaron Liu]

Make baseSubfield take in 𝕜 explicitly