From 318cb4bcc4e7d38b0adb634520e295992a3f61e3 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 29 Mar 2021 13:12:10 +0000 Subject: [PATCH] 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 --- src/category_theory/equivalence.lean | 8 + src/category_theory/essentially_small.lean | 210 +++++++++++++++++++++ src/category_theory/skeletal.lean | 30 ++- src/data/equiv/basic.lean | 7 + src/data/fintype/basic.lean | 13 +- src/logic/small.lean | 97 ++++++++++ 6 files changed, 358 insertions(+), 7 deletions(-) create mode 100644 src/category_theory/essentially_small.lean create mode 100644 src/logic/small.lean diff --git a/src/category_theory/equivalence.lean b/src/category_theory/equivalence.lean index c5fb20d8763d8..5e96a7f6f8664 100644 --- a/src/category_theory/equivalence.lean +++ b/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 diff --git a/src/category_theory/essentially_small.lean b/src/category_theory/essentially_small.lean new file mode 100644 index 0000000000000..bf2ba4d685a00 --- /dev/null +++ b/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 diff --git a/src/category_theory/skeletal.lean b/src/category_theory/skeletal.lean index 82964c6bb4789..eb83a7e075bd6 100644 --- a/src/category_theory/skeletal.lean +++ b/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. diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean index 5de89056562cc..37014f3cddf16 100644 --- a/src/data/equiv/basic.lean +++ b/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) diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean index 36ea0c4adc85c..efb977be8d4b8 100644 --- a/src/data/fintype/basic.lean +++ b/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 diff --git a/src/logic/small.lean b/src/logic/small.lean new file mode 100644 index 0000000000000..0c9637c35d883 --- /dev/null +++ b/src/logic/small.lean @@ -0,0 +1,97 @@ +/- +Copyright (c) 2021 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison +-/ +import data.equiv.encodable.basic +import data.fintype.basic + +/-! +# Small types + +A type is `w`-small if there exists an equivalence to some `S : Type w`. + +We provide a noncomputable model `shrink α : Type w`, and `equiv_shrink α : α ≃ shrink α`. + +A subsingleton type is `w`-small for any `w`. + +If `α ≃ β`, then `small.{w} α ↔ small.{w} β`. +-/ + +universes w v + +/-- +A type is `small.{w}` if there exists an equivalence to some `S : Type w`. +-/ +class small (α : Type v) : Prop := +(equiv_small : ∃ (S : Type w), nonempty (α ≃ S)) + +/-- +Constructor for `small α` from an explicit witness type and equivalence. +-/ +lemma small.mk' {α : Type v} {S : Type w} (e : α ≃ S) : small.{w} α := +⟨⟨S, ⟨e⟩⟩⟩ + +/-- +An arbitrarily chosen model in `Type w` for a `w`-small type. +-/ +@[nolint has_inhabited_instance] +def shrink (α : Type v) [small.{w} α] : Type w := +classical.some (@small.equiv_small α _) + +/-- +The noncomputable equivalence between a `w`-small type and a model. +-/ +noncomputable +def equiv_shrink (α : Type v) [small.{w} α] : α ≃ shrink α := +nonempty.some (classical.some_spec (@small.equiv_small α _)) + +@[priority 100] +instance small_self (α : Type v) : small.{v} α := +small.mk' (equiv.refl _) + +@[priority 100] +instance small_max (α : Type v) : small.{max w v} α := +small.mk' equiv.ulift.{w}.symm + +instance small_ulift (α : Type v) : small.{v} (ulift.{w} α) := +small.mk' equiv.ulift + +section +open_locale classical + +theorem small_congr {α : Type*} {β : Type*} (e : α ≃ β) : small.{w} α ↔ small.{w} β := +begin + fsplit, + { rintro ⟨S, ⟨f⟩⟩, + exact small.mk' (e.symm.trans f), }, + { rintro ⟨S, ⟨f⟩⟩, + exact small.mk' (e.trans f), }, +end + +instance small_subtype (α : Type v) [small.{w} α] (P : α → Prop) : small.{w} { x // P x } := +begin + rw small_congr (equiv_shrink α).subtype_equiv_of_subtype', + apply_instance, +end + +@[priority 100] +instance small_of_fintype (α : Type v) [fintype α] : small.{w} α := +begin + obtain ⟨n, ⟨e⟩⟩ := fintype.exists_equiv_fin α, + rw small_congr e, + apply_instance, +end + +theorem small_of_injective {α : Type*} {β : Type*} [small.{w} β] + (f : α → β) (hf : function.injective f) : small.{w} α := +begin + rw small_congr (equiv.set.range f hf), + apply_instance, +end + +@[priority 100] +instance small_of_encodable (α : Type v) [encodable α] : small.{w} α := +small_of_injective _ (encodable.encode_injective) + +end