zero_mul in ring instances

Stream: new members

[VayusElytra]

Hi, I am messing around with natural transformations and found something a little puzzling.

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)

variable (C : Type) [Category C]
variable (R : Type) [DivisionRing R]
variable (F : FunctCat C R)

--The 0 natural transformation from F to itself.
@[simp]
def ZeroEndomorphism : EndRing C R F where
  app X := 0

With these definitions I am defining a category of functors (from some category C to the category of K-modules for some ring K). Then EndRing is (or should be) the endomorphism ring of natural transformations from some functor F in my category to itself.
It has for a zero-object the natural transformation ZeroEndomorphism, which is just the 0 map for every component.
This is then part of the code to prove that this ring is indeed a ring:

--The endomorphism ring is a ring.
instance EndRingIsRing (R : Type) [DivisionRing R] (C : Type) [Category C]
  (F : FunctCat C R) : Ring (EndRing C R F) where
  add f g := f + g
  mul f g := g ≫ f --careful: f ⬝ g = f ∘ g here
  one := 𝟙 F
  zero := ZeroEndomorphism C R F
  zero_mul := by
    sorry

the tactic state immediately for zero_mul is: ∀ (a : EndRing C R F), 0 * a = 0, and hovering over 0 shows

@OfNat.ofNat (EndRing C R F) 0 Zero.toOfNat0 : EndRing C R F

What does this OfNat stuff mean? Is lean somehow interpreting the natural number 0 as an element of the endomorphism ring? I would really expect ZeroEndomorphism to show up somewhere, since that is what I defined as the zero element for this ring.

[Ruben Van de Velde]

OfNat is how numeric literals work in lean 4

[Ruben Van de Velde]

So @OfNat.ofNat (EndRing C R F) 0 Zero.toOfNat0 : EndRing C R F is the zero defined in the Zero instance for EndRing C R F

[VayusElytra]

Thank you very much, that is clear now!

[Eric Wieser]

This is surely a pretty-printing bug?

[VayusElytra]

What is pretty printing?

[Ira Fesefeldt]

Pretty printing is what is done to transform code into syntax in for example the infoview