CategoryTheory.InitiallySmall.initial_smallCategory
theorem CategoryTheory.InitiallySmall.initial_smallCategory :
∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [self : CategoryTheory.InitiallySmall J],
∃ S x F, F.Initial
This theorem states that for any type `J` that forms a small category under a given category theory structure, and provided `J` is initially small, there exists a functor `F` from `J` that is initial. In other words, if `J` is a small category, there's a functor that maps everything in `J` to a single object in another category.
More concisely: Given a small category `J` with an initial object under a given category theory structure, there exists an initial functor from `J` to another category.
|
CategoryTheory.FinallySmall.final_smallCategory
theorem CategoryTheory.FinallySmall.final_smallCategory :
∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [self : CategoryTheory.FinallySmall J], ∃ S x F, F.Final
This theorem states that for any small category `J` (a category whose objects form a set rather than a proper class), there exists a final functor from `J`. In other words, given any small category `J`, we can find a functor `F` such that for any object `x` in `J`, `F` maps `x` to some object `S` in a way that makes `F` a final functor. A final functor is a special kind of functor that has certain properties relating to the existence and uniqueness of morphisms.
More concisely: Every small category has a final functor.
|
CategoryTheory.FinallySmall.mk'
theorem CategoryTheory.FinallySmall.mk' :
∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {S : Type w} [inst_1 : CategoryTheory.SmallCategory S]
(F : CategoryTheory.Functor S J) [inst_2 : F.Final], CategoryTheory.FinallySmall J
The theorem `CategoryTheory.FinallySmall.mk'` states that for any types `J` and `S` where `J` is a category and `S` is a small category, and given a functor `F` from `S` to `J` which is also final, then `J` is finally small. In category theory terms, a category is finally small if there exists a small category and a final functor from the small category to it.
More concisely: If `J` is a category, `S` is a small category, and `F` is a final functor from `S` to `J`, then `J` is finally small.
|
CategoryTheory.InitiallySmall.mk'
theorem CategoryTheory.InitiallySmall.mk' :
∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {S : Type w} [inst_1 : CategoryTheory.SmallCategory S]
(F : CategoryTheory.Functor S J) [inst_2 : F.Initial], CategoryTheory.InitiallySmall J
The theorem `CategoryTheory.InitiallySmall.mk'` states that for any type `J` with a category structure, another type `S` with a small category structure, and a functor `F` from `S` to `J` that is initial (i.e., for any object in `J`, there exists precisely one morphism to it from the initial object in `S`), we can establish that `J` is initially small. In simpler terms, this means that `J` has a unique initial object that is in the same universe as it is, if we can find a small category and a functor behaving as described.
More concisely: If `J` is a type with a category structure, `S` is a small category, and `F` is a functor from `S` to `J` that is initial, then `J` has a unique initial object in the same universe.
|