CategoryTheory.hasLimit_of_created
theorem CategoryTheory.hasLimit_of_created :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D)
[inst_3 : CategoryTheory.Limits.HasLimit (K.comp F)] [inst_4 : CategoryTheory.CreatesLimit K F],
CategoryTheory.Limits.HasLimit K
This theorem states that, given two categories `C` and `D`, and two functors `K : J ⟶ C` and `F : C ⟶ D` such that `F` creates the limit of `K` and the composition `K ⋙ F` has a limit, then `K` itself also has a limit. Here, `J` is a category that serves as the domain of the functor `K`. In other words, if a functor `F` can create the limit of another functor `K`, and if the composition of `K` and `F` has a limit, then `K` must also have a limit.
More concisely: If functors `K : J ➝ C` and `F : C ➝ D` satisfy `F` preserves limits of `K` and `K ◦ F` has a limit, then `K` has a limit.
|
CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape
theorem CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor C D) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J D]
[inst_4 : CategoryTheory.CreatesColimitsOfShape J F], CategoryTheory.Limits.HasColimitsOfShape J C
The theorem states that if a functor `F` creates colimits of a certain shape `J`, and a category `D` has colimits of this shape, then a category `C` also has colimits of this shape. Here, `C`, `D`, and `J` are types representing categories, and `F` is a functor from `C` to `D`. Colimits are a concept in category theory that generalize the notion of limits in calculus and measure the "limiting behavior" of a diagram of objects and morphisms in a category. The shape of a colimit corresponds to the indexing category of the diagram.
More concisely: If functor `F` preserves colimits of shape `J` and category `D` has colimits of shape `J`, then category `C` has colimits of shape `J`.
|
CategoryTheory.hasColimits_of_hasColimits_createsColimits
theorem CategoryTheory.hasColimits_of_hasColimits_createsColimits :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D)
[inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₂, u₂} D]
[inst_3 : CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₁, u₁} C
This theorem states that if a functor `F` creates colimits and a category `D` has all colimits, then the category `C` also has all colimits. In other words, the presence of all colimits in a category and the ability of a functor to create these colimits ensures the existence of all colimits in another related category. This is a fundamental theorem in category theory, a branch of mathematics that deals with abstract algebraic structures.
More concisely: If `F` is a functor that preserves colimits and `D` is a category with all colimits, then the category `C` exhibiting the underlying objects and morphisms of `F D` has all colimits.
|
CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
theorem CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor C D) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J D]
[inst_4 : CategoryTheory.CreatesLimitsOfShape J F], CategoryTheory.Limits.HasLimitsOfShape J C
This theorem states that if a functor `F` from category `C` to category `D` creates limits of a particular shape `J`, and if `D` has limits of shape `J`, then `C` also has limits of shape `J`. This means that the existence of certain limits in the codomain category and the fact that `F` creates those limits imply the existence of such limits in the domain category.
More concisely: If functor `F` from category `C` to category `D` preserves limits of shape `J` and category `D` has limits of shape `J`, then category `C` also has limits of shape `J`.
|
CategoryTheory.hasLimits_of_hasLimits_createsLimits
theorem CategoryTheory.hasLimits_of_hasLimits_createsLimits :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D)
[inst_2 : CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} D]
[inst_3 : CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, u₁} C
The theorem `CategoryTheory.hasLimits_of_hasLimits_createsLimits` states that in the context of category theory, if a functor `F` from category `C` to `D` creates limits of a certain size, and the category `D` has all limits of that size, then the category `C` also has all limits of that size. This property is important in discussions about the existence of limits in categories.
More concisely: If a functor preserves limits of a certain size in a category and the target category has all limits of that size, then the source category also has all limits of that size.
|
CategoryTheory.hasColimit_of_created
theorem CategoryTheory.hasColimit_of_created :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D)
[inst_3 : CategoryTheory.Limits.HasColimit (K.comp F)] [inst_4 : CategoryTheory.CreatesColimit K F],
CategoryTheory.Limits.HasColimit K
This theorem states that if a functor `F` creates the colimit of another functor `K` and the composition of `K` and `F` has a colimit, then `K` itself also has a colimit. In this context, a colimit is a way of defining the "limit" of a diagram (represented as a functor `K`) within a category, and "creating a colimit" means providing a way to construct such a limit. This theorem provides a condition under which we can be sure that a given functor has a colimit within its category.
More concisely: If functor `F` creates colimits and the composition of `F` and `K` has a colimit, then functor `K` also has a colimit.
|