Adjoint lifting

This file gives two constructions for building left adjoints: the adjoint triangle theorem and the adjoint lifting theorem. The adjoint triangle theorem concerns a functor U : B ⥤ C with a left adjoint F such that ε_X : FUX ⟶ X is a regular epi. Then for any category A with coequalizers of reflexive pairs, a functor R : A ⥤ B has a left adjoint if (and only if) the composite R ⋙ U does. Note that the condition on U regarding ε_X is automatically satisfied in the case when U is a monadic functor, giving the corollary: monadicAdjointTriangleLift, i.e. if U is monadic, A has reflexive coequalizers then R : A ⥤ B has a left adjoint provided R ⋙ U does.

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

  Q
A → B

U ↓ ↓ V C → D R

where U and V are monadic and A has reflexive coequalizers, then if R has a left adjoint then Q has a left 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₂ : F' ⊣ R ⋙ U.

TODO

Dualise to lift right adjoints through comonads (by reversing 1-cells) and dualise to lift right adjoints through monads (by reversing 2-cells), and the combination.

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.LiftAdjoint.counitCoequalises {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {U : CategoryTheory.Functor B C} {F : CategoryTheory.Functor C B} (adj₁ : F ⊣ U) [(X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)] (X : B) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (adj₁.counit.app X) (_ : CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (U.toPrefunctor.map (adj₁.counit.app X))) (adj₁.counit.app X) = CategoryTheory.CategoryStruct.comp (adj₁.counit.app (F.toPrefunctor.obj (U.toPrefunctor.obj X))) (adj₁.counit.app X)))

To show that ε_X is a coequalizer for (FUε_X, ε_FUX), it suffices to assume it's always a coequalizer of something (i.e. a regular epi).

Equations

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

def CategoryTheory.LiftAdjoint.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 B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B) (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ CategoryTheory.Functor.comp R U) (X : B) : F'.toPrefunctor.obj (U.toPrefunctor.obj (F.toPrefunctor.obj (U.toPrefunctor.obj X))) ⟶ F'.toPrefunctor.obj (U.toPrefunctor.obj X)

(Implementation) To construct the left adjoint, we use the coequalizer of F' U ε_Y with the composite

F' U F U X ⟶ F' U F U R F U' X ⟶ F' U R F' U X ⟶ F' U X

where the first morphism is F' U F ι_UX, the second is F' U ε_RF'UX, and the third is δ_F'UX. We will show that this coequalizer exists and that it forms the object map for a left adjoint to R.

Equations

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

instance CategoryTheory.LiftAdjoint.instIsReflexivePairObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorObjToQuiverToCategoryStructToPrefunctorObjToPrefunctorCompIdMapMapAppCounitOtherMap {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 B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B) (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ CategoryTheory.Functor.comp R U) (X : B) : CategoryTheory.IsReflexivePair (F'.toPrefunctor.map (U.toPrefunctor.map (adj₁.counit.app X))) (CategoryTheory.LiftAdjoint.otherMap R F' adj₁ adj₂ X)

(F'Uε_X, otherMap X) is a reflexive pair: in particular if A has reflexive coequalizers then it has a coequalizer.

Equations

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

noncomputable def CategoryTheory.LiftAdjoint.constructLeftAdjointObj {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 B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B) (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ CategoryTheory.Functor.comp R U) [CategoryTheory.Limits.HasReflexiveCoequalizers A] (Y : B) : A

Construct the object part of the desired left adjoint as the coequalizer of F'Uε_Y with otherMap.

Equations

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

@[simp]

theorem CategoryTheory.LiftAdjoint.constructLeftAdjointEquiv_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 B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B) (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ CategoryTheory.Functor.comp R U) [CategoryTheory.Limits.HasReflexiveCoequalizers A] [(X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)] (Y : A) (X : B) : ∀ (a : CategoryTheory.LiftAdjoint.constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y), (CategoryTheory.LiftAdjoint.constructLeftAdjointEquiv R F' adj₁ adj₂ Y X) a = (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.LiftAdjoint.counitCoequalises adj₁ X) (R.toPrefunctor.obj Y)).symm { val := CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((adj₂.homEquiv (U.toPrefunctor.obj X) Y) ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F'.toPrefunctor.map (U.toPrefunctor.map (adj₁.counit.app X))) (CategoryTheory.LiftAdjoint.otherMap R F' adj₁ adj₂ X))) Y) a))) (adj₁.counit.app (R.toPrefunctor.obj Y)), property := (_ : (fun (b : F.toPrefunctor.obj (U.toPrefunctor.obj X) ⟶ R.toPrefunctor.obj Y) => CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (U.toPrefunctor.map (adj₁.counit.app X))) b = CategoryTheory.CategoryStruct.comp (adj₁.counit.app (F.toPrefunctor.obj (U.toPrefunctor.obj X))) b) (CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((adj₂.homEquiv (U.toPrefunctor.obj X) Y) ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F'.toPrefunctor.map (U.toPrefunctor.map (adj₁.counit.app X))) (CategoryTheory.LiftAdjoint.otherMap R F' adj₁ adj₂ X))) Y) a))) (adj₁.counit.app (R.toPrefunctor.obj Y)))) }

@[simp]

theorem CategoryTheory.LiftAdjoint.constructLeftAdjointEquiv_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 B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B) (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ CategoryTheory.Functor.comp R U) [CategoryTheory.Limits.HasReflexiveCoequalizers A] [(X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)] (Y : A) (X : B) : ∀ (a : X ⟶ R.toPrefunctor.obj Y), (CategoryTheory.LiftAdjoint.constructLeftAdjointEquiv R F' adj₁ adj₂ Y X).symm a = (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F'.toPrefunctor.map (U.toPrefunctor.map (adj₁.counit.app X))) (CategoryTheory.LiftAdjoint.otherMap R F' adj₁ adj₂ X))) Y).symm { val := (adj₂.homEquiv (U.toPrefunctor.obj X) Y).symm (CategoryTheory.CategoryStruct.comp (adj₁.unit.app (U.toPrefunctor.obj X)) (U.toPrefunctor.map ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.LiftAdjoint.counitCoequalises adj₁ X) (R.toPrefunctor.obj Y)) a))), property := (_ : (fun (b : F'.toPrefunctor.obj (U.toPrefunctor.obj X) ⟶ Y) => CategoryTheory.CategoryStruct.comp (F'.toPrefunctor.map (U.toPrefunctor.map (adj₁.counit.app X))) b = CategoryTheory.CategoryStruct.comp (CategoryTheory.LiftAdjoint.otherMap R F' adj₁ adj₂ X) b) ((adj₂.homEquiv (U.toPrefunctor.obj X) Y).symm (CategoryTheory.CategoryStruct.comp (adj₁.unit.app (U.toPrefunctor.obj X)) (U.toPrefunctor.map ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.LiftAdjoint.counitCoequalises adj₁ X) (R.toPrefunctor.obj Y)) a))))) }

