CategoryTheory.Limits.HasCountableLimits.out
theorem CategoryTheory.Limits.HasCountableLimits.out :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [self : CategoryTheory.Limits.HasCountableLimits C]
(J : Type) [inst_1 : CategoryTheory.SmallCategory J] [inst_2 : CategoryTheory.CountableCategory J],
CategoryTheory.Limits.HasLimitsOfShape J C
The theorem `CategoryTheory.Limits.HasCountableLimits.out` states that for any type `C` (interpreted as a category), which has countable limits, and for any type `J` (interpreted as a small category) with countably many objects and morphisms, `C` has all limits of shape `J`. Here, a limit of shape `J` in `C` is a limit over a diagram whose shape is `J`. A category having countable limits means that it has all limits over diagrams of shape `ℕ`, where `ℕ` is the set of natural numbers (interpreted as a category). A small category is a category whose objects and morphisms are in the same universe. A countable category is a category with countably many objects and morphisms.
More concisely: For any small, countable category J and any type C with countable limits, C has all limits indexed by J.
|
CategoryTheory.Limits.sequentialFunctor_map
theorem CategoryTheory.Limits.sequentialFunctor_map :
∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : CategoryTheory.IsCofiltered J],
Antitone (CategoryTheory.Limits.sequentialFunctor_obj J)
This theorem states that for any type `J` that satisfies the conditions of being countable, having a preorder, and being cofiltered in the category theory sense, the function `CategoryTheory.Limits.sequentialFunctor_obj J` is antitone. An antitone function is one where if `a ≤ b`, then `f b ≤ f a`. Specifically, in this context, `CategoryTheory.Limits.sequentialFunctor_obj J` maps natural numbers to elements of `J` in an antitone fashion.
More concisely: For any countable, preordered and cocofiltered type `J`, the function `CategoryTheory.Limits.sequentialFunctor_obj J` is an antitone function from natural numbers to elements of `J`.
|
CategoryTheory.Limits.HasCountableColimits.out
theorem CategoryTheory.Limits.HasCountableColimits.out :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [self : CategoryTheory.Limits.HasCountableColimits C]
(J : Type) [inst_1 : CategoryTheory.SmallCategory J] [inst_2 : CategoryTheory.CountableCategory J],
CategoryTheory.Limits.HasColimitsOfShape J C
The theorem `CategoryTheory.Limits.HasCountableColimits.out` states that for any type `C` that forms a category, and for any type `J` that forms a `SmallCategory` and a `CountableCategory`, if `C` has countable colimits, then `C` has colimits of shape `J`. Here, `SmallCategory` refers to a category where objects and morphisms reside in the same universe level, and `CountableCategory` refers to a category that has countably many objects and morphisms. A category has colimits of a certain shape if there exists a colimit for every diagram of that shape in the category.
More concisely: If `C` is a category with countably many objects and morphisms in the same universe level, and `C` has countable colimits, then `C` has colimits for every diagram shaped like a small category `J`.
|