feat(CategoryTheory): comma categories are accessible

Mathlib.lean

@@ -1692,6 +1692,7 @@ import Mathlib.CategoryTheory.CofilteredSystem
 import Mathlib.CategoryTheory.CommSq
 import Mathlib.CategoryTheory.Comma.Arrow
 import Mathlib.CategoryTheory.Comma.Basic
+import Mathlib.CategoryTheory.Comma.CardinalArrow
 import Mathlib.CategoryTheory.Comma.Final
 import Mathlib.CategoryTheory.Comma.LocallySmall
 import Mathlib.CategoryTheory.Comma.Over
@@ -2080,6 +2081,13 @@ import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
+import Mathlib.CategoryTheory.Presentable.Basic
+import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
+import Mathlib.CategoryTheory.Presentable.Comma
+import Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
+import Mathlib.CategoryTheory.Presentable.Limits
+import Mathlib.CategoryTheory.Presentable.LocallyPresentable
+import Mathlib.CategoryTheory.Presentable.ParallelMaps
 import Mathlib.CategoryTheory.Products.Associator
 import Mathlib.CategoryTheory.Products.Basic
 import Mathlib.CategoryTheory.Products.Bifunctor
@@ -4705,6 +4713,7 @@ import Mathlib.SetTheory.Cardinal.ENat
 import Mathlib.SetTheory.Cardinal.Finite
 import Mathlib.SetTheory.Cardinal.Finsupp
 import Mathlib.SetTheory.Cardinal.Free
+import Mathlib.SetTheory.Cardinal.HasCardinalLT
 import Mathlib.SetTheory.Cardinal.SchroederBernstein
 import Mathlib.SetTheory.Cardinal.Subfield
 import Mathlib.SetTheory.Cardinal.ToNat

Mathlib/CategoryTheory/Comma/Arrow.lean

