Theorems · Theorem · category theory

CategoryTheory.isLeftAdjoint_triangle_lift

∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B) (adj₁ : F ⊣ U)
  (h : (X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)) [CategoryTheory.Limits.HasCoreflexiveEqualizers C]
  [(L.comp F).IsLeftAdjoint], L.IsLeftAdjoint

The adjoint triangle theorem: Suppose U : A ⥤ B has a left adjoint F such that each unit η_X : X ⟶ UFX is a regular monomorphism. Then if a category C has equalizers of coreflexive pairs, then a functor L : C ⥤ B has a right adjoint if the composite L ⋙ F does. Note the converse is true (with weaker assumptions), by Adjunction.comp. See https://ncatlab.org/nlab/show/adjoint+triangle+theorem

Defined in

Mathlib.CategoryTheory.Adjunction.Lifting.Right

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasCoreflexiveEqualizersCategoryTheory.Functor.IsLeftAdjoint