Adjoint lifting #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
- 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 a coequalizer for (FUε_X, ε_FUX), it suffices to assume it's always a
coequalizer of something (i.e. a regular epi).
Equations
- category_theory.lift_adjoint.counit_coequalises adj₁ X = category_theory.limits.cofork.is_colimit.mk' (category_theory.limits.cofork.of_π (adj₁.counit.app X) _) (λ (s : category_theory.limits.cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app (F.obj (U.obj X)))), ⟨(category_theory.regular_epi.desc' (adj₁.counit.app X) s.π _).val, _⟩)
(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
Instances for category_theory.lift_adjoint.other_map
(F'Uε_X, other_map X) is a reflexive pair: in particular if A has reflexive coequalizers then
it has a coequalizer.
Construct the object part of the desired left adjoint as the coequalizer of F'Uε_Y with
other_map.
Equations
- category_theory.lift_adjoint.construct_left_adjoint_obj R F' adj₁ adj₂ Y = category_theory.limits.coequalizer (F'.map (U.map (adj₁.counit.app Y))) (category_theory.lift_adjoint.other_map R F' adj₁ adj₂ Y)
The homset equivalence which helps show that R is a right adjoint.
Equations
- category_theory.lift_adjoint.construct_left_adjoint_equiv R F' adj₁ adj₂ Y X = (((category_theory.limits.cofork.is_colimit.hom_iso (category_theory.limits.colimit.is_colimit (category_theory.limits.parallel_pair (F'.map (U.map (adj₁.counit.app X))) (category_theory.lift_adjoint.other_map R F' adj₁ adj₂ X))) Y).trans ((adj₂.hom_equiv (U.obj X) Y).subtype_equiv _)).trans ((adj₁.hom_equiv (U.obj X) (R.obj Y)).symm.subtype_equiv _)).trans (category_theory.limits.cofork.is_colimit.hom_iso (category_theory.lift_adjoint.counit_coequalises adj₁ X) (R.obj Y)).symm
Construct the left adjoint to R, with object map construct_left_adjoint_obj.
Equations
- category_theory.lift_adjoint.construct_left_adjoint R F' adj₁ adj₂ = category_theory.adjunction.left_adjoint_of_equiv (λ (X : B) (Y : A), category_theory.lift_adjoint.construct_left_adjoint_equiv R F' adj₁ adj₂ Y 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
- category_theory.adjoint_triangle_lift R adj₁ = {left := category_theory.lift_adjoint.construct_left_adjoint R (category_theory.left_adjoint (R ⋙ U)) adj₁ (category_theory.adjunction.of_right_adjoint (R ⋙ U)) (λ (X : B), _inst_4 X), adj := category_theory.adjunction.adjunction_of_equiv_left (λ (X : B) (Y : A), category_theory.lift_adjoint.construct_left_adjoint_equiv R (category_theory.left_adjoint (R ⋙ U)) adj₁ (category_theory.adjunction.of_right_adjoint (R ⋙ U)) Y X) _}
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
- category_theory.monadic_adjoint_triangle_lift U = let R' : A ⥤ (category_theory.adjunction.of_right_adjoint U).to_monad.algebra := R ⋙ category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint U), this : category_theory.is_right_adjoint (R' ⋙ (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint U)).inv) := category_theory.adjunction.right_adjoint_of_comp, this_1 : R' ⋙ (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint U)).inv ≅ R := category_theory.iso_whisker_left R (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint U)).as_equivalence.unit_iso.symm ≪≫ R.right_unitor in category_theory.adjunction.right_adjoint_of_nat_iso this_1
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
- category_theory.adjoint_square_lift Q V U R comm = let this : category_theory.is_right_adjoint (Q ⋙ V) := category_theory.adjunction.right_adjoint_of_nat_iso comm in category_theory.adjoint_triangle_lift Q (category_theory.adjunction.of_right_adjoint 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.
See https://ncatlab.org/nlab/show/adjoint+lifting+theorem
Equations
- category_theory.monadic_adjoint_square_lift Q V U R comm = let this : category_theory.is_right_adjoint (Q ⋙ V) := category_theory.adjunction.right_adjoint_of_nat_iso comm in category_theory.monadic_adjoint_triangle_lift V