diff --git a/Mathlib.lean b/Mathlib.lean index b84b3d08209ed8..17c42a8e0c67f1 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3275,19 +3275,25 @@ public import Mathlib.CategoryTheory.Presentable.Basic public import Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset public import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation public import Mathlib.CategoryTheory.Presentable.ColimitPresentation +public import Mathlib.CategoryTheory.Presentable.Comma public import Mathlib.CategoryTheory.Presentable.Dense public import Mathlib.CategoryTheory.Presentable.Directed public import Mathlib.CategoryTheory.Presentable.EssentiallyLarge public import Mathlib.CategoryTheory.Presentable.Finite public import Mathlib.CategoryTheory.Presentable.IsCardinalFiltered +public import Mathlib.CategoryTheory.Presentable.IsDiscrete public import Mathlib.CategoryTheory.Presentable.Limits public import Mathlib.CategoryTheory.Presentable.LocallyPresentable public import Mathlib.CategoryTheory.Presentable.OrthogonalReflection +public import Mathlib.CategoryTheory.Presentable.PreservesCardinalPresentable public import Mathlib.CategoryTheory.Presentable.Presheaf public import Mathlib.CategoryTheory.Presentable.Retracts public import Mathlib.CategoryTheory.Presentable.SharplyLT.Basic +public import Mathlib.CategoryTheory.Presentable.SharplyLT.Lemmas +public import Mathlib.CategoryTheory.Presentable.SolutionSetCondition public import Mathlib.CategoryTheory.Presentable.StrongGenerator public import Mathlib.CategoryTheory.Presentable.Type +public import Mathlib.CategoryTheory.Presentable.Uniformization public import Mathlib.CategoryTheory.Products.Associator public import Mathlib.CategoryTheory.Products.Basic public import Mathlib.CategoryTheory.Products.Bifunctor diff --git a/Mathlib/CategoryTheory/Comma/CardinalArrow.lean b/Mathlib/CategoryTheory/Comma/CardinalArrow.lean index b1f67c4c554b52..8c3a8df7e69dfa 100644 --- a/Mathlib/CategoryTheory/Comma/CardinalArrow.lean +++ b/Mathlib/CategoryTheory/Comma/CardinalArrow.lean @@ -5,10 +5,8 @@ Authors: Joël Riou -/ module -public import Mathlib.CategoryTheory.Comma.Arrow -public import Mathlib.CategoryTheory.FinCategory.Basic public import Mathlib.CategoryTheory.EssentiallySmall -public import Mathlib.Data.Set.Finite.Basic +public import Mathlib.CategoryTheory.FinCategory.Basic public import Mathlib.SetTheory.Cardinal.HasCardinalLT /-! @@ -114,4 +112,13 @@ lemma hasCardinalLT_of_hasCardinalLT_arrow HasCardinalLT C κ := h.of_injective (fun X ↦ Arrow.mk (𝟙 X)) (fun _ _ h ↦ congr_arg Comma.left h) +lemma hasCardinalLT_arrow_iff_of_isThin (C : Type u) [Category.{v} C] + [Quiver.IsThin C] (κ : Cardinal.{w}) (hκ : Cardinal.aleph0 ≤ κ) : + HasCardinalLT (Arrow C) κ ↔ HasCardinalLT C κ := + ⟨hasCardinalLT_of_hasCardinalLT_arrow, fun h ↦ + (hasCardinalLT_prod hκ h h).of_injective (fun f ↦ (f.left, f.right)) + (fun f g h ↦ + Arrow.ext (congr_arg _root_.Prod.fst h) (congr_arg _root_.Prod.snd h) + (by subsingleton))⟩ + end CategoryTheory diff --git a/Mathlib/CategoryTheory/EssentiallySmall.lean b/Mathlib/CategoryTheory/EssentiallySmall.lean index 6dd48924118145..ae5c40ff86c720 100644 --- a/Mathlib/CategoryTheory/EssentiallySmall.lean +++ b/Mathlib/CategoryTheory/EssentiallySmall.lean @@ -25,7 +25,6 @@ the type `Skeleton C` is `w`-small, and `C` is `w`-locally small. @[expose] public section - universe w w' v v' u u' open CategoryTheory diff --git a/Mathlib/CategoryTheory/Limits/Comma.lean b/Mathlib/CategoryTheory/Limits/Comma.lean index 31172ac7aeb408..d466ee5bc80337 100644 --- a/Mathlib/CategoryTheory/Limits/Comma.lean +++ b/Mathlib/CategoryTheory/Limits/Comma.lean @@ -71,25 +71,39 @@ noncomputable def coneOfPreserves [PreservesLimit (F ⋙ snd L R) R] (c₁ : Con · simp [← c₁.w t] · simp [← c₂.w t] } -set_option backward.isDefEq.respectTransparency false in +set_option backward.defeqAttrib.useBackward true in +/-- Let `F : J ⥤ Comma L R`. If `R` preserves the limit of +`F ⋙ snd _ _`, then `Comma.fst L R` and `Comma.snd L R` jointly +reflect the limit of `F`, i.e. if `c` is a cone for `F` which +becomes a limit after applying `Comma.fst L R` and `Comma.snd L R`, +then `c` is a limit. -/ +def fstSndJointlyReflectLimit {F : J ⥤ Comma L R} {c : Cone F} + [PreservesLimit (F ⋙ snd _ _) R] + (h₁ : IsLimit ((fst _ _).mapCone c)) + (h₂ : IsLimit ((snd _ _).mapCone c)) : + IsLimit c where + lift s := + { left := h₁.lift ((fst _ _).mapCone s) + right := h₂.lift ((snd _ _).mapCone s) + w := (isLimitOfPreserves R h₂).hom_ext (fun j ↦ by + simp [← Functor.map_comp, ← Functor.map_comp_assoc, ← CommaMorphism.w, + dsimp% h₂.fac ((snd _ _).mapCone s) j, + dsimp% h₁.fac ((fst _ _).mapCone s) j]) } + fac s j := by + ext + · exact h₁.fac ((fst _ _).mapCone s) j + · exact h₂.fac ((snd _ _).mapCone s) j + uniq s _ hm := by + ext + · exact h₁.uniq ((fst _ _).mapCone s) _ (by simp [← hm]) + · exact h₂.uniq ((snd _ _).mapCone s) _ (by simp [← hm]) + /-- Provided that `R` preserves the appropriate limit, then the cone in `coneOfPreserves` is a limit. -/ noncomputable def coneOfPreservesIsLimit [PreservesLimit (F ⋙ snd L R) R] {c₁ : Cone (F ⋙ fst L R)} (t₁ : IsLimit c₁) {c₂ : Cone (F ⋙ snd L R)} (t₂ : IsLimit c₂) : - IsLimit (coneOfPreserves F c₁ t₂) where - lift s := - { left := t₁.lift ((fst L R).mapCone s) - right := t₂.lift ((snd L R).mapCone s) - w := - (isLimitOfPreserves R t₂).hom_ext fun j => by - rw [coneOfPreserves_pt_hom, assoc, assoc, (isLimitOfPreserves R t₂).fac, - limitAuxiliaryCone_π_app, ← L.map_comp_assoc, t₁.fac, R.mapCone_π_app, - ← R.map_comp, t₂.fac] - exact (s.π.app j).w } - uniq s m w := by - apply CommaMorphism.ext - · exact t₁.uniq ((fst L R).mapCone s) _ (fun j => by simp [← w]) - · exact t₂.uniq ((snd L R).mapCone s) _ (fun j => by simp [← w]) + IsLimit (coneOfPreserves F c₁ t₂) := + fstSndJointlyReflectLimit t₁ t₂ /-- (Implementation). An auxiliary cocone which is useful in order to construct colimits in the comma category. -/ @@ -120,26 +134,40 @@ noncomputable def coconeOfPreserves [PreservesColimit (F ⋙ fst L R) L] {c₁ : · simp [← c₁.w t] · simp [← c₂.w t] } -set_option backward.isDefEq.respectTransparency false in +set_option backward.defeqAttrib.useBackward true in +/-- Let `F : J ⥤ Comma L R`. If `L` preserves the colimit of +`F ⋙ fst _ _`, then `Comma.fst L R` and `Comma.snd L R` jointly +reflect the colimit of `F`, i.e. if `c` is a cocone for `F` which +becomes a colimit after applying `Comma.fst L R` and `Comma.snd L R`, +then `c` is a colimit. -/ +def fstSndJointlyReflectColimit {F : J ⥤ Comma L R} {c : Cocone F} + [PreservesColimit (F ⋙ fst _ _) L] + (h₁ : IsColimit ((fst _ _).mapCocone c)) + (h₂ : IsColimit ((snd _ _).mapCocone c)) : + IsColimit c where + desc s := + { left := h₁.desc ((fst _ _).mapCocone s) + right := h₂.desc ((snd _ _).mapCocone s) + w := (isColimitOfPreserves L h₁).hom_ext (fun j ↦ by + simp [← Functor.map_comp_assoc, ← Functor.map_comp, + dsimp% h₁.fac ((fst _ _).mapCocone s) j, + dsimp% h₂.fac ((snd _ _).mapCocone s) j]) } + fac s j := by + ext + · exact h₁.fac ((fst _ _).mapCocone s) j + · exact h₂.fac ((snd _ _).mapCocone s) j + uniq s _ hm := by + ext + · exact h₁.uniq ((fst _ _).mapCocone s) _ (by simp [← hm]) + · exact h₂.uniq ((snd _ _).mapCocone s) _ (by simp [← hm]) + /-- Provided that `L` preserves the appropriate colimit, then the cocone in `coconeOfPreserves` is a colimit. -/ noncomputable def coconeOfPreservesIsColimit [PreservesColimit (F ⋙ fst L R) L] {c₁ : Cocone (F ⋙ fst L R)} (t₁ : IsColimit c₁) {c₂ : Cocone (F ⋙ snd L R)} (t₂ : IsColimit c₂) : - IsColimit (coconeOfPreserves F t₁ c₂) where - desc s := - { left := t₁.desc ((fst L R).mapCocone s) - right := t₂.desc ((snd L R).mapCocone s) - w := - (isColimitOfPreserves L t₁).hom_ext fun j => by - rw [coconeOfPreserves_pt_hom, (isColimitOfPreserves L t₁).fac_assoc, - colimitAuxiliaryCocone_ι_app, assoc, ← R.map_comp, t₂.fac, L.mapCocone_ι_app, ← - L.map_comp_assoc, t₁.fac] - exact (s.ι.app j).w } - uniq s m w := by - apply CommaMorphism.ext - · exact t₁.uniq ((fst L R).mapCocone s) _ (fun j => by simp [← w]) - · exact t₂.uniq ((snd L R).mapCocone s) _ (fun j => by simp [← w]) + IsColimit (coconeOfPreserves F t₁ c₂) := + fstSndJointlyReflectColimit t₁ t₂ instance hasLimit (F : J ⥤ Comma L R) [HasLimit (F ⋙ fst L R)] [HasLimit (F ⋙ snd L R)] [PreservesLimit (F ⋙ snd L R) R] : HasLimit F := diff --git a/Mathlib/CategoryTheory/ObjectProperty/Small.lean b/Mathlib/CategoryTheory/ObjectProperty/Small.lean index b78a4eb6bc8e70..f2a8189732d657 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Small.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Small.lean @@ -41,6 +41,17 @@ lemma Small.of_le {P Q : ObjectProperty C} [ObjectProperty.Small.{w} Q] (h : P ObjectProperty.Small.{w} P := small_of_injective (Subtype.map_injective h Function.injective_id) +lemma Small.exists_eq_ofObj (P : ObjectProperty C) [ObjectProperty.Small.{w} P] : + ∃ (ι : Type w) (X : ι → C), P = .ofObj X := + ⟨Shrink.{w} (Subtype P), fun i ↦ ((equivShrink _).symm i).val, + le_antisymm (fun X hX ↦ by + rw [ofObj_iff] + exact ⟨equivShrink _ ⟨X, hX⟩, by simp⟩) (by + rw [ofObj_le_iff] + intro i + obtain ⟨X, rfl⟩ := (equivShrink _).surjective i + simpa using X.prop)⟩ + instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] : ObjectProperty.Small.{w} P.op := small_of_injective P.subtypeOpEquiv.injective @@ -141,6 +152,14 @@ lemma EssentiallySmall.exists_small (P : ObjectProperty C) [P.IsClosedUnderIsomo obtain ⟨Q, _, hQ₁, hQ₂⟩ := exists_small_le P exact ⟨Q, inferInstance, le_antisymm hQ₂ (by rwa [isoClosure_le_iff])⟩ +lemma EssentiallySmall.exists_eq_isoClosure_ofObj + (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] + [ObjectProperty.EssentiallySmall.{w} P] : + ∃ (ι : Type w) (X : ι → C), P = (ObjectProperty.ofObj X).isoClosure := by + obtain ⟨P₀, _, h⟩ := exists_small.{w} P + obtain ⟨ι, X, rfl⟩ := Small.exists_eq_ofObj.{w} P₀ + exact ⟨ι, X, h⟩ + lemma EssentiallySmall.of_le {P Q : ObjectProperty C} [ObjectProperty.EssentiallySmall.{w} Q] (h : P ≤ Q) : ObjectProperty.EssentiallySmall.{w} P where diff --git a/Mathlib/CategoryTheory/Presentable/Basic.lean b/Mathlib/CategoryTheory/Presentable/Basic.lean index f1d14fbe781e7c..96769b61ee0d70 100644 --- a/Mathlib/CategoryTheory/Presentable/Basic.lean +++ b/Mathlib/CategoryTheory/Presentable/Basic.lean @@ -5,12 +5,8 @@ Authors: Joël Riou -/ module -public import Mathlib.CategoryTheory.Adjunction.Limits public import Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant -public import Mathlib.CategoryTheory.Limits.Preserves.Ulift -public import Mathlib.CategoryTheory.Limits.Types.Filtered public import Mathlib.CategoryTheory.Presentable.IsCardinalFiltered -public import Mathlib.SetTheory.Cardinal.HasCardinalLT /-! # Presentable objects @@ -22,7 +18,7 @@ a regular cardinal `κ` such that `Functor.IsCardinalAccessible`. An object `X` of a category is `κ`-presentable (`IsCardinalPresentable`) if the functor `Hom(X, _)` (i.e. `coyoneda.obj (op X)`) is `κ`-accessible. -Similarly as for accessible functors, we define a type class `IsAccessible`. +Similarly as for accessible functors, we define a type class `IsPresentable`. ## References * [Adámek, J. and Rosický, J., *Locally presentable and accessible categories*][Adamek_Rosicky_1994] @@ -110,18 +106,21 @@ end section -variable (F : C ⥤ D) - /-- A functor is accessible relative to a universe `w` if it is `κ`-accessible for some regular `κ : Cardinal.{w}`. -/ @[pp_with_univ] -class IsAccessible : Prop where - exists_cardinal : ∃ (κ : Cardinal.{w}) (_ : Fact κ.IsRegular), IsCardinalAccessible F κ +class IsAccessible (F : C ⥤ D) : Prop where + exists_cardinal (F) : ∃ (κ : Cardinal.{w}) (_ : Fact κ.IsRegular), IsCardinalAccessible F κ + +variable (F : C ⥤ D) lemma isAccessible_of_isCardinalAccessible (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalAccessible F κ] : IsAccessible.{w} F where exists_cardinal := ⟨κ, inferInstance, inferInstance⟩ +instance : IsAccessible.{w} (𝟭 C) := + ⟨.aleph0, Cardinal.fact_isRegular_aleph0, inferInstance⟩ + instance {E : Type u₃} [Category.{v₃} E] (F : C ⥤ D) (G : D ⥤ E) [IsAccessible.{w} F] [IsAccessible.{w} G] : IsAccessible.{w} (F ⋙ G) := by obtain ⟨κF, _, _⟩ := IsAccessible.exists_cardinal (F := F) @@ -150,7 +149,7 @@ abbrev IsCardinalPresentable : Prop := (coyoneda.obj (op X)).IsCardinalAccessibl variable (C) in /-- The property of objects that are `κ`-presentable. -/ -def isCardinalPresentable : ObjectProperty C := fun X ↦ IsCardinalPresentable X κ +abbrev isCardinalPresentable : ObjectProperty C := fun X ↦ IsCardinalPresentable X κ instance (X : (isCardinalPresentable C κ).FullSubcategory) : IsCardinalPresentable X.obj κ := @@ -237,6 +236,33 @@ lemma isCardinalPresentable_iff_of_isEquivalence · intro infer_instance +variable {X κ} in +set_option backward.isDefEq.respectTransparency false in +set_option backward.defeqAttrib.useBackward true in +open IsFiltered in +lemma IsCardinalPresentable.mk + (hX : ∀ (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] + (F : J ⥤ C) (c : Cocone F) (_ : IsColimit c), + (∀ (g : X ⟶ c.pt), ∃ (j : J) (f : X ⟶ F.obj j), f ≫ c.ι.app j = g) ∧ + (∀ (j : J) (f₁ f₂ : X ⟶ F.obj j) (_ : f₁ ≫ c.ι.app j = f₂ ≫ c.ι.app j), + ∃ (j' : J) (a : j ⟶ j'), f₁ ≫ F.map a = f₂ ≫ F.map a)) : + IsCardinalPresentable X κ where + preservesColimitOfShape J _ _ := + ⟨fun {F} ↦ ⟨fun {c} hc ↦ by + have := isFiltered_of_isCardinalFiltered J κ + rw [Types.isColimit_iff_coconeTypesIsColimit] + refine ⟨fun f₁ f₂ hf ↦ ?_, fun g ↦ ?_⟩ + · obtain ⟨j₁, f₁, rfl⟩ := Functor.ιColimitType_jointly_surjective _ f₁ + obtain ⟨j₂, f₂, rfl⟩ := Functor.ιColimitType_jointly_surjective _ f₂ + dsimp at f₁ f₂ hf + obtain ⟨j', a, ha⟩ := (hX J F c hc).2 _ (f₁ ≫ F.map (leftToMax j₁ j₂)) + (f₂ ≫ F.map (rightToMax j₁ j₂)) (by simpa) + simp only [Category.assoc] at ha + exact Functor.ιColimitType_eq_of_map_eq_map _ _ _ + (leftToMax j₁ j₂ ≫ a) (rightToMax j₁ j₂ ≫ a) (by simpa) + · obtain ⟨j, f, rfl⟩ := (hX J F c hc).1 g + exact ⟨Functor.ιColimitType _ j f, rfl⟩⟩⟩ + section variable {J : Type*} [Category* J] {D : J ⥤ C} @@ -344,18 +370,27 @@ end section -variable (C) (κ : Cardinal.{w}) [Fact κ.IsRegular] - /-- A category has `κ`-filtered colimits if it has colimits of shape `J` for any `κ`-filtered category `J`. -/ -class HasCardinalFilteredColimits : Prop where - hasColimitsOfShape (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] : +class HasCardinalFilteredColimits + (C : Type u₁) [Category.{v₁} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : Prop where + hasColimitsOfShape (C) (κ) (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] : HasColimitsOfShape J C := by intros; infer_instance attribute [instance] HasCardinalFilteredColimits.hasColimitsOfShape +variable (C) (κ : Cardinal.{w}) [Fact κ.IsRegular] + instance [HasColimitsOfSize.{w, w} C] : HasCardinalFilteredColimits.{w} C κ where +variable {κ} in +lemma HasCardinalFilteredColimits.of_le + [HasCardinalFilteredColimits C κ] {κ' : Cardinal.{w}} [Fact κ'.IsRegular] (h : κ ≤ κ') : + HasCardinalFilteredColimits C κ' where + hasColimitsOfShape J _ _ := by + have := IsCardinalFiltered.of_le J h + exact HasCardinalFilteredColimits.hasColimitsOfShape C κ J + end end CategoryTheory diff --git a/Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean b/Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean index ea4d3d2bcf4dd8..cfaea70ce4c809 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean @@ -5,10 +5,9 @@ Authors: Joël Riou -/ module -public import Mathlib.CategoryTheory.ObjectProperty.Small +public import Mathlib.CategoryTheory.Generator.StrongGenerator public import Mathlib.CategoryTheory.Presentable.Limits public import Mathlib.CategoryTheory.Presentable.Retracts -public import Mathlib.CategoryTheory.Generator.StrongGenerator /-! # Presentable generators @@ -33,7 +32,7 @@ such that `P.IsCardinalFilteredGenerator κ` holds. public section -universe w v u +universe w₁ w₂ w v u namespace CategoryTheory @@ -41,6 +40,10 @@ variable {C : Type u} [Category.{v} C] namespace Limits.ColimitPresentation +/-- If an object `X` admits a presentation `p` as a colimit of +a functor `p.diag : J ⥤ C` with values in `κ`-presentable objects, +then `X` is `κ'`-presentable if `κ ≤ κ'` and the cardinality +of `Arrow J` is `< κ'`. -/ lemma isCardinalPresentable {X : C} {J : Type w} [SmallCategory J] (p : ColimitPresentation J X) (κ : Cardinal.{w}) [Fact κ.IsRegular] (h : ∀ (j : J), IsCardinalPresentable (p.diag.obj j) κ) [LocallySmall.{w} C] @@ -58,6 +61,11 @@ namespace ObjectProperty variable {P : ObjectProperty C} +/-- If an object `X` admits a presentation `p : P.ColimitsOfShape J X` +as a colimit of a functor `p.diag : J ⥤ C` with values in objects +satisfying a property `P` such that `P ≤ isCardinalPresentable C κ`, +then `X` is `κ'`-presentable if `κ ≤ κ'` and the cardinality +of `Arrow J` is `< κ'`. -/ lemma ColimitOfShape.isCardinalPresentable {X : C} {J : Type w} [SmallCategory J] (p : P.ColimitOfShape J X) {κ : Cardinal.{w}} [Fact κ.IsRegular] (hP : P ≤ isCardinalPresentable C κ) [LocallySmall.{w} C] @@ -83,6 +91,17 @@ structure IsCardinalFilteredGenerator : Prop where namespace IsCardinalFilteredGenerator +lemma mk' (h₁ : P ≤ isCardinalPresentable C κ) + (h₂ : ∀ (X : C), ∃ (J : Type w₁) (_ : Category.{w₂} J) + (_ : EssentiallySmall.{w} J) (_ : IsCardinalFiltered J κ), P.colimitsOfShape J X) : + P.IsCardinalFilteredGenerator κ where + le_isCardinalPresentable := h₁ + exists_colimitsOfShape X := by + obtain ⟨J, _, _, _, p⟩ := h₂ X + exact ⟨SmallModel.{w} J, inferInstance, + IsCardinalFiltered.of_equivalence κ (equivSmallModel.{w} J), + by rwa [← P.colimitsOfShape_congr (equivSmallModel.{w} J)]⟩ + variable (h : P.IsCardinalFilteredGenerator κ) (X : C) include h in diff --git a/Mathlib/CategoryTheory/Presentable/Comma.lean b/Mathlib/CategoryTheory/Presentable/Comma.lean new file mode 100644 index 00000000000000..9b9244bcb904e5 --- /dev/null +++ b/Mathlib/CategoryTheory/Presentable/Comma.lean @@ -0,0 +1,502 @@ +/- +Copyright (c) 2024 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.CategoryTheory.Presentable.Dense +public import Mathlib.CategoryTheory.Presentable.IsDiscrete +public import Mathlib.CategoryTheory.Presentable.Uniformization +public import Mathlib.CategoryTheory.Presentable.LocallyPresentable +public import Mathlib.CategoryTheory.Limits.Comma +public import Mathlib.CategoryTheory.Limits.Final +public import Mathlib.CategoryTheory.Comma.LocallySmall +public import Mathlib.CategoryTheory.ObjectProperty.Comma + +/-! +# Comma categories are accessible + +-/ + +universe w v₁ v₂ v₃ u₁ u₂ u₃ + +@[expose] public section + +namespace CategoryTheory + +open Limits + +variable {C₁ : Type u₁} [Category.{v₁} C₁] {C₂ : Type u₂} [Category.{v₂} C₂] + {D : Type u₃} [Category.{v₃} D] + +namespace Comma + +variable (F₁ : C₁ ⥤ D) (F₂ : C₂ ⥤ D) + +section + +variable (κ : Cardinal.{w}) [Fact κ.IsRegular] + [HasCardinalFilteredColimits C₁ κ] [HasCardinalFilteredColimits C₂ κ] + [F₁.IsCardinalAccessible κ] + +instance : HasCardinalFilteredColimits (Comma F₁ F₂) κ where + hasColimitsOfShape J _ _ := by + have := Functor.preservesColimitsOfShape_of_isCardinalAccessible F₁ κ J + infer_instance + +instance : (Comma.fst F₁ F₂).IsCardinalAccessible κ where + preservesColimitOfShape J _ _ := by + have := Functor.preservesColimitsOfShape_of_isCardinalAccessible F₁ κ J + infer_instance + +instance : (Comma.snd F₁ F₂).IsCardinalAccessible κ where + preservesColimitOfShape J _ _ := by + have := Functor.preservesColimitsOfShape_of_isCardinalAccessible F₁ κ J + infer_instance + +end + +section + +variable (κ : Cardinal.{w}) [Fact κ.IsRegular] + +set_option backward.isDefEq.respectTransparency false in +set_option backward.defeqAttrib.useBackward true in +open IsFiltered in +variable {F₁ F₂ κ} in +lemma isCardinalPresentable_mk {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 (Comma.mk _ _ f) κ := + .mk (fun J _ _ G c hc ↦ by + have := isFiltered_of_isCardinalFiltered J κ + have := Functor.preservesColimitsOfShape_of_isCardinalAccessible F₁ κ J + have := Functor.preservesColimitsOfShape_of_isCardinalAccessible F₂ κ J + refine ⟨fun g ↦ ?_, fun j f₁ f₂ hf ↦ ?_⟩ + · obtain ⟨j, f₁, f₂, hf₁, hf₂⟩ : + ∃ (j : J) (f₁ : X₁ ⟶ (G.obj j).left) (f₂ : X₂ ⟶ (G.obj j).right), + f₁ ≫ (c.ι.app j).left = g.left ∧ f₂ ≫ (c.ι.app j).right = g.right := by + obtain ⟨j₁, f₁, hf₁⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ + (isColimitOfPreserves (fst _ _) hc) g.left + obtain ⟨j₂, f₂, hf₂⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ + (isColimitOfPreserves (snd _ _) hc) g.right + dsimp at f₁ f₂ hf₁ hf₂ + refine ⟨max j₁ j₂, f₁ ≫ (G.map (leftToMax j₁ j₂)).left, + f₂ ≫ (G.map (rightToMax j₁ j₂)).right, ?_, ?_⟩ + · rw [Category.assoc, ← hf₁, ← Comma.comp_left, Cocone.w] + · rw [Category.assoc, ← hf₂, ← Comma.comp_right, Cocone.w] + obtain ⟨j', a, ha⟩ := IsCardinalPresentable.exists_eq_of_isColimit' + κ (isColimitOfPreserves (snd _ _ ⋙ F₂) hc) + (F₁.map f₁ ≫ (G.obj j).hom) (f ≫ F₂.map f₂) (by + dsimp + simp only [Category.assoc, ← Functor.map_comp, hf₂, + ← (c.ι.app j).w, Functor.const_obj_obj, + ← Functor.map_comp_assoc, hf₁, g.w]) + refine ⟨j', { left := f₁ ≫ (G.map a).left, right := f₂ ≫ (G.map a).right }, ?_⟩ + ext + · dsimp + rw [Category.assoc, ← hf₁, ← Comma.comp_left, Cocone.w] + · dsimp + rw [Category.assoc, ← hf₂, ← Comma.comp_right, Cocone.w] + · obtain ⟨j₁, a, ha⟩ := IsCardinalPresentable.exists_eq_of_isColimit' + κ (isColimitOfPreserves (fst _ _) hc) f₁.left f₂.left + ((fst _ _).congr_map hf) + obtain ⟨j₂, b, hb⟩ := IsCardinalPresentable.exists_eq_of_isColimit' + κ (isColimitOfPreserves (snd _ _) hc) f₁.right f₂.right + ((snd _ _).congr_map hf) + dsimp at ha hb + obtain ⟨j', a', b', h⟩ := IsFiltered.span a b + refine ⟨j', a ≫ a', ?_⟩ + ext + · simp [reassoc_of% ha] + · simp only [h, Functor.map_comp, comp_right, reassoc_of% hb]) + +protected def isCardinalPresentable : ObjectProperty (Comma F₁ F₂) := + ObjectProperty.comma _ _ (isCardinalPresentable C₁ κ) (isCardinalPresentable C₂ κ) +deriving ObjectProperty.IsStableUnderRetracts + +lemma isCardinalPresentable_le + [HasCardinalFilteredColimits C₁ κ] [HasCardinalFilteredColimits C₂ κ] + [F₁.IsCardinalAccessible κ] [F₂.IsCardinalAccessible κ] + [F₁.PreservesCardinalPresentable κ] : + Comma.isCardinalPresentable F₁ F₂ κ ≤ isCardinalPresentable (Comma F₁ F₂) κ := by + intro f ⟨h₁, h₂⟩ + simp only [ObjectProperty.prop_inverseImage_iff, fst_obj, snd_obj] at h₁ h₂ + exact isCardinalPresentable_mk f.hom + +instance [ObjectProperty.EssentiallySmall.{w} (isCardinalPresentable C₁ κ)] + [ObjectProperty.EssentiallySmall.{w} (isCardinalPresentable C₂ κ)] + [LocallySmall.{w} D] : + ObjectProperty.EssentiallySmall.{w} (Comma.isCardinalPresentable F₁ F₂ κ) := by + dsimp only [Comma.isCardinalPresentable] + infer_instance + +namespace isCardinalAccessibleCategory + +variable {F₁ F₂} + +variable (f : Comma F₁ F₂) + +abbrev J := CostructuredArrow (Comma.isCardinalPresentable F₁ F₂ κ).ι f +abbrev J₁ := CostructuredArrow (isCardinalPresentable C₁ κ).ι f.left +abbrev J₂ := CostructuredArrow (isCardinalPresentable C₂ κ).ι f.right + +instance [IsCardinalAccessibleCategory C₁ κ] : IsFiltered (J₁ κ f) := + isFiltered_of_isCardinalFiltered _ κ + +instance [IsCardinalAccessibleCategory C₂ κ] : IsFiltered (J₂ κ f) := + isFiltered_of_isCardinalFiltered _ κ + +attribute [local instance] IsFiltered.nonempty + +abbrev J.fst (g : J κ f) : J₁ κ f := + CostructuredArrow.mk (Y := ⟨_, g.left.property.1⟩) (by exact g.hom.left) + +abbrev J.snd (g : J κ f) : J₂ κ f := + CostructuredArrow.mk (Y := ⟨_, g.left.property.2⟩) (by exact g.hom.right) +-- there must be some better way to define these functors +@[simps] +def π₁ : J κ f ⥤ J₁ κ f where + obj g := g.fst + map φ := CostructuredArrow.homMk (ObjectProperty.homMk (by exact φ.left.hom.left)) + (by exact congr_arg CommaMorphism.left (CostructuredArrow.w φ)) + +@[simps] +def π₂ : J κ f ⥤ J₂ κ f where + obj g := g.snd + map φ := CostructuredArrow.homMk (ObjectProperty.homMk (by exact φ.left.hom.right)) + (by exact congr_arg CommaMorphism.right (CostructuredArrow.w φ)) + +variable {κ f} + +abbrev J.mk (j₁ : J₁ κ f) (j₂ : J₂ κ f) (g : F₁.obj j₁.left.obj ⟶ F₂.obj j₂.left.obj) + (w : F₁.map j₁.hom ≫ f.hom = g ≫ F₂.map j₂.hom := by cat_disch) : + J κ f := + CostructuredArrow.mk (Y := ⟨Comma.mk _ _ g, j₁.left.property, j₂.left.property⟩) + { left := by exact j₁.hom + right := by exact j₂.hom } + +abbrev J.homMk {j j' : J κ f} (g₁ : j.fst ⟶ j'.fst) (g₂ : j.snd ⟶ j'.snd) + (h : F₁.map g₁.left.hom ≫ j'.left.obj.hom = + j.left.obj.hom ≫ F₂.map g₂.left.hom := by cat_disch) : + j ⟶ j' := + CostructuredArrow.homMk (ObjectProperty.homMk + { left := g₁.left.hom + right := g₂.left.hom }) (by + ext + · simpa using! CostructuredArrow.w g₁ + · simpa using! CostructuredArrow.w g₂) + +section + +variable [IsCardinalAccessibleCategory C₂ κ] [F₂.IsCardinalAccessible κ] + [F₁.PreservesCardinalPresentable κ] + +set_option backward.defeqAttrib.useBackward true in +lemma J.exists_hom' + {j j' : J κ f} (g₁ : j.fst ⟶ j'.fst) (g₂ : j.snd ⟶ j'.snd) : + ∃ (j₂ : J₂ κ f) (a : j'.snd ⟶ j₂), + F₁.map g₁.left.hom ≫ j'.left.obj.hom ≫ F₂.map a.left.hom = + j.left.obj.hom ≫ F₂.map g₂.left.hom ≫ F₂.map a.left.hom := by + have := Functor.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall + F₂ κ (J₂ κ f) + obtain ⟨j₂, a, ha⟩ := IsCardinalPresentable.exists_eq_of_isColimit' κ + (isColimitOfPreserves F₂ ((isCardinalPresentable C₂ κ).ι.denseAt f.right)) + (i := j'.snd) (F₁.map g₁.left.hom ≫ j'.left.obj.hom) + (j.left.obj.hom ≫ F₂.map g₂.left.hom) (by + dsimp + rw [Category.id_comp, Category.assoc, Category.assoc, ← Functor.map_comp, + ← dsimp% j'.hom.w, ← Functor.map_comp_assoc, dsimp% CostructuredArrow.w g₁, + dsimp% j.hom.w, dsimp% CostructuredArrow.w g₂]) + exact ⟨j₂, a, by cat_disch⟩ + +set_option backward.defeqAttrib.useBackward true in +lemma J.exists_hom {j j' : J κ f} (g₁ : j.fst ⟶ j'.fst) (g₂ : j.snd ⟶ j'.snd) : + ∃ (j'' : J κ f) (a : j ⟶ j'') (b : j' ⟶ j''), + g₁.left.hom ≫ b.left.hom.left = a.left.hom.left ∧ + g₂.left.hom ≫ b.left.hom.right = a.left.hom.right := by + obtain ⟨j₂, a, ha⟩ := J.exists_hom' g₁ g₂ + exact ⟨J.mk j'.fst j₂ (j'.left.obj.hom ≫ F₂.map a.left.hom) + (by simp [← dsimp% (CostructuredArrow.w a)]), J.homMk g₁ (g₂ ≫ a) (by simpa), + J.homMk (𝟙 _) a (by simp), by simp⟩ + +set_option backward.defeqAttrib.useBackward true in +lemma exists_of_j₁_of_j₂' (j₁ : J₁ κ f) (j₂ : J₂ κ f) : + ∃ (j₂' : J₂ κ f) (_ : j₂ ⟶ j₂') (b : F₁.obj j₁.left.obj ⟶ F₂.obj j₂'.left.obj), + F₁.map j₁.hom ≫ f.hom = b ≫ F₂.map j₂'.hom := by + have := Functor.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall F₂ κ + (J₂ κ f) + obtain ⟨k, a, ha⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ + (isColimitOfPreserves F₂ ((isCardinalPresentable C₂ κ).ι.denseAt f.right)) + (F₁.map j₁.hom ≫ f.hom) + dsimp at ha + simp only [Category.id_comp] at ha + obtain ⟨j₂', b, c, _⟩ := IsFilteredOrEmpty.cocone_objs j₂ k + refine ⟨j₂', b, a ≫ F₂.map c.left.hom, ?_⟩ + simp [← ha, ← Functor.map_comp, dsimp% CostructuredArrow.w c] + +set_option backward.defeqAttrib.useBackward true in +lemma exists_of_j₁_of_j₂ (j₁ : J₁ κ f) (j₂ : J₂ κ f) : + ∃ (j : J κ f) (_ : j₁ ⟶ j.fst), Nonempty (j₂ ⟶ j.snd) := by + obtain ⟨j₂', a, b, h⟩ := exists_of_j₁_of_j₂' j₁ j₂ + exact ⟨J.mk j₁ j₂' b h, 𝟙 _, ⟨a⟩⟩ + +lemma exists_of_j₁ (j₁ : J₁ κ f) : + ∃ (j : J κ f), Nonempty (j₁ ⟶ j.fst) := by + obtain ⟨j, a, _⟩ := exists_of_j₁_of_j₂ j₁ (Classical.arbitrary _) + exact ⟨j, ⟨a⟩⟩ + +lemma exists_of_j₂ [IsCardinalAccessibleCategory C₁ κ] (j₂ : J₂ κ f) : + ∃ (j : J κ f), Nonempty (j₂ ⟶ j.snd) := by + obtain ⟨j, _, ⟨a⟩⟩ := exists_of_j₁_of_j₂ (Classical.arbitrary _) j₂ + exact ⟨j, ⟨a⟩⟩ + +end + +variable [IsCardinalAccessibleCategory C₁ κ] [IsCardinalAccessibleCategory C₂ κ] + [F₁.IsCardinalAccessible κ] [F₂.IsCardinalAccessible κ] + [F₁.PreservesCardinalPresentable κ] [LocallySmall.{w} D] + +instance : PreservesColimitsOfShape (J₁ κ f) F₁ := + F₁.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall κ _ + +instance : PreservesColimitsOfShape (J₂ κ f) F₂ := + F₂.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall κ _ + +open IsCardinalFiltered in +set_option backward.defeqAttrib.useBackward true in +instance : IsCardinalFiltered (J κ f) κ := by + rw [isCardinalFiltered_iff'] + refine ⟨fun ι j hι ↦ ?_, fun ι j k g hι hι' ↦ ?_⟩ + · obtain ⟨j₁, ⟨a₁⟩⟩ := IsCardinalFiltered.exists_max (fun i ↦ (j i).fst) hι + obtain ⟨j₂, ⟨a₂⟩⟩ := IsCardinalFiltered.exists_max (fun i ↦ (j i).snd) hι + obtain ⟨j₂', b, c, h₁⟩ := exists_of_j₁_of_j₂' j₁ j₂ + choose j₂'' d h₂ using + fun i ↦ IsCardinalPresentable.exists_eq_of_isColimit' κ + (isColimitOfPreserves F₂ ((isCardinalPresentable C₂ κ).ι.denseAt f.right)) + (F₁.map (a₁ i).left.hom ≫ c) + ((j i).left.obj.hom ≫ F₂.map (a₂ i).left.hom ≫ F₂.map b.left.hom) (by + dsimp + rw [Category.id_comp, Category.assoc, Category.assoc, Category.assoc, + ← dsimp% h₁, ← F₁.map_comp_assoc, dsimp% CostructuredArrow.w (a₁ i), + ← F₂.map_comp, dsimp% CostructuredArrow.w b, ← F₂.map_comp, + dsimp% CostructuredArrow.w (a₂ i), dsimp% (j i).hom.w]) + dsimp at h₁ h₂ + simp only [Category.assoc] at h₂ + obtain ⟨l, e, g, fac⟩ := wideSpan d hι + refine ⟨J.mk j₁ l (c ≫ F₂.map g.left.hom) ?_, fun i ↦ ⟨?_⟩⟩ + · dsimp + rw [h₁, Category.assoc, ← Functor.map_comp, dsimp% CostructuredArrow.w g] + · refine J.homMk (a₁ i) (a₂ i ≫ b ≫ g) (by simp [← fac i, reassoc_of% h₂]) + · let g₁ (i : ι) := (π₁ κ f).map (g i) + let g₂ (i : ι) := (π₂ κ f).map (g i) + obtain ⟨l, a, ⟨b⟩⟩ := + exists_of_j₁_of_j₂ (coeq g₁ hι) (coeq g₂ hι) + obtain ⟨l', c, d, h₁, h₂⟩ := J.exists_hom (coeqHom g₁ hι ≫ a) (coeqHom g₂ hι ≫ b) + refine ⟨l', c, J.homMk (toCoeq g₁ hι ≫ a ≫ (π₁ κ f).map d) + (toCoeq g₂ hι ≫ b ≫ (π₂ κ f).map d) ?_, fun i ↦ ?_⟩ + · let i : ι := Classical.arbitrary _ + dsimp + rw [← dsimp% coeq_condition g₁ hι i, ← dsimp% coeq_condition g₂ hι i] + dsimp at h₁ h₂ ⊢ + simp only [Category.assoc] at h₁ h₂ ⊢ + rw [h₁, h₂] + simp only [Functor.map_comp, Category.assoc, CommaMorphism.w] + simp only [← Category.assoc] + congr 1 + exact (g i).left.hom.w + · ext + · simp [← dsimp% [g₁] coeq_condition g₁ hι i, ← h₁, g₁] + · simp [← dsimp% [g₂] coeq_condition g₂ hι i, ← h₂, g₂] + +instance : PreservesColimitsOfShape (J κ f) F₁ := + F₁.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall κ _ + +instance : IsFiltered (J κ f) := + isFiltered_of_isCardinalFiltered _ κ + +set_option backward.defeqAttrib.useBackward true in +instance : (π₁ κ f).Final := by + rw [Functor.final_iff_of_isFiltered] + refine ⟨exists_of_j₁, fun {d e} g₁ g₂ ↦ ?_⟩ + obtain ⟨j₁, a, ha⟩ := IsFilteredOrEmpty.cocone_maps g₁ g₂ + obtain ⟨j, b, ⟨c⟩⟩ := exists_of_j₁_of_j₂ j₁ e.snd + obtain ⟨j', g, h, h₁, h₂⟩ := J.exists_hom (a ≫ b) c + refine ⟨j', g, ?_⟩ + ext + simp [← h₁, reassoc_of% dsimp% (CostructuredArrow.proj _ _ ⋙ + ObjectProperty.ι _).congr_map ha] + +set_option backward.defeqAttrib.useBackward true in +instance : (π₂ κ f).Final := by + rw [Functor.final_iff_of_isFiltered] + refine ⟨exists_of_j₂, fun {d e} g₁ g₂ ↦ ?_⟩ + obtain ⟨j₂, a, ha⟩ := IsFilteredOrEmpty.cocone_maps g₁ g₂ + obtain ⟨j, b, ⟨c⟩⟩ := exists_of_j₁_of_j₂ e.fst j₂ + obtain ⟨j', g, h, h₁, h₂⟩ := J.exists_hom b (a ≫ c) + refine ⟨j', g, ?_⟩ + ext + simp [← h₂, reassoc_of% dsimp% (CostructuredArrow.proj _ _ ⋙ + ObjectProperty.ι _).congr_map ha] + +variable (κ f) in +abbrev functor : J κ f ⥤ Comma F₁ F₂ := + CostructuredArrow.proj (Comma.isCardinalPresentable F₁ F₂ κ).ι f ⋙ + (Comma.isCardinalPresentable F₁ F₂ κ).ι + +variable (κ f) in +abbrev cocone : Cocone (functor κ f) := + (Functor.LeftExtension.mk (𝟭 (Comma F₁ F₂)) + (Comma.isCardinalPresentable F₁ F₂ κ).ι.rightUnitor.inv).coconeAt f + +variable (κ f) in +noncomputable def isColimitCocone : IsColimit (cocone κ f) := by + refine Comma.fstSndJointlyReflectColimit ?_ ?_ + · exact (Functor.Final.isColimitWhiskerEquiv (π₁ κ f) _).2 + ((isCardinalPresentable C₁ κ).ι.denseAt f.left) + · exact (Functor.Final.isColimitWhiskerEquiv (π₂ κ f) _).2 + ((isCardinalPresentable C₂ κ).ι.denseAt f.right) + +instance : (Comma.isCardinalPresentable F₁ F₂ κ).ι.IsDense where + isDenseAt f := ⟨isColimitCocone κ f⟩ + +end isCardinalAccessibleCategory + +variable [IsCardinalAccessibleCategory C₁ κ] [IsCardinalAccessibleCategory C₂ κ] + [F₁.IsCardinalAccessible κ] [F₂.IsCardinalAccessible κ] + [F₁.PreservesCardinalPresentable κ] [LocallySmall.{w} D] + +protected lemma isCardinalFilteredGenerator_isCardinalPresentable : + (Comma.isCardinalPresentable F₁ F₂ κ).IsCardinalFilteredGenerator κ := + .mk' (isCardinalPresentable_le _ _ _) + (fun f ↦ ⟨(CostructuredArrow (Comma.isCardinalPresentable F₁ F₂ κ).ι f), inferInstance, + inferInstance, inferInstance, + ⟨_, _, (Comma.isCardinalPresentable F₁ F₂ κ).ι.denseAt f⟩, + fun g ↦ g.left.property⟩) + +instance : + IsCardinalAccessibleCategory (Comma F₁ F₂) κ where + exists_generator := + ⟨_, inferInstance, Comma.isCardinalFilteredGenerator_isCardinalPresentable.{w} F₁ F₂ κ⟩ + +protected lemma isCardinalPresentable_eq : + Comma.isCardinalPresentable F₁ F₂ κ = isCardinalPresentable (Comma F₁ F₂) κ := by + rw [(Comma.isCardinalFilteredGenerator_isCardinalPresentable + F₁ F₂ κ).isPresentable_eq_retractClosure, + ObjectProperty.retractClosure_eq_self] + +variable {F₁ F₂} in +protected lemma isCardinalPresentable_iff (f : Comma F₁ F₂) : + IsCardinalPresentable f κ ↔ + IsCardinalPresentable f.left κ ∧ IsCardinalPresentable f.right κ := by + change _ ↔ Comma.isCardinalPresentable F₁ F₂ κ f + rw [Comma.isCardinalPresentable_eq] + +instance : (Comma.fst F₁ F₂).PreservesCardinalPresentable κ where + le_inverseImage_isCardinalPresentable f hf := by + simp only [Comma.isCardinalPresentable_iff] at hf + tauto + +instance : (Comma.snd F₁ F₂).PreservesCardinalPresentable κ where + le_inverseImage_isCardinalPresentable f hf := by + simp only [Comma.isCardinalPresentable_iff] at hf + tauto + +end + +section + +variable [IsAccessibleCategory.{w} C₁] [IsAccessibleCategory.{w} C₂] + [Functor.IsAccessible.{w} F₁] [Functor.IsAccessible.{w} F₂] + [IsAccessibleCategory.{w} D] + +instance test : IsAccessibleCategory.{w} (Comma F₁ F₂) := by + obtain ⟨κ, _, _, _, _, _, _, _, _, _⟩ := + IsCardinalAccessibleCategory.uniformization_pair F₁ F₂ + exact ⟨κ, inferInstance, inferInstance⟩ + +instance : Functor.IsAccessible.{w} (Comma.fst F₁ F₂) := by + obtain ⟨κ, _, _, _, _, _, _, _, _, _⟩ := + IsCardinalAccessibleCategory.uniformization_pair F₁ F₂ + exact ⟨κ, inferInstance, inferInstance⟩ + +instance : Functor.IsAccessible.{w} (Comma.snd F₁ F₂) := by + obtain ⟨κ, _, _, _, _, _, _, _, _, _⟩ := + IsCardinalAccessibleCategory.uniformization_pair F₁ F₂ + exact ⟨κ, inferInstance, inferInstance⟩ + +end + +end Comma + +namespace Arrow + +variable [IsAccessibleCategory.{w} D] + +instance : IsAccessibleCategory.{w} (Arrow D) := + inferInstanceAs (IsAccessibleCategory.{w} (Comma _ _)) + +instance : Functor.IsAccessible.{w} (Arrow.leftFunc : Arrow D ⥤ D) := + inferInstanceAs (Functor.IsAccessible.{w} (Comma.fst _ _)) + +instance : Functor.IsAccessible.{w} (Arrow.rightFunc : Arrow D ⥤ D) := + inferInstanceAs (Functor.IsAccessible.{w} (Comma.snd _ _)) + +end Arrow + +namespace CostructuredArrow + +variable + [IsAccessibleCategory.{w} C₁] [IsAccessibleCategory.{w} C₂] + (F : C₁ ⥤ C₂) [Functor.IsAccessible.{w} F] (Y : C₂) + +instance : IsAccessibleCategory.{w} (CostructuredArrow F Y) := + inferInstanceAs (IsAccessibleCategory.{w} (Comma _ _)) + +instance : Functor.IsAccessible.{w} (CostructuredArrow.proj F Y) := + inferInstanceAs (Functor.IsAccessible.{w} (Comma.fst _ _)) + +end CostructuredArrow + +namespace StructuredArrow + +variable + [IsAccessibleCategory.{w} C₁] [IsAccessibleCategory.{w} C₂] + (F : C₁ ⥤ C₂) [Functor.IsAccessible.{w} F] (X : C₂) + +instance : IsAccessibleCategory.{w} (StructuredArrow X F) := + inferInstanceAs (IsAccessibleCategory.{w} (Comma _ _)) + +instance : Functor.IsAccessible.{w} (StructuredArrow.proj X F) := + inferInstanceAs (Functor.IsAccessible.{w} (Comma.snd _ _)) + +end StructuredArrow + +namespace Over + +variable [IsAccessibleCategory.{w} D] (Y : D) + +instance : IsAccessibleCategory.{w} (Over Y) := + inferInstanceAs (IsAccessibleCategory.{w} (CostructuredArrow _ _)) + +instance : Functor.IsAccessible.{w} (Over.forget Y) := + inferInstanceAs (Functor.IsAccessible.{w} (CostructuredArrow.proj _ _)) + +end Over + +namespace Under + +variable [IsAccessibleCategory.{w} D] (X : D) + +instance : IsAccessibleCategory.{w} (Under X) := + inferInstanceAs (IsAccessibleCategory.{w} (StructuredArrow _ _)) + +instance : Functor.IsAccessible.{w} (Under.forget X) := + inferInstanceAs (Functor.IsAccessible.{w} (StructuredArrow.proj _ _)) + +end Under + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean b/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean index 8be9d46f911933..2bb0a333bebad3 100644 --- a/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean +++ b/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean @@ -95,6 +95,11 @@ noncomputable def toMax (k : K) : S k ⟶ max S hS := (cocone (κ := κ) (Discrete.functor S) (by simpa using hS)).ι.app ⟨k⟩ +include hS in +lemma exists_max : + ∃ (j : J), Nonempty (∀ (k : K), S k ⟶ j) := + ⟨max S hS, ⟨toMax S hS⟩⟩ + end max section coeq @@ -302,6 +307,24 @@ lemma isCardinalFiltered_iff : ι.app i := a i ≫ b ι.naturality _ _ f := by simpa using hb (Arrow.mk f) }⟩ +/-- Same as `isCardinalFiltered_iff`, but for the second condition involving +coequalizing morphisms, we assume that the index type `ι` is nonempty. -/ +lemma isCardinalFiltered_iff' : + IsCardinalFiltered J κ ↔ + (∀ ⦃ι : Type w⦄ (j : ι → J) (_ : HasCardinalLT ι κ), + ∃ (k : J), ∀ (i : ι), Nonempty (j i ⟶ k)) ∧ + ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)) (_ : HasCardinalLT ι κ) (_ : Nonempty ι), + ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b := by + rw [isCardinalFiltered_iff] + refine ⟨fun h ↦ ⟨h.1, by tauto⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, fun ι j k f hι ↦ ?_⟩⟩ + by_cases hι' : Nonempty ι + · exact h₂ f hι hι' + · obtain ⟨l, hl⟩ := h₁ (fun (x : ULift.{w} (Fin 2)) ↦ match x with + | ULift.up 0 => j + | ULift.up 1 => k) + (hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out)) + exact ⟨l, (hl ⟨1⟩).some, (hl ⟨0⟩).some, by tauto⟩ + end lemma IsCardinalFiltered.multicoequalizer diff --git a/Mathlib/CategoryTheory/Presentable/IsDiscrete.lean b/Mathlib/CategoryTheory/Presentable/IsDiscrete.lean new file mode 100644 index 00000000000000..06919407740f83 --- /dev/null +++ b/Mathlib/CategoryTheory/Presentable/IsDiscrete.lean @@ -0,0 +1,93 @@ +/- +Copyright (c) 2026 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.CategoryTheory.Presentable.LocallyPresentable + +/-! # Presentable objects in discrete categories + +The purpose of this file is to show that a category with a single +object and a single morphism is locally presentable. + +-/ + +@[expose] public section + +universe w + +namespace CategoryTheory + +open Limits + +variable {C : Type*} [Category* C] [IsDiscrete C] + +namespace IsDiscrete + +attribute [local instance] IsFiltered.nonempty + +protected instance (priority := low) isCardinalPresentable + (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] : + IsCardinalPresentable X κ := + .mk (fun J _ _ F c hc ↦ by + have := isFiltered_of_isCardinalFiltered J κ + refine ⟨fun g ↦ ?_, fun j f₁ f₂ _ ↦ ⟨j, 𝟙 j, by subsingleton⟩⟩ + obtain rfl := IsDiscrete.eq_of_hom g + let j : J := Classical.arbitrary _ + exact ⟨j, eqToHom (IsDiscrete.eq_of_hom (c.ι.app j)).symm, by subsingleton⟩) + +set_option backward.defeqAttrib.useBackward true in +protected instance (priority := low) isCardinalAccessible + {D : Type*} [Category* D] + (F : C ⥤ D) (κ : Cardinal.{w}) [Fact κ.IsRegular] : + F.IsCardinalAccessible κ where + preservesColimitOfShape J _ _ := ⟨fun {K} ↦ ⟨fun {c} hc ↦ ⟨by + have := isFiltered_of_isCardinalFiltered J κ + let j : J := Classical.arbitrary _ + have : IsIso ((F.mapCocone c).ι.app j) := by + dsimp; infer_instance + exact Functor.IsEventuallyConstantFrom.isColimitOfIsIso (i₀ := j) + (fun _ _ ↦ by dsimp; infer_instance) _⟩⟩⟩ + +instance (priority := low) + {D : Type*} [Category* D] (F : C ⥤ D) : + Functor.IsAccessible.{w} F := + ⟨.aleph0, Cardinal.fact_isRegular_aleph0, inferInstance⟩ + +instance (priority := low) (κ : Cardinal.{w}) [Fact κ.IsRegular] + [Subsingleton C] [Nonempty C] : + IsCardinalFiltered C κ where + nonempty_cocone F _ := + ⟨Cocone.mk (Classical.arbitrary _) + { app _ := eqToHom (by subsingleton) }⟩ + +instance (α : Type*) [Preorder α] [Subsingleton α] : IsDiscrete α where + eq_of_hom _ := by subsingleton + +instance (priority := low) (κ : Cardinal.{w}) [Fact κ.IsRegular] + [Subsingleton C] [Nonempty C] : + IsCardinalLocallyPresentable C κ where + has_colimits_of_shape J := ⟨fun F ↦ + ⟨Cocone.mk (Classical.arbitrary C) + { app _ := eqToHom (by subsingleton) }, + { desc _ := eqToHom (by subsingleton) }⟩ ⟩ + exists_generator := by + let X : C := Classical.arbitrary _ + refine ⟨.ofObj (fun (_ : PUnit.{w + 1}) ↦ X), inferInstance, + fun _ _ ↦ IsDiscrete.isCardinalPresentable _ _, + fun Y ↦ ?_⟩ + obtain rfl := Subsingleton.elim X Y + exact ⟨PUnit.{w + 1}, inferInstance, inferInstance, + { diag := (Functor.const _).obj X + ι := 𝟙 _ + isColimit.desc _ := eqToHom (by subsingleton) }, fun _ ↦ ⟨⟨⟩⟩⟩ + +instance (priority := low) [Subsingleton C] [Nonempty C] : + IsLocallyPresentable.{w} C := + ⟨.aleph0, Cardinal.fact_isRegular_aleph0, inferInstance⟩ + +end IsDiscrete + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean b/Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean index 53c0ad5a5e8fc3..7fa3c21f828f4f 100644 --- a/Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean +++ b/Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean @@ -29,7 +29,7 @@ universe w v u namespace CategoryTheory -open Limits +open Limits Opposite section @@ -104,4 +104,22 @@ example [IsLocallyPresentable.{w} C] (X : C) : IsPresentable.{w} X := inferInsta end +lemma ObjectProperty.le_isCardinalPresentable + {C : Type u} [Category.{v} C] [IsAccessibleCategory.{w} C] + (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w} P] : + ∃ (κ' : Cardinal.{w}) (_ : Fact κ'.IsRegular), + P ≤ isCardinalPresentable C κ' := by + obtain ⟨Q, hQ, h₁, h₂⟩ := EssentiallySmall.exists_small_le.{w} P + choose κ hκ' hκ using fun (X : Subtype Q) ↦ + Functor.IsAccessible.exists_cardinal (coyoneda.obj (op X.val)) + obtain ⟨κ', h₃, h₄⟩ := HasCardinalLT.exists_regular_cardinal_forall + (fun i ↦ (κ i).ord.ToType) + have : Fact κ'.IsRegular := ⟨h₃⟩ + refine ⟨κ', inferInstance, h₂.trans ((isoClosure_le_iff _ _).2 ?_)⟩ + intro X hX + have := h₄ ⟨X, hX⟩ + simp only [hasCardinalLT_iff_cardinal_mk_lt, Cardinal.mk_toType, + Cardinal.card_ord] at this + exact isCardinalPresentable_monotone C this.le _ (hκ ⟨X, hX⟩) + end CategoryTheory diff --git a/Mathlib/CategoryTheory/Presentable/PreservesCardinalPresentable.lean b/Mathlib/CategoryTheory/Presentable/PreservesCardinalPresentable.lean new file mode 100644 index 00000000000000..1b5b6148326873 --- /dev/null +++ b/Mathlib/CategoryTheory/Presentable/PreservesCardinalPresentable.lean @@ -0,0 +1,60 @@ +/- +Copyright (c) 2026 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.CategoryTheory.Presentable.Basic + +/-! +# Functors which preserve `κ`-presentable objects + +-/ + +@[expose] public section + +universe w + +namespace CategoryTheory.Functor + +variable {C D E : Type*} [Category* C] [Category* D] [Category* E] + +/-- Let `F : C ⥤ D` be a functor and `κ` be a regular cardinal, we say +that `F.PreservesCardinalPresentable κ` holds if for any `X : C` +that is `κ`-presentable in `C`, the object `F.obj X` is `κ`-presentable in `D`. -/ +class PreservesCardinalPresentable + (F : C ⥤ D) (κ : Cardinal.{w}) [Fact κ.IsRegular] : Prop where + le_inverseImage_isCardinalPresentable (F κ) : + isCardinalPresentable C κ ≤ (isCardinalPresentable D κ).inverseImage F + +export PreservesCardinalPresentable (le_inverseImage_isCardinalPresentable) + +instance (F : C ⥤ D) (κ : Cardinal.{w}) [Fact κ.IsRegular] (X : C) + [IsCardinalPresentable X κ] [F.PreservesCardinalPresentable κ] : + IsCardinalPresentable (F.obj X) κ := + le_inverseImage_isCardinalPresentable F κ _ (by assumption) + +instance (κ : Cardinal.{w}) [Fact κ.IsRegular] : + (𝟭 C).PreservesCardinalPresentable κ where + le_inverseImage_isCardinalPresentable := by rfl + +instance (F : C ⥤ D) (G : D ⥤ E) (κ : Cardinal.{w}) [Fact κ.IsRegular] + [F.PreservesCardinalPresentable κ] [G.PreservesCardinalPresentable κ] : + (F ⋙ G).PreservesCardinalPresentable κ where + le_inverseImage_isCardinalPresentable X hX := by + simp only [ObjectProperty.prop_inverseImage_iff, comp_obj] + infer_instance + +lemma PreservesCardinalPresentable.of_iso {F G : C ⥤ D} (e : F ≅ G) + (κ : Cardinal.{w}) [Fact κ.IsRegular] [F.PreservesCardinalPresentable κ] : + G.PreservesCardinalPresentable κ where + le_inverseImage_isCardinalPresentable X _ := + isCardinalPresentable_of_iso (e.app X) κ + +lemma PreservesCardinalPresentable.iff_of_iso {F G : C ⥤ D} (e : F ≅ G) + (κ : Cardinal.{w}) [Fact κ.IsRegular] : + F.PreservesCardinalPresentable κ ↔ G.PreservesCardinalPresentable κ := + ⟨fun _ ↦ .of_iso e _, fun _ ↦ .of_iso e.symm _⟩ + +end CategoryTheory.Functor diff --git a/Mathlib/CategoryTheory/Presentable/SharplyLT/Basic.lean b/Mathlib/CategoryTheory/Presentable/SharplyLT/Basic.lean index 1fe915d41331d6..a67228c8b23fe6 100644 --- a/Mathlib/CategoryTheory/Presentable/SharplyLT/Basic.lean +++ b/Mathlib/CategoryTheory/Presentable/SharplyLT/Basic.lean @@ -5,9 +5,10 @@ Authors: Joël Riou -/ module +public import Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure public import Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset public import Mathlib.CategoryTheory.Presentable.Dense -public import Mathlib.Order.TransfiniteIteration +public import Mathlib.CategoryTheory.Presentable.Directed /-! # Sharply smaller regular cardinals @@ -22,16 +23,18 @@ cardinals `κ₁ < κ₂`, this condition can be described in different ways: (iv) for any `κ₁`-directed partially ordered type `X` and any subset `A` of `X` of cardinality `< κ₂`, there exists a `κ₁`-directed subset `B` of `X` containing `A` that is of cardinality `< κ₂`. -The equivalence of these conditions (i)-(iv) is Theorem 2.11 in the book by Adámek and Rosický -((i) → (iii) is `exists_cofinal_of_isCardinalAccessibleCategory_cardinalDirectedPoset`, -(iii) → (iv) is `exists_isCardinalFiltered_set_of_exists_cofinal`, (ii) → (i) is obvious; -the rest is TODO @joelriou). Here, we take (i) as the definition. +The equivalence of these conditions (i)-(iv) is Theorem 2.11 in the book by Adámek and Rosický. +Here, we take (i) as the definition, and the equivalences between the various definitions +is obtained in the lemma `Cardinal.SharplyLT.tfae`. In particular, using (ii), +we show that `Cardinal.SharplyLT` is transitive. ## References * [Adámek, J. and Rosický, J., *Locally presentable and accessible categories*][Adamek_Rosicky_1994] -/ +@[expose] public section + universe w v u open CategoryTheory Limits @@ -260,6 +263,339 @@ public lemma exists_isCardinalFiltered_set_of_exists_cofinal (h₀ : κ₁ < κ end +section + +variable (hκ : κ₁ < κ₂) + (hκ' : ∀ {X : Type w} [PartialOrder X] [IsCardinalFiltered X κ₁] + (A : Set X) (_ : HasCardinalLT A κ₂), + ∃ (B : Set X), A ⊆ B ∧ IsCardinalFiltered B κ₁ ∧ HasCardinalLT B κ₂) + +variable (κ₁ κ₂) in +/-- Given a partially ordered type `J`, this is the type +of subsets of `J` that are `κ₁`-directed and of cardinality `< κ₂`. -/ +def IsCardinalFilteredAndHasCardinalLT + (J : Type w) [PartialOrder J] (A : Set J) : Prop := + IsCardinalFiltered A κ₁ ∧ HasCardinalLT A κ₂ + +namespace IsCardinalFilteredAndHasCardinalLT + +variable (κ₁ κ₂) {C : Type u} [Category.{v} C] {X : C} + {J : Type w} [PartialOrder J] + (p : (isCardinalPresentable C κ₁).ColimitOfShape J X) + +variable [IsCardinalAccessibleCategory C κ₁] + +instance (A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)) : + HasColimit ((Subtype.mono_coe A.val).functor ⋙ p.diag) := by + have : IsCardinalFiltered (Subtype A.val) κ₁ := A.prop.1 + infer_instance + +/-- The singleton `{j}`, as a term in +`IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J`. -/ +abbrev singleton (j : J) : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J) := + ⟨{j}, by + letI : OrderTop ({j} : Set J) := + { top := ⟨j, by simp⟩ + le_top := by simp } + exact isCardinalFiltered_of_hasTerminal _ _, + hasCardinalLT_of_finite _ _ (IsRegular.aleph0_le Fact.out)⟩ + +/-- A pair `{j ≤ j'}`, as a term in +`IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J`. -/ +abbrev pair {j j' : J} (h : j ≤ j') : + Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J) := + ⟨{j, j'}, by + letI : OrderTop ({j, j'} : Set J) := + { top := ⟨j', by simp⟩ + le_top := by aesop } + apply isCardinalFiltered_of_hasTerminal, + hasCardinalLT_of_finite _ _ (IsRegular.aleph0_le Fact.out)⟩ + +lemma le_pair {j j' : J} (h : j ≤ j') : + singleton κ₁ κ₂ j ≤ pair κ₁ κ₂ h := by + rw [Subtype.mk_le_mk] + simp + +lemma le_pair' {j j' : J} (h : j ≤ j') : + singleton κ₁ κ₂ j' ≤ pair κ₁ κ₂ h := by + rw [Subtype.mk_le_mk] + simp + +/-- Given a presentation `p` of `X : C` as a colimit indexed by a partially +ordered type `J` of `κ₁`-presentable objects and `A` a subset of `J` +that is `κ₁`-directed and of cardinality `< κ₂`, this is +the colimit of the restriction of the diagram `p.diag` to `A`. -/ +noncomputable abbrev colimit + (A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)) : C := + Limits.colimit ((Subtype.mono_coe A.val).functor ⋙ p.diag) + +/-- The inclusions in `colimit`. -/ +noncomputable abbrev colimit.ι + (A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)) (a : J) (ha : a ∈ A.val) : + p.diag.obj a ⟶ colimit κ₁ κ₂ p A := + Limits.colimit.ι ((Subtype.mono_coe A.val).functor ⋙ p.diag) ⟨a, ha⟩ + +omit [Fact κ₂.IsRegular] in +@[reassoc (attr := simp)] +lemma colimit.w (A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)) + {a b : J} (hab : a ≤ b) (ha : a ∈ A.val) (hb : b ∈ A.val) : + p.diag.map (homOfLE hab) ≫ colimit.ι κ₁ κ₂ p A b hb = colimit.ι κ₁ κ₂ p A a ha := + Limits.colimit.w ((Subtype.mono_coe A.val).functor ⋙ p.diag) + (j := ⟨a, ha⟩) (j' := ⟨b, hb⟩) (homOfLE hab) + +set_option backward.defeqAttrib.useBackward true in +/-- The functoriality of `colimit` with respect to the subset `A`. -/ +noncomputable def colimit.map + {A₁ A₂ : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)} (hA : A₁ ≤ A₂) : + colimit κ₁ κ₂ p A₁ ⟶ colimit κ₁ κ₂ p A₂ := + colimit.desc _ (Cocone.mk _ + { app j := colimit.ι κ₁ κ₂ p A₂ j.val (hA j.prop) + naturality j₁ j₂ f := by + simpa using! colimit.w κ₁ κ₂ p A₂ (leOfHom f) (hA j₁.prop) (hA j₂.prop) }) + +omit [Fact κ₂.IsRegular] in +@[reassoc (attr := simp)] +lemma colimit.ι_map {A₁ A₂ : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)} + (hA : A₁ ≤ A₂) (j : J) (hj : j ∈ A₁.val) : + colimit.ι κ₁ κ₂ p A₁ j hj ≫ colimit.map κ₁ κ₂ p hA = colimit.ι κ₁ κ₂ p A₂ j (hA hj) := + colimit.ι_desc .. + +omit [Fact κ₂.IsRegular] in +@[ext] +lemma colimit.hom_ext + {A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)} {T : C} + {φ₁ φ₂ : colimit κ₁ κ₂ p A ⟶ T} + (h : ∀ (j : J) (hj : j ∈ A.val), colimit.ι κ₁ κ₂ p A j hj ≫ φ₁ = + colimit.ι κ₁ κ₂ p A j hj ≫ φ₂) : + φ₁ = φ₂ := by + ext + apply h + +set_option backward.defeqAttrib.useBackward true in +/-- As `X` is the colimit of a diagram `p.diag`, this is the induced morphism +`colimit κ₁ κ₂ p A ⟶ X` from the colimit of the restriction of this diagram to `A`. -/ +noncomputable def colimit.π + (A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)) : colimit κ₁ κ₂ p A ⟶ X := + colimit.desc _ (Cocone.mk _ + { app a := by exact p.ι.app a + naturality _ _ _ := by simpa using p.ι.naturality _ }) + +omit [Fact κ₂.IsRegular] in +@[reassoc (attr := simp)] +lemma colimit.ι_π + (A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)) (a : J) (ha : a ∈ A.val) : + colimit.ι κ₁ κ₂ p A a ha ≫ colimit.π κ₁ κ₂ p A = p.ι.app a := + colimit.ι_desc .. + +omit [Fact κ₂.IsRegular] in +@[reassoc (attr := simp)] +lemma colimit.map_π {A₁ A₂ : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)} (hA : A₁ ≤ A₂) : + colimit.map κ₁ κ₂ p hA ≫ colimit.π κ₁ κ₂ p A₂ = colimit.π κ₁ κ₂ p A₁ := by + ext + simp + +/-- Given a presentation `p` of `X : C` as a colimit indexed by a partially +ordered type `J` of `κ₁`-presentable objects, this is the functor which sends +a subset `A` of `J` that is `κ₁`-directed and of cardinality `< κ₂` to the +colimit of the restriction to `A` of the diagram `p.diag`. -/ +@[simps] +noncomputable def functor : + Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J) ⥤ C where + obj A := colimit κ₁ κ₂ p A + map f := colimit.map κ₁ κ₂ p f.le + map_id _ := by ext; simp + map_comp f g := by ext; simp + +set_option backward.defeqAttrib.useBackward true in +/-- The cocone for `functor κ₁ κ₂ p` with point `X`. -/ +@[simps] +noncomputable def cocone : Cocone (functor κ₁ κ₂ p) where + pt := X + ι.app j := colimit.π κ₁ κ₂ p j + +namespace isColimit + +variable {κ₁ κ₂ p} (s : Cocone (functor κ₁ κ₂ p)) + +set_option backward.defeqAttrib.useBackward true in +/-- Auxiliary definition for `isColimit`. -/ +@[simps] +noncomputable def coconeDesc : Cocone p.diag where + pt := s.pt + ι.app j := colimit.ι _ _ _ _ _ (by simp) ≫ s.ι.app (singleton κ₁ κ₂ j) + ι.naturality j j' f := by + simpa [← s.w (homOfLE (le_pair κ₁ κ₂ (leOfHom f))), + ← s.w (homOfLE (le_pair' κ₁ κ₂ (leOfHom f)))] + using! colimit.w_assoc .. + +/-- Auxiliary definition for `isColimit`. -/ +noncomputable def desc : X ⟶ s.pt := p.isColimit.desc (coconeDesc s) + +set_option backward.defeqAttrib.useBackward true in +@[reassoc (attr := simp)] +lemma fac (j : J) : + dsimp% p.ι.app j ≫ desc s = + colimit.ι _ _ _ _ _ (by simp) ≫ s.ι.app (singleton κ₁ κ₂ j) := + p.isColimit.fac (coconeDesc s) j + +set_option backward.defeqAttrib.useBackward true in +@[reassoc] +lemma fac' (A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)) : + colimit.π κ₁ κ₂ p A ≫ desc s = s.ι.app A := by + ext j hj + let φ : singleton κ₁ κ₂ j ⟶ A := homOfLE (by + rw [Subtype.mk_le_mk] + simpa) + simp [colimit.ι_π_assoc, fac, ← s.w φ] + +end isColimit + +open isColimit in +set_option backward.defeqAttrib.useBackward true in +/-- Given a presentation `p` of `X : C` as a colimit indexed by a partially +ordered type `J` of `κ₁`-presentable objects, `X` is also the colimit +of all the colimits of the restrictions of the diagram `p.diag` +to the subsets `A` of `J` that are `κ₁`-directed and of cardinality `< κ₂`. -/ +noncomputable def isColimit : IsColimit (cocone κ₁ κ₂ p) where + desc s := desc s + fac s A := fac' s A + uniq s m hm := + p.isColimit.hom_ext (fun j ↦ by simp [fac s j, ← hm]) + +variable {κ₁ κ₂} in +include hκ' in +lemma isCardinalFiltered_subtype [IsCardinalFiltered J κ₁] : + IsCardinalFiltered (Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)) κ₂ := + isCardinalFiltered_preorder _ _ (fun K f hK ↦ by + rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK + obtain ⟨B, hB₁, hB₂, hB₃⟩ := hκ' (⋃ (k : K), (f k).val) + (hasCardinalLT_iUnion _ hK (fun k ↦ (f k).prop.2)) + exact ⟨⟨B, hB₂, hB₃⟩, fun k ↦ (Set.subset_iUnion _ k).trans hB₁⟩) + +end IsCardinalFilteredAndHasCardinalLT + +variable (C : Type u) [Category.{v} C] + +variable (κ₁ κ₂) in +/-- This is the closure of `κ₁`-presentable objects in the category `C` with respect +to colimits indexed by categories `J` such that `Arrow J` is of cardinality < `κ₂`. +When `C` is `κ₁`-accessible and `κ₁` is sharply smaller than `κ₂`, then any +object of `C` is a `κ₂`-filtered colimit of objects in this closure, +see `Cardinal.SharplyLT.isCardinalFilteredGenerator` below. -/ +public abbrev generator : ObjectProperty C := + (isCardinalPresentable C κ₁).colimitsCardinalClosure κ₂ + +include hκ in +lemma generator_le_isCardinalPresentable [LocallySmall.{w} C] : + generator κ₁ κ₂ C ≤ isCardinalPresentable C κ₂ := + ObjectProperty.colimitsCardinalClosure_le _ _ + (fun _ _ hJ ↦ isClosedUnderColimitsOfShape_isCardinalPresentable C hJ) + (isCardinalPresentable_monotone _ hκ.le) + +open IsCardinalFilteredAndHasCardinalLT in +include hκ hκ' in +/-- This is part of the proof of the implication (iv) → (ii) in the +characterizations of `SharplyLT κ₁ κ₂` in the docstring of this file. +See the lemma `Cardinal.SharplyLT.isCardinalFilteredGenerator` for the +version of this lemma with the assumption `SharplyLT κ₁ κ₂` instead of the +condition (iv). -/ +lemma isCardinalFilteredGenerator' + [IsCardinalAccessibleCategory C κ₁] : + (generator κ₁ κ₂ C).IsCardinalFilteredGenerator κ₂ where + le_isCardinalPresentable := generator_le_isCardinalPresentable hκ C + exists_colimitsOfShape X := by + have hκ₁ := isCardinalFilteredGenerator_isCardinalPresentable C κ₁ + obtain ⟨J, _, _, ⟨p⟩⟩ : + ∃ (J : Type w) (_ : PartialOrder J) (_ : IsCardinalFiltered J κ₁), + Nonempty ((isCardinalPresentable C κ₁).ColimitOfShape J X) := by + obtain ⟨J₀, _, _, ⟨p₀⟩⟩ := hκ₁.exists_colimitsOfShape X + obtain ⟨J, _, _, F, _⟩ := IsCardinalFiltered.exists_cardinal_directed J₀ κ₁ + exact ⟨_, _, inferInstance, ⟨p₀.reindex F⟩⟩ + refine ⟨Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J), inferInstance, + isCardinalFiltered_subtype hκ', + ⟨{ diag := _, ι := _, isColimit := isColimit κ₁ κ₂ p, prop_diag_obj A := ?_ }⟩⟩ + have : (generator κ₁ κ₂ C).IsClosedUnderColimitsOfShape (Subtype A.val) := by + apply ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure + rw [hasCardinalLT_arrow_iff_of_isThin _ _ (IsRegular.aleph0_le Fact.out)] + exact A.prop.2 + exact ObjectProperty.prop_colimit _ _ + (fun ⟨a, ha⟩ ↦ ObjectProperty.le_colimitsCardinalClosure _ _ _ + (p.prop_diag_obj a)) + +include hκ hκ' in +/-- This is the implication (iv) → (ii) in the characterizations +of `SharplyLT κ₁ κ₂` in the docstring of this file. +See the lemma `Cardinal.SharplyLT.isCardinalAccessibleCategory` +for the version of the lemma with the assumption `SharplyLT κ₁ κ₂` +instead of the condition (iv). -/ +lemma isCardinalAccessibleCategory' + (C : Type u) [Category.{v} C] [IsCardinalAccessibleCategory C κ₁] : + IsCardinalAccessibleCategory C κ₂ where + toHasCardinalFilteredColimits := .of_le C hκ.le + exists_generator := ⟨_, inferInstance, isCardinalFilteredGenerator' hκ hκ' C⟩ + +end + +public lemma tfae (h : κ₁ < κ₂) : + List.TFAE [SharplyLT κ₁ κ₂, + /- (i) -/ IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂, + /- (ii) -/ ∀ (C : Type (w + 1)) [Category.{w} C] [IsCardinalAccessibleCategory C κ₁], + IsCardinalAccessibleCategory C κ₂, + /- (iii) -/ ∀ (X : Type w) (_ : HasCardinalLT X κ₂), + ∃ (A : Set (CardinalDirectedPoset.SetCardinalLT κ₁ X)), HasCardinalLT A κ₂ ∧ IsCofinal A, + /- (iv) -/ ∀ ⦃X : Type w⦄ [PartialOrder X] [IsCardinalFiltered X κ₁] (A : Set X) + (_ : HasCardinalLT A κ₂), + ∃ (B : Set X), A ⊆ B ∧ IsCardinalFiltered B κ₁ ∧ HasCardinalLT B κ₂] := by + tfae_have 1 ↔ 2 := + ⟨fun h ↦ h.isCardinalAccessible_cardinalDirectedPoset, fun _ ↦ ⟨h, inferInstance⟩⟩ + tfae_have 3 → 2 := fun h' ↦ h' _ + tfae_have 2 → 4 := fun _ X hX ↦ + exists_cofinal_of_isCardinalAccessibleCategory_cardinalDirectedPoset h.le hX + tfae_have 4 → 5 := fun h' X _ _ A hA ↦ + exists_isCardinalFiltered_set_of_exists_cofinal h h' _ hA + tfae_have 5 → 3 := fun h' C _ _ ↦ isCardinalAccessibleCategory' h (fun A hA ↦ h' A hA) C + tfae_finish + +public lemma exists_cofinal (h : SharplyLT κ₁ κ₂) + {X : Type w} (hX : HasCardinalLT X κ₂) : + ∃ (A : Set (CardinalDirectedPoset.SetCardinalLT κ₁ X)), + HasCardinalLT A κ₂ ∧ IsCofinal A := by + have := (tfae h.lt).out 1 3 + exact this.1 h.isCardinalAccessible_cardinalDirectedPoset X hX + +public lemma of_exists_cofinal (h₀ : κ₁ < κ₂) + (h : ∀ (X : Type w) (_ : HasCardinalLT X κ₂), + ∃ (A : Set (CardinalDirectedPoset.SetCardinalLT κ₁ X)), + HasCardinalLT A κ₂ ∧ IsCofinal A) : + SharplyLT κ₁ κ₂ := + ((tfae h₀).out 3 0).1 h + +public lemma exists_isCardinalFiltered_set (h : SharplyLT κ₁ κ₂) + {X : Type w} [PartialOrder X] [IsCardinalFiltered X κ₁] + (A : Set X) (hA : HasCardinalLT A κ₂) : + ∃ (B : Set X), A ⊆ B ∧ IsCardinalFiltered B κ₁ ∧ HasCardinalLT B κ₂ := by + have := (tfae h.lt).out 1 4 + exact this.1 h.isCardinalAccessible_cardinalDirectedPoset A hA + +public lemma isCardinalFilteredGenerator (h : SharplyLT κ₁ κ₂) + (C : Type u) [Category.{v} C] [IsCardinalAccessibleCategory C κ₁] : + (generator κ₁ κ₂ C).IsCardinalFilteredGenerator κ₂ := + isCardinalFilteredGenerator' h.lt (h.exists_isCardinalFiltered_set) C + +public lemma isCardinalAccessibleCategory (h : SharplyLT κ₁ κ₂) + (C : Type u) [Category.{v} C] [IsCardinalAccessibleCategory C κ₁] : + IsCardinalAccessibleCategory C κ₂ where + toHasCardinalFilteredColimits := .of_le C h.le + exists_generator := ⟨_, inferInstance, h.isCardinalFilteredGenerator C⟩ + +public lemma trans (h₁₂ : SharplyLT κ₁ κ₂) {κ₃ : Cardinal.{w}} [Fact κ₃.IsRegular] + (h₂₃ : SharplyLT κ₂ κ₃) : + SharplyLT κ₁ κ₃ where + lt := h₁₂.lt.trans h₂₃.lt + isCardinalAccessible_cardinalDirectedPoset := by + have := h₁₂.isCardinalAccessible_cardinalDirectedPoset + exact h₂₃.isCardinalAccessibleCategory _ + end SharplyLT end Cardinal diff --git a/Mathlib/CategoryTheory/Presentable/SharplyLT/Lemmas.lean b/Mathlib/CategoryTheory/Presentable/SharplyLT/Lemmas.lean new file mode 100644 index 00000000000000..c2066281b4be8e --- /dev/null +++ b/Mathlib/CategoryTheory/Presentable/SharplyLT/Lemmas.lean @@ -0,0 +1,133 @@ +/- +Copyright (c) 2026 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.CategoryTheory.Presentable.SharplyLT.Basic +public import Mathlib.SetTheory.Cardinal.Arithmetic + +/-! +# Lemmas about sharply smaller regular cardinals + +-/ + +@[expose] public section + +universe u + +open CategoryTheory Limits + +lemma Cardinal.mk_iio_le_lift (κ : Cardinal.{u}) : + Cardinal.mk (Set.Iio κ) ≤ Cardinal.lift.{u + 1} κ := by + conv_rhs => rw [← card_ord κ, ← mk_Iio_ordinal] + rw [Cardinal.le_def] + exact ⟨⟨fun ⟨a, ha⟩ ↦ ⟨a.ord, by simpa⟩, fun _ _ h ↦ by aesop⟩⟩ + +namespace CategoryTheory.CardinalDirectedPoset.SetCardinalLT + +variable (κ : Cardinal.{u}) (X : Type u) + +def fromSigma (x : Σ (κ' : Set.Iio κ), κ'.val.ord.ToType → X) : SetCardinalLT κ X := + ⟨Set.range x.2, + HasCardinalLT.of_surjective + (by simpa only [hasCardinalLT_iff_cardinal_mk_lt, + Cardinal.mk_toType, Cardinal.card_ord] using! x.1.prop) _ + Set.rangeFactorization_surjective⟩ + +lemma fromSigma_surjective : Function.Surjective (fromSigma κ X) := by + rintro ⟨A, hA⟩ + rw [hasCardinalLT_iff_cardinal_mk_lt] at hA + let e : (Cardinal.mk A).ord.ToType ≃ A := + Nonempty.some (by simp [← Cardinal.lift_mk_eq']) + refine ⟨⟨⟨_, hA⟩, Subtype.val ∘ e⟩, ?_⟩ + rw [Subtype.mk_eq_mk] + simp [fromSigma] + +end CategoryTheory.CardinalDirectedPoset.SetCardinalLT + +namespace Cardinal.SharplyLT + +open CardinalDirectedPoset + +lemma of_pow_lt {κ₁ κ₂ : Cardinal.{u}} [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] + (h₀ : κ₁ < κ₂) (h : ∀ (α β : Cardinal.{u}), α < κ₁ → β < κ₂ → β ^ α < κ₂) : + SharplyLT κ₁ κ₂ := + .of_exists_cofinal h₀ (fun X hX ↦ by + refine ⟨.univ, ?_, by simp⟩ + rw [hasCardinalLT_iff_of_equiv (Equiv.Set.univ _)] + refine HasCardinalLT.of_surjective ?_ _ (SetCardinalLT.fromSigma_surjective _ _) + refine hasCardinalLT_sigma _ _ ?_ (fun ⟨α, hα⟩ ↦ ?_) + · refine lt_of_le_of_lt (le_trans ?_ (Cardinal.mk_iio_le_lift κ₁)) (by simpa) + rw [lift_id'.{u, u + 1}] + · simpa [hasCardinalLT_iff_cardinal_mk_lt] using + h _ _ hα (by rwa [hasCardinalLT_iff_cardinal_mk_lt] at hX)) + +lemma of_le {κ₁ κ₂ : Cardinal.{u}} [Fact κ₁.IsRegular] --[Fact κ₂.IsRegular] + (h₀ : κ₁ ≤ κ₂) (hκ₂ : Cardinal.aleph0 ≤ κ₂) : + letI : Fact (Cardinal.IsRegular (Order.succ (2 ^ κ₂))) := + ⟨isRegular_succ (hκ₂.trans (cantor _).le)⟩ + SharplyLT κ₁ (Order.succ (2 ^ κ₂)) := by + letI : Fact (Cardinal.IsRegular (Order.succ (2 ^ κ₂))) := + ⟨isRegular_succ (hκ₂.trans (cantor _).le)⟩ + refine of_pow_lt ?_ (fun α β hα hβ ↦ ?_) + · simp only [Order.lt_succ_iff] + exact h₀.trans (cantor _).le + · simp only [Order.lt_succ_iff] at hβ ⊢ + refine (power_le_power_right hβ).trans ?_ + rw [← power_mul] + refine power_le_power_left (by simp) ?_ + conv_rhs => rw [← mul_eq_self hκ₂] + exact mul_le_mul_right (hα.le.trans h₀) _ + +-- to be moved +lemma _root_.Cardinal.exists_le_of_small {ι : Type*} [Small.{u} ι] + (κ : ι → Cardinal.{u}) : + ∃ (κ' : Cardinal.{u}), ∀ (i : ι), κ i ≤ κ' := by + let T (i : Shrink.{u} ι) : Type u := (κ ((equivShrink _).symm i)).ord.ToType + refine ⟨Cardinal.mk (Sigma T), fun i ↦ ?_⟩ + obtain ⟨i, rfl⟩ := (equivShrink.{u} _).symm.surjective i + simpa [T] using Cardinal.mk_le_of_injective + (sigma_mk_injective (β := fun i ↦ (κ ((equivShrink _).symm i)).ord.ToType)) + +lemma exists_of_small {ι : Type*} [Small.{u} ι] (κ : ι → Cardinal.{u}) + [∀ i, Fact (κ i).IsRegular] : + ∃ (κ' : Cardinal.{u}) (_ : Fact κ'.IsRegular), + ∀ i, SharplyLT (κ i) κ' := by + obtain ⟨κ₀, hκ₀, h⟩ : + ∃ (κ₀ : Cardinal.{u}), Cardinal.aleph0 ≤ κ₀ ∧ ∀ (i : ι), κ i ≤ κ₀ := by + obtain ⟨κ', h⟩ := Cardinal.exists_le_of_small κ + exact ⟨max κ' .aleph0, by simp, fun i ↦ (h i).trans (by simp)⟩ + exact ⟨Order.succ (2 ^ κ₀), ⟨isRegular_succ (hκ₀.trans (cantor _).le)⟩, + fun i ↦ of_le (h i) hκ₀⟩ + +lemma exists_of_pair (κ₁ κ₂ : Cardinal.{u}) + [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] : + ∃ (κ' : Cardinal.{u}) (_ : Fact κ'.IsRegular), + SharplyLT κ₁ κ' ∧ SharplyLT κ₂ κ' := by + let f (i : Fin 2) : Cardinal.{u} := match i with + | 0 => κ₁ + | 1 => κ₂ + have (i : _) : Fact (f i).IsRegular := match i with + | 0 => by assumption + | 1 => by assumption + obtain ⟨κ', _, h₂⟩ := exists_of_small f + exact ⟨κ', inferInstance, h₂ 0, h₂ 1⟩ + +lemma exists_of_triple (κ₁ κ₂ κ₃ : Cardinal.{u}) + [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] [Fact κ₃.IsRegular] : + ∃ (κ' : Cardinal.{u}) (_ : Fact κ'.IsRegular), + SharplyLT κ₁ κ' ∧ SharplyLT κ₂ κ' ∧ SharplyLT κ₃ κ':= by + let f (i : Fin 3) : Cardinal.{u} := match i with + | 0 => κ₁ + | 1 => κ₂ + | 2 => κ₃ + have (i : _) : Fact (f i).IsRegular := match i with + | 0 => by assumption + | 1 => by assumption + | 2 => by assumption + obtain ⟨κ', _, h₂⟩ := exists_of_small f + exact ⟨κ', inferInstance, h₂ 0, h₂ 1, h₂ 2⟩ + +end Cardinal.SharplyLT diff --git a/Mathlib/CategoryTheory/Presentable/SolutionSetCondition.lean b/Mathlib/CategoryTheory/Presentable/SolutionSetCondition.lean new file mode 100644 index 00000000000000..b3ea7db90ceb49 --- /dev/null +++ b/Mathlib/CategoryTheory/Presentable/SolutionSetCondition.lean @@ -0,0 +1,41 @@ +/- +Copyright (c) 2025 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou, Dagur Asgeirsson +-/ +module + +public import Mathlib.CategoryTheory.Presentable.Comma +public import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems + +/-! +# Accessible functor satisfy the solution set condition + +-/ + +@[expose] public section + +universe w + +namespace CategoryTheory + +variable {C D : Type*} [Category* C] [Category* D] + +attribute [local instance] IsFiltered.nonempty in +lemma SolutionSetCondition.of_isCardinalAccessible + [IsAccessibleCategory.{w} C] [IsAccessibleCategory.{w} D] + (F : C ⥤ D) [Functor.IsAccessible.{w} F] : + SolutionSetCondition.{w} F := by + intro Y + obtain ⟨κ, _, _⟩ := IsAccessibleCategory.exists_cardinal.{w} (StructuredArrow Y F) + obtain ⟨ι, X₀, h⟩ := ObjectProperty.EssentiallySmall.exists_eq_isoClosure_ofObj.{w} + (isCardinalPresentable (StructuredArrow Y F) κ) + refine ⟨ι, fun i ↦ (X₀ i).right, fun i ↦ (X₀ i).hom, + fun X g ↦ ?_⟩ + let E := CostructuredArrow (isCardinalPresentable _ κ).ι (StructuredArrow.mk g) + have : IsFiltered E := isFiltered_of_isCardinalFiltered _ κ + let γ : E := Classical.arbitrary _ + obtain ⟨_, ⟨i⟩, ⟨e⟩⟩ := h.le _ γ.left.property + exact ⟨i, _, StructuredArrow.w (e.inv ≫ γ.hom)⟩ + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/Presentable/Uniformization.lean b/Mathlib/CategoryTheory/Presentable/Uniformization.lean new file mode 100644 index 00000000000000..b1253057b517cb --- /dev/null +++ b/Mathlib/CategoryTheory/Presentable/Uniformization.lean @@ -0,0 +1,172 @@ +/- +Copyright (c) 2026 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.CategoryTheory.Presentable.SharplyLT.Lemmas +public import Mathlib.CategoryTheory.Presentable.PreservesCardinalPresentable + +/-! +# The uniformization theorem + +-/ + +@[expose] public section + +universe w v v' u u' + +open CategoryTheory Limits Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT in +lemma Cardinal.SharplyLT.exists_retract_of_isCardinalPresentable + {κ₁ κ₂ : Cardinal.{w}} [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] + (hκ : κ₁.SharplyLT κ₂) {C : Type u} [Category.{v} C] + [IsCardinalAccessibleCategory C κ₁] (X : C) [IsCardinalPresentable X κ₂] : + ∃ (Y : C) (_ : Retract X Y) (J : Type w) (_ : PartialOrder J), + IsCardinalFiltered J κ₁ ∧ HasCardinalLT J κ₂ ∧ + Nonempty ((isCardinalPresentable C κ₁).ColimitOfShape J Y) := by + have hκ₁ := isCardinalFilteredGenerator_isCardinalPresentable C κ₁ + obtain ⟨J, _, _, ⟨p⟩⟩ : + ∃ (J : Type w) (_ : PartialOrder J) (_ : IsCardinalFiltered J κ₁), + Nonempty ((isCardinalPresentable C κ₁).ColimitOfShape J X) := by + obtain ⟨J₀, _, _, ⟨p₀⟩⟩ := hκ₁.exists_colimitsOfShape X + obtain ⟨J, _, _, F, _⟩ := IsCardinalFiltered.exists_cardinal_directed J₀ κ₁ + exact ⟨_, _, inferInstance, ⟨p₀.reindex F⟩⟩ + have : IsCardinalFiltered (Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)) κ₂ := + isCardinalFiltered_subtype hκ.exists_isCardinalFiltered_set + obtain ⟨K, i, hi⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ₂ + (isColimit κ₁ κ₂ p) (𝟙 X) + exact ⟨colimit κ₁ κ₂ p K, + { i := i, r := colimit.π κ₁ κ₂ p K }, Subtype K.val, + inferInstance, K.prop.1, K.prop.2, ⟨.colimit _ (fun k ↦ p.prop_diag_obj _)⟩⟩ + +namespace CategoryTheory + +open Limits + +namespace IsCardinalAccessibleCategory + +variable {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D] + +lemma uniformization' + (F : C ⥤ D) {κ₁ κ₂ : Cardinal.{w}} [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] + [IsCardinalAccessibleCategory C κ₁] [IsCardinalAccessibleCategory D κ₁] + [F.IsCardinalAccessible κ₁] (hκ : κ₁.SharplyLT κ₂) + (hF : isCardinalPresentable C κ₁ ≤ (isCardinalPresentable D κ₂).inverseImage F) : + isCardinalPresentable C κ₂ ≤ (isCardinalPresentable D κ₂).inverseImage F := by + intro X hX + simp only [isCardinalPresentable_iff] at hX + obtain ⟨Y, r, J, _, _, hJ, ⟨p⟩⟩ := hκ.exists_retract_of_isCardinalPresentable X + refine (isCardinalPresentable D κ₂).prop_of_retract (r.map F) ?_ + have := F.preservesColimitsOfShape_of_isCardinalAccessible κ₁ + have (j : J) : IsCardinalPresentable ((p.diag ⋙ F).obj j) κ₂ := hF _ (p.prop_diag_obj j) + exact isCardinalPresentable_of_isColimit _ (isColimitOfPreserves F p.isColimit) _ + ((hasCardinalLT_arrow_iff_of_isThin _ _ (Cardinal.IsRegular.aleph0_le Fact.out)).2 hJ) + +lemma uniformization_of_small + [IsAccessibleCategory.{w} C] [IsAccessibleCategory.{w} D] + {ι : Type*} [Small.{w} ι] (F : ι → C ⥤ D) + [∀ i, Functor.IsAccessible.{w} (F i)] : + ∃ (κ : Cardinal.{w}) (_ : Fact κ.IsRegular), + IsCardinalAccessibleCategory C κ ∧ + IsCardinalAccessibleCategory D κ ∧ + (∀ i, (F i).IsCardinalAccessible κ) ∧ + ∀ i, isCardinalPresentable C κ ≤ (isCardinalPresentable D κ).inverseImage (F i) := by + obtain ⟨κ, _, _, _, _⟩ : + ∃ (κ : Cardinal.{w}) (_ : Fact κ.IsRegular), + IsCardinalAccessibleCategory C κ ∧ IsCardinalAccessibleCategory D κ ∧ + ∀ (i : ι), (F i).IsCardinalAccessible κ := by + obtain ⟨κ₁, _, _⟩ := IsAccessibleCategory.exists_cardinal C + obtain ⟨κ₂, _, _⟩ := IsAccessibleCategory.exists_cardinal D + choose κ₃ _ hκ₃ using fun i ↦ Functor.IsAccessible.exists_cardinal (F i) + obtain ⟨κ₃', hκ₃' , hκ₃''⟩ := + HasCardinalLT.exists_regular_cardinal_forall (fun i ↦ (κ₃ i).ord.ToType) + have : Fact κ₃'.IsRegular := ⟨hκ₃'⟩ + obtain ⟨κ, _, hκ₁, hκ₂, hκ₃⟩ := Cardinal.SharplyLT.exists_of_triple κ₁ κ₂ κ₃' + refine ⟨κ, inferInstance, hκ₁.isCardinalAccessibleCategory C, + hκ₂.isCardinalAccessibleCategory D, + fun i ↦ Functor.isCardinalAccessible_of_le _ (show κ₃ i ≤ κ from ?_)⟩ + have := (hκ₃'' i) + simp only [hasCardinalLT_iff_cardinal_mk_lt, Cardinal.mk_toType, Cardinal.card_ord] at this + exact this.le.trans hκ₃.le + obtain ⟨κ₀, _, hκ₀⟩ : ∃ (κ₀ : Cardinal.{w}) (_ : Fact κ₀.IsRegular), + ∀ (i : ι), (isCardinalPresentable C κ).map (F i) ≤ isCardinalPresentable D κ₀ := by + choose κ' hκ' hκ'' using + fun i ↦ ObjectProperty.le_isCardinalPresentable.{w} ((isCardinalPresentable C κ).map (F i)) + obtain ⟨κ'', h₁, h₂⟩ := + HasCardinalLT.exists_regular_cardinal_forall (fun i ↦ (κ' i).ord.ToType) + have : Fact κ''.IsRegular := ⟨h₁⟩ + refine ⟨κ'', inferInstance, fun i ↦ (hκ'' i).trans ?_⟩ + have := h₂ i + simp only [hasCardinalLT_iff_cardinal_mk_lt, Cardinal.mk_toType, Cardinal.card_ord] at this + exact isCardinalPresentable_monotone _ this.le + obtain ⟨κ', _, h₁, h₂⟩ := Cardinal.SharplyLT.exists_of_pair κ κ₀ + exact ⟨κ', inferInstance, h₁.isCardinalAccessibleCategory C, + h₁.isCardinalAccessibleCategory D, + fun i ↦ Functor.isCardinalAccessible_of_le _ h₁.le, + fun i ↦ uniformization' _ h₁ + (fun X hX ↦ isCardinalPresentable_monotone _ h₂.le _ + (hκ₀ i _ (ObjectProperty.prop_map_obj _ _ hX)))⟩ + +lemma uniformization (F : C ⥤ D) + [IsAccessibleCategory.{w} C] [IsAccessibleCategory.{w} D] + [Functor.IsAccessible.{w} F] : + ∃ (κ : Cardinal.{w}) (_ : Fact κ.IsRegular), + IsCardinalAccessibleCategory C κ ∧ + IsCardinalAccessibleCategory D κ ∧ + F.IsCardinalAccessible κ ∧ + isCardinalPresentable C κ ≤ (isCardinalPresentable D κ).inverseImage F := by + obtain ⟨κ, _, h₁, h₂, h₃, h₄⟩ := uniformization_of_small (fun (_ : Fin 1) ↦ F) + exact ⟨κ, inferInstance, h₁, h₂, h₃ 0, h₄ 0⟩ + +lemma uniformization_pair + {C₁ C₂ D₁ D₂ : Type*} [Category* C₁] [Category* C₂] [Category* D₁] [Category* D₂] + (F₁ : C₁ ⥤ D₁) (F₂ : C₂ ⥤ D₂) + [IsAccessibleCategory.{w} C₁] [IsAccessibleCategory.{w} C₂] + [IsAccessibleCategory.{w} D₁] [IsAccessibleCategory.{w} D₂] + [Functor.IsAccessible.{w} F₁] [Functor.IsAccessible.{w} F₂] : + ∃ (κ : Cardinal.{w}) (_ : Fact κ.IsRegular), + IsCardinalAccessibleCategory C₁ κ ∧ IsCardinalAccessibleCategory D₁ κ ∧ + IsCardinalAccessibleCategory C₂ κ ∧ IsCardinalAccessibleCategory D₂ κ ∧ + F₁.IsCardinalAccessible κ ∧ F₂.IsCardinalAccessible κ ∧ + F₁.PreservesCardinalPresentable κ ∧ + F₂.PreservesCardinalPresentable κ := by + obtain ⟨κ, _, _, _, _, _, _, _⟩ : + ∃ (κ : Cardinal.{w}) (_ : Fact κ.IsRegular), + IsCardinalAccessibleCategory C₁ κ ∧ IsCardinalAccessibleCategory D₁ κ ∧ + IsCardinalAccessibleCategory C₂ κ ∧ IsCardinalAccessibleCategory D₂ κ ∧ + F₁.IsCardinalAccessible κ ∧ F₂.IsCardinalAccessible κ := by + obtain ⟨κ₁, _, _⟩ := IsAccessibleCategory.exists_cardinal C₁ + obtain ⟨κ₁', _, _⟩ := IsAccessibleCategory.exists_cardinal D₁ + obtain ⟨κ₁'', _, _⟩ := Functor.IsAccessible.exists_cardinal F₁ + obtain ⟨κ₂, _, _⟩ := IsAccessibleCategory.exists_cardinal C₂ + obtain ⟨κ₂', _, _⟩ := IsAccessibleCategory.exists_cardinal D₂ + obtain ⟨κ₂'', _, _⟩ := Functor.IsAccessible.exists_cardinal F₂ + obtain ⟨α₁, _, h₁, h₁', h₁''⟩ := Cardinal.SharplyLT.exists_of_triple κ₁ κ₁' κ₁'' + obtain ⟨α₂, _, h₂, h₂', h₂''⟩ := Cardinal.SharplyLT.exists_of_triple κ₂ κ₂' κ₂'' + obtain ⟨κ, _, hκ₁, hκ₂⟩ := Cardinal.SharplyLT.exists_of_pair α₁ α₂ + exact ⟨κ, inferInstance, + (h₁.trans hκ₁).isCardinalAccessibleCategory C₁, + (h₁'.trans hκ₁).isCardinalAccessibleCategory D₁, + (h₂.trans hκ₂).isCardinalAccessibleCategory C₂, + (h₂'.trans hκ₂).isCardinalAccessibleCategory D₂, + Functor.isCardinalAccessible_of_le _ (h₁''.trans hκ₁).le, + Functor.isCardinalAccessible_of_le _ (h₂''.trans hκ₂).le⟩ + obtain ⟨κ₁, _, hκ₁⟩ := ((isCardinalPresentable C₁ κ).map F₁).le_isCardinalPresentable + obtain ⟨κ₂, _, hκ₂⟩ := ((isCardinalPresentable C₂ κ).map F₂).le_isCardinalPresentable + obtain ⟨κ', _, hκ, hκ₁', hκ₂'⟩ := Cardinal.SharplyLT.exists_of_triple κ κ₁ κ₂ + refine ⟨κ', inferInstance, hκ.isCardinalAccessibleCategory _, + hκ.isCardinalAccessibleCategory _, hκ.isCardinalAccessibleCategory _, + hκ.isCardinalAccessibleCategory _, + Functor.isCardinalAccessible_of_le _ hκ.le, + Functor.isCardinalAccessible_of_le _ hκ.le, + ⟨uniformization' _ hκ (fun X₁ hX₁ ↦ ?_)⟩, + ⟨uniformization' _ hκ (fun X₂ hX₂ ↦ ?_)⟩⟩ + · have := hκ₁ _ (ObjectProperty.prop_map_obj _ F₁ hX₁) + exact isCardinalPresentable_of_le _ hκ₁'.le + · have := hκ₂ _ (ObjectProperty.prop_map_obj _ F₂ hX₂) + exact isCardinalPresentable_of_le _ hκ₂'.le + +end IsCardinalAccessibleCategory + +end CategoryTheory