feat(category_theory): essentially_small categories (#6801)

Preparation for `well_powered`, then for `complete_semilattice_Inf|Sup` on `subobject X`, then for work on chain complexes.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/equivalence.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
 -/
 import category_theory.fully_faithful
+import category_theory.full_subcategory
 import category_theory.whiskering
 import category_theory.essential_image
 import tactic.slice
@@ -538,6 +539,13 @@ is_equivalence.mk (equivalence_inverse F)
   e.inverse.map f = e.inverse.map g ↔ f = g :=
 functor_map_inj_iff e.symm f g
 
+instance ess_surj_induced_functor {C' : Type*} (e : C' ≃ D) : ess_surj (induced_functor e) :=
+{ mem_ess_image := λ Y, ⟨e.symm Y, by simp⟩, }
+
+noncomputable
+instance induced_functor_of_equiv {C' : Type*} (e : C' ≃ D) : is_equivalence (induced_functor e) :=
+equivalence_of_fully_faithfully_ess_surj _
+
 end equivalence
 
 end category_theory

src/category_theory/essentially_small.lean

@@ -0,0 +1,210 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import logic.small
+import category_theory.skeletal
+
+/-!
+# Essentially small categories.
+
+A category given by `(C : Type u) [category.{v} C]` is `w`-essentially small
+if there exists a `small_model C : Type w` equipped with `[small_category (small_model C)]`.
+
+A category is `w`-locally small if every hom type is `w`-small.
+
+The main theorem here is that a category is `w`-essentially small iff
+the type `skeleton C` is `w`-small, and `C` is `w`-locally small.
+-/
+
+universes w v v' u u'
+
+open category_theory
+
+variables (C : Type u) [category.{v} C]
+
+namespace category_theory
+
+/-- A category is `essentially_small.{w}` if there exists
+an equivalence to some `S : Type w` with `[small_category S]`. -/
+class essentially_small (C : Type u) [category.{v} C] : Prop :=
+(equiv_small_category : ∃ (S : Type w) [small_category S], by exactI nonempty (C ≌ S))
+
+/-- Constructor for `essentially_small C` from an explicit small category witness. -/
+lemma essentially_small.mk' {C : Type u} [category.{v} C] {S : Type w} [small_category S]
+  (e : C ≌ S) : essentially_small.{w} C :=
+⟨⟨S, _, ⟨e⟩⟩⟩
+
+/--
+An arbitrarily chosen small model for an essentially small category.
+-/
+@[nolint has_inhabited_instance]
+def small_model (C : Type u) [category.{v} C] [essentially_small.{w} C] : Type w :=
+classical.some (@essentially_small.equiv_small_category C _ _)
+
+noncomputable
+instance small_category_small_model
+  (C : Type u) [category.{v} C] [essentially_small.{w} C] : small_category (small_model C) :=
+classical.some (classical.some_spec (@essentially_small.equiv_small_category C _ _))
+
+/--
+The (noncomputable) categorical equivalence between
+an essentially small category and its small model.
+-/
+noncomputable
+def equiv_small_model (C : Type u) [category.{v} C] [essentially_small.{w} C] : C ≌ small_model C :=
+nonempty.some (classical.some_spec (classical.some_spec
+  (@essentially_small.equiv_small_category C _ _)))
+
+lemma essentially_small_congr {C : Type u} [category.{v} C] {D : Type u'} [category.{v'} D]
+  (e : C ≌ D) : essentially_small.{w} C ↔ essentially_small.{w} D :=
+begin
+  fsplit,
+  { rintro ⟨S, 𝒮, ⟨f⟩⟩,
+    resetI,
+    exact essentially_small.mk' (e.symm.trans f), },
+  { rintro ⟨S, 𝒮, ⟨f⟩⟩,
+    resetI,
+    exact essentially_small.mk' (e.trans f), },
+end
+
+/--
+A category is `w`-locally small if every hom set is `w`-small.
+
+See `shrink_homs C` for a category instance where every hom set has been replaced by a small model.
+-/
+class locally_small (C : Type u) [category.{v} C] : Prop :=
+(hom_small : ∀ X Y : C, small.{w} (X ⟶ Y) . tactic.apply_instance)
+
+instance (C : Type u) [category.{v} C] [locally_small.{w} C] (X Y : C) :
+  small (X ⟶ Y) :=
+locally_small.hom_small X Y
+
+lemma locally_small_congr {C : Type u} [category.{v} C] {D : Type u'} [category.{v'} D]
+  (e : C ≌ D) : locally_small.{w} C ↔ locally_small.{w} D :=
+begin
+  fsplit,
+  { rintro ⟨L⟩,
+    fsplit,
+    intros X Y,
+    specialize L (e.inverse.obj X) (e.inverse.obj Y),
+    refine (small_congr _).mpr L,
+    exact equiv_of_fully_faithful e.inverse, },
+  { rintro ⟨L⟩,
+    fsplit,
+    intros X Y,
+    specialize L (e.functor.obj X) (e.functor.obj Y),
+    refine (small_congr _).mpr L,
+    exact equiv_of_fully_faithful e.functor, },
+end
+
+@[priority 100]
+instance locally_small_self (C : Type u) [category.{v} C] : locally_small.{v} C := {}
+
+@[priority 100]
+instance locally_small_of_essentially_small
+  (C : Type u) [category.{v} C] [essentially_small.{w} C] : locally_small.{w} C :=
+(locally_small_congr (equiv_small_model C)).mpr (category_theory.locally_small_self _)
+
+/--
+We define a type alias `shrink_homs C` for `C`. When we have `locally_small.{w} C`,
+we'll put a `category.{w}` instance on `shrink_homs C`.
+-/
+@[nolint has_inhabited_instance]
+def shrink_homs (C : Type u) := C
+
+namespace shrink_homs
+
+section
+variables {C' : Type*} -- a fresh variable with no category instance attached
+
+/-- Help the typechecker by explicitly translating from `C` to `shrink_homs C`. -/
+def to_shrink_homs {C' : Type*} (X : C') : shrink_homs C' := X
+/-- Help the typechecker by explicitly translating from `shrink_homs C` to `C`. -/
+def from_shrink_homs {C' : Type*} (X : shrink_homs C') : C' := X
+
+@[simp] lemma to_from (X : C') : from_shrink_homs (to_shrink_homs X) = X := rfl
+@[simp] lemma from_to (X : shrink_homs C') : to_shrink_homs (from_shrink_homs X) = X := rfl
+
+end
+
+variables (C) [locally_small.{w} C]
+
+@[simps]
+noncomputable
+instance : category.{w} (shrink_homs C) :=
+{ hom := λ X Y, shrink (from_shrink_homs X ⟶ from_shrink_homs Y),
+  id := λ X, equiv_shrink _ (𝟙 (from_shrink_homs X)),
+  comp := λ X Y Z f g,
+    equiv_shrink _ (((equiv_shrink _).symm f) ≫ ((equiv_shrink _).symm g)), }.
+
+/-- Implementation of `shrink_homs.equivalence`. -/
+@[simps]
+noncomputable
+def functor : C ⥤ shrink_homs C :=
+{ obj := λ X, to_shrink_homs X,
+  map := λ X Y f, equiv_shrink (X ⟶ Y) f, }
+
+/-- Implementation of `shrink_homs.equivalence`. -/
+@[simps]
+noncomputable
+def inverse : shrink_homs C ⥤ C :=
+{ obj := λ X, from_shrink_homs X,
+  map := λ X Y f, (equiv_shrink (from_shrink_homs X ⟶ from_shrink_homs Y)).symm f, }
+
+/--
+The categorical equivalence between `C` and `shrink_homs C`, when `C` is locally small.
+-/
+@[simps]
+noncomputable
+def equivalence : C ≌ shrink_homs C :=
+equivalence.mk (functor C) (inverse C)
+  (nat_iso.of_components (λ X, iso.refl X) (by tidy))
+  (nat_iso.of_components (λ X, iso.refl X) (by tidy))
+
+end shrink_homs
+
+/--
+A category is essentially small if and only if
+the underlying type of its skeleton (i.e. the "set" of isomorphism classes) is small,
+and it is locally small.
+-/
+theorem essentially_small_iff (C : Type u) [category.{v} C] :
+  essentially_small.{w} C ↔ small.{w} (skeleton C) ∧ locally_small.{w} C :=
+begin
+  -- This theorem is the only bit of real work in this file.
+  fsplit,
+  { intro h,
+    fsplit,
+    { rcases h with ⟨S, 𝒮, ⟨e⟩⟩,
+      resetI,
+      refine ⟨⟨skeleton S, ⟨_⟩⟩⟩,
+      exact e.skeleton_equiv, },
+    { resetI, apply_instance, }, },
+  { rintro ⟨⟨S, ⟨e⟩⟩, L⟩,
+    resetI,
+    let e' := (shrink_homs.equivalence C).skeleton_equiv.symm,
+    refine ⟨⟨S, _, ⟨_⟩⟩⟩,
+    apply induced_category.category (e'.trans e).symm,
+    refine (shrink_homs.equivalence C).trans
+      ((from_skeleton _).as_equivalence.symm.trans
+      ((induced_functor (e'.trans e).symm).as_equivalence.symm)), },
+end
+
+/--
+Any thin category is locally small.
+-/
+@[priority 100]
+instance locally_small_of_thin {C : Type u} [category.{v} C] [∀ X Y : C, subsingleton (X ⟶ Y)] :
+  locally_small.{w} C := {}
+
+/--
+A thin category is essentially small if and only if the underlying type of its skeleton is small.
+-/
+theorem essentially_small_iff_of_thin
+  {C : Type u} [category.{v} C] [∀ X Y : C, subsingleton (X ⟶ Y)] :
+  essentially_small.{w} C ↔ small.{w} (skeleton C) :=
+by simp [essentially_small_iff, category_theory.locally_small_of_thin]
+
+end category_theory

src/category_theory/skeletal.lean

@@ -77,16 +77,34 @@ instance : ess_surj (from_skeleton C) :=
 noncomputable instance : is_equivalence (from_skeleton C) :=
 equivalence.equivalence_of_fully_faithfully_ess_surj (from_skeleton C)
 
+lemma skeleton_skeletal : skeletal (skeleton C) :=
+begin
+  rintro X Y ⟨h⟩,
+  have : X.out ≈ Y.out := ⟨(from_skeleton C).map_iso h⟩,
+  simpa using quotient.sound this,
+end
+
 /-- The `skeleton` of `C` given by choice is a skeleton of `C`. -/
 noncomputable def skeleton_is_skeleton : is_skeleton_of C (skeleton C) (from_skeleton C) :=
-{ skel :=
-  begin
-    rintro X Y ⟨h⟩,
-    have : X.out ≈ Y.out := ⟨(from_skeleton C).map_iso h⟩,
-    simpa using quotient.sound this,
-  end,
+{ skel := skeleton_skeletal C,
   eqv := from_skeleton.is_equivalence C }
 
+section
+variables {C D}
+
+/--
+Two categories which are categorically equivalent have skeletons with equivalent objects.
+-/
+noncomputable
+def equivalence.skeleton_equiv (e : C ≌ D) : skeleton C ≃ skeleton D :=
+let f := ((from_skeleton C).as_equivalence.trans e).trans (from_skeleton D).as_equivalence.symm in
+{ to_fun := f.functor.obj,
+  inv_fun := f.inverse.obj,
+  left_inv := λ X, skeleton_skeletal C ⟨(f.unit_iso.app X).symm⟩,
+  right_inv := λ Y, skeleton_skeletal D ⟨(f.counit_iso.app Y)⟩, }
+
+end
+
 /--
 Construct the skeleton category by taking the quotient of objects. This construction gives a
 preorder with nice definitional properties, but is only really appropriate for thin categories.

src/data/equiv/basic.lean

@@ -2065,6 +2065,13 @@ def equiv_of_subsingleton_of_subsingleton [subsingleton α] [subsingleton β]
   left_inv := λ _, subsingleton.elim _ _,
   right_inv := λ _, subsingleton.elim _ _ }
 
+/-- A nonempty subsingleton type is (noncomputably) equivalent to `punit`. -/
+noncomputable
+def equiv.punit_of_nonempty_of_subsingleton {α : Sort*} [h : nonempty α] [subsingleton α] :
+  α ≃ punit.{v} :=
+equiv_of_subsingleton_of_subsingleton
+ (λ _, punit.star) (λ _, h.some)
+
 /-- `unique (unique α)` is equivalent to `unique α`. -/
 def unique_unique_equiv : unique (unique α) ≃ unique α :=
 equiv_of_subsingleton_of_subsingleton (λ h, h.default)

src/data/fintype/basic.lean

@@ -370,7 +370,7 @@ theorem card_eq {α β} [F : fintype α] [G : fintype β] : card α = card β 
      ... ≃ β : (trunc.out (equiv_fin β)).symm⟩,
 λ ⟨f⟩, card_congr f⟩
 
-/-- Subsingleton types are fintypes (with zero or one terms). -/
+/-- Any subsingleton type with a witness is a fintype (with one term). -/
 def of_subsingleton (a : α) [subsingleton α] : fintype α :=
 ⟨{a}, λ b, finset.mem_singleton.2 (subsingleton.elim _ _)⟩
 
@@ -380,6 +380,17 @@ def of_subsingleton (a : α) [subsingleton α] : fintype α :=
 @[simp] theorem card_of_subsingleton (a : α) [subsingleton α] :
   @fintype.card _ (of_subsingleton a) = 1 := rfl
 
+open_locale classical
+variables (α)
+
+/-- Any subsingleton type is (noncomputably) a fintype (with zero or one terms). -/
+@[priority 100]
+noncomputable instance of_subsingleton' [subsingleton α] : fintype α :=
+if h : nonempty α then
+  of_subsingleton (nonempty.some h)
+else
+  ⟨∅, (λ a, false.elim (h ⟨a⟩))⟩
+
 end fintype
 
 namespace set