The uniformization theorem

The main result in this file is IsCardinalAccessibleCategory.uniformization which says that if F : C ⥤ D is an accessible functor between accessible categories, there exists a regular cardinal κ such that C and D are κ-accessible categories, and F is a κ-accessible functor which preserves κ-presentable objects.

References

• Adámek, J. and Rosický, J., Locally presentable and accessible categories

theorem Cardinal.SharplyLT.exists_retract_of_isCardinalPresentable {κ₁ κ₂ : Cardinal.{w}} [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] (hκ : κ₁.SharplyLT κ₂) {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsCardinalAccessibleCategory C κ₁] (X : C) [CategoryTheory.IsCardinalPresentable X κ₂] : ∃ (Y : C) (x : CategoryTheory.Retract X Y) (J : Type w) (x : PartialOrder J), CategoryTheory.IsCardinalFiltered J κ₁ ∧ HasCardinalLT J κ₂ ∧ Nonempty ((CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J Y)

theorem CategoryTheory.IsCardinalAccessibleCategory.uniformization_aux {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) {κ₁ κ₂ : Cardinal.{w}} [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] [IsCardinalAccessibleCategory C κ₁] [IsCardinalAccessibleCategory D κ₁] [F.IsCardinalAccessible κ₁] (hκ : κ₁.SharplyLT κ₂) (hF : isCardinalPresentable C κ₁ ≤ (isCardinalPresentable D κ₂).inverseImage F) : F.PreservesCardinalPresentable κ₂

theorem CategoryTheory.IsCardinalAccessibleCategory.uniformization_of_small {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [IsAccessibleCategory.{w, v_1, u_1} C] [IsAccessibleCategory.{w, v_2, u_2} D] {ι : Type u_3} [Small.{w, u_3} ι] (F : ι → Functor C D) [∀ (i : ι), Functor.IsAccessible.{w, v_1, v_2, u_1, u_2} (F i)] : ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalAccessibleCategory C κ ∧ IsCardinalAccessibleCategory D κ ∧ (∀ (i : ι), (F i).IsCardinalAccessible κ) ∧ ∀ (i : ι), (F i).PreservesCardinalPresentable κ

Uniformization theorem for accessible categories: if F i : C ⥤ D for i : ι is a small family of accessible functors between accessible categories, there exists a regular cardinal κ such that C and D are κ-accessible, and the functors F i are κ-accessible functors which preserve κ-presentable objects.

theorem CategoryTheory.IsCardinalAccessibleCategory.uniformization {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [IsAccessibleCategory.{w, v_1, u_1} C] [IsAccessibleCategory.{w, v_2, u_2} D] (F : Functor C D) [Functor.IsAccessible.{w, v_1, v_2, u_1, u_2} F] : ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalAccessibleCategory C κ ∧ IsCardinalAccessibleCategory D κ ∧ F.IsCardinalAccessible κ ∧ F.PreservesCardinalPresentable κ

Uniformization theorem for accessible categories: if F is an accessible functor between accessible categories, there exists a regular cardinal κ such that C and D are κ-accessible, the functor F is κ-accessible and preserves κ-presentable objects.

theorem CategoryTheory.IsCardinalAccessibleCategory.uniformization_pair {C₁ : Type u_3} {C₂ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} [Category.{v_3, u_3} C₁] [Category.{v_4, u_4} C₂] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [IsAccessibleCategory.{w, v_3, u_3} C₁] [IsAccessibleCategory.{w, v_4, u_4} C₂] [IsAccessibleCategory.{w, v_5, u_5} D₁] [IsAccessibleCategory.{w, v_6, u_6} D₂] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) [Functor.IsAccessible.{w, v_3, v_5, u_3, u_5} F₁] [Functor.IsAccessible.{w, v_4, v_6, u_4, u_6} F₂] : ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalAccessibleCategory C₁ κ ∧ IsCardinalAccessibleCategory D₁ κ ∧ IsCardinalAccessibleCategory C₂ κ ∧ IsCardinalAccessibleCategory D₂ κ ∧ F₁.IsCardinalAccessible κ ∧ F₂.IsCardinalAccessible κ ∧ F₁.PreservesCardinalPresentable κ ∧ F₂.PreservesCardinalPresentable κ

If F₁ : C₁ ⥤ D₁ and F₂ : C₂ ⥤ D₂ are accessible functors between accessible categories, there exists a regular cardinal κ such that F₁ and F₂ are κ-accessible functors between κ-accessible categories and they preserve κ-presentable objects.