Adjoint lifting

This file gives two constructions for building right adjoints: the adjoint triangle theorem and the adjoint lifting theorem.

The adjoint triangle theorem concerns a functor F : B ⥤ A with a right adjoint U such that η_X : X ⟶ UFX is a regular mono. Then for any category C with equalizers of coreflexive pairs, a functor L : C ⥤ B has a right adjoint if (and only if) the composite L ⋙ F does. Note that the condition on F regarding η_X is automatically satisfied in the case when F is a comonadic functor, giving the corollary: isLeftAdjoint_triangle_lift_comonadic, i.e. if F is comonadic, C has coreflexive equalizers then L : C ⥤ B has a right adjoint provided L ⋙ F does.

The adjoint lifting theorem says that given a commutative square of functors (up to isomorphism):

      Q
    A → B
  U ↓   ↓ V
    C → D
      L

where V is comonadic, U has a right adjoint, and A has coreflexive equalizers, then if L has a right adjoint then Q has a right adjoint.

Implementation

It is more convenient to prove this theorem by assuming we are given the explicit adjunction rather than just a functor known to be a right adjoint. In docstrings, we write (η, ε) for the unit and counit of the adjunction adj₁ : F ⊣ U and (ι, δ) for the unit and counit of the adjunction adj₂ : L ⋙ F ⊣ U'.

This file has been adapted from Mathlib/CategoryTheory/Adjunction/Lifting/Left.lean. Please try to keep them in sync.

TODO

• Dualise to lift left adjoints through comonads (by reversing 2-cells).
• Investigate whether it is possible to give a more explicit description of the lifted adjoint, especially in the case when the isomorphism comm is Iso.refl _

References

• https://ncatlab.org/nlab/show/adjoint+triangle+theorem
• https://ncatlab.org/nlab/show/adjoint+lifting+theorem
• Adjoint Lifting Theorems for Categories of Algebras (PT Johnstone, 1975)
• A unified approach to the lifting of adjoints (AJ Power, 1988)

def CategoryTheory.LiftRightAdjoint.unitEqualises {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] {U : Functor A B} {F : Functor B A} (adj₁ : F ⊣ U) [(X : B) → RegularMono (adj₁.unit.app X)] (X : B) : Limits.IsLimit (Limits.Fork.ofι (adj₁.unit.app X) ⋯)

To show that η_X is an equalizer for (UFη_X, η_UFX), it suffices to assume it's always an equalizer of something (i.e. a regular mono).

Equations

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

def CategoryTheory.LiftRightAdjoint.otherMap {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor A B} {F : Functor B A} (L : Functor C B) (U' : Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') (X : B) : U'.obj (F.obj X) ⟶ U'.obj (F.obj (U.obj (F.obj X)))

(Implementation) To construct the right adjoint, we use the equalizer of U' F η_X with the composite

U' F X ⟶ U' F L U' F X ⟶ U' F U F L U' F X ⟶ U' F U F X

where the first morphism is ι_U'FX, the second is U' F η_LU'FX and the third is U' F U δ_FX. We will show that this equalizer exists and that it forms the object map for a right adjoint to L.

Equations

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

instance CategoryTheory.LiftRightAdjoint.instIsCoreflexivePairMapAppUnitOtherMap {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor A B} {F : Functor B A} (L : Functor C B) (U' : Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') (X : B) : IsCoreflexivePair (U'.map (F.map (adj₁.unit.app X))) (otherMap L U' adj₁ adj₂ X)

