CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape
theorem CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} J] [inst_2 : CategoryTheory.Limits.HasColimitsOfShape Jᵒᵖ C],
CategoryTheory.Limits.HasLimitsOfShape J Cᵒᵖ
The theorem states that if a category `C` has colimits of a certain shape `Jᵒᵖ`, then we can construct limits in the opposite category `Cᵒᵖ` of the same shape `J`. This theorem demonstrates a duality between limits and colimits in category theory, which is a cornerstone of the subject.
More concisely: If category `C` has colimits of shape `Jᵒᵖ`, then the opposite category `Cᵒᵖ` has limits of shape `J`.
|
CategoryTheory.Limits.hasColimit_of_hasLimit_leftOp
theorem CategoryTheory.Limits.hasColimit_of_hasLimit_leftOp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ)
[inst_2 : CategoryTheory.Limits.HasLimit F.leftOp], CategoryTheory.Limits.HasColimit F
The theorem `CategoryTheory.Limits.hasColimit_of_hasLimit_leftOp` states that for any category `C` and any small category `J`, if a functor `F` from `J` to the opposite category of `C` (`Cᵒᵖ`) has a limit when considered as a functor from the opposite category of `J` (`Jᵒᵖ`) to `C`, then `F` itself has a colimit. In essence, the existence of a limit for the functor's left-opposite implies the existence of a colimit for the functor.
More concisely: If a functor from a small category to the opposite category of a category has a limit as a functor from the opposite category, then it has a colimit.
|
CategoryTheory.Limits.hasLimit_of_hasColimit_leftOp
theorem CategoryTheory.Limits.hasLimit_of_hasColimit_leftOp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ)
[inst_2 : CategoryTheory.Limits.HasColimit F.leftOp], CategoryTheory.Limits.HasLimit F
This theorem states that if we have a functor `F.leftOp : Jᵒᵖ ⥤ C` which has a colimit, then we can construct a limit for the initial functor `F : J ⥤ Cᵒᵖ`. In simpler terms, it asserts a duality between limits and colimits in the setting of category theory. If one functor has a colimit (a universal cone from another functor to it), then the opposite functor has a limit (a universal cone from it to another functor).
More concisely: If a functor `F : J ⥤ C` has a right adjoint `F.leftOp : Jᵒᵖ ⥤ C` with a right adjoint cone having a limit, then `F` has a left adjoint and the left adjoint cone is the limit.
|