# mathlibdocumentation

This file gives two constructions for building left adjoints: the adjoint triangle theorem and the adjoint lifting theorem. The adjoint triangle theorem says that given 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: monadic_adjoint_triangle_lift, 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 #

def category_theory.lift_adjoint.counit_coequalises {B : Type u₂} {C : Type u₃} {U : B C} {F : C B} (adj₁ : F U) [Π (X : B), category_theory.regular_epi (adj₁.counit.app X)] (X : B) :

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
def category_theory.lift_adjoint.other_map {A : Type u₁} {B : Type u₂} {C : Type u₃} {U : B C} {F : C B} (R : A B) (F' : C A) (adj₁ : F U) (adj₂ : F' R 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
@[instance]
def category_theory.lift_adjoint.other_map.category_theory.is_reflexive_pair {A : Type u₁} {B : Type u₂} {C : Type u₃} {U : B C} {F : C B} (R : A B) (F' : C A) (adj₁ : F U) (adj₂ : F' R U) (X : B) :

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

def category_theory.lift_adjoint.construct_left_adjoint_obj {A : Type u₁} {B : Type u₂} {C : Type u₃} {U : B C} {F : C B} (R : A B) (F' : C A) (adj₁ : F U) (adj₂ : F' R U) (Y : B) :
A

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

Equations
def category_theory.lift_adjoint.construct_left_adjoint_equiv {A : Type u₁} {B : Type u₂} {C : Type u₃} {U : B C} {F : C B} (R : A B) (F' : C A) (adj₁ : F U) (adj₂ : F' R U) [Π (X : B), category_theory.regular_epi (adj₁.counit.app X)] (Y : A) (X : B) :
adj₂ X Y) (X R.obj Y)

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

Equations
@[simp]
theorem category_theory.lift_adjoint.construct_left_adjoint_equiv_symm_apply {A : Type u₁} {B : Type u₂} {C : Type u₃} {U : B C} {F : C B} (R : A B) (F' : C A) (adj₁ : F U) (adj₂ : F' R U) [Π (X : B), category_theory.regular_epi (adj₁.counit.app X)] (Y : A) (X : B) (ᾰ : X R.obj Y) :
@[simp]
theorem category_theory.lift_adjoint.construct_left_adjoint_equiv_apply {A : Type u₁} {B : Type u₂} {C : Type u₃} {U : B C} {F : C B} (R : A B) (F' : C A) (adj₁ : F U) (adj₂ : F' R U) [Π (X : B), category_theory.regular_epi (adj₁.counit.app X)] (Y : A) (X : B) (ᾰ : adj₂ X Y) :
def category_theory.lift_adjoint.construct_left_adjoint {A : Type u₁} {B : Type u₂} {C : Type u₃} {U : B C} {F : C B} (R : A B) (F' : C A) (adj₁ : F U) (adj₂ : F' R U) [Π (X : B), category_theory.regular_epi (adj₁.counit.app X)] :
B A

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

Equations
def category_theory.adjoint_triangle_lift {A : Type u₁} {B : Type u₂} {C : Type u₃} {U : B C} {F : C B} (R : A B) (adj₁ : F U) [Π (X : B), category_theory.regular_epi (adj₁.counit.app X)]  :

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
def category_theory.monadic_adjoint_triangle_lift {A : Type u₁} {B : Type u₂} {C : Type u₃} (U : B C) {R : A B}  :

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

Equations
def category_theory.adjoint_square_lift {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} (Q : A B) (V : B D) (U : A C) (R : C D) (comm : U R Q V) [Π (X : B), ]  :

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.

Equations
• comm =
def category_theory.monadic_adjoint_square_lift {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} (Q : A B) (V : B D) (U : A C) (R : C D) (comm : U R Q V)  :

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.

Equations
• comm =