Lemmas that should go into Mathlib.CategoryTheory.Adjunction.Triple.

theorem CategoryTheory.Adjunction.Triple.homEquiv_counit_unit_app_eq_H_map_unit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F H : Functor C D} {G : Functor D C} (t : Triple F G H) {X : C} : (t.adj₂.homEquiv (H.obj X) ((F.comp G).obj X)) (CategoryStruct.comp (t.adj₂.counit.app X) (t.adj₁.unit.app X)) = H.map (t.adj₁.unit.app X)

For an adjoint triple F ⊣ G ⊣ H, the components of the natural transformation H ⋙ G ⟶ F ⋙ G obtained from the units and counits of the adjunctions are under the second adjunction adjunct to the image of the unit of the first adjunction under H.

theorem CategoryTheory.Adjunction.Triple.homEquiv_symm_counit_unit_app_eq_F_map_counit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F H : Functor C D} {G : Functor D C} (t : Triple F G H) {X : C} : (t.adj₁.homEquiv ((H.comp G).obj X) (F.obj X)).symm (CategoryStruct.comp (t.adj₂.counit.app X) (t.adj₁.unit.app X)) = F.map (t.adj₂.counit.app X)

For an adjoint triple F ⊣ G ⊣ H, the components of the natural transformation H ⋙ G ⟶ F ⋙ G obtained from the units and counits of the adjunctions are under the first adjunction adjunct to the image of the counit of the second adjunction under F.

theorem CategoryTheory.Adjunction.Triple.counit_unit_app_eq_map_HToF {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} (t : Triple F G H) [G.Full] [G.Faithful] {X : C} : CategoryStruct.comp (t.adj₂.counit.app X) (t.adj₁.unit.app X) = G.map (t.rightToLeft.app X)

For an adjoint triple F ⊣ G ⊣ H where G is fully faithful, the components of the natural transformation H ⋙ G ⟶ F ⋙ G obtained from the units and counits of the adjunctions are simply the images of the components of the natural transformation H ⟶ F under G.

theorem CategoryTheory.Adjunction.Triple.epi_rightToLeft_iff_epi_whiskerRight_adj₁_unit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F H : Functor C D} {G : Functor D C} (t : Triple F G H) [G.Full] [G.Faithful] [Limits.HasPushouts D] : Epi t.rightToLeft ↔ Epi (Functor.whiskerRight t.adj₁.unit H)

For an adjoint triple F ⊣ G ⊣ H where G is fully faithful and its codomain has all pushouts, the natural transformation H ⟶ F is epic iff the unit of the adjunction F ⊣ G whiskered with H is.

theorem CategoryTheory.Adjunction.Triple.epi_rightToLeft_iff {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} (t : Triple F G H) [G.Full] [G.Faithful] [Limits.HasPushouts C] [Limits.HasPushouts D] [H.PreservesEpimorphisms] : Epi t.rightToLeft ↔ Epi (CategoryStruct.comp t.adj₂.counit t.adj₁.unit)

For an adjoint triple F ⊣ G ⊣ H where G is fully faithful, H preserves epimorphisms (which is for example the case if H has a further right adjoint) and both categories have all pushouts, the natural transformation H ⟶ F is epic iff the natural transformation H ⋙ G ⟶ F ⋙ G obtained from the units and counits of the adjunctions is.

theorem CategoryTheory.Adjunction.Triple.homEquiv_counit_unit_app_eq_G_map_unit {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} (t : Triple F G H) {X : D} : (t.adj₁.homEquiv (G.obj X) ((G.comp H).obj X)) (CategoryStruct.comp (t.adj₁.counit.app X) (t.adj₂.unit.app X)) = G.map (t.adj₂.unit.app X)

For an adjoint triple F ⊣ G ⊣ H, the components of the natural transformation G ⋙ F ⟶ G ⋙ H obtained from the units and counits of the adjunctions are under the first adjunction adjunct to the image of the unit of the second adjunction under G.

theorem CategoryTheory.Adjunction.Triple.homEquiv_symm_counit_unit_app_eq_G_map_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} (t : Triple F G H) {X : D} : (t.adj₂.homEquiv ((G.comp F).obj X) (G.obj X)).symm (CategoryStruct.comp (t.adj₁.counit.app X) (t.adj₂.unit.app X)) = G.map (t.adj₁.counit.app X)

For an adjoint triple F ⊣ G ⊣ H, the components of the natural transformation G ⋙ F ⟶ G ⋙ H obtained from the units and counits of the adjunctions are under the second adjunction adjunct to the image of the counit of the first adjunction under G.

theorem CategoryTheory.Adjunction.Triple.counit_unit_app_eq_FToH_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F H : Functor C D} {G : Functor D C} (t : Triple F G H) [F.Full] [F.Faithful] {X : D} : CategoryStruct.comp (t.adj₁.counit.app X) (t.adj₂.unit.app X) = t.leftToRight.app (G.obj X)

For an adjoint triple F ⊣ G ⊣ H where F and H are fully faithful, the components of the natural transformation G ⋙ F ⟶ G ⋙ H obtained from the units and counits of the adjunctions are simply the components of the natural transformation F ⟶ H at G.

theorem CategoryTheory.Adjunction.Triple.mono_leftToRight_iff_mono_whiskerLeft_unit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F H : Functor C D} {G : Functor D C} (t : Triple F G H) [F.Full] [F.Faithful] [Limits.HasPullbacks D] : Mono t.leftToRight ↔ Mono (F.whiskerLeft t.adj₂.unit)

For an adjoint triple F ⊣ G ⊣ H where F and H are fully faithful and their codomain has all pullbacks, the natural transformation F ⟶ H is monic iff F whiskered with the unit of the adjunction G ⊣ H is.

theorem CategoryTheory.Adjunction.Triple.mono_leftToRight_iff {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F H : Functor C D} {G : Functor D C} (t : Triple F G H) [F.Full] [F.Faithful] [Limits.HasPullbacks D] : Mono t.leftToRight ↔ Mono (CategoryStruct.comp t.adj₁.counit t.adj₂.unit)

For an adjoint triple F ⊣ G ⊣ H where F and H are fully faithful and their codomain has all pullbacks, the natural transformation F ⟶ H is monic iff the natural transformation G ⋙ F ⟶ G ⋙ H obtained from the units and counits of the adjunctions is.