Zulip Chat Archive

Stream: new members

Topic: comma category


view this post on Zulip Jakob Scholbach (Mar 29 2021 at 19:46):

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

view this post on Zulip 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

view this post on Zulip Jakob Scholbach (Mar 29 2021 at 19:53):

Aha!

view this post on Zulip 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

view this post on Zulip Jakob Scholbach (Mar 29 2021 at 19:59):

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

view this post on Zulip 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 :-)

view this post on Zulip Adam Topaz (Mar 29 2021 at 21:21):

@Jakob Scholbach note that we have docs#category_theory.comma.fst and docs#category_theory.comma.snd

view this post on Zulip Adam Topaz (Mar 29 2021 at 21:23):

What's going on with this topic BTW? It looks like at some point the topic no topic was renamed to comma category? :rofl:

view this post on Zulip Bryan Gin-ge Chen (Mar 29 2021 at 21:30):

Adam Topaz said:

What's going on with this topic BTW? It looks like at some point the topic no topic was renamed to comma category? :rofl:

Let me see if I can fix it...

view this post on Zulip Bryan Gin-ge Chen (Mar 29 2021 at 21:30):

OK, I think the topics are split now.


Last updated: May 14 2021 at 23:14 UTC