Zulip Chat Archive

Stream: Is there code for X?

Topic: Category of diagrams


view this post on Zulip Adam Topaz (Mar 01 2021 at 22:02):

I'm looking for some construction of "the category of diagrams" along the following lines:

import category_theory.eq_to_hom
import category_theory.whiskering
import category_theory.essential_image

open category_theory

universes v u
variables (C : Type u) [category.{v} C]

@[ext]
structure diagram :=
(J : Type v)
[small_cat : small_category J]
(F : J  C)

namespace diagram

variable {C}

instance : has_coe_to_sort (diagram C) := Type v, λ X, X.J
instance {X : diagram C} : small_category X := X.small_cat

@[ext]
structure hom (X Y : diagram C) :=
(i : X  Y)
(j : X.F.ess_image  Y.F.ess_image)
(comm : i  Y.F.to_ess_image  X.F.to_ess_image  j)

@[simps]
def id (X : diagram C) : hom X X :=
{ i := functor.id _,
  j := functor.id _,
  comm :=
  { hom := 𝟙 _,
    inv := 𝟙 _  } }

@[simps]
def comp {X Y Z : diagram C} (f : hom X Y) (g : hom Y Z) : hom X Z :=
{ i := f.i  g.i,
  j := f.j  g.j,
  comm :=
    functor.associator f.i g.i _ ≪≫
    iso_whisker_left f.i g.comm ≪≫
    (functor.associator _ _ _).symm ≪≫
    iso_whisker_right f.comm g.j ≪≫
    functor.associator _ f.j g.j }

instance : category (diagram C) :=
{ hom := hom,
  id := λ X, id _,
  comp := λ X Y Z, comp,
  id_comp' := begin
    intros a b f,
    ext,
    { apply category_theory.functor.ext, tidy },
    { apply category_theory.functor.ext, tidy },
    recover,
    tidy,
  end,
  comp_id' := begin
    intros a b f,
    ext,
    { apply category_theory.functor.ext, tidy },
    { apply category_theory.functor.ext, tidy },
    recover,
    tidy,
  end,
  assoc' := begin
    intros a b c d f g h,
    ext,
    { apply category_theory.functor.ext, tidy },
    { apply category_theory.functor.ext, tidy },
    recover,
    tidy,
  end }

end diagram

And while I'm asking, I also don't really understand why recover is necessary in the last few proofs (I get an error if these lines are removed).
Finally, if someone has any ideas about how to make this construction less "evil" (due to the use of category_theory.functor.ext), that would also be helpful!

view this post on Zulip Scott Morrison (Mar 01 2021 at 23:20):

Isn't this construction just inherently 'evil'? There's a 2-category of diagrams that wouldn't be.

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

Yeah, youre right.

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

I just never imagined that something so mundane like the category of diagrams should really be a 2-category.

view this post on Zulip Adam Topaz (Mar 01 2021 at 23:25):

But I guess whenever you need to talk about commuting diagrams of functors, you're forced into 2-categories.


Last updated: May 16 2021 at 05:21 UTC