noncomputable def CategoryTheory.LiftAdjoint.constructLeftAdjointEquiv {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 B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B) (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ CategoryTheory.Functor.comp R U) [CategoryTheory.Limits.HasReflexiveCoequalizers A] [(X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)] (Y : A) (X : B) : (CategoryTheory.LiftAdjoint.constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) ≃ (X ⟶ R.toPrefunctor.obj Y)

The homset equivalence which helps show that R is a right adjoint.

Equations

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

noncomputable def CategoryTheory.LiftAdjoint.constructLeftAdjoint {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 B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B) (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ CategoryTheory.Functor.comp R U) [CategoryTheory.Limits.HasReflexiveCoequalizers A] [(X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)] : CategoryTheory.Functor B A

Construct the left adjoint to R, with object map constructLeftAdjointObj.

Equations

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

noncomputable def CategoryTheory.adjointTriangleLift {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 B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B) (adj₁ : F ⊣ U) [(X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)] [CategoryTheory.Limits.HasReflexiveCoequalizers A] [CategoryTheory.IsRightAdjoint (CategoryTheory.Functor.comp R U)] : CategoryTheory.IsRightAdjoint R

The adjoint triangle theorem: Suppose U : B ⥤ C has a left adjoint F such that each counit ε_X : FUX ⟶ X is a regular epimorphism. Then if a category A has coequalizers of reflexive pairs, then a functor R : A ⥤ B has a left adjoint if the composite R ⋙ U does.

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

Equations

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

noncomputable def CategoryTheory.monadicAdjointTriangleLift {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 B C) [CategoryTheory.MonadicRightAdjoint U] {R : CategoryTheory.Functor A B} [CategoryTheory.Limits.HasReflexiveCoequalizers A] [CategoryTheory.IsRightAdjoint (CategoryTheory.Functor.comp R U)] : CategoryTheory.IsRightAdjoint R

If R ⋙ U has a left adjoint, the domain of R has reflexive coequalizers and U is a monadic functor, then R has a left adjoint. This is a special case of adjointTriangleLift which is often more useful in practice.

Equations

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

noncomputable def CategoryTheory.adjointSquareLift {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) (R : CategoryTheory.Functor C D) (comm : CategoryTheory.Functor.comp U R ≅ CategoryTheory.Functor.comp Q V) [CategoryTheory.IsRightAdjoint U] [CategoryTheory.IsRightAdjoint V] [CategoryTheory.IsRightAdjoint R] [(X : B) → CategoryTheory.RegularEpi ((CategoryTheory.Adjunction.ofRightAdjoint V).counit.app X)] [CategoryTheory.Limits.HasReflexiveCoequalizers A] : CategoryTheory.IsRightAdjoint Q

Suppose we have a commutative square of functors

  Q
A → B

U ↓ ↓ V C → D R

where U has a left adjoint, A has reflexive coequalizers and V has a left adjoint such that each component of the counit is a regular epi. Then Q has a left adjoint if R has a left adjoint.

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

Equations

• CategoryTheory.adjointSquareLift Q V U R comm = CategoryTheory.adjointTriangleLift Q (CategoryTheory.Adjunction.ofRightAdjoint V)

noncomputable def CategoryTheory.monadicAdjointSquareLift {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) (R : CategoryTheory.Functor C D) (comm : CategoryTheory.Functor.comp U R ≅ CategoryTheory.Functor.comp Q V) [CategoryTheory.IsRightAdjoint U] [CategoryTheory.MonadicRightAdjoint V] [CategoryTheory.IsRightAdjoint R] [CategoryTheory.Limits.HasReflexiveCoequalizers A] : CategoryTheory.IsRightAdjoint Q

Suppose we have a commutative square of functors

  Q
A → B

U ↓ ↓ V C → D R

where U has a left adjoint, A has reflexive coequalizers and V is monadic. Then Q has a left adjoint if R has a left adjoint.

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

Equations

• CategoryTheory.monadicAdjointSquareLift Q V U R comm = CategoryTheory.monadicAdjointTriangleLift V