Adjoint triples

This file concerns adjoint triples F ⊣ G ⊣ H of functors F H : C ⥤ D, G : D ⥤ C.

Currently, the only result is that F is fully faithful if and only if H is fully faithful.

theorem CategoryTheory.Adjunction.isIso_unit_iff_isIso_counit {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj₁ : F ⊣ G) (adj₂ : G ⊣ H) : CategoryTheory.IsIso adj₁.unit ↔ CategoryTheory.IsIso adj₂.counit

noncomputable def CategoryTheory.Adjunction.fullyFaithfulEquiv {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj₁ : F ⊣ G) (adj₂ : G ⊣ H) : F.FullyFaithful ≃ H.FullyFaithful

Given an adjoint triple F ⊣ G ⊣ H, the left adjoint F is fully faithful if and only if the right adjoint H is fully faithful.

Equations

• One or more equations did not get rendered due to their size.