Compatibilities for left adjoints from compatibilities satisfied by right adjoints

In this file, given isomorphisms between compositions of right adjoint functors, we obtain isomorphisms between the corresponding compositions of the left adjoint functors, and show that the left adjoint functors satisfy properties similar to the left/right unitality and the associativity of pseudofunctors if the right adjoint functors satisfy the corresponding properties.

This shall be used to study the behaviour with respect to composition of the pullback functors on presheaves of modules, by reducing these definitions and properties to the (obvious) case of the pushforward functors. Similar results shall be obtained for sheaves of modules (TODO).

def CategoryTheory.Adjunction.leftAdjointIdIso {C₀ : Type u_1} [Category.{u_5, u_1} C₀] {F G : Functor C₀ C₀} (adj : F ⊣ G) (e : G ≅ Functor.id C₀) : F ≅ Functor.id C₀

If a right adjoint functor is isomorphic to the identity functor, so is the left adjoint.

Equations

• adj.leftAdjointIdIso e = (CategoryTheory.conjugateIsoEquiv CategoryTheory.Adjunction.id adj).symm e.symm

theorem CategoryTheory.Adjunction.leftAdjointIdIso_inv_app {C₀ : Type u_1} [Category.{u_5, u_1} C₀] {F G : Functor C₀ C₀} (adj : F ⊣ G) (e : G ≅ Functor.id C₀) (X : C₀) : (adj.leftAdjointIdIso e).inv.app X = CategoryStruct.comp (adj.unit.app X) (e.hom.app (F.obj X))

theorem CategoryTheory.Adjunction.leftAdjointIdIso_hom_app {C₀ : Type u_1} [Category.{u_5, u_1} C₀] {F G : Functor C₀ C₀} (adj : F ⊣ G) (e : G ≅ Functor.id C₀) (X : C₀) : (adj.leftAdjointIdIso e).hom.app X = CategoryStruct.comp (F.map (e.inv.app X)) (adj.counit.app X)

