Skip to content

Commit af84080

Browse files
joelrioujoelriou
committed
feat(CategoryTheory/Localization): generalize results about adjunctions (#26365)
In this PR, results about adjunctions, localization of categories and calculus of fractions are slightly generalized. In particular, we show that under certain circumstances, adjoint functors are localization functors. (This shall be used in the proof of the fundamental lemma of homotopical algebra #26303.) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
1 parent 4c1fedd commit af84080

File tree

2 files changed

+109
-25
lines changed

2 files changed

+109
-25
lines changed

‎Mathlib/CategoryTheory/Localization/CalculusOfFractions/OfAdjunction.lean‎

Lines changed: 90 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,14 @@ import Mathlib.CategoryTheory.Localization.CalculusOfFractions
1010
/-!
1111
# The calculus of fractions deduced from an adjunction
1212
13-
If `G ⊣ F` is an adjunction, and `F` is fully faithful,
14-
then there is a left calculus of fractions for
15-
the inverse image by `G` of the class of isomorphisms.
13+
If `G ⊣ F` is an adjunction, `F` is fully faithful,
14+
and `W` is a class of morphisms that is inverted by `G`
15+
and such that the morphism `adj.unit.app X` belongs to `W`
16+
for any object `X`, then `G` is a localization functor
17+
with respect to `W`. Moreover, if `W` is multiplicative,
18+
then `W` has a calculus of left fractions. This
19+
holds in particular if `W` is the inverse image of
20+
the class of isomorphisms by `G`.
1621
1722
(The dual statement is also obtained.)
1823
@@ -25,36 +30,97 @@ open MorphismProperty
2530
namespace Adjunction
2631

2732
variable {C₁ C₂ : Type*} [Category C₁] [Category C₂]
28-
{G : C₁ ⥤ C₂} {F : C₂ ⥤ C₁} [F.Full] [F.Faithful]
33+
{G : C₁ ⥤ C₂} {F : C₂ ⥤ C₁}
2934

30-
lemma hasLeftCalculusOfFractions (adj : G ⊣ F) :
31-
((isomorphisms C₂).inverseImage G).HasLeftCalculusOfFractions where
35+
lemma hasLeftCalculusOfFractions (adj : G ⊣ F) (W : MorphismProperty C₁)
36+
[W.IsMultiplicative] (hW : W.IsInvertedBy G) (hW' : (W.functorCategory C₁) adj.unit) :
37+
W.HasLeftCalculusOfFractions where
3238
exists_leftFraction X Y φ := by
33-
obtain ⟨W, s, _, f, rfl⟩ := φ.cases
34-
have : IsIso (G.map s) := by assumption
39+
obtain ⟨T, s, _, f, rfl⟩ := φ.cases
40+
dsimp
41+
have := hW s (by assumption)
3542
exact ⟨{
3643
f := adj.unit.app X ≫ F.map (inv (G.map s)) ≫ F.map (G.map f)
3744
s := adj.unit.app Y
38-
hs := by
39-
simp only [inverseImage_iff, isomorphisms.iff]
40-
infer_instance }, by
45+
hs := hW' Y}, by
4146
have := adj.unit.naturality s
4247
dsimp at this ⊢
4348
rw [reassoc_of% this, Functor.map_inv, IsIso.hom_inv_id_assoc, adj.unit_naturality]⟩
4449
ext X' X Y f₁ f₂ s _ h := by
45-
have : IsIso (G.map s) := by assumption
46-
refine ⟨_, adj.unit.app Y, ?_, ?_⟩
47-
· simp only [inverseImage_iff, isomorphisms.iff]
48-
infer_instance
49-
· rw [← adj.unit_naturality f₁, ← adj.unit_naturality f₂]
50-
congr 2
51-
rw [← cancel_epi (G.map s), ← G.map_comp, ← G.map_comp, h]
52-
53-
lemma hasRightCalculusOfFractions (adj : F ⊣ G) :
54-
((isomorphisms C₂).inverseImage G).HasRightCalculusOfFractions := by
55-
suffices ((isomorphisms C₂).inverseImage G).op.HasLeftCalculusOfFractions from
56-
inferInstanceAs ((isomorphisms C₂).inverseImage G).op.unop.HasRightCalculusOfFractions
57-
simpa only [← isomorphisms_op] using adj.op.hasLeftCalculusOfFractions
50+
have := hW s (by assumption)
51+
refine ⟨_, adj.unit.app Y, hW' _, ?_⟩
52+
rw [← adj.unit_naturality f₁, ← adj.unit_naturality f₂]
53+
congr 2
54+
rw [← cancel_epi (G.map s), ← G.map_comp, ← G.map_comp, h]
55+
56+
lemma hasRightCalculusOfFractions (adj : F ⊣ G) (W : MorphismProperty C₁)
57+
[W.IsMultiplicative] (hW : W.IsInvertedBy G) (hW' : (W.functorCategory _) adj.counit) :
58+
W.HasRightCalculusOfFractions :=
59+
have := hasLeftCalculusOfFractions adj.op W.op hW.op (fun _ ↦ hW' _)
60+
inferInstanceAs W.op.unop.HasRightCalculusOfFractions
61+
62+
section
63+
64+
variable [F.Full] [F.Faithful]
65+
66+
lemma isLocalization_leftAdjoint
67+
(adj : G ⊣ F) (W : MorphismProperty C₁)
68+
(hW : W.IsInvertedBy G) (hW' : (W.functorCategory C₁) adj.unit) :
69+
G.IsLocalization W := by
70+
let Φ : W.Localization ⥤ C₂ := Localization.lift _ hW W.Q
71+
let e : W.Q ⋙ Φ ≅ G := by apply Localization.fac
72+
have : IsIso (Functor.whiskerRight adj.unit W.Q) := by
73+
rw [NatTrans.isIso_iff_isIso_app]
74+
intro X
75+
exact Localization.inverts W.Q W _ (hW' X)
76+
have : Localization.Lifting W.Q W (G ⋙ F ⋙ W.Q) (Φ ⋙ F ⋙ W.Q) :=
77+
⟨(Functor.associator _ _ _).symm ≪≫ Functor.isoWhiskerRight e _⟩
78+
exact Functor.IsLocalization.of_equivalence_target W.Q W _
79+
(Equivalence.mk Φ (F ⋙ W.Q)
80+
(Localization.liftNatIso W.Q W W.Q (G ⋙ F ⋙ W.Q) _ _
81+
(W.Q.leftUnitor.symm ≪≫ asIso (Functor.whiskerRight adj.unit W.Q) ≪≫
82+
Functor.associator _ _ _))
83+
(Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft _ e ≪≫ asIso adj.counit)) e
84+
85+
lemma isLocalization_rightAdjoint
86+
(adj : F ⊣ G) (W : MorphismProperty C₁)
87+
(hW : W.IsInvertedBy G) (hW' : (W.functorCategory C₁) adj.counit) :
88+
G.IsLocalization W := by
89+
simpa using isLocalization_leftAdjoint adj.op W.op hW.op (fun X ↦ hW' X.unop)
90+
91+
lemma functorCategory_inverseImage_isomorphisms_unit (adj : G ⊣ F) :
92+
((isomorphisms C₂).inverseImage G).functorCategory C₁ adj.unit := by
93+
intro
94+
simp only [Functor.id_obj, Functor.comp_obj, inverseImage_iff, isomorphisms.iff]
95+
infer_instance
96+
97+
lemma functorCategory_inverseImage_isomorphisms_counit (adj : F ⊣ G) :
98+
((isomorphisms C₂).inverseImage G).functorCategory C₁ adj.counit := by
99+
intro
100+
simp only [Functor.id_obj, Functor.comp_obj, inverseImage_iff, isomorphisms.iff]
101+
infer_instance
102+
103+
lemma isLocalization_leftAdjoint' (adj : G ⊣ F) :
104+
G.IsLocalization ((isomorphisms C₂).inverseImage G) :=
105+
adj.isLocalization_leftAdjoint _ (fun _ _ _ h ↦ h)
106+
adj.functorCategory_inverseImage_isomorphisms_unit
107+
108+
lemma isLocalization_rightAdjoint' (adj : F ⊣ G) :
109+
G.IsLocalization ((isomorphisms C₂).inverseImage G) :=
110+
adj.isLocalization_rightAdjoint _ (fun _ _ _ h ↦ h)
111+
adj.functorCategory_inverseImage_isomorphisms_counit
112+
113+
lemma hasLeftCalculusOfFractions' (adj : G ⊣ F) :
114+
((isomorphisms C₂).inverseImage G).HasLeftCalculusOfFractions :=
115+
hasLeftCalculusOfFractions adj _ (fun _ _ _ h ↦ h)
116+
adj.functorCategory_inverseImage_isomorphisms_unit
117+
118+
lemma hasRightCalculusOfFractions' (adj : F ⊣ G) :
119+
((isomorphisms C₂).inverseImage G).HasRightCalculusOfFractions :=
120+
hasRightCalculusOfFractions adj _ (fun _ _ _ h ↦ h)
121+
adj.functorCategory_inverseImage_isomorphisms_counit
122+
123+
end
58124

59125
end Adjunction
60126

‎Mathlib/CategoryTheory/Localization/Opposite.lean‎

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2022 Joël Riou. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Joël Riou
55
-/
6-
import Mathlib.CategoryTheory.Localization.Predicate
6+
import Mathlib.CategoryTheory.Localization.Equivalence
77

88
/-!
99
@@ -55,6 +55,24 @@ instance IsLocalization.op : L.op.IsLocalization W.op :=
5555
IsLocalization.of_equivalence_target W.Q.op W.op L.op (Localization.equivalenceFromModel L W).op
5656
(NatIso.op (Localization.qCompEquivalenceFromModelFunctorIso L W).symm)
5757

58+
instance IsLocalization.unop (L : Cᵒᵖ ⥤ Dᵒᵖ) (W : MorphismProperty Cᵒᵖ)
59+
[L.IsLocalization W] : L.unop.IsLocalization W.unop :=
60+
have : CatCommSq (opOpEquivalence C).functor L.op L.unop
61+
(opOpEquivalence D).functor := ⟨Iso.refl _⟩
62+
of_equivalences L.op W.op L.unop W.unop
63+
(opOpEquivalence C) (opOpEquivalence D)
64+
(fun _ _ _ hf ↦ MorphismProperty.le_isoClosure _ _ hf)
65+
(fun _ _ _ hf ↦ by
66+
have := Localization.inverts L W _ hf
67+
dsimp
68+
infer_instance)
69+
70+
@[simp]
71+
lemma op_iff (L : C ⥤ D) (W : MorphismProperty C) :
72+
L.op.IsLocalization W.op ↔ L.IsLocalization W :=
73+
⟨fun _ ↦ inferInstanceAs (L.op.unop.IsLocalization W.op.unop),
74+
fun _ ↦ inferInstance⟩
75+
5876
end Functor
5977

6078
namespace Localization

0 commit comments

Comments
 (0)