Adjoint triples

This file concerns adjoint triples F ⊣ G ⊣ H of functors F H : C ⥤ D, G : D ⥤ C. We first prove that F is fully faithful iff H is, and then prove results about the two special cases where G is fully faithful or F and H are.

Main results

All results are about an adjoint triple F ⊣ G ⊣ H where adj₁ : F ⊣ G and adj₂ : G ⊣ H. We bundle the adjunctions in a structure Triple F G H.

• fullyFaithfulEquiv: F is fully faithful iff H is.
• rightToLeft: the canonical natural transformation H ⟶ F that exists whenever G is fully faithful. This is defined as the preimage of adj₂.counit ≫ adj₁.unit under whiskering with G, but formulas in terms of the units resp. counits of the adjunctions are also given.
• whiskerRight_rightToLeft: whiskering rightToLeft : H ⟶ F with G yields adj₂.counit ≫ adj₁.unit : H ⋙ G ⟶ F ⋙ G.
• epi_rightToLeft_app_iff_epi_map_adj₁_unit_app: rightToLeft : H ⟶ F is epic at X iff the image of adj₁.unit.app X under H is.
• epi_rightToLeft_app_iff_epi_map_adj₂_counit_app: rightToLeft : H ⟶ F is epic at X iff the image of adj₂.counit.app X under F is.
• epi_rightToLeft_app_iff: when H preserves epimorphisms, rightToLeft : H ⟶ F is epic at X iff adj₂.counit ≫ adj₁.unit : H ⋙ G ⟶ F ⋙ G is.
• leftToRight: the canonical natural transformation F ⟶ H that exists whenever F and H are fully faithful. This is defined in terms of the units of the adjunctions, but a formula in terms of the counits is also given.
• whiskerLeft_leftToRight: whiskering G with leftToRight : F ⟶ H yields adj₁.counit ≫ adj₂.unit : G ⋙ F ⟶ G ⋙ H.
• mono_leftToRight_app_iff_mono_adj₂_unit_app: leftToRight : F ⟶ H is monic at X iff adj₂.unit is monic at F.obj X.
• mono_leftToRight_app_iff_mono_adj₁_counit_app: leftToRight : F ⟶ H is monic at X iff adj₁.unit is monic at H.obj X.
• mono_leftToRight_app_iff: leftToRight : H ⟶ F is componentwise monic iff adj₁.counit ≫ adj₂.unit : G ⋙ F ⟶ G ⋙ H is.

structure CategoryTheory.Adjunction.Triple {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) (G : Functor D C) (H : Functor C D) : Type (max (max (max u_1 u_2) u_3) u_4)

Structure containing the two adjunctions of an adjoint triple F ⊣ G ⊣ H.

• adj₁ : F ⊣ G

  Adjunction F ⊣ G of the adjoint triple F ⊣ G ⊣ H.

• adj₂ : G ⊣ H

  Adjunction G ⊣ H of the adjoint triple F ⊣ G ⊣ H.

theorem CategoryTheory.Adjunction.Triple.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 : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) : IsIso t.adj₁.unit ↔ IsIso t.adj₂.counit

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

def CategoryTheory.Adjunction.Triple.op {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) : Triple H.op G.op F.op

The adjoint triple H.op ⊣ G.op ⊣ F.op dual to an adjoint triple F ⊣ G ⊣ H.

Equations

• t.op = { adj₁ := t.adj₂.op, adj₂ := t.adj₁.op }

@[simp]

theorem CategoryTheory.Adjunction.Triple.op_adj₂ {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) : t.op.adj₂ = t.adj₁.op

@[simp]

theorem CategoryTheory.Adjunction.Triple.op_adj₁ {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) : t.op.adj₁ = t.adj₂.op

noncomputable def CategoryTheory.Adjunction.Triple.rightToLeft {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : 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.

Equations

• t.rightToLeft = ((CategoryTheory.Functor.FullyFaithful.ofFullyFaithful G).whiskeringRight C).preimage (CategoryTheory.CategoryStruct.comp t.adj₂.counit t.adj₁.unit)

@[simp]

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

For an adjoint triple F ⊣ G ⊣ H where G is fully faithful, whiskering the natural transformation H ⟶ F with G yields the composition of the counit of the second adjunction with the unit of the first adjunction.

theorem CategoryTheory.Adjunction.Triple.whiskerRight_rightToLeft_assoc {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) [G.Full] [G.Faithful] {Z : Functor C C} (h : F.comp G ⟶ Z) : CategoryStruct.comp (Functor.whiskerRight t.rightToLeft G) h = CategoryStruct.comp t.adj₂.counit (CategoryStruct.comp t.adj₁.unit h)

@[simp]

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

For an adjoint triple F ⊣ G ⊣ H where G is fully faithful, the images of the components of the natural transformation H ⟶ F under G are the components of the composition of counit of the second adjunction with the unit of the first adjunction.

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

theorem CategoryTheory.Adjunction.Triple.rightToLeft_eq_units {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) [G.Full] [G.Faithful] : t.rightToLeft = CategoryStruct.comp H.leftUnitor.inv (CategoryStruct.comp (Functor.whiskerRight t.adj₁.unit H) (CategoryStruct.comp (F.associator G H).hom (CategoryStruct.comp (inv (F.whiskerLeft t.adj₂.unit)) F.rightUnitor.hom)))

The natural transformation H ⟶ F for an adjoint triple F ⊣ G ⊣ H with G fully faithful is also equal to the whiskered unit H ⟶ F ⋙ G ⋙ H of the first adjunction followed by the inverse of the whiskered unit F ⟶ F ⋙ G ⋙ H of the second.

theorem CategoryTheory.Adjunction.Triple.rightToLeft_eq_counits {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) [G.Full] [G.Faithful] : t.rightToLeft = CategoryStruct.comp H.rightUnitor.inv (CategoryStruct.comp (inv (H.whiskerLeft t.adj₁.counit)) (CategoryStruct.comp (H.associator G F).inv (CategoryStruct.comp (Functor.whiskerRight t.adj₂.counit F) F.leftUnitor.hom)))

The natural transformation H ⟶ F for an adjoint triple F ⊣ G ⊣ H with G fully faithful is also equal to the inverse of the whiskered counit H ⋙ G ⋙ F ⟶ H of the first adjunction followed by the whiskered counit H ⋙ G ⋙ F ⟶ F of the second.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Adjunction.Triple.rightToLeft_app_adj₂_unit_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) [G.Full] [G.Faithful] (X : C) {Z : D} (h : H.obj (G.obj (F.obj X)) ⟶ Z) : CategoryStruct.comp (t.rightToLeft.app X) (CategoryStruct.comp (t.adj₂.unit.app (F.obj X)) h) = CategoryStruct.comp (H.map (t.adj₁.unit.app X)) h

