Theorems · Theorem · category theory

CategoryTheory.isLeftAdjoint_triangle_lift_comonadic

∀ {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]
  (F : CategoryTheory.Functor B A) [CategoryTheory.ComonadicLeftAdjoint F] {L : CategoryTheory.Functor C B}
  [CategoryTheory.Limits.HasCoreflexiveEqualizers C] [(L.comp F).IsLeftAdjoint], L.IsLeftAdjoint

If L ⋙ F has a right adjoint, the domain of L has coreflexive equalizers and F is a comonadic functor, then L has a right adjoint. This is a special case of isLeftAdjoint_triangle_lift which is often more useful in practice.

Defined in

Mathlib.CategoryTheory.Adjunction.Lifting.Right

Cited by

1 results in Mathlib

Foundations

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

Assumes

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