Theorems · Definition · category theory

CategoryTheory.Adjunction.Triple.rightToLeft

{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 → [G.Full] → [G.Faithful] → H ⟶ F

The natural transformation H ⟶ F that exists for every adjoint triple F ⊣ G ⊣ H where G is fully faithful, given here as the preimage of adj₂.counit ≫ adj₁.unit : H ⋙ G ⟶ F ⋙ G under whiskering with G.

Defined in

Mathlib.CategoryTheory.Adjunction.Triple

Cited by

19 results in Mathlib

Foundations

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

Assumes

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