@@ -333,4 +333,25 @@ def Arrow.isoOfNatIso {C D : Type*} [Category C] [Category D] {F G : C ⥤ D} (e
     (f : Arrow C) : F.mapArrow.obj f ≅ G.mapArrow.obj f :=
   Arrow.isoMk (e.app f.left) (e.app f.right)
 
+variable (T)
+
+/-- `Arrow T` is equivalent to a sigma type. -/
+@[simps!]
+def Arrow.equivSigma :
+    Arrow T ≃ Σ (X Y : T), X ⟶ Y where
+  toFun f := ⟨_, _, f.hom⟩
+  invFun x := Arrow.mk x.2.2
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+/-- The equivalence `Arrow (Discrete S) ≃ S`. -/
+def Arrow.discreteEquiv (S : Type u) : Arrow (Discrete S) ≃ S where
+  toFun f := f.left.as
+  invFun s := Arrow.mk (𝟙 (Discrete.mk s))
+  left_inv := by
+    rintro ⟨⟨_⟩, ⟨_⟩, f⟩
+    obtain rfl := Discrete.eq_of_hom f
+    rfl
+  right_inv _ := rfl
+
 end CategoryTheory

Mathlib/CategoryTheory/Comma/CardinalArrow.lean

@@ -0,0 +1,121 @@
+/-
+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
+-/
+
+import Mathlib.CategoryTheory.Comma.Arrow
+import Mathlib.CategoryTheory.FinCategory.Basic
+import Mathlib.CategoryTheory.EssentiallySmall
+import Mathlib.Data.Set.Finite.Basic
+import Mathlib.SetTheory.Cardinal.HasCardinalLT
+
+/-!
+# Cardinal of Arrow
+
+We obtain various results about the cardinality of `Arrow C`. For example,
+If `A` is a (small) category, `Arrow C` is finite iff `FinCategory C` holds.
+
+-/
+
+universe w w' v u
+
+namespace CategoryTheory
+
+lemma Arrow.finite_iff (C : Type u) [SmallCategory C] :
+    Finite (Arrow C) ↔ Nonempty (FinCategory C) := by
+  constructor
+  · intro
+    refine ⟨?_, fun a b ↦ ?_⟩
+    · have := Finite.of_injective (fun (a : C) ↦ Arrow.mk (𝟙 a))
+        (fun _ _  ↦ congr_arg Comma.left)
+      apply Fintype.ofFinite
+    · have := Finite.of_injective (fun (f : a ⟶ b) ↦ Arrow.mk f)
+        (fun f g h ↦ by
+          change (Arrow.mk f).hom = (Arrow.mk g).hom
+          congr)
+      apply Fintype.ofFinite
+  · rintro ⟨_⟩
+    have := Fintype.ofEquiv  _ (Arrow.equivSigma C).symm
+    infer_instance
+
+instance Arrow.finite {C : Type u} [SmallCategory C] [FinCategory C] :
+    Finite (Arrow C) := by
+  rw [Arrow.finite_iff]
+  exact ⟨inferInstance⟩
+
+/-- The bijection `Arrow Cᵒᵖ ≃ Arrow C`. -/
+def Arrow.opEquiv (C : Type u) [Category.{v} C] : Arrow Cᵒᵖ ≃ Arrow C where
+  toFun f := Arrow.mk f.hom.unop
+  invFun g := Arrow.mk g.hom.op
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+@[simp]
+lemma hasCardinal_arrow_op_iff (C : Type u) [Category.{v} C] (κ : Cardinal.{w}) :
+    HasCardinalLT (Arrow Cᵒᵖ) κ ↔ HasCardinalLT (Arrow C) κ :=
+  hasCardinalLT_iff_of_equiv (Arrow.opEquiv C) κ
+
+@[simp]
+lemma hasCardinalLT_arrow_discrete_iff {X : Type u} (κ : Cardinal.{w}) :
+    HasCardinalLT (Arrow (Discrete X)) κ ↔ HasCardinalLT X κ :=
+  hasCardinalLT_iff_of_equiv (Arrow.discreteEquiv X) κ
+
+lemma small_of_small_arrow (C : Type u) [Category.{v} C] [Small.{w} (Arrow C)] :
+    Small.{w} C :=
+  small_of_injective (f := fun X ↦ Arrow.mk (𝟙 X)) (fun _ _ h ↦ congr_arg Comma.left h)
+
+lemma locallySmall_of_small_arrow (C : Type u) [Category.{v} C] [Small.{w} (Arrow C)] :
+    LocallySmall.{w} C where
+  hom_small X Y :=
+    small_of_injective (f := fun f ↦ Arrow.mk f) (fun f g h ↦ by
+      change (Arrow.mk f).hom = (Arrow.mk g).hom
+      congr)
+
+/-- The bijection `Arrow.{w} (ShrinkHoms C) ≃ Arrow C`. -/
+noncomputable def Arrow.shrinkHomsEquiv (C : Type u) [Category.{v} C] [LocallySmall.{w} C] :
+    Arrow.{w} (ShrinkHoms C) ≃ Arrow C where
+  toFun := (ShrinkHoms.equivalence C).inverse.mapArrow.obj
+  invFun := (ShrinkHoms.equivalence C).functor.mapArrow.obj
+  left_inv _ := by simp [Functor.mapArrow]; rfl
+  right_inv _ := by simp [Functor.mapArrow]; rfl
+
+-- to be moved
+lemma Arrow.ext {C : Type u} [Category.{v} C] {f g : Arrow C}
+    (h₁ : f.left = g.left) (h₂ : f.right = g.right)
+    (h₃ : f.hom = eqToHom h₁ ≫ g.hom ≫ eqToHom h₂.symm) : f = g := by
+  obtain ⟨X, Y, f⟩ := f
+  obtain ⟨X', Y', g⟩ := g
+  obtain rfl : X = X' := h₁
+  obtain rfl : Y = Y' := h₂
+  obtain rfl : f = g := by simpa using h₃
+  rfl
+
+/-- The bijection `Arrow (Shrink C) ≃ Arrow C`. -/
+noncomputable def Arrow.shrinkEquiv (C : Type u) [Category.{v} C] [Small.{w} C] :
+    Arrow (Shrink.{w} C) ≃ Arrow C where
+  toFun := (Shrink.equivalence C).inverse.mapArrow.obj
+  invFun := (Shrink.equivalence C).functor.mapArrow.obj
+  left_inv f := Arrow.ext (by simp [Shrink.equivalence])
+    (by simp [Shrink.equivalence]) (by simp [Shrink.equivalence]; rfl)
+  right_inv _ := Arrow.ext (by simp [Shrink.equivalence])
+    (by simp [Shrink.equivalence]) (by simp [Shrink.equivalence])
+
+@[simp]
+lemma hasCardinalLT_arrow_shrinkHoms_iff (C : Type u) [Category.{v} C] [LocallySmall.{w'} C]
+    (κ : Cardinal.{w}) :
+    HasCardinalLT (Arrow.{w'} (ShrinkHoms C)) κ ↔ HasCardinalLT (Arrow C) κ :=
+  hasCardinalLT_iff_of_equiv (Arrow.shrinkHomsEquiv C) κ
+
+@[simp]
+lemma hasCardinalLT_arrow_shrink_iff (C : Type u) [Category.{v} C] [Small.{w'} C]
+    (κ : Cardinal.{w}) :
+    HasCardinalLT (Arrow (Shrink.{w'} C)) κ ↔ HasCardinalLT (Arrow C) κ :=
+  hasCardinalLT_iff_of_equiv (Arrow.shrinkEquiv C) κ
+
+lemma hasCardinalLT_of_hasCardinalLT_arrow
+    {C : Type u} [Category.{v} C] {κ : Cardinal.{w}} (h : HasCardinalLT (Arrow C) κ) :
+    HasCardinalLT C κ :=
+  h.of_injective (fun X ↦ Arrow.mk (𝟙 X)) (fun _ _ h ↦ congr_arg Comma.left h)
+
+end CategoryTheory

Mathlib/CategoryTheory/EssentiallySmall.lean

@@ -22,7 +22,7 @@ the type `Skeleton C` is `w`-small, and `C` is `w`-locally small.
 -/
 
 
-universe w v v' u u'
+universe w w' v v' u u'
 
 open CategoryTheory
 
@@ -188,8 +188,32 @@ noncomputable instance [Small.{w} C] : Category.{v} (Shrink.{w} C) :=
   InducedCategory.category (equivShrink C).symm
 
 /-- The categorical equivalence between `C` and `Shrink C`, when `C` is small. -/
-noncomputable def equivalence [Small.{w} C] : C ≌ Shrink.{w} C :=
-  (inducedFunctor (equivShrink C).symm).asEquivalence.symm
+noncomputable def equivalence [Small.{w} C] : C ≌ Shrink.{w} C where
+  functor :=
+    { obj := equivShrink C
+      map {X Y} f := by
+        change (equivShrink C).symm _ ⟶ (equivShrink C).symm _
+        exact eqToHom (by simp) ≫ f ≫ eqToHom (by simp)
+      map_comp f g := by
+        dsimp
+        erw [Category.assoc, Category.assoc, Category.assoc]
+        rw [eqToHom_trans_assoc, eqToHom_refl, Category.id_comp] }
+  inverse := inducedFunctor (equivShrink C).symm
+  unitIso := NatIso.ofComponents (fun X ↦ eqToIso (by simp))
+  counitIso := NatIso.ofComponents (fun X ↦ eqToIso (by simp)) (fun {X Y} f ↦ by
+    dsimp
+    erw [Category.assoc, Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id]
+    · rfl
+    · simp)
+  functor_unitIso_comp X := by
+    dsimp
+    simp only [eqToHom_trans]
+    exact eqToHom_trans (by simp) _
+
+instance (C : Type u) [Category.{v} C] [Small.{w'} C] [LocallySmall.{w} C] :
+    LocallySmall.{w} (Shrink.{w'} C) where
+  hom_small _ _ := small_of_injective
+    (fun _ _ h ↦ (Shrink.equivalence.{w'} C).inverse.map_injective h)
 
 end Shrink
 

Mathlib/CategoryTheory/Limits/Comma.lean

@@ -153,6 +153,24 @@ instance hasColimitsOfSize [HasColimitsOfSize.{w, w'} A] [HasColimitsOfSize.{w,
     [PreservesColimitsOfSize.{w, w'} L] : HasColimitsOfSize.{w, w'} (Comma L R) :=
   ⟨fun _ _ => inferInstance⟩
 
+instance preservesColimitsOfShape_fst
+    [HasColimitsOfShape J A] [HasColimitsOfShape J B]
+    [PreservesColimitsOfShape J L] :
+    PreservesColimitsOfShape J (Comma.fst L R) where
+  preservesColimit {F} :=
+    preservesColimit_of_preserves_colimit_cocone (h :=
+      coconeOfPreservesIsColimit F (colimit.isColimit _) (colimit.isColimit _))
+      ((colimit.isColimit _))
+
+instance preservesColimitsOfShape_snd
+    [HasColimitsOfShape J A] [HasColimitsOfShape J B]
+    [PreservesColimitsOfShape J L] :
+    PreservesColimitsOfShape J (Comma.snd L R) where
+  preservesColimit {F} :=
+    preservesColimit_of_preserves_colimit_cocone (h :=
+      coconeOfPreservesIsColimit F (colimit.isColimit _) (colimit.isColimit _))
+      ((colimit.isColimit _))
+
 end Comma
 
 namespace Arrow

Mathlib/CategoryTheory/Limits/TypesFiltered.lean

@@ -75,6 +75,16 @@ noncomputable def isColimitOf (t : Cocone F) (hsurj : ∀ x : t.pt, ∃ i xi, x
 
 variable [IsFilteredOrEmpty J]
 
+/-- Recognizing filtered colimits of types. The injectivity condition here is
+slightly easier to check as compared to `isColimitOf`. -/
+noncomputable def isColimitOf' (t : Cocone F) (hsurj : ∀ x : t.pt, ∃ i xi, x = t.ι.app i xi)
+    (hinj : ∀ i x y, t.ι.app i x = t.ι.app i y → ∃ (k : _) (f : i ⟶ k), F.map f x = F.map f y) :
+    IsColimit t :=
+  isColimitOf _ _ hsurj (fun i j xi xj h ↦ by
+    obtain ⟨k, g, hg⟩ := hinj (IsFiltered.max i j) (F.map (IsFiltered.leftToMax i j) xi)
+      (F.map (IsFiltered.rightToMax i j) xj) (by simp [FunctorToTypes.naturality, h])
+    exact ⟨k, IsFiltered.leftToMax i j ≫ g, IsFiltered.rightToMax i j ≫ g, by simpa using hg⟩)
+
 protected theorem rel_equiv : _root_.Equivalence (FilteredColimit.Rel.{v, u} F) where
   refl x := ⟨x.1, 𝟙 x.1, 𝟙 x.1, rfl⟩
   symm := fun ⟨k, f, g, h⟩ => ⟨k, g, f, h.symm⟩
@@ -99,9 +109,7 @@ protected theorem rel_eq_eqvGen_quot_rel :
   · rw [← (FilteredColimit.rel_equiv F).eqvGen_iff]
     exact Relation.EqvGen.mono (rel_of_quot_rel F)
 
-variable [HasColimit F]
-
-theorem colimit_eq_iff_aux {i j : J} {xi : F.obj i} {xj : F.obj j} :
+theorem colimit_eq_iff_aux [HasColimit F] {i j : J} {xi : F.obj i} {xj : F.obj j} :
     (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj ↔
       FilteredColimit.Rel.{v, u} F ⟨i, xi⟩ ⟨j, xj⟩ := by
   dsimp
@@ -110,6 +118,7 @@ theorem colimit_eq_iff_aux {i j : J} {xi : F.obj i} {xj : F.obj j} :
 
 theorem isColimit_eq_iff {t : Cocone F} (ht : IsColimit t) {i j : J} {xi : F.obj i} {xj : F.obj j} :
     t.ι.app i xi = t.ι.app j xj ↔ ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj := by
+  have : HasColimit F := ⟨_, ht⟩
   refine Iff.trans ?_ (colimit_eq_iff_aux F)
   rw [← (IsColimit.coconePointUniqueUpToIso ht (colimitCoconeIsColimit F)).toEquiv.injective.eq_iff]
   convert Iff.rfl
@@ -118,7 +127,19 @@ theorem isColimit_eq_iff {t : Cocone F} (ht : IsColimit t) {i j : J} {xi : F.obj
   · exact (congrFun
       (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xj).symm
 
-theorem colimit_eq_iff {i j : J} {xi : F.obj i} {xj : F.obj j} :
+variable {F} in
+theorem isColimit_eq_iff' {t : Cocone F} (ht : IsColimit t) {i : J} (x y : F.obj i) :
+    t.ι.app i x = t.ι.app i y ↔ ∃ (j : _) (f : i ⟶ j), F.map f x = F.map f y := by
+  rw [isColimit_eq_iff _ ht]
+  constructor
+  · rintro ⟨k, f, g, h⟩
+    refine ⟨IsFiltered.coeq f g, f ≫ IsFiltered.coeqHom f g, ?_⟩
+    conv_rhs => rw [IsFiltered.coeq_condition]
+    simp only [FunctorToTypes.map_comp_apply, h]
+  · rintro ⟨j, f, h⟩
+    exact ⟨j, f, f, h⟩
+
+theorem colimit_eq_iff [HasColimit F] {i j : J} {xi : F.obj i} {xj : F.obj j} :
     colimit.ι F i xi = colimit.ι F j xj ↔
       ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj :=
   isColimit_eq_iff _ (colimit.isColimit F)