[Merged by Bors] - feat: existence of a limit in a concrete category implies smallness

Mathlib.lean

@@ -1256,6 +1256,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
 import Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
 import Mathlib.CategoryTheory.Limits.SmallComplete
 import Mathlib.CategoryTheory.Limits.Types
+import Mathlib.CategoryTheory.Limits.TypesFiltered
 import Mathlib.CategoryTheory.Limits.Unit
 import Mathlib.CategoryTheory.Limits.VanKampen
 import Mathlib.CategoryTheory.Limits.Yoneda

Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

@@ -6,7 +6,7 @@ Authors: Justus Springer
 import Mathlib.Algebra.Category.MonCat.Limits
 import Mathlib.CategoryTheory.Limits.Preserves.Filtered
 import Mathlib.CategoryTheory.ConcreteCategory.Elementwise
-import Mathlib.CategoryTheory.Limits.Types
+import Mathlib.CategoryTheory.Limits.TypesFiltered
 
 #align_import algebra.category.Mon.filtered_colimits from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
 

Mathlib/CategoryTheory/Filtered/Final.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Filtered.Connected
+import Mathlib.CategoryTheory.Limits.TypesFiltered
 import Mathlib.CategoryTheory.Limits.Final
 
 /-!

Mathlib/CategoryTheory/Limits/ConcreteCategory.lean

@@ -5,7 +5,8 @@ Authors: Scott Morrison, Adam Topaz
 -/
 import Mathlib.CategoryTheory.ConcreteCategory.Basic
 import Mathlib.CategoryTheory.Limits.Preserves.Basic
-import Mathlib.CategoryTheory.Limits.Types
+import Mathlib.CategoryTheory.Limits.TypesFiltered
+import Mathlib.CategoryTheory.Limits.Yoneda
 import Mathlib.Tactic.ApplyFun
 
 #align_import category_theory.limits.concrete_category from "leanprover-community/mathlib"@"c3019c79074b0619edb4b27553a91b2e82242395"
@@ -25,6 +26,15 @@ attribute [local instance] ConcreteCategory.instFunLike ConcreteCategory.hasCoeT
 
 section Limits
 
+/-- If a functor `G : J ⥤ C` to a concrete category has a limit and that `forget C`
+is corepresentable, then `G ⋙ forget C).sections` is small. -/
+lemma Concrete.small_sections_of_hasLimit
+    {C : Type u} [Category.{v} C] [ConcreteCategory.{v} C]
+    [(forget C).Corepresentable] {J : Type w} [Category.{t} J] (G : J ⥤ C) [HasLimit G] :
+    Small.{v} (G ⋙ forget C).sections := by
+  rw [← Types.hasLimit_iff_small_sections]
+  infer_instance
+
 variable {C : Type u} [Category.{v} C] [ConcreteCategory.{max w v} C] {J : Type w} [SmallCategory J]
   (F : J ⥤ C) [PreservesLimit F (forget C)]
 

Mathlib/CategoryTheory/Limits/Filtered.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
+import Mathlib.CategoryTheory.Filtered.Basic
 import Mathlib.CategoryTheory.Limits.HasLimits
 import Mathlib.CategoryTheory.Limits.Types
 

Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Limits.ColimitLimit
 import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
 import Mathlib.CategoryTheory.Limits.Preserves.Finite
 import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
+import Mathlib.CategoryTheory.Limits.TypesFiltered
 import Mathlib.CategoryTheory.ConcreteCategory.Basic
 import Mathlib.CategoryTheory.Products.Bifunctor
 import Mathlib.Data.Countable.Small

Mathlib/CategoryTheory/Limits/Final.lean

@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Comma.StructuredArrow
 import Mathlib.CategoryTheory.IsConnected
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
 import Mathlib.CategoryTheory.Limits.Shapes.Types
+import Mathlib.CategoryTheory.Filtered.Basic
 import Mathlib.CategoryTheory.Limits.Yoneda
 import Mathlib.CategoryTheory.PUnit
 

