Skip to content

Commit c6660d9

Browse files
int-y1mattrobballScott Morrison
committed
feat: port CategoryTheory.Adjunction.Lifting (#4414)
Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
1 parent 0726e5e commit c6660d9

File tree

2 files changed

+258
-0
lines changed

2 files changed

+258
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -819,6 +819,7 @@ import Mathlib.CategoryTheory.Adjunction.Basic
819819
import Mathlib.CategoryTheory.Adjunction.Comma
820820
import Mathlib.CategoryTheory.Adjunction.Evaluation
821821
import Mathlib.CategoryTheory.Adjunction.FullyFaithful
822+
import Mathlib.CategoryTheory.Adjunction.Lifting
822823
import Mathlib.CategoryTheory.Adjunction.Limits
823824
import Mathlib.CategoryTheory.Adjunction.Mates
824825
import Mathlib.CategoryTheory.Adjunction.Opposites

‎Mathlib/CategoryTheory/Adjunction/Lifting.lean‎

Lines changed: 257 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,257 @@
1+
/-
2+
Copyright (c) 2020 Bhavik Mehta. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Bhavik Mehta
5+
6+
! This file was ported from Lean 3 source module category_theory.adjunction.lifting
7+
! leanprover-community/mathlib commit 9bc7dfa6e50f902fb0684c9670a680459ebaed68
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
12+
import Mathlib.CategoryTheory.Limits.Shapes.Reflexive
13+
import Mathlib.CategoryTheory.Monad.Adjunction
14+
import Mathlib.CategoryTheory.Monad.Coequalizer
15+
16+
/-!
17+
# Adjoint lifting
18+
19+
This file gives two constructions for building left adjoints: the adjoint triangle theorem and the
20+
adjoint lifting theorem.
21+
The adjoint triangle theorem concerns a functor `U : B ⥤ C` with a left adjoint `F` such
22+
that `ε_X : FUX ⟶ X` is a regular epi. Then for any category `A` with coequalizers of reflexive
23+
pairs, a functor `R : A ⥤ B` has a left adjoint if (and only if) the composite `R ⋙ U` does.
24+
Note that the condition on `U` regarding `ε_X` is automatically satisfied in the case when `U` is
25+
a monadic functor, giving the corollary: `monadicAdjointTriangleLift`, i.e. if `U` is monadic,
26+
`A` has reflexive coequalizers then `R : A ⥤ B` has a left adjoint provided `R ⋙ U` does.
27+
28+
The adjoint lifting theorem says that given a commutative square of functors (up to isomorphism):
29+
30+
Q
31+
A → B
32+
U ↓ ↓ V
33+
C → D
34+
R
35+
36+
where `U` and `V` are monadic and `A` has reflexive coequalizers, then if `R` has a left adjoint
37+
then `Q` has a left adjoint.
38+
39+
## Implementation
40+
41+
It is more convenient to prove this theorem by assuming we are given the explicit adjunction rather
42+
than just a functor known to be a right adjoint. In docstrings, we write `(η, ε)` for the unit
43+
and counit of the adjunction `adj₁ : F ⊣ U` and `(ι, δ)` for the unit and counit of the adjunction
44+
`adj₂ : F' ⊣ R ⋙ U`.
45+
46+
## TODO
47+
48+
Dualise to lift right adjoints through comonads (by reversing 1-cells) and dualise to lift right
49+
adjoints through monads (by reversing 2-cells), and the combination.
50+
51+
## References
52+
* https://ncatlab.org/nlab/show/adjoint+triangle+theorem
53+
* https://ncatlab.org/nlab/show/adjoint+lifting+theorem
54+
* Adjoint Lifting Theorems for Categories of Algebras (PT Johnstone, 1975)
55+
* A unified approach to the lifting of adjoints (AJ Power, 1988)
56+
-/
57+
58+
59+
namespace CategoryTheory
60+
61+
open Category Limits
62+
63+
universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
64+
65+
variable {A : Type u₁} {B : Type u₂} {C : Type u₃}
66+
67+
variable [Category.{v₁} A] [Category.{v₂} B] [Category.{v₃} C]
68+
69+
-- Hide implementation details in this namespace
70+
namespace LiftAdjoint
71+
72+
variable {U : B ⥤ C} {F : C ⥤ B} (R : A ⥤ B) (F' : C ⥤ A)
73+
74+
variable (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R ⋙ U)
75+
76+
/-- To show that `ε_X` is a coequalizer for `(FUε_X, ε_FUX)`, it suffices to assume it's always a
77+
coequalizer of something (i.e. a regular epi).
78+
-/
79+
def counitCoequalises [∀ X : B, RegularEpi (adj₁.counit.app X)] (X : B) :
80+
IsColimit (Cofork.ofπ (adj₁.counit.app X) (adj₁.counit_naturality _)) :=
81+
Cofork.IsColimit.mk' _ fun s => by
82+
refine' ⟨(RegularEpi.desc' (adj₁.counit.app X) s.π _).1, _, _⟩
83+
· rw [← cancel_epi (adj₁.counit.app (RegularEpi.W (adj₁.counit.app X)))]
84+
rw [← adj₁.counit_naturality_assoc RegularEpi.left]
85+
dsimp only [Functor.comp_obj]
86+
rw [← s.condition, ← F.map_comp_assoc, ← U.map_comp, RegularEpi.w, U.map_comp,
87+
F.map_comp_assoc, s.condition, ← adj₁.counit_naturality_assoc RegularEpi.right]
88+
· apply (RegularEpi.desc' (adj₁.counit.app X) s.π _).2
89+
· intro m hm
90+
rw [← cancel_epi (adj₁.counit.app X)]
91+
apply hm.trans (RegularEpi.desc' (adj₁.counit.app X) s.π _).2.symm
92+
#align category_theory.lift_adjoint.counit_coequalises CategoryTheory.LiftAdjoint.counitCoequalises
93+
94+
/-- (Implementation)
95+
To construct the left adjoint, we use the coequalizer of `F' U ε_Y` with the composite
96+
97+
`F' U F U X ⟶ F' U F U R F U' X ⟶ F' U R F' U X ⟶ F' U X`
98+
99+
where the first morphism is `F' U F ι_UX`, the second is `F' U ε_RF'UX`, and the third is `δ_F'UX`.
100+
We will show that this coequalizer exists and that it forms the object map for a left adjoint to
101+
`R`.
102+
-/
103+
def otherMap (X) : F'.obj (U.obj (F.obj (U.obj X))) ⟶ F'.obj (U.obj X) :=
104+
F'.map (U.map (F.map (adj₂.unit.app _) ≫ adj₁.counit.app _)) ≫ adj₂.counit.app _
105+
#align category_theory.lift_adjoint.other_map CategoryTheory.LiftAdjoint.otherMap
106+
107+
/-- `(F'Uε_X, otherMap X)` is a reflexive pair: in particular if `A` has reflexive coequalizers then
108+
it has a coequalizer.
109+
-/
110+
instance (X : B) :
111+
IsReflexivePair (F'.map (U.map (adj₁.counit.app X))) (otherMap _ _ adj₁ adj₂ X) :=
112+
IsReflexivePair.mk' (F'.map (adj₁.unit.app (U.obj X)))
113+
(by
114+
rw [← F'.map_comp, adj₁.right_triangle_components]
115+
apply F'.map_id)
116+
(by
117+
dsimp [otherMap]
118+
rw [← F'.map_comp_assoc, U.map_comp, adj₁.unit_naturality_assoc,
119+
adj₁.right_triangle_components, comp_id, adj₂.left_triangle_components])
120+
121+
variable [HasReflexiveCoequalizers A]
122+
123+
/-- Construct the object part of the desired left adjoint as the coequalizer of `F'Uε_Y` with
124+
`otherMap`.
125+
-/
126+
noncomputable def constructLeftAdjointObj (Y : B) : A :=
127+
coequalizer (F'.map (U.map (adj₁.counit.app Y))) (otherMap _ _ adj₁ adj₂ Y)
128+
#align category_theory.lift_adjoint.construct_left_adjoint_obj CategoryTheory.LiftAdjoint.constructLeftAdjointObj
129+
130+
/-- The homset equivalence which helps show that `R` is a right adjoint. -/
131+
@[simps!] -- Porting note: Originally `@[simps (config := { rhsMd := semireducible })]`
132+
noncomputable def constructLeftAdjointEquiv [∀ X : B, RegularEpi (adj₁.counit.app X)] (Y : A)
133+
(X : B) : (constructLeftAdjointObj _ _ adj₁ adj₂ X ⟶ Y) ≃ (X ⟶ R.obj Y) :=
134+
calc
135+
(constructLeftAdjointObj _ _ adj₁ adj₂ X ⟶ Y) ≃
136+
{ f : F'.obj (U.obj X) ⟶ Y //
137+
F'.map (U.map (adj₁.counit.app X)) ≫ f = otherMap _ _ adj₁ adj₂ _ ≫ f } :=
138+
Cofork.IsColimit.homIso (colimit.isColimit _) _
139+
_ ≃ { g : U.obj X ⟶ U.obj (R.obj Y) //
140+
U.map (F.map g ≫ adj₁.counit.app _) = U.map (adj₁.counit.app _) ≫ g } := by
141+
apply (adj₂.homEquiv _ _).subtypeEquiv _
142+
intro f
143+
rw [← (adj₂.homEquiv _ _).injective.eq_iff, eq_comm, adj₂.homEquiv_naturality_left,
144+
otherMap, assoc, adj₂.homEquiv_naturality_left, ← adj₂.counit_naturality,
145+
adj₂.homEquiv_naturality_left, adj₂.homEquiv_unit, adj₂.right_triangle_components,
146+
comp_id, Functor.comp_map, ← U.map_comp, assoc, ← adj₁.counit_naturality,
147+
adj₂.homEquiv_unit, adj₂.homEquiv_unit, F.map_comp, assoc]
148+
rfl
149+
_ ≃ { z : F.obj (U.obj X) ⟶ R.obj Y // _ } := by
150+
apply (adj₁.homEquiv _ _).symm.subtypeEquiv
151+
intro g
152+
rw [← (adj₁.homEquiv _ _).symm.injective.eq_iff, adj₁.homEquiv_counit,
153+
adj₁.homEquiv_counit, adj₁.homEquiv_counit, F.map_comp, assoc, U.map_comp, F.map_comp,
154+
assoc, adj₁.counit_naturality, adj₁.counit_naturality_assoc]
155+
apply eq_comm
156+
_ ≃ (X ⟶ R.obj Y) := (Cofork.IsColimit.homIso (counitCoequalises adj₁ X) _).symm
157+
#align category_theory.lift_adjoint.construct_left_adjoint_equiv CategoryTheory.LiftAdjoint.constructLeftAdjointEquiv
158+
159+
/-- Construct the left adjoint to `R`, with object map `constructLeftAdjointObj`. -/
160+
noncomputable def constructLeftAdjoint [∀ X : B, RegularEpi (adj₁.counit.app X)] : B ⥤ A := by
161+
refine' Adjunction.leftAdjointOfEquiv (fun X Y => constructLeftAdjointEquiv R _ adj₁ adj₂ Y X) _
162+
intro X Y Y' g h
163+
rw [constructLeftAdjointEquiv_apply, constructLeftAdjointEquiv_apply,
164+
Equiv.symm_apply_eq, Subtype.ext_iff]
165+
dsimp
166+
rw [Cofork.IsColimit.homIso_natural, Cofork.IsColimit.homIso_natural]
167+
erw [adj₂.homEquiv_naturality_right]
168+
simp_rw [Functor.comp_map]
169+
simp
170+
#align category_theory.lift_adjoint.construct_left_adjoint CategoryTheory.LiftAdjoint.constructLeftAdjoint
171+
172+
end LiftAdjoint
173+
174+
/-- The adjoint triangle theorem: Suppose `U : B ⥤ C` has a left adjoint `F` such that each counit
175+
`ε_X : FUX ⟶ X` is a regular epimorphism. Then if a category `A` has coequalizers of reflexive
176+
pairs, then a functor `R : A ⥤ B` has a left adjoint if the composite `R ⋙ U` does.
177+
178+
Note the converse is true (with weaker assumptions), by `Adjunction.comp`.
179+
See https://ncatlab.org/nlab/show/adjoint+triangle+theorem
180+
-/
181+
noncomputable def adjointTriangleLift {U : B ⥤ C} {F : C ⥤ B} (R : A ⥤ B) (adj₁ : F ⊣ U)
182+
[∀ X : B, RegularEpi (adj₁.counit.app X)] [HasReflexiveCoequalizers A]
183+
[IsRightAdjoint (R ⋙ U)] : IsRightAdjoint R where
184+
left := LiftAdjoint.constructLeftAdjoint R _ adj₁ (Adjunction.ofRightAdjoint _)
185+
adj := Adjunction.adjunctionOfEquivLeft _ _
186+
#align category_theory.adjoint_triangle_lift CategoryTheory.adjointTriangleLift
187+
188+
/-- If `R ⋙ U` has a left adjoint, the domain of `R` has reflexive coequalizers and `U` is a monadic
189+
functor, then `R` has a left adjoint.
190+
This is a special case of `adjointTriangleLift` which is often more useful in practice.
191+
-/
192+
noncomputable def monadicAdjointTriangleLift (U : B ⥤ C) [MonadicRightAdjoint U] {R : A ⥤ B}
193+
[HasReflexiveCoequalizers A] [IsRightAdjoint (R ⋙ U)] : IsRightAdjoint R := by
194+
let R' : A ⥤ _ := R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
195+
rsuffices : IsRightAdjoint R'
196+
· let this : IsRightAdjoint (R' ⋙ (Monad.comparison (Adjunction.ofRightAdjoint U)).inv) := by
197+
infer_instance
198+
· let this : R' ⋙ (Monad.comparison (Adjunction.ofRightAdjoint U)).inv ≅ R :=
199+
(isoWhiskerLeft R (Monad.comparison _).asEquivalence.unitIso.symm : _) ≪≫ R.rightUnitor
200+
exact Adjunction.rightAdjointOfNatIso this
201+
let this : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.ofRightAdjoint U).toMonad) :=
202+
Adjunction.rightAdjointOfNatIso
203+
(isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm : _)
204+
let this : ∀ X, RegularEpi ((Monad.adj (Adjunction.ofRightAdjoint U).toMonad).counit.app X) := by
205+
intro X
206+
simp only [Monad.adj_counit]
207+
exact ⟨_, _, _, _, Monad.beckAlgebraCoequalizer X⟩
208+
exact adjointTriangleLift R' (Monad.adj _)
209+
#align category_theory.monadic_adjoint_triangle_lift CategoryTheory.monadicAdjointTriangleLift
210+
211+
variable {D : Type u₄}
212+
213+
variable [Category.{v₄} D]
214+
215+
/-- Suppose we have a commutative square of functors
216+
217+
Q
218+
A → B
219+
U ↓ ↓ V
220+
C → D
221+
R
222+
223+
where `U` has a left adjoint, `A` has reflexive coequalizers and `V` has a left adjoint such that
224+
each component of the counit is a regular epi.
225+
Then `Q` has a left adjoint if `R` has a left adjoint.
226+
227+
See https://ncatlab.org/nlab/show/adjoint+lifting+theorem
228+
-/
229+
noncomputable def adjointSquareLift (Q : A ⥤ B) (V : B ⥤ D) (U : A ⥤ C) (R : C ⥤ D)
230+
(comm : U ⋙ R ≅ Q ⋙ V) [IsRightAdjoint U] [IsRightAdjoint V] [IsRightAdjoint R]
231+
[∀ X, RegularEpi ((Adjunction.ofRightAdjoint V).counit.app X)] [HasReflexiveCoequalizers A] :
232+
IsRightAdjoint Q :=
233+
letI := Adjunction.rightAdjointOfNatIso comm
234+
adjointTriangleLift Q (Adjunction.ofRightAdjoint V)
235+
#align category_theory.adjoint_square_lift CategoryTheory.adjointSquareLift
236+
237+
/-- Suppose we have a commutative square of functors
238+
239+
Q
240+
A → B
241+
U ↓ ↓ V
242+
C → D
243+
R
244+
245+
where `U` has a left adjoint, `A` has reflexive coequalizers and `V` is monadic.
246+
Then `Q` has a left adjoint if `R` has a left adjoint.
247+
248+
See https://ncatlab.org/nlab/show/adjoint+lifting+theorem
249+
-/
250+
noncomputable def monadicAdjointSquareLift (Q : A ⥤ B) (V : B ⥤ D) (U : A ⥤ C) (R : C ⥤ D)
251+
(comm : U ⋙ R ≅ Q ⋙ V) [IsRightAdjoint U] [MonadicRightAdjoint V] [IsRightAdjoint R]
252+
[HasReflexiveCoequalizers A] : IsRightAdjoint Q :=
253+
letI := Adjunction.rightAdjointOfNatIso comm
254+
monadicAdjointTriangleLift V
255+
#align category_theory.monadic_adjoint_square_lift CategoryTheory.monadicAdjointSquareLift
256+
257+
end CategoryTheory

0 commit comments

Comments
 (0)