CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence
theorem CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J]
(E : CategoryTheory.Functor D C) [inst_3 : E.IsEquivalence] [inst : CategoryTheory.Limits.HasLimitsOfShape J C],
CategoryTheory.Limits.HasLimitsOfShape J D
This theorem states that for any categories `C`, `D` and `J`, if `C` has limits of shape `J` and we have a functor `E` that is an equivalence from `D` to `C`, then `D` also has limits of shape `J`. In other words, "limits of shape-ness" can be carried over to another category through an equivalence. This relates to an important concept in category theory, where certain properties can be transported across equivalent categories.
More concisely: If `C` has limits of shape `J` and `E: D ⥤ C` is an equivalence of categories, then `D` has limits of shape `J`.
|
CategoryTheory.Adjunction.has_limits_of_equivalence
theorem CategoryTheory.Adjunction.has_limits_of_equivalence :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor D C) [inst_2 : E.IsEquivalence]
[inst : CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₁, u₁} C],
CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₂, u₂} D
This theorem states that if we have a category `C` that has limits of some size, and we have a functor `E` from another category `D` to `C` that forms an equivalence of categories, then `D` also has limits of the same size. In other words, the existence of limits of a certain size in a category can be transported across an equivalence of categories.
More concisely: If `C` is a category with limits of size `S` and `E : D -> C` is an equivalence of categories, then `D` also has limits of size `S`.
|
CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence
theorem CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J]
(E : CategoryTheory.Functor C D) [inst_3 : E.IsEquivalence]
[inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D], CategoryTheory.Limits.HasColimitsOfShape J C
This theorem states that given any category `C`, category `D`, and an index category `J`, if there is a functor `E` from `C` to `D` that is an equivalence of categories, and if `D` has colimits of shape `J`, then `C` also has colimits of shape `J`. In other words, a `HasColimitsOfShape` instance can be transported across an equivalence of categories.
More concisely: If `C` and `D` are equivalent categories and `D` has colimits of shape `J`, then `C` also has colimits of shape `J`.
|
CategoryTheory.Adjunction.has_colimits_of_equivalence
theorem CategoryTheory.Adjunction.has_colimits_of_equivalence :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (E : CategoryTheory.Functor C D) [inst_2 : E.IsEquivalence]
[inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₂, u₂} D],
CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C
This theorem states that for any two categories `C` and `D`, given an equivalence functor `E` from `C` to `D` and assuming that the category `D` has colimits of any size, then the category `C` also has colimits of any size. In other words, the presence of colimits in a category can be transported across an equivalence of categories.
More concisely: If `C` and `D` are categories with `D` having colimits of any size, and `E: C -> D` is an equivalence functor, then `C` also has colimits of any size.
|