CategoryTheory.solutionSetCondition_of_isRightAdjoint
theorem CategoryTheory.solutionSetCondition_of_isRightAdjoint :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u} [inst_1 : CategoryTheory.Category.{v, u} D]
(G : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.IsRightAdjoint G],
CategoryTheory.SolutionSetCondition G
This theorem states that if a functor `G` from category `D` to `C` is a right adjoint, then it satisfies the solution set condition. In category theory, a functor is a right adjoint if there exists another functor such that the two form an adjoint pair with the first functor being the right part of the pair. The solution set condition is a property of a functor that states that for any object in the target category and any morphism to the functor of an object in the source category, there is a set of morphisms in the source category such that each morphism makes a certain diagram commute.
More concisely: If functor `G` from category `D` to `C` is a right adjoint, then it satisfies the solution set condition.
|
CategoryTheory.Limits.hasColimits_of_hasLimits_of_isCoseparating
theorem CategoryTheory.Limits.hasColimits_of_hasLimits_of_isCoseparating :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasLimits C]
[inst_2 : CategoryTheory.WellPowered C] {𝒢 : Set C} [inst_3 : Small.{v, u} ↑𝒢],
CategoryTheory.IsCoseparating 𝒢 → CategoryTheory.Limits.HasColimits C
This theorem, which is a consequence of the special adjoint functor theorem, states that if a category `C` is complete, well-powered, and has a small coseparating set `𝒢`, then `C` is cocomplete. In other words, for any category `C` that satisfies these conditions, the category `C` has all small colimits. Here, a category is complete if it has all small limits, it is well-powered if each of its objects has a set-sized collection of subobjects, and a set `𝒢` is called a coseparating set in `C` if for every pair of morphisms `f` and `g` with the same source and target in `C`, if `f` followed by `h` equals `g` followed by `h` for all `h` with codomain in `𝒢`, then `f` equals `g`.
More concisely: If a complete and well-powered category `C` with a small coseparating set has small colimits for all diagrams with codomains in the coseparating set, then `C` has all small colimits.
|
CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparating
theorem CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparating :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
[inst_2 : CategoryTheory.WellPowered Cᵒᵖ] {𝒢 : Set C} [inst_3 : Small.{v, u} ↑𝒢],
CategoryTheory.IsSeparating 𝒢 → CategoryTheory.Limits.HasLimits C
The theorem `CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparating` asserts that if a category `C` is cocomplete, well-copowered, and has a small separating set, then it is complete. Here, cocomplete means that `C` has all (small) colimits, and a separating set is a collection of functors `C(G, -)` for `G ∈ 𝒢` that are collectively faithful, i.e., if composite morphisms `h ≫ f = h ≫ g` for all `h` with domain in `𝒢` implies `f = g`. Well-copowered refers to the condition that every object in the opposite category `Cᵒᵖ` has a small projection (a property related to the size of certain collections of morphisms). In this context, a category is complete if it has all (small) limits.
More concisely: If a cocomplete, well-copowered category with a small separating set is given, then it has all small limits.
|