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}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
{F H : Functor C D}
{G : Functor D C}
(adj₁ : F ⊣ G)
(adj₂ : G ⊣ H)
:
noncomputable def
CategoryTheory.Adjunction.fullyFaithfulEquiv
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
{F H : Functor C D}
{G : 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.