Mathlib/CategoryTheory/Limits/Preserves/Finite.lean

@@ -108,6 +108,14 @@ class PreservesFiniteProducts (F : C ⥤ D) where
 
 attribute [instance] PreservesFiniteProducts.preserves
 
+instance compPreservesFiniteProducts (F : C ⥤ D) (G : D ⥤ E)
+    [PreservesFiniteProducts F] [PreservesFiniteProducts G] :
+    PreservesFiniteProducts (F ⋙ G) where
+  preserves _ _ := by infer_instance
+
+noncomputable instance (F : C ⥤ D) [PreservesFiniteLimits F] : PreservesFiniteProducts F where
+  preserves _ _ := by infer_instance
+
 /-- A functor is said to preserve finite colimits, if it preserves all colimits of
 shape `J`, where `J : Type` is a finite category.
 -/
@@ -184,4 +192,12 @@ class PreservesFiniteCoproducts (F : C ⥤ D) where
 
 attribute [instance] PreservesFiniteCoproducts.preserves
 
+instance compPreservesFiniteCoproducts (F : C ⥤ D) (G : D ⥤ E)
+    [PreservesFiniteCoproducts F] [PreservesFiniteCoproducts G] :
+    PreservesFiniteCoproducts (F ⋙ G) where
+  preserves _ _ := by infer_instance
+
+noncomputable instance (F : C ⥤ D) [PreservesFiniteColimits F] : PreservesFiniteCoproducts F where
+  preserves _ _ := by infer_instance
+
 end CategoryTheory.Limits

Mathlib/CategoryTheory/Limits/Types.lean

@@ -6,7 +6,7 @@ Authors: Scott Morrison, Reid Barton
 import Mathlib.Data.TypeMax
 import Mathlib.Logic.UnivLE
 import Mathlib.CategoryTheory.Limits.Shapes.Images
-import Mathlib.CategoryTheory.Filtered.Basic
+
 
 #align_import category_theory.limits.types from "leanprover-community/mathlib"@"4aa2a2e17940311e47007f087c9df229e7f12942"
 
@@ -15,9 +15,6 @@ import Mathlib.CategoryTheory.Filtered.Basic
 
 We show that the category of types has all (co)limits, by providing the usual concrete models.
 
-We also give a characterisation of filtered colimits in `Type`, via
-`colimit.ι F i xi = colimit.ι F j xj ↔ ∃ k (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj`.
-
 Next, we prove the category of types has categorical images, and that these agree with the range of
 a function.
 
@@ -147,12 +144,12 @@ noncomputable def limitConeIsLimit : IsLimit (limitCone.{v, u} F) where
 
 end
 
-theorem hasLimit_iff_small_sections : HasLimit F ↔ Small.{u} F.sections :=
+end Small
+
+theorem hasLimit_iff_small_sections (F : J ⥤ Type u): HasLimit F ↔ Small.{u} F.sections :=
   ⟨fun _ => .mk ⟨_, ⟨(Equiv.ofBijective _
     ((isLimit_iff_bijective_sectionOfCone (limit.cone F)).mp ⟨limit.isLimit _⟩)).symm⟩⟩,
-   fun _ => ⟨_, limitConeIsLimit F⟩⟩
-
-end Small
+   fun _ => ⟨_, Small.limitConeIsLimit F⟩⟩
 
 -- TODO: If `UnivLE` works out well, we will eventually want to deprecate these
 -- definitions, and probably as a first step put them in namespace or otherwise rename them.
@@ -198,7 +195,7 @@ section UnivLE
 open UnivLE
 
 instance hasLimit [Small.{u} J] (F : J ⥤ Type u) : HasLimit F :=
-  (Small.hasLimit_iff_small_sections F).mpr inferInstance
+  (hasLimit_iff_small_sections F).mpr inferInstance
 
 instance hasLimitsOfShape [Small.{u} J] : HasLimitsOfShape J (Type u) where
 