@[simp]

theorem CategoryTheory.Adjunction.Triple.op_rightToLeft {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) [G.Full] [G.Faithful] : t.op.rightToLeft = NatTrans.op t.rightToLeft

For an adjoint triple F ⊣ G ⊣ H where G is fully faithful, the natural transformation F.op ⟶ H.op obtained from the dual adjoint triple H.op ⊣ G.op ⊣ F.op is dual to the natural transformation H ⟶ F.

theorem CategoryTheory.Adjunction.Triple.epi_rightToLeft_app_iff_epi_map_adj₁_unit_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) [G.Full] [G.Faithful] {X : C} : Epi (t.rightToLeft.app X) ↔ Epi (H.map (t.adj₁.unit.app X))

For an adjoint triple F ⊣ G ⊣ H where G is fully faithful, the natural transformation H ⟶ F is epic at X iff the image of the unit of the adjunction F ⊣ G under H is.

theorem CategoryTheory.Adjunction.Triple.epi_rightToLeft_app_iff_epi_map_adj₂_counit_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) [G.Full] [G.Faithful] {X : C} : Epi (t.rightToLeft.app X) ↔ Epi (F.map (t.adj₂.counit.app X))

For an adjoint triple F ⊣ G ⊣ H where G is fully faithful, the natural transformation H ⟶ F is epic at X iff the image of the counit of the adjunction G ⊣ H under F is.

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

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

noncomputable def CategoryTheory.Adjunction.Triple.leftToRight {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : 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.

Equations

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

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

theorem CategoryTheory.Adjunction.Triple.leftToRight_eq_counits {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) [F.Full] [F.Faithful] [H.Full] [H.Faithful] : t.leftToRight = CategoryStruct.comp F.leftUnitor.inv (CategoryStruct.comp (inv (Functor.whiskerRight t.adj₂.counit F)) (CategoryStruct.comp (H.associator G F).hom (CategoryStruct.comp (H.whiskerLeft t.adj₁.counit) H.rightUnitor.hom)))

The natural transformation F ⟶ H for an adjoint triple F ⊣ G ⊣ H with F and H fully faithful is also equal to the inverse of the whiskered counit H ⋙ G ⋙ F ⟶ F of the second adjunction followed by the whiskered counit H ⋙ G ⋙ F ⟶ H of the first.

@[simp]

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

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

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

@[simp]

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

For an adjoint triple F ⊣ G ⊣ H where F and H are fully faithful, whiskering G with the natural transformation F ⟶ H yields the composition of the counit of the first adjunction with the unit of the second adjunction.

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Adjunction.Triple.leftToRight_op {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) [F.Full] [F.Faithful] [H.Full] [H.Faithful] : t.op.leftToRight = NatTrans.op t.leftToRight

For an adjoint triple F ⊣ G ⊣ H where F and H are fully faithful, the natural transformation H.op ⟶ F.op obtained from the dual adjoint triple H.op ⊣ G.op ⊣ F.op is dual to the natural transformation F ⟶ H.

theorem CategoryTheory.Adjunction.Triple.mono_leftToRight_app_iff_mono_adj₂_unit_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) [F.Full] [F.Faithful] {X : C} : Mono (t.leftToRight.app X) ↔ Mono (t.adj₂.unit.app (F.obj X))

For an adjoint triple F ⊣ G ⊣ H where F and H are fully faithful, the natural transformation F ⟶ H is monic at X iff the unit of the adjunction G ⊣ H is monic at F.obj X.

theorem CategoryTheory.Adjunction.Triple.mono_leftToRight_app_iff_mono_adj₁_counit_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {F : Functor C D} {G : Functor D C} {H : Functor C D} (t : Triple F G H) [F.Full] [F.Faithful] [H.Full] [H.Faithful] {X : C} : Mono (t.leftToRight.app X) ↔ Mono (t.adj₁.counit.app (H.obj X))

For an adjoint triple F ⊣ G ⊣ H where F and H are fully faithful, the natural transformation F ⟶ H is monic at X iff the counit of the adjunction F ⊣ G is monic at H.obj X.

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

For an adjoint triple F ⊣ G ⊣ H where F and H are fully faithful, the natural transformation F ⟶ H is componentwise monic iff the natural transformation G ⋙ F ⟶ G ⋙ H obtained from the units and counits of the adjunctions is. Note that unlike epi_rightToLeft_app_iff, this equivalence does not make sense on a per-object basis because the components of the two natural transformations are indexed by different categories.