Comma categories are accessible #
Let F₁ : C₁ ⥤ D and F₂ : C₂ ⥤ D be κ-accessible functors between
κ-accessible categories. If we also assume that F₁ preserves κ-presentable
objects (a property which holds for a well chosen regular cardinal κ according to
the uniformization theorem, see the file
Mathlib/CategoryTheory/Presentable/Uniformization.lean), we show that
the comma category Comma F₁ F₂ is also κ-accessible (see the instance
Comma.isCardinalAccessibleCategory).
The key point in the technical proof is that if f : Comma F₁ F₂, then f
is the κ-filtered colimit (indexed by a category denoted J κ f here) of the
g : Comma F₁ F₂ equipped with a morphism g ⟶ f such that both g.left
and g.right are κ-presentable. In order to do this, we basically need
to show that the first and second functors π₁ : J κ f ⥤ J₁ κ f and
π₂ : J κ f ⥤ J₂ κ f are final (where J₁ κ f is the category of morphisms
X ⟶ f.left where X is κ-presentable, and similarly J₂ κ f is the
category of morphisms Y ⟶ f.right where Y is κ-presentable).
Then, the colimit of those g.left for g ⟶ f in J κ f identify to the
colimit of such X indexed by J₁ κ f which is f.left because
κ-presentable objects in C₁ form a dense full subcategory
(see the file Mathlib/CategoryTheory/Presentable/Dense.lean),
and similarly the colimit of those g.right for g ⟶ f in J κ f
identify to f.right.
References #
The property of objects in Comma F₁ F₂ which consists of
morphisms F₁.obj X₁ ⟶ F₂.obj X₂ where both X₁ abd X₂ are κ-presentable.
When both F₁ and F₂ are κ-accessible functors (between κ-accessible categories)
and F₁ preserves κ-presentable objects, we show that this property of objects
coincides with the κ-presentable objects of Comma F₁ F₂,
see the lemma Comma.isCardinalPresentable_eq.