Zulip Chat Archive

another newbie question: I want to define a projection functor from a comma category. In one case this works, in the other it doesn't -- why?
(The error message I get in the first case is type mismatch at field 'obj' λ (X : comma L R), X.left has type comma L R → auto_param A (name.mk_string "obviously" name.anonymous) but is expected to have type comma L R → A_1

import category_theory.comma

namespace category_theory

universes v v₁ v₂ v₃ u u₁ u₂ u₃
variables {A : Type u₁} [category.{v} A]
variables {B : Type u₂} [category.{v} B]
variables {T : Type u₃} [category.{v} T]

variables {L : A ⥤ T} {R : B ⥤ T}

def proj_left_fails {A : Type u₁} [category.{v} A] {B : Type u₂} [category.{v} B] {T : Type u₃} [category.{v} T] :
  (comma.{v v v} L R) ⥤ A :=
{ obj := λ X , X.left,
  map := λ X Y f, f.left }

def proj_left_works : (comma.{v v v} L R) ⥤ A :=
{ obj := λ X, X.left,
  map := λ X Y f, f.left }

end category_theory

Markus Himmel (Mar 29 2021 at 19:52):

In the first case, you have two different things called A, and L and R are declared using the first A, but the A in (comma L R) \func A is the second A

Jakob Scholbach (Mar 29 2021 at 19:53):

Aha!

Markus Himmel (Mar 29 2021 at 19:55):

The error message tries to hint at this by calling them A and A_1, but the auto_param stuff (which can be ignored) obscures this

Jakob Scholbach (Mar 29 2021 at 19:59):

OK, I see. Will watch out for _1 in the future...

Kevin Buzzard (Mar 29 2021 at 20:12):

The trick with all that autoparam nonsense is to just note that you can just cross out the auto_param and also the name.mk_string stuff and then it's easier to read what it actually says :-)