(U'Fη_X, otherMap X) is a coreflexive pair: in particular if C has coreflexive equalizers then this pair has an equalizer.

noncomputable def CategoryTheory.LiftRightAdjoint.constructRightAdjointObj {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor A B} {F : Functor B A} (L : Functor C B) (U' : Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') [Limits.HasCoreflexiveEqualizers C] (Y : B) : C

Construct the object part of the desired right adjoint as the equalizer of U'Fη_Y with otherMap.

Equations

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

noncomputable def CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor A B} {F : Functor B A} (L : Functor C B) (U' : Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') [Limits.HasCoreflexiveEqualizers C] [(X : B) → RegularMono (adj₁.unit.app X)] (Y : C) (X : B) : (Y ⟶ constructRightAdjointObj L U' adj₁ adj₂ X) ≃ (L.obj Y ⟶ X)

The homset equivalence which helps show that L is a left adjoint.

Equations

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

@[simp]

theorem CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_symm_apply {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor A B} {F : Functor B A} (L : Functor C B) (U' : Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') [Limits.HasCoreflexiveEqualizers C] [(X : B) → RegularMono (adj₁.unit.app X)] (Y : C) (X : B) (a✝ : L.obj Y ⟶ X) : (constructRightAdjointEquiv L U' adj₁ adj₂ Y X).symm a✝ = (Limits.Fork.IsLimit.homIso (Limits.limit.isLimit (Limits.parallelPair (U'.map (F.map (adj₁.unit.app X))) (otherMap L U' adj₁ adj₂ X))) Y).symm ⟨(adj₂.homEquiv Y (F.obj X)) ((adj₁.homEquiv (L.obj Y) (F.obj X)).symm ↑((Limits.Fork.IsLimit.homIso (unitEqualises adj₁ X) (L.obj Y)) a✝)), ⋯⟩

@[simp]

theorem CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor A B} {F : Functor B A} (L : Functor C B) (U' : Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') [Limits.HasCoreflexiveEqualizers C] [(X : B) → RegularMono (adj₁.unit.app X)] (Y : C) (X : B) (a✝ : Y ⟶ constructRightAdjointObj L U' adj₁ adj₂ X) : (constructRightAdjointEquiv L U' adj₁ adj₂ Y X) a✝ = (Limits.Fork.IsLimit.homIso (unitEqualises adj₁ X) (L.obj Y)).symm ⟨(adj₁.homEquiv (L.obj Y) (F.obj X)) ((adj₂.homEquiv Y (F.obj X)).symm ↑((Limits.Fork.IsLimit.homIso (Limits.limit.isLimit (Limits.parallelPair (U'.map (F.map (adj₁.unit.app X))) (otherMap L U' adj₁ adj₂ X))) Y) a✝)), ⋯⟩

noncomputable def CategoryTheory.LiftRightAdjoint.constructRightAdjoint {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor A B} {F : Functor B A} (L : Functor C B) (U' : Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') [Limits.HasCoreflexiveEqualizers C] [(X : B) → RegularMono (adj₁.unit.app X)] : Functor B C

Construct the right adjoint to L, with object map constructRightAdjointObj.

Equations

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

theorem CategoryTheory.isLeftAdjoint_triangle_lift {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor A B} {F : Functor B A} (L : Functor C B) (adj₁ : F ⊣ U) [(X : B) → RegularMono (adj₁.unit.app X)] [Limits.HasCoreflexiveEqualizers C] [(L.comp F).IsLeftAdjoint] : L.IsLeftAdjoint

The adjoint triangle theorem: Suppose U : A ⥤ B has a left adjoint F such that each unit η_X : X ⟶ UFX is a regular monomorphism. Then if a category C has equalizers of coreflexive pairs, then a functor L : C ⥤ B has a right adjoint if the composite L ⋙ F does.

Note the converse is true (with weaker assumptions), by Adjunction.comp. See https://ncatlab.org/nlab/show/adjoint+triangle+theorem

theorem CategoryTheory.isLeftAdjoint_triangle_lift_comonadic {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (F : Functor B A) [ComonadicLeftAdjoint F] {L : Functor C B} [Limits.HasCoreflexiveEqualizers C] [(L.comp F).IsLeftAdjoint] : L.IsLeftAdjoint

If L ⋙ F has a right adjoint, the domain of L has coreflexive equalizers and F is a comonadic functor, then L has a right adjoint. This is a special case of isLeftAdjoint_triangle_lift which is often more useful in practice.

theorem CategoryTheory.isLeftAdjoint_square_lift {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (Q : Functor A B) (V : Functor B D) (U : Functor A C) (L : Functor C D) (comm : U.comp L ≅ Q.comp V) [U.IsLeftAdjoint] [V.IsLeftAdjoint] [L.IsLeftAdjoint] [(X : B) → RegularMono ((Adjunction.ofIsLeftAdjoint V).unit.app X)] [Limits.HasCoreflexiveEqualizers A] : Q.IsLeftAdjoint

Suppose we have a commutative square of functors

      Q
    A → B
  U ↓   ↓ V
    C → D
      R

where U has a right adjoint, A has coreflexive equalizers and V has a right adjoint such that each component of the counit is a regular mono. Then Q has a right adjoint if L has a right adjoint.

See https://ncatlab.org/nlab/show/adjoint+lifting+theorem

theorem CategoryTheory.isLeftAdjoint_square_lift_comonadic {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] (Q : Functor A B) (V : Functor B D) (U : Functor A C) (L : Functor C D) (comm : U.comp L ≅ Q.comp V) [U.IsLeftAdjoint] [ComonadicLeftAdjoint V] [L.IsLeftAdjoint] [Limits.HasCoreflexiveEqualizers A] : Q.IsLeftAdjoint

Suppose we have a commutative square of functors

      Q
    A → B
  U ↓   ↓ V
    C → D
      R

where U has a right adjoint, A has reflexive equalizers and V is comonadic. Then Q has a right adjoint if L has a right adjoint.

See https://ncatlab.org/nlab/show/adjoint+lifting+theorem