Theorems · Definition · category theory

CategoryTheory.Adjunction.Triple.leftToRight

{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            {H : CategoryTheory.Functor C D} → CategoryTheory.Adjunction.Triple F G H → [F.Full] → [F.Faithful] → F ⟶ H

The natural transformation F ⟶ H that exists for every adjoint triple F ⊣ G ⊣ H where F and H are fully faithful, given here as the whiskered unit F ⟶ F ⋙ G ⋙ H of the second adjunction followed by the inverse of the whiskered unit F ⋙ G ⋙ H ⟶ H of the first.

Defined in

Mathlib.CategoryTheory.Adjunction.Triple

Cited by

18 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.FullCategoryTheory.Functor.Faithful