def CategoryTheory.Adjunction.leftAdjointCompNatTrans {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [Category.{u_5, u_1} C₀] [Category.{u_6, u_2} C₁] [Category.{u_7, u_3} C₂] {F₀₁ : Functor C₀ C₁} {F₁₂ : Functor C₁ C₂} {F₀₂ : Functor C₀ C₂} {G₁₀ : Functor C₁ C₀} {G₂₁ : Functor C₂ C₁} {G₂₀ : Functor C₂ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (τ₀₁₂ : G₂₀ ⟶ G₂₁.comp G₁₀) : F₀₁.comp F₁₂ ⟶ F₀₂

A natural transformation G₂₀ ⟶ G₂₁ ⋙ G₁₀ involving right adjoint functors induces a natural transformation F₀₁ ⋙ F₁₂ ⟶ F₀₂ between the corresponding left adjoint functors.

Equations

• adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂ = (CategoryTheory.conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)).symm τ₀₁₂

theorem CategoryTheory.Adjunction.leftAdjointCompNatTrans_app {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [Category.{u_5, u_1} C₀] [Category.{u_6, u_2} C₁] [Category.{u_7, u_3} C₂] {F₀₁ : Functor C₀ C₁} {F₁₂ : Functor C₁ C₂} {F₀₂ : Functor C₀ C₂} {G₁₀ : Functor C₁ C₀} {G₂₁ : Functor C₂ C₁} {G₂₀ : Functor C₂ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (τ₀₁₂ : G₂₀ ⟶ G₂₁.comp G₁₀) (X : C₀) : (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂).app X = CategoryStruct.comp (F₁₂.map (F₀₁.map (adj₀₂.unit.app X))) (CategoryStruct.comp (F₁₂.map (F₀₁.map (τ₀₁₂.app (F₀₂.obj X)))) (CategoryStruct.comp (F₁₂.map (adj₀₁.counit.app (G₂₁.obj (F₀₂.obj X)))) (adj₁₂.counit.app (F₀₂.obj X))))

def CategoryTheory.Adjunction.leftAdjointCompIso {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [Category.{u_5, u_1} C₀] [Category.{u_6, u_2} C₁] [Category.{u_7, u_3} C₂] {F₀₁ : Functor C₀ C₁} {F₁₂ : Functor C₁ C₂} {F₀₂ : Functor C₀ C₂} {G₁₀ : Functor C₁ C₀} {G₂₁ : Functor C₂ C₁} {G₂₀ : Functor C₂ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (e₀₁₂ : G₂₁.comp G₁₀ ≅ G₂₀) : F₀₁.comp F₁₂ ≅ F₀₂

A natural isomorphism G₂₁ ⋙ G₁₀ ≅ G₂₀ involving right adjoint functors induces a natural isomorphism F₀₁ ⋙ F₁₂ ≅ F₀₂ between the corresponding left adjoint functors.

Equations

• adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂ = (CategoryTheory.conjugateIsoEquiv adj₀₂ (adj₀₁.comp adj₁₂)).symm e₀₁₂.symm

theorem CategoryTheory.Adjunction.leftAdjointCompIso_hom_app {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [Category.{u_5, u_1} C₀] [Category.{u_6, u_2} C₁] [Category.{u_7, u_3} C₂] {F₀₁ : Functor C₀ C₁} {F₁₂ : Functor C₁ C₂} {F₀₂ : Functor C₀ C₂} {G₁₀ : Functor C₁ C₀} {G₂₁ : Functor C₂ C₁} {G₂₀ : Functor C₂ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (e₀₁₂ : G₂₁.comp G₁₀ ≅ G₂₀) (X : C₀) : (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂).hom.app X = CategoryStruct.comp (F₁₂.map (F₀₁.map (adj₀₂.unit.app X))) (CategoryStruct.comp (F₁₂.map (F₀₁.map (e₀₁₂.inv.app (F₀₂.obj X)))) (CategoryStruct.comp (F₁₂.map (adj₀₁.counit.app (G₂₁.obj (F₀₂.obj X)))) (adj₁₂.counit.app (F₀₂.obj X))))

theorem CategoryTheory.Adjunction.leftAdjointCompIso_inv_app {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [Category.{u_5, u_1} C₀] [Category.{u_6, u_2} C₁] [Category.{u_7, u_3} C₂] {F₀₁ : Functor C₀ C₁} {F₁₂ : Functor C₁ C₂} {F₀₂ : Functor C₀ C₂} {G₁₀ : Functor C₁ C₀} {G₂₁ : Functor C₂ C₁} {G₂₀ : Functor C₂ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (e₀₁₂ : G₂₁.comp G₁₀ ≅ G₂₀) (X : C₀) : (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂).inv.app X = CategoryStruct.comp (F₀₂.map (adj₀₁.unit.app X)) (CategoryStruct.comp (F₀₂.map (G₁₀.map (adj₁₂.unit.app (F₀₁.obj X)))) (CategoryStruct.comp (F₀₂.map (e₀₁₂.hom.app (F₁₂.obj (F₀₁.obj X)))) (adj₀₂.counit.app (F₁₂.obj (F₀₁.obj X)))))

theorem CategoryTheory.Adjunction.leftAdjointCompIso_hom {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [Category.{u_5, u_1} C₀] [Category.{u_7, u_2} C₁] [Category.{u_6, u_3} C₂] {F₀₁ : Functor C₀ C₁} {F₁₂ : Functor C₁ C₂} {F₀₂ : Functor C₀ C₂} {G₁₀ : Functor C₁ C₀} {G₂₁ : Functor C₂ C₁} {G₂₀ : Functor C₂ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (e₀₁₂ : G₂₁.comp G₁₀ ≅ G₂₀) : (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂).hom = adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ e₀₁₂.inv

theorem CategoryTheory.Adjunction.leftAdjointCompIso_comp_id {C₀ : Type u_1} {C₁ : Type u_2} [Category.{u_5, u_1} C₀] [Category.{u_6, u_2} C₁] {F₀₁ : Functor C₀ C₁} {F₁₁' : Functor C₁ C₁} {G₁₀ : Functor C₁ C₀} {G₁'₁ : Functor C₁ C₁} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₁' : F₁₁' ⊣ G₁'₁) (e₀₁₁' : G₁'₁.comp G₁₀ ≅ G₁₀) (e₁'₁ : G₁'₁ ≅ Functor.id C₁) (h : e₀₁₁' = Functor.isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor) : adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ e₀₁₁' = F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor

theorem CategoryTheory.Adjunction.leftAdjointCompIso_id_comp {C₀ : Type u_1} {C₁ : Type u_2} [Category.{u_5, u_1} C₀] [Category.{u_6, u_2} C₁] {F₀₀' : Functor C₀ C₀} {F₀'₁ : Functor C₀ C₁} {G₀'₀ : Functor C₀ C₀} {G₁₀' : Functor C₁ C₀} (adj₀₀' : F₀₀' ⊣ G₀'₀) (adj₀'₁ : F₀'₁ ⊣ G₁₀') (e₀₀'₁ : G₁₀'.comp G₀'₀ ≅ G₁₀') (e₀'₀ : G₀'₀ ≅ Functor.id C₀) (h : e₀₀'₁ = G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor) : adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ e₀₀'₁ = Functor.isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor

theorem CategoryTheory.Adjunction.leftAdjointCompNatTrans₀₁₃_eq_conjugateEquiv_symm {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [Category.{u_6, u_1} C₀] [Category.{u_7, u_2} C₁] [Category.{u_8, u_3} C₂] [Category.{u_5, u_4} C₃] {F₀₁ : Functor C₀ C₁} {F₁₂ : Functor C₁ C₂} {F₂₃ : Functor C₂ C₃} {F₁₃ : Functor C₁ C₃} {F₀₃ : Functor C₀ C₃} {G₁₀ : Functor C₁ C₀} {G₂₁ : Functor C₂ C₁} {G₃₂ : Functor C₃ C₂} {G₃₁ : Functor C₃ C₁} {G₃₀ : Functor C₃ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₂₃ : F₂₃ ⊣ G₃₂) (adj₁₃ : F₁₃ ⊣ G₃₁) (adj₀₃ : F₀₃ ⊣ G₃₀) (τ₁₂₃ : G₃₁ ⟶ G₃₂.comp G₂₁) (τ₀₁₃ : G₃₀ ⟶ G₃₁.comp G₁₀) : CategoryStruct.comp (F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃)) (adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃) = (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm (CategoryStruct.comp τ₀₁₃ (Functor.whiskerRight τ₁₂₃ G₁₀))

theorem CategoryTheory.Adjunction.leftAdjointCompNatTrans₀₂₃_eq_conjugateEquiv_symm {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [Category.{u_6, u_1} C₀] [Category.{u_7, u_2} C₁] [Category.{u_8, u_3} C₂] [Category.{u_5, u_4} C₃] {F₀₁ : Functor C₀ C₁} {F₁₂ : Functor C₁ C₂} {F₂₃ : Functor C₂ C₃} {F₀₂ : Functor C₀ C₂} {F₀₃ : Functor C₀ C₃} {G₁₀ : Functor C₁ C₀} {G₂₁ : Functor C₂ C₁} {G₃₂ : Functor C₃ C₂} {G₂₀ : Functor C₂ C₀} {G₃₀ : Functor C₃ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₂₃ : F₂₃ ⊣ G₃₂) (adj₀₂ : F₀₂ ⊣ G₂₀) (adj₀₃ : F₀₃ ⊣ G₃₀) (τ₀₁₂ : G₂₀ ⟶ G₂₁.comp G₁₀) (τ₀₂₃ : G₃₀ ⟶ G₃₂.comp G₂₀) : CategoryStruct.comp (F₀₁.associator F₁₂ F₂₃).inv (CategoryStruct.comp (Functor.whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃) (adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃)) = (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm (CategoryStruct.comp τ₀₂₃ (CategoryStruct.comp (G₃₂.whiskerLeft τ₀₁₂) (G₃₂.associator G₂₁ G₁₀).inv))

theorem CategoryTheory.Adjunction.leftAdjointCompNatTrans_assoc {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [Category.{u_5, u_1} C₀] [Category.{u_8, u_2} C₁] [Category.{u_7, u_3} C₂] [Category.{u_6, u_4} C₃] {F₀₁ : Functor C₀ C₁} {F₁₂ : Functor C₁ C₂} {F₂₃ : Functor C₂ C₃} {F₀₂ : Functor C₀ C₂} {F₁₃ : Functor C₁ C₃} {F₀₃ : Functor C₀ C₃} {G₁₀ : Functor C₁ C₀} {G₂₁ : Functor C₂ C₁} {G₃₂ : Functor C₃ C₂} {G₂₀ : Functor C₂ C₀} {G₃₁ : Functor C₃ C₁} {G₃₀ : Functor C₃ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₂₃ : F₂₃ ⊣ G₃₂) (adj₀₂ : F₀₂ ⊣ G₂₀) (adj₁₃ : F₁₃ ⊣ G₃₁) (adj₀₃ : F₀₃ ⊣ G₃₀) (τ₀₁₂ : G₂₀ ⟶ G₂₁.comp G₁₀) (τ₁₂₃ : G₃₁ ⟶ G₃₂.comp G₂₁) (τ₀₁₃ : G₃₀ ⟶ G₃₁.comp G₁₀) (τ₀₂₃ : G₃₀ ⟶ G₃₂.comp G₂₀) (h : CategoryStruct.comp τ₀₂₃ (G₃₂.whiskerLeft τ₀₁₂) = CategoryStruct.comp τ₀₁₃ (CategoryStruct.comp (Functor.whiskerRight τ₁₂₃ G₁₀) (G₃₂.associator G₂₁ G₁₀).hom)) : CategoryStruct.comp (F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃)) (adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃) = CategoryStruct.comp (F₀₁.associator F₁₂ F₂₃).inv (CategoryStruct.comp (Functor.whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃) (adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃))

theorem CategoryTheory.Adjunction.leftAdjointCompIso_assoc {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [Category.{u_5, u_1} C₀] [Category.{u_7, u_2} C₁] [Category.{u_6, u_3} C₂] [Category.{u_8, u_4} C₃] {F₀₁ : Functor C₀ C₁} {F₁₂ : Functor C₁ C₂} {F₂₃ : Functor C₂ C₃} {F₀₂ : Functor C₀ C₂} {F₁₃ : Functor C₁ C₃} {F₀₃ : Functor C₀ C₃} {G₁₀ : Functor C₁ C₀} {G₂₁ : Functor C₂ C₁} {G₃₂ : Functor C₃ C₂} {G₂₀ : Functor C₂ C₀} {G₃₁ : Functor C₃ C₁} {G₃₀ : Functor C₃ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₂₃ : F₂₃ ⊣ G₃₂) (adj₀₂ : F₀₂ ⊣ G₂₀) (adj₁₃ : F₁₃ ⊣ G₃₁) (adj₀₃ : F₀₃ ⊣ G₃₀) (e₀₁₂ : G₂₁.comp G₁₀ ≅ G₂₀) (e₁₂₃ : G₃₂.comp G₂₁ ≅ G₃₁) (e₀₁₃ : G₃₁.comp G₁₀ ≅ G₃₀) (e₀₂₃ : G₃₂.comp G₂₀ ≅ G₃₀) (h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ Functor.isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃) : F₀₁.isoWhiskerLeft (adj₁₂.leftAdjointCompIso adj₂₃ adj₁₃ e₁₂₃) ≪≫ adj₀₁.leftAdjointCompIso adj₁₃ adj₀₃ e₀₁₃ = (F₀₁.associator F₁₂ F₂₃).symm ≪≫ Functor.isoWhiskerRight (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂) F₂₃ ≪≫ adj₀₂.leftAdjointCompIso adj₂₃ adj₀₃ e₀₂₃