@@ -623,124 +620,6 @@ theorem jointly_surjective' (x : colimit F) :
   jointly_surjective F (colimit.isColimit F) x
 #align category_theory.limits.types.jointly_surjective' CategoryTheory.Limits.Types.jointly_surjective'
 
-namespace FilteredColimit
-
-/- For filtered colimits of types, we can give an explicit description
-  of the equivalence relation generated by the relation used to form
-  the colimit.  -/
-
-/-- An alternative relation on `Σ j, F.obj j`,
-which generates the same equivalence relation as we use to define the colimit in `Type` above,
-but that is more convenient when working with filtered colimits.
-
-Elements in `F.obj j` and `F.obj j'` are equivalent if there is some `k : J` to the right
-where their images are equal.
--/
-protected def Rel (x y : Σ j, F.obj j) : Prop :=
-  ∃ (k : _) (f : x.1 ⟶ k) (g : y.1 ⟶ k), F.map f x.2 = F.map g y.2
-#align category_theory.limits.types.filtered_colimit.rel CategoryTheory.Limits.Types.FilteredColimit.Rel
-
-theorem rel_of_quot_rel (x y : Σ j, F.obj j) :
-    Quot.Rel F x y → FilteredColimit.Rel.{v, u} F x y :=
-  fun ⟨f, h⟩ => ⟨y.1, f, 𝟙 y.1, by rw [← h, FunctorToTypes.map_id_apply]⟩
-#align category_theory.limits.types.filtered_colimit.rel_of_quot_rel CategoryTheory.Limits.Types.FilteredColimit.rel_of_quot_rel
-
-theorem eqvGen_quot_rel_of_rel (x y : Σ j, F.obj j) :
-    FilteredColimit.Rel.{v, u} F x y → EqvGen (Quot.Rel F) x y := fun ⟨k, f, g, h⟩ => by
-  refine' EqvGen.trans _ ⟨k, F.map f x.2⟩ _ _ _
-  · exact (EqvGen.rel _ _ ⟨f, rfl⟩)
-  · exact (EqvGen.symm _ _ (EqvGen.rel _ _ ⟨g, h⟩))
-#align category_theory.limits.types.filtered_colimit.eqv_gen_quot_rel_of_rel CategoryTheory.Limits.Types.FilteredColimit.eqvGen_quot_rel_of_rel
-
---attribute [local elab_without_expected_type] nat_trans.app
-
-/-- Recognizing filtered colimits of types. -/
-noncomputable def isColimitOf (t : Cocone F) (hsurj : ∀ x : t.pt, ∃ i xi, x = t.ι.app i xi)
-    (hinj :
-      ∀ i j xi xj,
-        t.ι.app i xi = t.ι.app j xj → ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj) :
-    IsColimit t := by
-  -- Strategy: Prove that the map from "the" colimit of F (defined above) to t.X
-  -- is a bijection.
-  apply IsColimit.ofIsoColimit (colimit.isColimit F)
-  refine' Cocones.ext (Equiv.toIso (Equiv.ofBijective _ _)) _
-  · exact colimit.desc F t
-  · constructor
-    · show Function.Injective _
-      intro a b h
-      rcases jointly_surjective F (colimit.isColimit F) a with ⟨i, xi, rfl⟩
-      rcases jointly_surjective F (colimit.isColimit F) b with ⟨j, xj, rfl⟩
-      replace h : (colimit.ι F i ≫ colimit.desc F t) xi = (colimit.ι F j ≫ colimit.desc F t) xj := h
-      rw [colimit.ι_desc, colimit.ι_desc] at h
-      rcases hinj i j xi xj h with ⟨k, f, g, h'⟩
-      change colimit.ι F i xi = colimit.ι F j xj
-      rw [← colimit.w F f, ← colimit.w F g]
-      change colimit.ι F k (F.map f xi) = colimit.ι F k (F.map g xj)
-      rw [h']
-    · show Function.Surjective _
-      intro x
-      rcases hsurj x with ⟨i, xi, rfl⟩
-      use colimit.ι F i xi
-      apply Colimit.ι_desc_apply
-  · intro j
-    apply colimit.ι_desc
-#align category_theory.limits.types.filtered_colimit.is_colimit_of CategoryTheory.Limits.Types.FilteredColimit.isColimitOf
-
-variable [IsFilteredOrEmpty J]
-
-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⟩
-  trans {x y z} := fun ⟨k, f, g, h⟩ ⟨k', f', g', h'⟩ =>
-    let ⟨l, fl, gl, _⟩ := IsFilteredOrEmpty.cocone_objs k k'
-    let ⟨m, n, hn⟩ := IsFilteredOrEmpty.cocone_maps (g ≫ fl) (f' ≫ gl)
-    ⟨m, f ≫ fl ≫ n, g' ≫ gl ≫ n,
-      calc
-        F.map (f ≫ fl ≫ n) x.2 = F.map (fl ≫ n) (F.map f x.2) := by simp
-        _ = F.map (fl ≫ n) (F.map g y.2) := by rw [h]
-        _ = F.map ((g ≫ fl) ≫ n) y.2 := by simp
-        _ = F.map ((f' ≫ gl) ≫ n) y.2 := by rw [hn]
-        _ = F.map (gl ≫ n) (F.map f' y.2) := by simp
-        _ = F.map (gl ≫ n) (F.map g' z.2) := by rw [h']
-        _ = F.map (g' ≫ gl ≫ n) z.2 := by simp⟩
-#align category_theory.limits.types.filtered_colimit.rel_equiv CategoryTheory.Limits.Types.FilteredColimit.rel_equiv
-
-protected theorem rel_eq_eqvGen_quot_rel :
-    FilteredColimit.Rel.{v, u} F = EqvGen (Quot.Rel F) := by
-  ext ⟨j, x⟩ ⟨j', y⟩
-  constructor
-  · apply eqvGen_quot_rel_of_rel
-  · rw [← (FilteredColimit.rel_equiv F).eqvGen_iff]
-    exact EqvGen.mono (rel_of_quot_rel F)
-#align category_theory.limits.types.filtered_colimit.rel_eq_eqv_gen_quot_rel CategoryTheory.Limits.Types.FilteredColimit.rel_eq_eqvGen_quot_rel
-
-theorem colimit_eq_iff_aux {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
-  rw [← (equivShrink _).symm.injective.eq_iff, Equiv.symm_apply_apply, Equiv.symm_apply_apply,
-    Quot.eq, FilteredColimit.rel_eq_eqvGen_quot_rel]
-#align category_theory.limits.types.filtered_colimit.colimit_eq_iff_aux CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff_aux
-
-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
-  refine' Iff.trans _ (colimit_eq_iff_aux F)
-  rw [← (IsColimit.coconePointUniqueUpToIso ht (colimitCoconeIsColimit F)).toEquiv.injective.eq_iff]
-  convert Iff.rfl
-  · exact (congrFun
-      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xi).symm
-  · exact (congrFun
-      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xj).symm
-#align category_theory.limits.types.filtered_colimit.is_colimit_eq_iff CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff
-
-theorem colimit_eq_iff {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)
-#align category_theory.limits.types.filtered_colimit.colimit_eq_iff CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff
-
-end FilteredColimit
-
 variable {α β : Type u} (f : α ⟶ β)
 
 section
@@ -809,16 +688,65 @@ end Types
 
 open Functor Opposite
 
+section
+
+variable {J C : Type*} [Category J] [Category C]
+
+/-- Sections of `F ⋙ coyoneda.obj (op X)` identify to natural
+transformations `(const J).obj X ⟶ F`. -/
+@[simps]
+def compCoyonedaSectionsEquiv (F : J ⥤ C) (X : C) :
+    (F ⋙ coyoneda.obj (op X)).sections ≃ ((const J).obj X ⟶ F) where
+  toFun s :=
+    { app := fun j => s.val j
+      naturality := fun j j' f => by
+        dsimp
+        rw [Category.id_comp]
+        exact (s.property f).symm }
+  invFun τ := ⟨τ.app, fun {j j'} f => by simpa using (τ.naturality f).symm⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+/-- Sections of `F.op ⋙ yoneda.obj X` identify to natural
+transformations `F ⟶ (const J).obj X`. -/
+@[simps]
+def opCompYonedaSectionsEquiv (F : J ⥤ C) (X : C) :
+    (F.op ⋙ yoneda.obj X).sections ≃ (F ⟶ (const J).obj X) where
+  toFun s :=
+    { app := fun j => s.val (op j)
+      naturality := fun j j' f => by
+        dsimp
+        rw [Category.comp_id]
+        exact (s.property f.op) }
+  invFun τ := ⟨fun j => τ.app j.unop, fun {j j'} f => by simp [τ.naturality f.unop]⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+/-- Sections of `F ⋙ yoneda.obj X` identify to natural
+transformations `(const J).obj X ⟶ F`. -/
+@[simps]
+def compYonedaSectionsEquiv (F : J ⥤ Cᵒᵖ) (X : C) :
+    (F ⋙ yoneda.obj X).sections ≃ ((const J).obj (op X) ⟶ F) where
+  toFun s :=
+    { app := fun j => (s.val j).op
+      naturality := fun j j' f => by
+        dsimp
+        rw [Category.id_comp]
+        exact Quiver.Hom.unop_inj (s.property f).symm }
+  invFun τ := ⟨fun j => (τ.app j).unop,
+    fun {j j'} f => Quiver.Hom.op_inj (by simpa using (τ.naturality f).symm)⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+end
+
 variable {J : Type v} [SmallCategory J] {C : Type u} [Category.{v} C]
 
 /-- A cone on `F` with cone point `X` is the same as an element of `lim Hom(X, F·)`. -/
-@[simps]
+@[simps!]
 noncomputable def limitCompCoyonedaIsoCone (F : J ⥤ C) (X : C) :
-    limit (F ⋙ coyoneda.obj (op X)) ≅ ((const J).obj X ⟶ F) where
-  hom := fun x => ⟨fun j => limit.π (F ⋙ coyoneda.obj (op X)) j x,
-    fun j j' f => by simpa using (congrFun (limit.w (F ⋙ coyoneda.obj (op X)) f) x).symm⟩
-  inv := fun ι => Types.Limit.mk _ (fun j => ι.app j)
-    fun j j' f => by simpa using (ι.naturality f).symm
+    limit (F ⋙ coyoneda.obj (op X)) ≅ ((const J).obj X ⟶ F) :=
+  ((Types.limitEquivSections _).trans (compCoyonedaSectionsEquiv F X)).toIso
 
 /-- A cone on `F` with cone point `X` is the same as an element of `lim Hom(X, F·)`,
     naturally in `X`. -/
@@ -836,12 +764,10 @@ noncomputable def whiskeringLimYonedaIsoCones : whiskeringLeft _ _ _ ⋙
   NatIso.ofComponents coyonedaCompLimIsoCones
 
 /-- A cocone on `F` with cocone point `X` is the same as an element of `lim Hom(F·, X)`. -/
-@[simps]
+@[simps!]
 noncomputable def limitCompYonedaIsoCocone (F : J ⥤ C) (X : C) :
-    limit (F.op ⋙ yoneda.obj X) ≅ (F ⟶ (const J).obj X) where
-  hom := fun x => ⟨fun j => limit.π (F.op ⋙ yoneda.obj X) (Opposite.op j) x,
-    fun j j' f => by simpa using congrFun (limit.w (F.op ⋙ yoneda.obj X) f.op) x⟩
-  inv := fun ι => Types.Limit.mk _ (fun j => ι.app j.unop) (by simp)
+    limit (F.op ⋙ yoneda.obj X) ≅ (F ⟶ (const J).obj X) :=
+  ((Types.limitEquivSections _).trans (opCompYonedaSectionsEquiv F X)).toIso
 
 /-- A cocone on `F` with cocone point `X` is the same as an element of `lim Hom(F·, X)`,
     naturally in `X`. -/