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 #
- 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
commisIso.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)
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
Instances For
(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
Instances For
(U'Fη_X, otherMap X) is a coreflexive pair: in particular if C has coreflexive equalizers
then this pair has an equalizer.
Construct the object part of the desired right adjoint as the equalizer of U'Fη_Y with
otherMap.
Equations
Instances For
The homset equivalence which helps show that L is a left adjoint.
Equations
Instances For
Construct the right adjoint to L, with object map constructRightAdjointObj.
Equations
Instances For
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
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.
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
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