Fibered Categories

Stream: Displayed Categories

[Floris van Doorn]

Tim Lichtnau (a former - unfortunately deceased - student of mine) formalized fibered categories as his first project in Lean, for my course I taught 1.5 years ago. As a non-expert, those seem very similar to displayed categories (what are the differences?). His project is here, and maybe is helpful, perhaps just to get inspiration:
https://github.com/timlichtnau/LeanCourse23/tree/master/LeanCourse/Project

[Sina Hazratpour 𓃵]

Thanks @Floris van Doorn for bringing this up, i was not aware of this. I see that Tim followed the fibration notes of Thomas Streicher -- who also very unfortunately passed away recently -- quite closely in his formalization, which is great! I'm sure there will be things there that we can borrow from his formalization, of course giving credit to his work as well.

[Fernando Chu]

As for the question of what are the differences, it is mostly just a matter of presentation. Displayed categories is a notion of fibered categories tailored to MLTT, the idea is that the fibers overs some category C are encoded as a function D : C -> Type, so that that the fiber over c : C is just D c, in contrast of having to take a subtype, which gives rise to eqToHom problems.

[Sina Hazratpour 𓃵]

And i think, crucially, displayed categories do not use equality of objects in their definition while Grothendieck fibrations do. Working with equality of objects in categories, and especially rewriting along them is painful and leads to the dTT hell.

[Floris van Doorn]

Yes. Tim worked around that by not rewriting with equalities of objects, but only using eqToHom to constructor an (iso)morphism from an equality.

[Sina Hazratpour 𓃵]

Indeed, using eqToHom to promote equalities to isos is the standard "trick" we use in mathlib for dealing with equality of objects. Displayed categories offer an alternative approach where instead of being bothered by equality of objects, we shift the problem to the dependent equality of morphisms, so for instance we have an axiom id_comp_cast as part of the definition of displayed categories which says

(𝟙ₒ X) ≫ₒ g = (id_comp f).symm ▸ g

Here morphism g lives in some would-be-category D and lies over a morphism f in C, and the displayed composition (𝟙ₒ X) ≫ₒ g lies over the composition 𝟙 ≫ f in C which is equal to f by id_comp. So, here we also rewrite along equalities, but rather equality of morphisms than objects. If you have a functor P : E ⥤ C the fibres (strict, iso, lax) give you different displayed structures, see for instance:
https://github.com/sinhp/displayed_categories/blob/e42efa2e244c1c285dc1c269af70755dd11ae90f/DisplayedCategories/Basic.lean#L547

[Sina Hazratpour 𓃵]

By the way, the potential to use displayed categories was mentioned by @Reid Barton here, but so far, I don't think we had a Lean formalization of them.

[Johan Commelin]

@Sina Hazratpour 𓃵 that link is broken

[Sina Hazratpour 𓃵]

Johan Commelin said:

Sina Hazratpour 𓃵 that link is broken

thanks, fixed!