HPow instance on linear maps, rfl failure

Stream: new members

[VayusElytra]

Hello, I am working on the following definitions and had a couple questions. FunctCat is a category of functors, and EndRing C R F is the set of all natural transformations from one of these functors to itself. It forms a ring when equipped with pointwise addition and composition.

abbrev FunctCat (C : Type*) [Category C] (K : Type*) [DivisionRing K]
   := (C ⥤ ModuleCat K)

abbrev EndRing (C : Type) [Category C] (R : Type) [DivisionRing R]
  (F : FunctCat C R) := (F ⟶ F)

1) Is the ring structure on EndRing something that is already implemented in Lean? I've already done the work to implement it on my own, but of course it'd be more sensible to use pre-existing constructions.

2) In the following code snippet:

variable (C : Type) [Category C]
variable (R : Type) [DivisionRing R]
variable (F : FunctCat C R)
variable (θ : EndRing C R F) (n : ℕ)
#check LinearMap.range ((θ.app X) ^ n)

Lean is upset and complains that it cannot synthesize an instance HPow (F.obj X ⟶ F.obj X) ℕ. I don't understand why this fails; things of type F.obj X ⟶ F.obj X get coerced into linear maps between these spaces, and there is obviously an instance of HPow on linear maps. How do I fix this?

3) In my code that proves that EndRing is actually a ring:

instance EndRingIsRing (R : Type) [DivisionRing R] (C : Type) [Category C]
  (F : FunctCat C R) : Ring (EndRing C R F) where
  zero_mul := ZeroMul C R F
  mul_zero := MulZero C R F
  one_mul := OneMul C R F
  mul_one := MulOne C R F
  zero_add := ZeroAdd C R F
  add_assoc := EndAddAssoc C R F
  add_zero := AddZero C R F
  add_comm := EndAddComm C R F
  nsmul := nsmulRec
  zsmul := zsmulRec
  add_left_neg := AddLeftNeg C R F
  left_distrib := LeftDistrib C R F
  right_distrib := RightDistrib C R F
  mul_assoc := MulAssoc C R F

I get an error that "the rfl tactic failed", which is very strange to me since rfl is not used anywhere in this instance statement, and all of the lemmas work individually. Why is that? I can provide an MWE if necessary

[Eric Wieser]

rfl is being used in a proof for one of the fields you did not provide

[Eric Wieser]

My guess would be that it relates to natCast or intCast

[Eric Wieser]

You might be able to work out the field from the type mentioned in the error message

[VayusElytra]

How can I know what fields there are left that I did not provide?

[Matthew Ballard]

Manually currently. Write

instance EndRingIsRing (R : Type) [DivisionRing R] (C : Type) [Category C]
  (F : FunctCat C R) : Ring (EndRing C R F) := _

then click on the little :light_bulb: and choose maximal skeleton. That will give you all fields.

[VayusElytra]

Thank you! I'm not quite sure what field was problematic still, but specifying more of them does resolve this problem.

[Kevin Buzzard]

How can I know what fields there are left that I did not provide?

Another way is to look at the API docs for docs#Ring

[Eric Wieser]

Do we have an open issue somewhere about this error message being unhelpful and not mentioning the field name?

[Matthew Ballard]

Yes lean#2950

[Matthew Ballard]

Pretty popular too