Typeclass synthesis fails with extra assumption

Stream: new members

[Dion Leijnse]

In the following code, Lean fails to infer the instance Algebra R (myQuot R I) in the last lemma, and the problem seems to be due to adding the assumption that R is a field. What is going on here, and how can I access the algebra structures in lemmas where I require R to be a field?

import Mathlib

variable (R : Type) [CommRing R]
variable (I : Ideal R)

def myQuot : Type :=
  R ⧸ I
deriving CommRing, Algebra R

lemma test1 : algebraMap R (myQuot R I) 1 = 1 := by sorry

lemma test2 [Field R] : algebraMap R (myQuot R I) 1 = 1 := by sorry
  -- failed to synthesize instance of type class Algebra R (myQuot R I)

[Riccardo Brasca]

You both have CommRing R and Field R, so now you have two (totally unrelated) ring structure on R.

[Dion Leijnse]

Thanks! So the way to go is to add an assumption IsField R?

[Riccardo Brasca]

You can do something like

import Mathlib

variable (R : Type)

section CommRing

variable [CommRing R] (I : Ideal R)

def myQuot : Type :=
  R ⧸ I
deriving CommRing, Algebra R

lemma test1 : algebraMap R (myQuot R I) 1 = 1 := by sorry

end CommRing

section Field

variable [Field R] (I : Ideal R)

lemma test2 : algebraMap R (myQuot R I) 1 = 1 := by sorry

end Field

[Riccardo Brasca]

Also using IsField is OK.

[Riccardo Brasca]

It depends a little on what you want to do (do you really want to speak about an ideal of a field?)

[Dion Leijnse]

Riccardo Brasca said:

It depends a little on what you want to do (do you really want to speak about an ideal of a field?)

No, but this was a MWE extracted from something more complicated (where R is a polynomial ring over a field)

[Dion Leijnse]

Riccardo Brasca said:

You can do something like

import Mathlib

variable (R : Type)

section CommRing

variable [CommRing R] (I : Ideal R)

def myQuot : Type :=
  R ⧸ I
deriving CommRing, Algebra R

lemma test1 : algebraMap R (myQuot R I) 1 = 1 := by sorry

end CommRing

section Field

variable [Field R] (I : Ideal R)

lemma test2 : algebraMap R (myQuot R I) 1 = 1 := by sorry

end Field

Thanks, this does indeed look like a better solution (because it would be nice to just use the instance Field R where I work with it).

[Riccardo Brasca]

A maybe more elegant solution is just to declare R and K at the beginning, with the relevant assumptions.