4
$\begingroup$

In any category $\mathcal{C}$ with pullbacks, we can define an internal category $\mathscr{C}$ in $\mathcal{C}$ as an object ${\bf Ob}_\mathscr{C}$ of objects and an object ${\bf Hom}_\mathscr{C}$ of arrows, together with arrows $${\sf dom},{\sf cod}:{\bf Hom}_\mathscr{C}\rightrightarrows{\bf Ob}_\mathscr{C},$$ $$1^\mathscr{C}:{\bf Ob}_\mathscr{C}\to{\bf Hom}_\mathscr{C},$$ $$\circ^\mathscr{C}:{\bf Hom}_\mathscr{C}\times_{{\bf Ob}_\mathscr{C}}{\bf Hom}_\mathscr{C}\to{\bf Hom}_\mathscr{C}$$ satisfying the expected commutative diagrams. Where I'm slightly confused is the associativity axiom, since the 'object of composable triples' can be taken as either one of the two isomorphic options below

I have no problem showing that they're isomorphic and I understand that pullbacks are usually only defined up to isomorphism anyway, but when expressing the associativity axiom we technically need both to appear in the diagram:

I haven't seen mention of this on the nlab page linked above, or the introductions to internal categories in Jacob's fibered category theory book, or Borceux/Janelidze's Galois theories book, which makes me wonder if this is just overly pedantic, but when I went to construct an example of an internal category and prove it satisfied the axioms I ran into this issue in the proof.

Is there some well-known trick for sweeping things like this under the rug in computations, or do we need to keep track of isomorphisms between internal data for computations to shake out correctly?

Improve this question
$\endgroup$
16
  • 3
    $\begingroup$ This is usually swept under the rug, yes. Morally this is should be justified by the coherence theorem for monoidal categories but I don’t think it literally applies in this situation. $\endgroup$
    – Zhen Lin
    Mar 17, 2021 at 4:57
  • 3
    $\begingroup$ Also, this is a particular case of the general situation with monoids in any monoidal category (the one at hand being the monoidal category of endospans of the object of objects). $\endgroup$
    – მამუკა ჯიბლაძე
    Mar 17, 2021 at 5:12
  • 2
    $\begingroup$ In some treatments of internal categories, an in particular in some of Charles Ehresmann's old versions, the objects of composable pairs and triples is part of the data, so that internal categories are models of finite limit sketches, where the appropriate pullbacks are all given. $\endgroup$
    – David Roberts ♦
    Mar 17, 2021 at 6:28
  • 1
    $\begingroup$ Segal-style approaches to encoding associative and commutative structures avoid such problems by encoding objects of composable tuples separately, and then imposing an axiom that says that composable pairs are pullbacks of objects of arrows etc. The advantage of this is that the definition of an object itself can be concisely stated as a presheaf on Δ or Γ or a similar category, and then one only needs to state Segal's axioms. $\endgroup$
    – Dmitri Pavlov
    Mar 17, 2021 at 15:40
  • 3
    $\begingroup$ In the Elephant, a truncated version of Segal's approach is taken to defining internal categories (Def B 2.3.1). So the object of composable pairs is part of the data. $\endgroup$
    – Tim Campion ♦
    Mar 18, 2021 at 13:06

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.