Internal Categories

Stream: Is there code for X?

[Sina Hazratpour]

Has someone formalized internal categories? I could not find them on mathlib. I need them for a project, I'd be happy to formalize it but wanted to check if anyone has already done it.

[David Michael Roberts]

I'd love to know if and when you find out or do it yourself.

[David Michael Roberts]

What sort of ambient categories are you thinking of working in? Finitely complete? More general?

[Sina Hazratpour]

For my project, I was thinking of finitely complete categories as ambient categories. One source where internal categories are developed extensively is Street's "Categories in categories, and size matters": http://maths.mq.edu.au/~street/Cicasm.pdf

There is also the view of internal categories as monads in the bicategory of spans, but also the ambient category is finitely complete.

What do you have in mind as the more general framework? like

[David Michael Roberts]

For Mathlib, you really shouldn't assume finite completeness, as you'd not cover Lie groupoids. Definition 3.1 of http://www.tac.mta.ca/tac/volumes/30/55/30-55abs.html is a hint for the groupoid case. But it works more generally.

Ehresmann's sketched structures (finite limit sketches, here, or LE sketches) is another viewpoint.
Instead of giving objects of objects and morphisms, you also give the object of composable pairs together with a proof this is a pullback as needed (and an object for composable triples - cf section 4.9 of http://www.tac.mta.ca/tac/reprints/articles/12/tr12abs.html). And then for cases where you can construct things as a pullback, you get it for free.

I think Borceaux's Handbook and Johnstone's Elephant do a bit more on internal categories on top of Street's paper.

[Sina Hazratpour]

@David Michael Roberts Thanks for the references.
The definition you suggested is indeed more general than the one when we assume finite completeness, and it makes sense to aim for formalizing the more general definition.

[David Michael Roberts]

There's also https://arxiv.org/abs/1101.2363, if I may.

[Bhavik Mehta]

I made an attempt 5 years ago here: https://github.com/b-mehta/topos/blob/3e659c47be27494ceb4460be9a1236902aa388ee/src/internal_category.lean, but a lot has changed in mathlib since then! Looking at this code, I took the approach of Ehresmann as mentioned above, without finite completeness, but I only recall reading the Elephant at the time (it was a while ago though, so my memory of this is hazy!)

[Sina Hazratpour]

Thanks for sharing this @Bhavik Mehta .
Unless i don't read it correctly, it seem in the line 14 you do assume finite completeness.
https://github.com/b-mehta/topos/blob/3e659c47be27494ceb4460be9a1236902aa388ee/src/internal_category.lean#L14
i guess the only pullback we need is that of src and tgt, so can make that part of the data of the internal category structure.
Also, perhaps similar to the internal monoids in mathlib4, internal categories can be a class rather than structure.

[Bhavik Mehta]

Oops, you're correct, I linked the wrong version! That version does indeed assume finite completeness and have objects of objects and morphisms and not composable pairs. The one I was thinking about is here: https://github.com/b-mehta/topos/blob/master/src/internal_category.lean So it looks like I tried both approaches!

[pro-Lie stabilizer]

Internal categories can be taken to have 13 dependent summands not counting the extra entries for the existence of pullbacks and the entries used to pull back src and tgt.

The same dependent-summand-count idea gives 6 entries for an internal presheaf, such as the one defined in chapter 7 of Janelidze & Borceux ' s monograph Galois Theories. Including the internal category this entails 13 + 6 = 19. An internal natural transformation should have 4, and an internal functor has 6 (though the count there is not the same as the six in the internal presheaf).

@Bhavik Mehta Did you make any of these as well? It wouldn't be a bad idea to package these.

An endofunction Cat → Cat ensues from the approach in which no finite limits are assumed to exist, and in which internal functor is added to the considerations, since internal functors make an internal category (a cartesian closed one).

For the internal presheaf that twocategory problem isn't there: (X : Cat )→ (C : InternalCategory X) → Cat for the category of internal presheaves with internal presheaf morphisms (4 dependent summands).