Documentation

Mathlib.CategoryTheory.Adjunction.Lifting.Right

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 #

References #

source
def CategoryTheory.LiftRightAdjoint.unitEqualizes {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) (h : (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.
Instances For
    source
    @[reducible, inline, deprecated CategoryTheory.LiftRightAdjoint.unitEqualizes (since := "2026-10-05")]
    abbrev 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) (h : (X : B) → RegularMono (adj₁.unit.app X)) (X : B) :
    Limits.IsLimit (Limits.Fork.ofι (adj₁.unit.app X) ⋯)

    Deprecated alias for unitEqualizes.

    Equations
    Instances For
      source
      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.
      Instances For
        source
        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.

        source
        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.
        Instances For
          source
          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] (h : (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.
          Instances For
            source
            @[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] (h : (X : B) → RegularMono (adj₁.unit.app X)) (Y : C) (X : B) (a✝ : L.obj Y ⟶ X) :
            (constructRightAdjointEquiv L U' adj₁ adj₂ h 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 (unitEqualizes adj₁ h X) (L.obj Y)) a✝)), ⋯⟩
            source
            @[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] (h : (X : B) → RegularMono (adj₁.unit.app X)) (Y : C) (X : B) (a✝ : Y ⟶ constructRightAdjointObj L U' adj₁ adj₂ X) :
            (constructRightAdjointEquiv L U' adj₁ adj₂ h Y X) a✝ = (Limits.Fork.IsLimit.homIso (unitEqualizes adj₁ h 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✝)), ⋯⟩
            source
            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] (h : (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.
            Instances For
              source
              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) (h : (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

              source
              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.

              source
              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] (h : (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
      L

              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

              source
              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
      L

              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