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. 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₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (adj₁ : F ⊣ U) [(X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)] (X : B) : CategoryTheory.Limits.IsLimit (CategoryTheory.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₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B) (U' : CategoryTheory.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₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B) (U' : CategoryTheory.Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') (X : B) : CategoryTheory.IsCoreflexivePair (U'.map (F.map (adj₁.unit.app X))) (CategoryTheory.LiftRightAdjoint.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.

Equations

• ⋯ = ⋯

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

@[simp]

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

noncomputable def CategoryTheory.LiftRightAdjoint.constructRightAdjoint {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B) (U' : CategoryTheory.Functor A C) (adj₁ : F ⊣ U) (adj₂ : L.comp F ⊣ U') [CategoryTheory.Limits.HasCoreflexiveEqualizers C] [(X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)] : CategoryTheory.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₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {U : CategoryTheory.Functor A B} {F : CategoryTheory.Functor B A} (L : CategoryTheory.Functor C B) (adj₁ : F ⊣ U) [(X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)] [CategoryTheory.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₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor B A) [CategoryTheory.ComonadicLeftAdjoint F] {L : CategoryTheory.Functor C B} [CategoryTheory.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₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (Q : CategoryTheory.Functor A B) (V : CategoryTheory.Functor B D) (U : CategoryTheory.Functor A C) (L : CategoryTheory.Functor C D) (comm : U.comp L ≅ Q.comp V) [U.IsLeftAdjoint] [V.IsLeftAdjoint] [L.IsLeftAdjoint] [(X : B) → CategoryTheory.RegularMono ((CategoryTheory.Adjunction.ofIsLeftAdjoint V).unit.app X)] [CategoryTheory.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₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (Q : CategoryTheory.Functor A B) (V : CategoryTheory.Functor B D) (U : CategoryTheory.Functor A C) (L : CategoryTheory.Functor C D) (comm : U.comp L ≅ Q.comp V) [U.IsLeftAdjoint] [CategoryTheory.ComonadicLeftAdjoint V] [L.IsLeftAdjoint] [CategoryTheory.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