Theorems · Theorem · category theory

CategoryTheory.isLeftAdjoint_of_preservesColimits_of_isSeparating

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [CategoryTheory.Limits.HasColimits C] [CategoryTheory.WellPowered.{v, v, u} Cᵒᵖ] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.Small.{v, v, u} P],
  P.IsSeparating → ∀ (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimits F], F.IsLeftAdjoint

The special adjoint functor theorem: if F : C ⥤ D preserves colimits and C is cocomplete, well-copowered and has a small separating set, then F has a right adjoint.

Defined in

Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Cited by

1 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasColimitsCategoryTheory.WellPoweredCategoryTheory.ObjectProperty.SmallCategoryTheory.Limits.PreservesColimits