Documentation

Mathlib.CategoryTheory.Adjunction.Lifting.Left

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: isRightAdjoint_triangle_lift_monadic, 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 V is monadic, U has a left adjoint, 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.

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

TODO #

References #

source
def CategoryTheory.LiftLeftAdjoint.counitCoequalizes {B : Type u₂} {C : Type u₃} [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor B C} {F : Functor C B} (adj₁ : F ⊣ U) (h : (X : B) → RegularEpi (adj₁.counit.app X)) (X : B) :
Limits.IsColimit (Limits.Cofork.ofπ (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.
Instances For
    source
    @[reducible, inline, deprecated CategoryTheory.LiftLeftAdjoint.counitCoequalizes (since := "2026-10-05")]
    abbrev CategoryTheory.LiftLeftAdjoint.counitCoequalises {B : Type u₂} {C : Type u₃} [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor B C} {F : Functor C B} (adj₁ : F ⊣ U) (h : (X : B) → RegularEpi (adj₁.counit.app X)) (X : B) :
    Limits.IsColimit (Limits.Cofork.ofπ (adj₁.counit.app X) ⋯)

    Deprecated alias for counitCoequalizes.

    Equations
    Instances For
      source
      def CategoryTheory.LiftLeftAdjoint.otherMap {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor B C} {F : Functor C B} (R : Functor A B) (F' : Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U) (X : B) :
      F'.obj (U.obj (F.obj (U.obj X))) ⟶ F'.obj (U.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.
      Instances For
        source
        instance CategoryTheory.LiftLeftAdjoint.instIsReflexivePairMapAppCounitOtherMap {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor B C} {F : Functor C B} (R : Functor A B) (F' : Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U) (X : B) :
        IsReflexivePair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)

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

        source
        noncomputable def CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor B C} {F : Functor C B} (R : Functor A B) (F' : Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U) [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.
        Instances For
          source
          noncomputable def CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor B C} {F : Functor C B} (R : Functor A B) (F' : Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U) [Limits.HasReflexiveCoequalizers A] (h : (X : B) → RegularEpi (adj₁.counit.app X)) (Y : A) (X : B) :
          (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) ≃ (X ⟶ R.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.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor B C} {F : Functor C B} (R : Functor A B) (F' : Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U) [Limits.HasReflexiveCoequalizers A] (h : (X : B) → RegularEpi (adj₁.counit.app X)) (Y : A) (X : B) (a✝ : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) :
            (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X) a✝ = (Limits.Cofork.IsColimit.homIso (counitCoequalizes adj₁ h X) (R.obj Y)).symm ⟨(adj₁.homEquiv (U.obj X) (R.obj Y)).symm ((adj₂.homEquiv (U.obj X) Y) ↑((Limits.Cofork.IsColimit.homIso (Limits.colimit.isColimit (Limits.parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X))) Y) a✝)), ⋯⟩
            source
            @[simp]
            theorem CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_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 B C} {F : Functor C B} (R : Functor A B) (F' : Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U) [Limits.HasReflexiveCoequalizers A] (h : (X : B) → RegularEpi (adj₁.counit.app X)) (Y : A) (X : B) (a✝ : X ⟶ R.obj Y) :
            (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X).symm a✝ = (Limits.Cofork.IsColimit.homIso (Limits.colimit.isColimit (Limits.parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X))) Y).symm ⟨(adj₂.homEquiv (U.obj X) Y).symm ((adj₁.homEquiv (U.obj X) (R.obj Y)) ↑((Limits.Cofork.IsColimit.homIso (counitCoequalizes adj₁ h X) (R.obj Y)) a✝)), ⋯⟩
            source
            noncomputable def CategoryTheory.LiftLeftAdjoint.constructLeftAdjoint {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {U : Functor B C} {F : Functor C B} (R : Functor A B) (F' : Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U) [Limits.HasReflexiveCoequalizers A] (h : (X : B) → RegularEpi (adj₁.counit.app X)) :
            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.
            Instances For
              source
              theorem CategoryTheory.isRightAdjoint_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 B C} {F : Functor C B} (R : Functor A B) (adj₁ : F ⊣ U) (h : (X : B) → RegularEpi (adj₁.counit.app X)) [Limits.HasReflexiveCoequalizers A] [(R.comp U).IsRightAdjoint] :
              R.IsRightAdjoint

              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

              source
              theorem CategoryTheory.isRightAdjoint_triangle_lift_monadic {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (U : Functor B C) [MonadicRightAdjoint U] {R : Functor A B} [Limits.HasReflexiveCoequalizers A] [(R.comp U).IsRightAdjoint] :
              R.IsRightAdjoint

              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 isRightAdjoint_triangle_lift which is often more useful in practice.

              source
              theorem CategoryTheory.isRightAdjoint_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) (R : Functor C D) (comm : U.comp R ≅ Q.comp V) [U.IsRightAdjoint] [V.IsRightAdjoint] [R.IsRightAdjoint] (h : (X : B) → RegularEpi ((Adjunction.ofIsRightAdjoint V).counit.app X)) [Limits.HasReflexiveCoequalizers A] :
              Q.IsRightAdjoint

              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

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

              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