CategoryTheory.Limits.hasFiniteLimits_of_hasFiniteLimits_of_size
theorem CategoryTheory.Limits.hasFiniteLimits_of_hasFiniteLimits_of_size :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
(∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J},
CategoryTheory.FinCategory J → CategoryTheory.Limits.HasLimitsOfShape J C) →
CategoryTheory.Limits.HasFiniteLimits C
This theorem, `CategoryTheory.Limits.hasFiniteLimits_of_hasFiniteLimits_of_size`, states that for any category `C`, if for every type `J` (that has a `SmallCategory` structure and is a `FinCategory`), `C` has limits of shape `J`, then `C` has finite limits. In other words, if a category has all limits of a certain shape where that shape comes from a small, finite category, then the category itself has finite limits.
More concisely: If every small, finite category `J` has finite limits in a category `C`, then `C` has finite limits.
|
CategoryTheory.Limits.HasFiniteWidePushouts.out
theorem CategoryTheory.Limits.HasFiniteWidePushouts.out :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasFiniteWidePushouts C]
(J : Type) [inst_1 : Finite J],
CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Limits.WidePushoutShape J) C
The theorem `CategoryTheory.Limits.HasFiniteWidePushouts.out` states that for any given category `C` and any finite type `J`, if `C` has all finite wide pushouts, then `C` has colimits of the shape `CategoryTheory.Limits.WidePushoutShape J`. Here, `CategoryTheory.Limits.WidePushoutShape J` is a type that represents a shape for wide pushouts, which is simply expressed as `Option J` for any type `J`. In the context of category theory, a colimit is a universal cone to a diagram from a category, and a wide pushout is a particular kind of colimit.
More concisely: If a category `C` has all finite wide pushouts, then `C` has colimits of the shape `Option J` for any finite type `J`.
|
CategoryTheory.Limits.HasFiniteColimits.out
theorem CategoryTheory.Limits.HasFiniteColimits.out :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasFiniteColimits C]
(J : Type) [𝒥 : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J],
CategoryTheory.Limits.HasColimitsOfShape J C
The theorem `CategoryTheory.Limits.HasFiniteColimits.out` states that for any category `C` of type `u`, and any smaller category `J` that has both objects and morphisms from the same universe, if `C` has finite colimits and `J` is a finite category, then `C` has colimits of shape `J`. In other words, if a category has all finite colimits, it also has colimits over any finite small category.
More concisely: If `C` is a category of type `u` with finite colimits and `J` is a finite category, then `C` has colimits indexed by `J`.
|
CategoryTheory.Limits.hasFiniteColimits_of_hasFiniteColimits_of_size
theorem CategoryTheory.Limits.hasFiniteColimits_of_hasFiniteColimits_of_size :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
(∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J},
CategoryTheory.FinCategory J → CategoryTheory.Limits.HasColimitsOfShape J C) →
CategoryTheory.Limits.HasFiniteColimits C
This theorem, `CategoryTheory.Limits.hasFiniteColimits_of_hasFiniteColimits_of_size`, states that for any type `C` that is a category, if for every type `J`, which is a small category, and `J` is a finite category, we have `C` has colimits of shape `J`, then `C` has finite colimits. In less technical terms, this theorem allows us to derive the existence of finite colimits in a category `C` by providing colimits for `C` at an arbitrary universe level.
More concisely: If every small and finite category `J` has colimits in a category `C`, then `C` has finite colimits.
|
CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits
theorem CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteLimits C],
CategoryTheory.Limits.HasFiniteWidePullbacks C
This theorem states that in the context of category theory, if a category `C` has all finite limits, it will also have finite wide pullbacks. Finite wide pullbacks are a specific type of limit, hence if a category possesses all finite limits, it automatically includes finite wide pullbacks. Therefore, given any category `C` with finite limits, we can assure that it has finite wide pullbacks.
More concisely: If a category has all finite limits, then it has all finite wide pullbacks.
|
CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits
theorem CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteColimits C],
CategoryTheory.Limits.HasFiniteWidePushouts C
This theorem states that for any category `C`, if `C` has all finite colimits, then `C` also has finite wide pushouts. Here, a finite wide pushout is a special case of colimits, which are more general concepts in category theory. The importance of this theorem lies in its ability to guarantee the existence of finite wide pushouts under the assumption that all finite colimits exist in the category.
More concisely: If `C` is a category with all finite colimits, then `C` has all finite wide pushouts.
|
CategoryTheory.Limits.HasFiniteWidePullbacks.out
theorem CategoryTheory.Limits.HasFiniteWidePullbacks.out :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasFiniteWidePullbacks C]
(J : Type) [inst_1 : Finite J],
CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C
The theorem `CategoryTheory.Limits.HasFiniteWidePullbacks.out` states that for any category `C` and for any finite type `J`, if `C` has all finite wide pullbacks, then `C` also has all limits of shape `CategoryTheory.Limits.WidePullbackShape J`. In other words, if we can construct finite wide pullbacks in `C`, then we can also construct all limits in `C` that have the shape of wide pullbacks indexed by the elements of `J`. Here, a wide pullback is a limit of a diagram where one object, known as the apex, has morphisms to all other objects, and there are no further morphisms between the other objects. The `CategoryTheory.Limits.WidePullbackShape J` is a definition that describes the shape of such wide pullbacks.
More concisely: If a category has all finite wide pullbacks, then it has all limits of shape `CategoryTheory.Limits.WidePullbackShape J`.
|
CategoryTheory.Limits.HasFiniteLimits.out
theorem CategoryTheory.Limits.HasFiniteLimits.out :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasFiniteLimits C] (J : Type)
[𝒥 : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J],
CategoryTheory.Limits.HasLimitsOfShape J C
This theorem states that for any type `C` that forms a category and has finite limits, and any type `J` that forms a small category and has a finite number of morphisms and objects, `C` has all limits over `J`. In mathematical terms, given a category `C` and a small, finitely-presented category `J`, all the limits of shape `J` exist in the category `C`. This theorem is a part of the theory of category theory and its importance lies in its applications to the study of structures and processes in mathematics.
More concisely: Given a category `C` with finite limits and a small, finitely-presented category `J`, `C` has all limits indexed by `J`.
|