mathlib3 documentation

category_theory.essentially_small

Essentially small categories. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[class]

structure category_theory.essentially_small (C : Type u) [category_theory.category C] :

Prop

equiv_small_category : ∃ (S : Type ?) (_x : category_theory.small_category S), nonempty (C ≌ S)

A category is essentially_small.{w} if there exists an equivalence to some S : Type w with [small_category S].

theorem category_theory.essentially_small.mk' {C : Type u} [category_theory.category C] {S : Type w} [category_theory.small_category S] (e : C ≌ S) :

category_theory.essentially_small C

Constructor for essentially_small C from an explicit small category witness.

@[nolint]

def category_theory.small_model (C : Type u) [category_theory.category C] [category_theory.essentially_small C] :

An arbitrarily chosen small model for an essentially small category.

Equations

category_theory.small_model C = classical.some category_theory.essentially_small.equiv_small_category

Instances for category_theory.small_model

category_theory.small_category_small_model

@[protected, instance]

noncomputable def category_theory.small_category_small_model (C : Type u) [category_theory.category C] [category_theory.essentially_small C] :

category_theory.small_category (category_theory.small_model C)

Equations

category_theory.small_category_small_model C = classical.some _

noncomputable def category_theory.equiv_small_model (C : Type u) [category_theory.category C] [category_theory.essentially_small C] :

C ≌ category_theory.small_model C

The (noncomputable) categorical equivalence between an essentially small category and its small model.

Equations

category_theory.equiv_small_model C = nonempty.some _

theorem category_theory.essentially_small_congr {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] (e : C ≌ D) :

category_theory.essentially_small C ↔ category_theory.essentially_small D

theorem category_theory.discrete.essentially_small_of_small {α : Type u} [small α] :

category_theory.essentially_small (category_theory.discrete α)

theorem category_theory.essentially_small_self (C : Type u) [category_theory.category C] :

category_theory.essentially_small C

@[class]

structure category_theory.locally_small (C : Type u) [category_theory.category C] :

Prop

hom_small : (∀ (X Y : C), small (X ⟶ Y)) . "apply_instance"

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.

Instances of this typeclass

@[protected, instance]

def category_theory.quiver.hom.small (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X Y : C) :

small (X ⟶ Y)

theorem category_theory.locally_small_congr {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] (e : C ≌ D) :

category_theory.locally_small C ↔ category_theory.locally_small D

@[protected, instance]

def category_theory.locally_small_self (C : Type u) [category_theory.category C] :

category_theory.locally_small C

@[protected, instance]

def category_theory.locally_small_of_essentially_small (C : Type u) [category_theory.category C] [category_theory.essentially_small C] :

category_theory.locally_small C

@[nolint]

def category_theory.shrink_homs (C : Type u) :

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.

Equations

category_theory.shrink_homs C = C

Instances for category_theory.shrink_homs

category_theory.shrink_homs.category_theory.category

def category_theory.shrink_homs.to_shrink_homs {C' : Type u_1} (X : C') :

category_theory.shrink_homs C'

Help the typechecker by explicitly translating from C to shrink_homs C.

Equations

category_theory.shrink_homs.to_shrink_homs X = X

def category_theory.shrink_homs.from_shrink_homs {C' : Type u_1} (X : category_theory.shrink_homs C') :

C'

Help the typechecker by explicitly translating from shrink_homs C to C.

Equations

X.from_shrink_homs = X

@[simp]

theorem category_theory.shrink_homs.to_from {C' : Type u_1} (X : C') :

(category_theory.shrink_homs.to_shrink_homs X).from_shrink_homs = X

@[simp]

theorem category_theory.shrink_homs.from_to {C' : Type u_1} (X : category_theory.shrink_homs C') :

category_theory.shrink_homs.to_shrink_homs X.from_shrink_homs = X

@[protected, instance]

noncomputable def category_theory.shrink_homs.category_theory.category (C : Type u) [category_theory.category C] [category_theory.locally_small C] :

category_theory.category (category_theory.shrink_homs C)

Equations

category_theory.shrink_homs.category_theory.category C = {to_category_struct := {to_quiver := {hom := λ (X Y : category_theory.shrink_homs C), shrink (X.from_shrink_homs ⟶ Y.from_shrink_homs)}, id := λ (X : category_theory.shrink_homs C), ⇑(equiv_shrink (X.from_shrink_homs ⟶ X.from_shrink_homs)) (𝟙 X.from_shrink_homs), comp := λ (X Y Z : category_theory.shrink_homs C) (f : X ⟶ Y) (g : Y ⟶ Z), ⇑(equiv_shrink (X.from_shrink_homs ⟶ Z.from_shrink_homs)) (⇑((equiv_shrink (X.from_shrink_homs ⟶ Y.from_shrink_homs)).symm) f ≫ ⇑((equiv_shrink (Y.from_shrink_homs ⟶ Z.from_shrink_homs)).symm) g)}, id_comp' := _, comp_id' := _, assoc' := _}

@[simp]

theorem category_theory.shrink_homs.category_theory.category_id (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X : category_theory.shrink_homs C) :

𝟙 X = ⇑(equiv_shrink (X.from_shrink_homs ⟶ X.from_shrink_homs)) (𝟙 X.from_shrink_homs)

@[simp]

theorem category_theory.shrink_homs.category_theory.category_comp (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X Y Z : category_theory.shrink_homs C) (f : X ⟶ Y) (g : Y ⟶ Z) :

f ≫ g = ⇑(equiv_shrink (X.from_shrink_homs ⟶ Z.from_shrink_homs)) (⇑((equiv_shrink (X.from_shrink_homs ⟶ Y.from_shrink_homs)).symm) f ≫ ⇑((equiv_shrink (Y.from_shrink_homs ⟶ Z.from_shrink_homs)).symm) g)

@[simp]

theorem category_theory.shrink_homs.functor_obj (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X : C) :

(category_theory.shrink_homs.functor C).obj X = category_theory.shrink_homs.to_shrink_homs X

noncomputable def category_theory.shrink_homs.functor (C : Type u) [category_theory.category C] [category_theory.locally_small C] :

C ⥤ category_theory.shrink_homs C

Implementation of shrink_homs.equivalence.

Equations

category_theory.shrink_homs.functor C = {obj := λ (X : C), category_theory.shrink_homs.to_shrink_homs X, map := λ (X Y : C) (f : X ⟶ Y), ⇑(equiv_shrink (X ⟶ Y)) f, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.shrink_homs.functor_map (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X Y : C) (f : X ⟶ Y) :

(category_theory.shrink_homs.functor C).map f = ⇑(equiv_shrink (X ⟶ Y)) f

@[simp]

theorem category_theory.shrink_homs.inverse_map (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X Y : category_theory.shrink_homs C) (f : X ⟶ Y) :

(category_theory.shrink_homs.inverse C).map f = ⇑((equiv_shrink (X.from_shrink_homs ⟶ Y.from_shrink_homs)).symm) f

@[simp]

theorem category_theory.shrink_homs.inverse_obj (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X : category_theory.shrink_homs C) :

(category_theory.shrink_homs.inverse C).obj X = X.from_shrink_homs

noncomputable def category_theory.shrink_homs.inverse (C : Type u) [category_theory.category C] [category_theory.locally_small C] :

category_theory.shrink_homs C ⥤ C

Implementation of shrink_homs.equivalence.

Equations

category_theory.shrink_homs.inverse C = {obj := λ (X : category_theory.shrink_homs C), X.from_shrink_homs, map := λ (X Y : category_theory.shrink_homs C) (f : X ⟶ Y), ⇑((equiv_shrink (X.from_shrink_homs ⟶ Y.from_shrink_homs)).symm) f, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.shrink_homs.equivalence_functor_obj (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X : C) :

(category_theory.shrink_homs.equivalence C).functor.obj X = category_theory.shrink_homs.to_shrink_homs X

noncomputable def category_theory.shrink_homs.equivalence (C : Type u) [category_theory.category C] [category_theory.locally_small C] :

C ≌ category_theory.shrink_homs C

The categorical equivalence between C and shrink_homs C, when C is locally small.

Equations

category_theory.shrink_homs.equivalence C = category_theory.equivalence.mk (category_theory.shrink_homs.functor C) (category_theory.shrink_homs.inverse C) (category_theory.nat_iso.of_components (λ (X : C), category_theory.iso.refl X) _) (category_theory.nat_iso.of_components (λ (X : category_theory.shrink_homs C), category_theory.iso.refl X) _)

@[simp]

theorem category_theory.shrink_homs.equivalence_unit_iso_hom_app (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X : C) :

(category_theory.shrink_homs.equivalence C).unit_iso.hom.app X = 𝟙 X

@[simp]

theorem category_theory.shrink_homs.equivalence_inverse_map (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X Y : category_theory.shrink_homs C) (f : X ⟶ Y) :

(category_theory.shrink_homs.equivalence C).inverse.map f = ⇑((equiv_shrink (X.from_shrink_homs ⟶ Y.from_shrink_homs)).symm) f

@[simp]

theorem category_theory.shrink_homs.equivalence_inverse_obj (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X : category_theory.shrink_homs C) :

(category_theory.shrink_homs.equivalence C).inverse.obj X = X.from_shrink_homs

@[simp]

theorem category_theory.shrink_homs.equivalence_counit_iso_hom_app (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X : category_theory.shrink_homs C) :

(category_theory.shrink_homs.equivalence C).counit_iso.hom.app X = ⇑(equiv_shrink (X.from_shrink_homs ⟶ X.from_shrink_homs)) (𝟙 X.from_shrink_homs)

@[simp]

theorem category_theory.shrink_homs.equivalence_functor_map (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X Y : C) (f : X ⟶ Y) :

(category_theory.shrink_homs.equivalence C).functor.map f = ⇑(equiv_shrink (X ⟶ Y)) f

@[simp]

theorem category_theory.shrink_homs.equivalence_counit_iso_inv_app (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X : category_theory.shrink_homs C) :

(category_theory.shrink_homs.equivalence C).counit_iso.inv.app X = ⇑(equiv_shrink (X.from_shrink_homs ⟶ X.from_shrink_homs)) (𝟙 X.from_shrink_homs)

@[simp]

theorem category_theory.shrink_homs.equivalence_unit_iso_inv_app (C : Type u) [category_theory.category C] [category_theory.locally_small C] (X : C) :

(category_theory.shrink_homs.equivalence C).unit_iso.inv.app X = 𝟙 X

theorem category_theory.essentially_small_iff (C : Type u) [category_theory.category C] :

category_theory.essentially_small C ↔ small (category_theory.skeleton C) ∧ category_theory.locally_small C

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.

@[protected, instance]

def category_theory.locally_small_of_thin {C : Type u} [category_theory.category C] [quiver.is_thin C] :

category_theory.locally_small C

Any thin category is locally small.

theorem category_theory.essentially_small_iff_of_thin {C : Type u} [category_theory.category C] [quiver.is_thin C] :

category_theory.essentially_small C ↔ small (category_theory.skeleton C)

A thin category is essentially small if and only if the underlying type of its skeleton is small.