Functor.map name collision

Stream: mathlib4

[Richard Osborn]

I am currently looking at some category theory files and it looks at though Functor.map is being interpreted as the Functor.map from Init.Prelude. Is there a work around for this? CategoryTheory.Functor.map isn't recognized.

[Richard Osborn]

#mwe

import Mathlib.CategoryTheory.Functor.Basic

#check Functor.map -- Functor.map : (?m.5 → ?m.6) → ?m.3 ?m.5 → ?m.3 ?m.6
#check CategoryTheory.Functor.map -- ERROR: unknown constant 'CategoryTheory.Functor.map'

[Eric Wieser]

Does docs4#CategoryTheory.Functor.map exist?

[Eric Wieser]

I think it should refer to docs4#Prefunctor.map (docs#prefunctor.map)

[Eric Wieser]

This is the same problem as this thread

[Richard Osborn]

Ok, so if I want something like @Functor.map _ _ _ _ F X Y, I would need to write @Prefunctor.map _ _ _ _ F.toPrefunctor X Y? That's unfortunate if true.

[Richard Osborn]

Looks like this is hardly a solution. :(
#mwe

import Mathlib.CategoryTheory.Functor.Basic

namespace CategoryTheory

variable [Category.{u} C] [Category.{v} D]

class Faithful (F : C ⥤ D) : Prop where
  -- Want: map_injective : ∀ {X Y : C}, Function.Injective (@Functor.map C _ D _ F X Y) := by aesop_cat
  map_injective : ∀ {X Y : C}, Function.Injective (@Prefunctor.map C _ D _ F.toPrefunctor X Y) := by aesop_cat

-- Want: map_injective (F : C ⥤ D) [Faithful F] : Function.Injective <| (@Functor.map C _ D _ F X Y) :=
theorem map_injective (F : C ⥤ D) [Faithful F] : Function.Injective <| (@Prefunctor.map C _ D _ F.toPrefunctor X Y) :=
  -- Type Error: F has type  C ⥤ D
  -- Expected type: Prefunctor.map ?m.501.toPrefunctor ?m.505 = Prefunctor.map ?m.501.toPrefunctor ?m.506 : Prop
  Faithful.map_injective F

end CategoryTheory

I'm certainly not familiar enough with lean4 to know what to do instead.

[Scott Morrison]

That is a bit unfortunate, and I'm not seeing an easy workaround. In this particular case, it's not going to come up very often (we just don't talk about Functor.map as a function that often). Nearly always we have F.map f, which of course works fine.

[Scott Morrison]

You can leave porting notes at both map_injectives, but don't let this hold up a port.

[Reid Barton]

Does something like (F.map : (X \--> Y) \to (F.obj X \--> F.obj Y)) work?

[Richard Osborn]

I am still getting this type error in the proof of map_injective:

application type mismatch
  Faithful.map_injective F
argument
  F
has type
  C ⥤ D : Type (max u v u_1 u_2)
but is expected to have type
  Prefunctor.map ?m.794.toPrefunctor ?m.798 = Prefunctor.map ?m.794.toPrefunctor ?m.799 : Prop

[Scott Morrison]

Look at the type signature: F is implicit.

[Scott Morrison]

Back in mathlib3 we had

class faithful (F : C ⥤ D) : Prop :=
(map_injective' [] : ∀ {X Y : C}, function.injective (@functor.map _ _ _ _ F X Y) . obviously)

and the [] there made the F argument explicit.

[Scott Morrison]

As far as I can tell, there is no analogue of this in Lean 4, and so mathport just drops it.

[Scott Morrison]

But for here, just omitting the F suffices.

[Mario Carneiro]

Scott Morrison said:

That is a bit unfortunate, and I'm not seeing an easy workaround. In this particular case, it's not going to come up very often (we just don't talk about Functor.map as a function that often). Nearly always we have F.map f, which of course works fine.

In that case, can't you do (F.map \.)?