CategoryTheory.LocallySmall.hom_small
theorem CategoryTheory.LocallySmall.hom_small :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.LocallySmall.{w, v, u} C] (X Y : C),
Small.{w, v} (X ⟶ Y)
This theorem states that in the context of category theory, if a category `C` is locally small (meaning that for any two objects in this category, the set of all morphisms between them is a small set), then the hom-types (the types of morphisms between two objects) of this category are also small. Specifically, for any two objects `X` and `Y` in the category, the type of morphisms from `X` to `Y` is a small type.
More concisely: In a locally small category, the set of morphisms between any two objects forms a small set.
|
CategoryTheory.EssentiallySmall.mk'
theorem CategoryTheory.EssentiallySmall.mk' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : Type w} [inst_1 : CategoryTheory.SmallCategory S],
(C ≌ S) → CategoryTheory.EssentiallySmall.{w, v, u} C
The theorem `CategoryTheory.EssentiallySmall.mk'` states that for any category `C` defined in some type universe `u` and with morphisms in universe `v`, if there exists a small category `S` (that is a category with objects and morphisms in the same universe level) such that `C` is equivalent to `S` (denoted by `C ≌ S`), then `C` is essentially small. In this context, a category is called essentially small if it is equivalent to a small category.
More concisely: If a category `C` is equivalent to a small category `S`, then `C` is essentially small.
|
CategoryTheory.essentiallySmall_iff
theorem CategoryTheory.essentiallySmall_iff :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
CategoryTheory.EssentiallySmall.{w, v, u} C ↔
Small.{w, u} (CategoryTheory.Skeleton C) ∧ CategoryTheory.LocallySmall.{w, v, u} C
The theorem `CategoryTheory.essentiallySmall_iff` states that for any category `C`, the category is essentially small if and only if the underlying type of its skeleton category (the set of isomorphism classes) is small, and it is also locally small. In other words, a category 'C' is essentially small if it satisfies two conditions: (1) the set of isomorphism classes, which is considered as the skeleton of the category, is a small set, and (2) the category has the property of being locally small, i.e., the hom-sets between any two objects in the category form a small set.
More concisely: A category is essentially small if and only if its skeleton and hom-sets form small sets.
|
CategoryTheory.essentiallySmall_of_small_of_locallySmall
theorem CategoryTheory.essentiallySmall_of_small_of_locallySmall :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Small.{w, u} C]
[inst_2 : CategoryTheory.LocallySmall.{w, v, u} C], CategoryTheory.EssentiallySmall.{w, v, u} C
This theorem states that for any type `C` which is a category (given by `CategoryTheory.Category C`), if `C` is a small category (given by `Small C`) and is locally small (given by `CategoryTheory.LocallySmall C`), then `C` is essentially small (given by `CategoryTheory.EssentiallySmall C`). In terms of category theory, a category is small if its objects form a set (rather than a proper class), locally small if for any two objects there is a set of morphisms between them, and essentially small if it is equivalent to a small category. This theorem thus asserts that a small and locally small category is essentially small.
More concisely: A small and locally small category is essentially small.
|
CategoryTheory.EssentiallySmall.equiv_smallCategory
theorem CategoryTheory.EssentiallySmall.equiv_smallCategory :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.EssentiallySmall.{w, v, u} C],
∃ S x, Nonempty (C ≌ S)
This theorem states that for any essentially small category 'C', there exists a small category 'S' such that 'C' is equivalent to 'S'. Here, an essentially small category is a category such that there exists a small category (i.e., a category whose objects and morphisms form a set instead of a proper class) that is equivalent to it. In other words, it establishes a correspondence between essentially small categories and small categories.
More concisely: Every essentially small category is equivalent to some small category.
|
CategoryTheory.essentiallySmall_iff_of_thin
theorem CategoryTheory.essentiallySmall_iff_of_thin :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Quiver.IsThin C],
CategoryTheory.EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (CategoryTheory.Skeleton C)
The theorem `CategoryTheory.essentiallySmall_iff_of_thin` states that for any category `C` that is a thin category (meaning it doesn't have any parallel arrows), the category `C` is essentially small (i.e., its objects are isomorphic to a set, not necessarily a proper class) if and only if the skeleton of `C` is small. The skeleton of a category is a category that has the same isomorphism classes as the original category, but with only one object from each isomorphism class. The statement "the skeleton of `C` is small" means that there exists a set that contains exactly one object from each isomorphism class of `C`.
More concisely: A thin category is essentially small if and only if its skeleton is a small category.
|