Comma categories are accessible #
Let F₁ : C₁ ⥤ D and F₂ : C₂ ⥤ D be accessible functors between
accessible categories, then Comma F₁ F₂ is also an accessible
category (Comma.isAccessibleCategory); similar results hold for Arrow,
CostructuredArrow, StructuredArrow, Under, Over categories.
This is obtained as a consequence of the uniformization theorem for accessible
categories (see the file Mathlib/CategoryTheory/Presentable/Uniformization.lean)
and the more precise result Comma.isCardinalAccessibleCategory which says that
Comma F₁ F₂ is a κ-accessible category when F₁ and F₂ are κ-accessible
functors between κ-accessible categories and that F₁ preserves
κ-presentable objects.
The key point in the technical proof of Comma.isCardinalAccessibleCategory
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 #
- [Adámek, J. and Rosický, J., Locally presentable and accessible categories][Adamek_Rosicky_1994]
instance
CategoryTheory.Comma.instHasCardinalFilteredColimits
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[F₁.IsCardinalAccessible κ]
[HasCardinalFilteredColimits C₁ κ]
[HasCardinalFilteredColimits C₂ κ]
:
HasCardinalFilteredColimits (Comma F₁ F₂) κ
instance
CategoryTheory.Comma.instIsCardinalAccessibleFst
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[F₁.IsCardinalAccessible κ]
[HasCardinalFilteredColimits C₁ κ]
[HasCardinalFilteredColimits C₂ κ]
:
(fst F₁ F₂).IsCardinalAccessible κ
instance
CategoryTheory.Comma.instIsCardinalAccessibleSnd
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[F₁.IsCardinalAccessible κ]
[HasCardinalFilteredColimits C₁ κ]
[HasCardinalFilteredColimits C₂ κ]
:
(snd F₁ F₂).IsCardinalAccessible κ
theorem
CategoryTheory.Comma.isCardinalPresentable_mk
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{F₁ : Functor C₁ D}
{F₂ : Functor C₂ D}
{κ : Cardinal.{w}}
[Fact κ.IsRegular]
{X₁ : C₁}
{X₂ : C₂}
[HasCardinalFilteredColimits C₁ κ]
[HasCardinalFilteredColimits C₂ κ]
[F₁.IsCardinalAccessible κ]
[F₂.IsCardinalAccessible κ]
[IsCardinalPresentable X₁ κ]
[IsCardinalPresentable X₂ κ]
[F₁.PreservesCardinalPresentable κ]
(f : F₁.obj X₁ ⟶ F₂.obj X₂)
:
IsCardinalPresentable { left := X₁, right := X₂, hom := f } κ
def
CategoryTheory.Comma.isCardinalPresentable
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
:
ObjectProperty (Comma F₁ F₂)
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.
Equations
Instances For
instance
CategoryTheory.Comma.instIsStableUnderRetractsIsCardinalPresentable
{C₁ : Type u_3}
{C₂ : Type u_4}
{D : Type u_6}
[Category.{u_1, u_3} C₁]
[Category.{u_2, u_4} C₂]
[Category.{u_5, u_6} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
(κ : Cardinal.{u_7})
[Fact κ.IsRegular]
:
theorem
CategoryTheory.Comma.isCardinalPresentable_le
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[HasCardinalFilteredColimits C₁ κ]
[HasCardinalFilteredColimits C₂ κ]
[F₁.IsCardinalAccessible κ]
[F₂.IsCardinalAccessible κ]
[F₁.PreservesCardinalPresentable κ]
:
instance
CategoryTheory.Comma.instEssentiallySmallIsCardinalPresentableOfIsCardinalPresentableOfLocallySmall
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[ObjectProperty.EssentiallySmall.{w, v_1, u_1} (isCardinalPresentable C₁ κ)]
[ObjectProperty.EssentiallySmall.{w, v_2, u_2} (isCardinalPresentable C₂ κ)]
[LocallySmall.{w, v_3, u_3} D]
:
instance
CategoryTheory.Comma.isCardinalAccessibleCategory.instIsDenseFullSubcategoryIsCardinalPresentableι
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{F₁ : Functor C₁ D}
{F₂ : Functor C₂ D}
{κ : Cardinal.{w}}
[Fact κ.IsRegular]
[IsCardinalAccessibleCategory C₁ κ]
[IsCardinalAccessibleCategory C₂ κ]
[F₁.IsCardinalAccessible κ]
[F₂.IsCardinalAccessible κ]
[F₁.PreservesCardinalPresentable κ]
[LocallySmall.{w, v_3, u_3} D]
:
(Comma.isCardinalPresentable F₁ F₂ κ).ι.IsDense
theorem
CategoryTheory.Comma.isCardinalFilteredGenerator_isCardinalPresentable
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[IsCardinalAccessibleCategory C₁ κ]
[IsCardinalAccessibleCategory C₂ κ]
[F₁.IsCardinalAccessible κ]
[F₂.IsCardinalAccessible κ]
[F₁.PreservesCardinalPresentable κ]
[LocallySmall.{w, v_3, u_3} D]
:
instance
CategoryTheory.Comma.isCardinalAccessibleCategory
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[IsCardinalAccessibleCategory C₁ κ]
[IsCardinalAccessibleCategory C₂ κ]
[F₁.IsCardinalAccessible κ]
[F₂.IsCardinalAccessible κ]
[F₁.PreservesCardinalPresentable κ]
[LocallySmall.{w, v_3, u_3} D]
:
IsCardinalAccessibleCategory (Comma F₁ F₂) κ
theorem
CategoryTheory.Comma.isCardinalPresentable_eq
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[IsCardinalAccessibleCategory C₁ κ]
[IsCardinalAccessibleCategory C₂ κ]
[F₁.IsCardinalAccessible κ]
[F₂.IsCardinalAccessible κ]
[F₁.PreservesCardinalPresentable κ]
[LocallySmall.{w, v_3, u_3} D]
:
theorem
CategoryTheory.Comma.isCardinalPresentable_iff
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{F₁ : Functor C₁ D}
{F₂ : Functor C₂ D}
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[IsCardinalAccessibleCategory C₁ κ]
[IsCardinalAccessibleCategory C₂ κ]
[F₁.IsCardinalAccessible κ]
[F₂.IsCardinalAccessible κ]
[F₁.PreservesCardinalPresentable κ]
[LocallySmall.{w, v_3, u_3} D]
(f : Comma F₁ F₂)
:
instance
CategoryTheory.Comma.instPreservesCardinalPresentableFst
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[IsCardinalAccessibleCategory C₁ κ]
[IsCardinalAccessibleCategory C₂ κ]
[F₁.IsCardinalAccessible κ]
[F₂.IsCardinalAccessible κ]
[F₁.PreservesCardinalPresentable κ]
[LocallySmall.{w, v_3, u_3} D]
:
(fst F₁ F₂).PreservesCardinalPresentable κ
instance
CategoryTheory.Comma.instPreservesCardinalPresentableSnd
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[IsCardinalAccessibleCategory C₁ κ]
[IsCardinalAccessibleCategory C₂ κ]
[F₁.IsCardinalAccessible κ]
[F₂.IsCardinalAccessible κ]
[F₁.PreservesCardinalPresentable κ]
[LocallySmall.{w, v_3, u_3} D]
:
(snd F₁ F₂).PreservesCardinalPresentable κ
instance
CategoryTheory.Comma.isAccessibleCategory
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
[LocallySmall.{w, v_3, u_3} D]
[IsAccessibleCategory.{w, v_1, u_1} C₁]
[IsAccessibleCategory.{w, v_2, u_2} C₂]
[Functor.IsAccessible.{w, v_1, v_3, u_1, u_3} F₁]
[Functor.IsAccessible.{w, v_2, v_3, u_2, u_3} F₂]
[IsAccessibleCategory.{w, v_3, u_3} D]
:
instance
CategoryTheory.Comma.instIsAccessibleFst
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
[IsAccessibleCategory.{w, v_1, u_1} C₁]
[IsAccessibleCategory.{w, v_2, u_2} C₂]
[Functor.IsAccessible.{w, v_1, v_3, u_1, u_3} F₁]
[Functor.IsAccessible.{w, v_2, v_3, u_2, u_3} F₂]
[IsAccessibleCategory.{w, v_3, u_3} D]
:
instance
CategoryTheory.Comma.instIsAccessibleSnd
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
(F₁ : Functor C₁ D)
(F₂ : Functor C₂ D)
[IsAccessibleCategory.{w, v_1, u_1} C₁]
[IsAccessibleCategory.{w, v_2, u_2} C₂]
[Functor.IsAccessible.{w, v_1, v_3, u_1, u_3} F₁]
[Functor.IsAccessible.{w, v_2, v_3, u_2, u_3} F₂]
[IsAccessibleCategory.{w, v_3, u_3} D]
:
instance
CategoryTheory.CostructuredArrow.instIsAccessibleCategory
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[IsAccessibleCategory.{w, v_1, u_1} C₁]
[IsAccessibleCategory.{w, v_2, u_2} C₂]
(F : Functor C₁ C₂)
[Functor.IsAccessible.{w, v_1, v_2, u_1, u_2} F]
(Y : C₂)
:
instance
CategoryTheory.CostructuredArrow.instIsAccessibleProj
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[IsAccessibleCategory.{w, v_1, u_1} C₁]
[IsAccessibleCategory.{w, v_2, u_2} C₂]
(F : Functor C₁ C₂)
[Functor.IsAccessible.{w, v_1, v_2, u_1, u_2} F]
(Y : C₂)
:
instance
CategoryTheory.StructuredArrow.instIsAccessibleCategory
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[IsAccessibleCategory.{w, v_1, u_1} C₁]
[IsAccessibleCategory.{w, v_2, u_2} C₂]
(F : Functor C₁ C₂)
[Functor.IsAccessible.{w, v_1, v_2, u_1, u_2} F]
(X : C₂)
:
instance
CategoryTheory.StructuredArrow.instIsAccessibleProj
{C₁ : Type u_1}
{C₂ : Type u_2}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[IsAccessibleCategory.{w, v_1, u_1} C₁]
[IsAccessibleCategory.{w, v_2, u_2} C₂]
(F : Functor C₁ C₂)
[Functor.IsAccessible.{w, v_1, v_2, u_1, u_2} F]
(X : C₂)
:
instance
CategoryTheory.Over.instIsAccessibleCategory
{D : Type u_3}
[Category.{v_3, u_3} D]
[IsAccessibleCategory.{w, v_3, u_3} D]
(Y : D)
:
instance
CategoryTheory.Over.instIsAccessibleForget
{D : Type u_3}
[Category.{v_3, u_3} D]
[IsAccessibleCategory.{w, v_3, u_3} D]
(Y : D)
:
instance
CategoryTheory.Under.instIsAccessibleCategory
{D : Type u_3}
[Category.{v_3, u_3} D]
[IsAccessibleCategory.{w, v_3, u_3} D]
(X : D)
:
instance
CategoryTheory.Under.instIsAccessibleForget
{D : Type u_3}
[Category.{v_3, u_3} D]
[IsAccessibleCategory.{w, v_3, u_3} D]
(X : D)
: