Skip to content

Commit 25e35a4

Browse files
joelrioujoelriou
committed
feat(Algebra/Homology): the bounded below derived category (#40944)
In this PR, we show that the bounded below derived category is the localization of the bounded below homotopy category with respect to quasi-isomorphisms.
1 parent b8ddb25 commit 25e35a4

6 files changed

Lines changed: 305 additions & 3 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -589,6 +589,7 @@ public import Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
589589
public import Mathlib.Algebra.Homology.DerivedCategory.KInjective
590590
public import Mathlib.Algebra.Homology.DerivedCategory.KProjective
591591
public import Mathlib.Algebra.Homology.DerivedCategory.Linear
592+
public import Mathlib.Algebra.Homology.DerivedCategory.Plus
592593
public import Mathlib.Algebra.Homology.DerivedCategory.ShortExact
593594
public import Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
594595
public import Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom

‎Mathlib/Algebra/Homology/DerivedCategory/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -237,7 +237,7 @@ their compatibilities with shifts. -/
237237
def singleFunctors : SingleFunctors C (DerivedCategory C) ℤ :=
238238
(HomotopyCategory.singleFunctors C).postcomp Qh
239239

240-
/-- The shift functor `C ⥤ DerivedCategory C` which sends `X : C` to the
240+
/-- The single functor `C ⥤ DerivedCategory C` which sends `X : C` to the
241241
single cochain complex with `X` sitting in degree `n : ℤ`. -/
242242
abbrev singleFunctor (n : ℤ) := (singleFunctors C).functor n
243243

‎Mathlib/Algebra/Homology/DerivedCategory/HomologySequence.lean‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,22 @@ lemma isIso_Qh_map_iff {X Y : HomotopyCategory C (ComplexShape.up ℤ)} (f : X
8585
infer_instance
8686
· exact Localization.inverts Qh (HomotopyCategory.quasiIso _ _) _
8787

88+
lemma isIso_iff {K L : DerivedCategory C} (f : K ⟶ L) :
89+
IsIso f ↔ ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f) := by
90+
refine ⟨fun hf n ↦ inferInstance, fun hf ↦ ?_⟩
91+
refine ((MorphismProperty.isomorphisms (DerivedCategory C)).arrow_iso_iff
92+
(Qh.mapArrow.objObjPreimageIso (Arrow.mk f))).1 ?_
93+
let g := Qh.mapArrow.objPreimage (Arrow.mk f)
94+
change IsIso (Qh.map g.hom)
95+
rw [isIso_Qh_map_iff, HomotopyCategory.mem_quasiIso_iff]
96+
intro n
97+
have e : Arrow.mk ((homologyFunctor C n).map f) ≅
98+
Arrow.mk ((HomotopyCategory.homologyFunctor _ _ n).map g.hom) :=
99+
((homologyFunctor C n).mapArrow.mapIso
100+
((Qh.mapArrow.objObjPreimageIso (Arrow.mk f)).symm)) ≪≫
101+
((Functor.mapArrowFunctor _ _).mapIso (homologyFunctorFactorsh C n)).app (Arrow.mk g.hom)
102+
exact ((MorphismProperty.isomorphisms C).arrow_iso_iff e).1 (hf n)
103+
88104
instance (n : ℤ) : (homologyFunctor C n).IsHomological :=
89105
Functor.isHomological_of_localization Qh
90106
(homologyFunctor C n) _ (homologyFunctorFactorsh C n)

‎Mathlib/Algebra/Homology/DerivedCategory/Plus.lean‎

Lines changed: 228 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,228 @@
1+
/-
2+
Copyright (c) 2026 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
module
7+
8+
public import Mathlib.Algebra.Homology.DerivedCategory.KInjective
9+
public import Mathlib.Algebra.Homology.DerivedCategory.TStructure
10+
public import Mathlib.Algebra.Homology.HomotopyCategory.Plus
11+
public import Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
12+
public import Mathlib.CategoryTheory.Triangulated.TStructure.Induced
13+
14+
/-!
15+
# The bounded below derived category
16+
17+
Let `C` be an abelian category. In this file, we show that
18+
the bounded below derived category `DerivedCategory.Plus C` (defined
19+
as a full subcategory of `DerivedCategory C`) is the localization
20+
of the bounded below homotopy category `HomotopyCategory.Plus C`
21+
with respect to quasi-isomorphisms.
22+
23+
-/
24+
25+
@[expose] public section
26+
27+
open CategoryTheory Category Triangulated Limits
28+
29+
variable {C : Type*} [Category* C] [Abelian C]
30+
31+
namespace HomotopyCategory.Plus
32+
33+
variable (C)
34+
35+
/-- The property of objects in `HomotopyCategory.Plus C` that is satisfied
36+
by acyclic complexes. -/
37+
abbrev subcategoryAcyclic :
38+
ObjectProperty (HomotopyCategory.Plus C) :=
39+
(HomotopyCategory.subcategoryAcyclic C).inverseImage (HomotopyCategory.Plus.ι C)
40+
41+
set_option backward.defeqAttrib.useBackward true in
42+
lemma quasiIso_eq_subcategoryAcyclic_trW :
43+
HomotopyCategory.Plus.quasiIso C = (subcategoryAcyclic C).trW := by
44+
ext K L f
45+
obtain ⟨M, g, h, mem⟩ := CategoryTheory.Pretriangulated.distinguished_cocone_triangle f
46+
have := (HomotopyCategory.subcategoryAcyclic C).trW_iff_of_distinguished _
47+
((HomotopyCategory.Plus.ι C).map_distinguished _ mem)
48+
rw [← HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic] at this
49+
rwa [dsimp% (subcategoryAcyclic C).trW_iff_of_distinguished _ mem]
50+
51+
end HomotopyCategory.Plus
52+
53+
namespace DerivedCategory
54+
55+
open TStructure
56+
57+
variable [HasDerivedCategory C]
58+
59+
namespace Plus
60+
61+
/-- The localization functor `HomotopyCategory.Plus C ⥤ DerivedCategory.Plus C`. -/
62+
noncomputable def Qh : HomotopyCategory.Plus C ⥤ Plus C :=
63+
t.plus.lift (HomotopyCategory.Plus.ι _ ⋙ DerivedCategory.Qh) (by
64+
rintro ⟨K, hK⟩
65+
obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective K
66+
obtain ⟨n, _⟩ := (HomotopyCategory.plus_quotient_obj_iff _).mp hK
67+
exact ⟨n, t.isGE_of_iso ((quotientCompQhIso C).symm.app K) n⟩)
68+
69+
noncomputable instance : (Qh : _ ⥤ Plus C).CommShift ℤ := by
70+
dsimp only [Qh]
71+
infer_instance
72+
73+
set_option backward.isDefEq.respectTransparency false in
74+
instance : (Qh : _ ⥤ Plus C).IsTriangulated := by
75+
dsimp only [Qh]
76+
infer_instance
77+
78+
set_option backward.isDefEq.respectTransparency false in
79+
lemma Qh_map_bijective_of_isKInjective (K L : HomotopyCategory.Plus C)
80+
(_ : CochainComplex.IsKInjective L.1.as) : Function.Bijective (Qh.map : (K ⟶ L) → _) := by
81+
have := CochainComplex.IsKInjective.Qh_map_bijective K.1 L.1.as
82+
rw [← Function.Bijective.of_comp_iff _
83+
((HomotopyCategory.Plus.fullyFaithfulι C).map_bijective _ _)] at this
84+
rwa [← Function.Bijective.of_comp_iff' (t.plus.fullyFaithfulι.map_bijective _ _)]
85+
86+
instance : (HomotopyCategory.plus C).IsVerdierRightLocalizing
87+
(HomotopyCategory.subcategoryAcyclic C) where
88+
fac {K L} φ hK hL := by
89+
obtain ⟨K : CochainComplex _ _, rfl⟩ := HomotopyCategory.quotient_obj_surjective K
90+
obtain ⟨L : CochainComplex _ _, rfl⟩ := HomotopyCategory.quotient_obj_surjective L
91+
simp only [HomotopyCategory.plus_quotient_obj_iff] at hL
92+
obtain ⟨n, hn⟩ := hL
93+
obtain ⟨φ, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective φ
94+
rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hK
95+
refine ⟨(HomotopyCategory.quotient _ _).obj (K.truncGE n),
96+
(HomotopyCategory.quotient _ _).map (K.πTruncGE n),
97+
(HomotopyCategory.quotient _ _).map (CochainComplex.truncGEMap φ n ≫ inv (L.πTruncGE n)),
98+
?_, ?_, by simp [← Functor.map_comp]⟩
99+
· simp only [HomotopyCategory.plus_quotient_obj_iff]
100+
exact ⟨n, inferInstance⟩
101+
· rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic]
102+
exact hK.truncGE _
103+
104+
variable (C)
105+
106+
/-- The functor `DerivedCategory.Plus.Qh : HomotopyCategory.Plus C ⥤ DerivedCategory.Plus C`
107+
is induced by `DerivedCategory.Qh : HomotopyCategory C (.up ℤ) ⥤ DerivedCategory C`. -/
108+
noncomputable def QhCompιIsoιCompQh :
109+
Qh ⋙ Plus.ι ≅ HomotopyCategory.Plus.ι C ⋙ DerivedCategory.Qh := Iso.refl _
110+
111+
instance : (Qh (C := C)).EssSurj where
112+
mem_essImage := by
113+
intro ⟨X, n, K, e, h⟩
114+
refine ⟨⟨(HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K, ?_⟩,
115+
⟨Plus.ι.preimageIso ((quotientCompQhIso C).app _ ≪≫ e.symm)⟩⟩
116+
simp only [HomotopyCategory.plus_quotient_obj_iff]
117+
exact ⟨n, h⟩
118+
119+
instance : Qh.IsLocalization (HomotopyCategory.Plus.subcategoryAcyclic C).trW :=
120+
((HomotopyCategory.plus C).triangulatedLocalizerMorphism
121+
(HomotopyCategory.subcategoryAcyclic C)).isLocalization_of_isLocalizedFullyFaithful
122+
(QhCompιIsoιCompQh C).symm
123+
124+
instance : Qh.IsLocalization (HomotopyCategory.Plus.quasiIso C) := by
125+
rw [HomotopyCategory.Plus.quasiIso_eq_subcategoryAcyclic_trW]
126+
infer_instance
127+
128+
/-- The single functors `C ⥤ DerivedCategory.Plus C` for all `n : ℤ` along with
129+
their compatibilities with shifts. -/
130+
noncomputable def singleFunctors : SingleFunctors C (Plus C) ℤ :=
131+
SingleFunctors.lift (DerivedCategory.singleFunctors C) Plus.ι
132+
(fun n => t.plus.lift (DerivedCategory.singleFunctor C n)
133+
(fun _ => ⟨n, inferInstance⟩))
134+
(fun _ => Iso.refl _)
135+
136+
/-- The single functor `C ⥤ DerivedCategory.Plus C` which sends `X : C` to the
137+
single cochain complex with `X` sitting in degree `n : ℤ`. -/
138+
noncomputable abbrev singleFunctor (n : ℤ) : C ⥤ Plus C := (singleFunctors C).functor n
139+
140+
/-- The single functors on `DerivedCategory.Plus C` are induced by the
141+
single functors on `DerivedCategory C`. -/
142+
noncomputable def singleFunctorιIso (n : ℤ) :
143+
singleFunctor C n ⋙ Plus.ι ≅ DerivedCategory.singleFunctor C n :=
144+
Iso.refl _
145+
146+
instance (n : ℤ) : (singleFunctor C n).Additive := by
147+
dsimp [singleFunctor, singleFunctors]
148+
infer_instance
149+
150+
/-- The homology functor `DerivedCategory.Plus C ⥤ C` in degree `n : ℤ`. -/
151+
noncomputable def homologyFunctor (n : ℤ) : Plus C ⥤ C :=
152+
Plus.ι ⋙ DerivedCategory.homologyFunctor C n
153+
deriving Functor.IsHomological
154+
155+
instance : (Qh (C := C)).mapArrow.EssSurj :=
156+
Localization.essSurj_mapArrow _
157+
(HomotopyCategory.Plus.subcategoryAcyclic C).trW
158+
159+
variable {C}
160+
161+
/-- The canonical t-structure on `DerivedCategory.Plus C`. -/
162+
noncomputable abbrev TStructure.t : TStructure (DerivedCategory.Plus C) :=
163+
(DerivedCategory.TStructure.t (C := C)).plus.tStructure DerivedCategory.TStructure.t
164+
165+
/-- Given `X : DerivedCategory.Plus C` and `n : ℤ`, this property means
166+
that `X` is `≥ n` for the canonical t-structure. -/
167+
abbrev IsGE (X : Plus C) (n : ℤ) : Prop := Plus.TStructure.t.IsGE X n
168+
169+
/-- Given `X : DerivedCategory.Plus C` and `n : ℤ`, this property means
170+
that `X` is `≤ n` for the canonical t-structure. -/
171+
abbrev IsLE (X : Plus C) (n : ℤ) : Prop := Plus.TStructure.t.IsLE X n
172+
173+
lemma isGE_ι_obj_iff (X : Plus C) (n : ℤ) :
174+
(ι.obj X).IsGE n ↔ X.IsGE n := by
175+
constructor
176+
all_goals exact fun h ↦ ⟨h.1⟩
177+
178+
lemma isLE_ι_obj_iff (X : Plus C) (n : ℤ) :
179+
(ι.obj X).IsLE n ↔ X.IsLE n := by
180+
constructor
181+
all_goals exact fun h ↦ ⟨h.1⟩
182+
183+
instance (X : Plus C) (n : ℤ) [X.IsGE n] : (ι.obj X).IsGE n := by
184+
rw [isGE_ι_obj_iff]
185+
infer_instance
186+
187+
instance (X : Plus C) (n : ℤ) [X.IsLE n] : (ι.obj X).IsLE n := by
188+
rw [isLE_ι_obj_iff]
189+
infer_instance
190+
191+
noncomputable instance : (DerivedCategory.Plus.homologyFunctor C 0).ShiftSequence ℤ :=
192+
inferInstanceAs ((ι ⋙ DerivedCategory.homologyFunctor C 0).ShiftSequence ℤ)
193+
194+
instance (X : C) (n : ℤ) : ((singleFunctor C n).obj X).IsGE n := by
195+
rw [← isGE_ι_obj_iff]
196+
change DerivedCategory.TStructure.t.IsGE ((DerivedCategory.singleFunctor C n).obj X) n
197+
infer_instance
198+
199+
instance (X : C) (n : ℤ) : ((singleFunctor C n).obj X).IsLE n := by
200+
rw [← isLE_ι_obj_iff]
201+
change DerivedCategory.TStructure.t.IsLE ((DerivedCategory.singleFunctor C n).obj X) n
202+
infer_instance
203+
204+
lemma isZero_homology_of_isGE
205+
(X : Plus C) (n : ℤ) [X.IsGE n] (i : ℤ) (hi : i < n) :
206+
IsZero ((homologyFunctor C i).obj X) :=
207+
(ι.obj X).isZero_of_isGE n i hi
208+
209+
lemma isZero_homology_of_isLE
210+
(X : Plus C) (n : ℤ) [X.IsLE n] (i : ℤ) (hi : n < i) :
211+
IsZero ((homologyFunctor C i).obj X) :=
212+
(ι.obj X).isZero_of_isLE n i hi
213+
214+
lemma isIso_iff {X Y : Plus C} (f : X ⟶ Y) :
215+
IsIso f ↔ ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f) := by
216+
refine ⟨fun _ _ ↦ inferInstance, fun _ ↦ ?_⟩
217+
have : IsIso (ι.map f) := by rwa [DerivedCategory.isIso_iff]
218+
exact isIso_of_fully_faithful ι _
219+
220+
/-- The localization functor `CochainComplex.Plus C ⥤ DerivedCategory.Plus C`. -/
221+
noncomputable def Q : CochainComplex.Plus C ⥤ DerivedCategory.Plus C :=
222+
HomotopyCategory.Plus.quotient C ⋙ Qh
223+
224+
-- TODO: show that `Q` is indeed a localization functor with respect to quasi-isomorphisms
225+
226+
end Plus
227+
228+
end DerivedCategory

‎Mathlib/Algebra/Homology/DerivedCategory/TStructure.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -193,7 +193,6 @@ lemma exists_iso_singleFunctor_obj_of_isGE_of_isLE
193193
obtain ⟨Y, ⟨e'⟩⟩ := CochainComplex.exists_iso_single K n
194194
exact ⟨Y, ⟨e ≪≫ Q.mapIso e'⟩⟩
195195

196-
197196
open DerivedCategory.TStructure
198197

199198
variable (C)

‎Mathlib/Algebra/Homology/HomotopyCategory/Plus.lean‎

Lines changed: 59 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ of `HomotopyCategory C (.up ℤ)` consisting of bounded below cochain complexes.
2323

2424
open CategoryTheory Limits ZeroObject Pretriangulated HomotopicalAlgebra
2525

26-
variable (C : Type*) [Category* C] [Preadditive C]
26+
variable (C D : Type*) [Category* C] [Category* D] [Preadditive C] [Preadditive D]
2727
(A : Type*) [Category* A] [Abelian A]
2828

2929
namespace CochainComplex
@@ -248,3 +248,61 @@ end
248248
end Plus
249249

250250
end HomotopyCategory
251+
252+
namespace CategoryTheory
253+
254+
namespace Functor
255+
256+
variable {C D}
257+
variable (F : C ⥤ D) [F.Additive]
258+
259+
set_option backward.defeqAttrib.useBackward true in
260+
/-- The functor between bounded below homotopy categories that is induced
261+
by an additive functor. -/
262+
def mapHomotopyCategoryPlus : HomotopyCategory.Plus C ⥤ HomotopyCategory.Plus D :=
263+
(HomotopyCategory.plus D).lift
264+
(HomotopyCategory.Plus.ι C ⋙ F.mapHomotopyCategory (ComplexShape.up ℤ)) (by
265+
rintro ⟨X, hX⟩
266+
obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective X
267+
dsimp
268+
simp only [HomotopyCategory.plus_quotient_obj_iff] at hX ⊢
269+
obtain ⟨n, _⟩ := hX
270+
exact ⟨n, inferInstanceAs (CochainComplex.IsStrictlyGE
271+
((F.mapHomologicalComplex _).obj K) n)⟩)
272+
273+
noncomputable instance :
274+
F.mapHomotopyCategoryPlus.CommShift ℤ :=
275+
inferInstanceAs (((HomotopyCategory.plus D).lift (HomotopyCategory.Plus.ι C ⋙
276+
F.mapHomotopyCategory (.up ℤ)) _).CommShift ℤ)
277+
278+
set_option backward.isDefEq.respectTransparency false in
279+
instance [HasZeroObject C] [HasBinaryBiproducts C] [HasZeroObject D] [HasBinaryBiproducts D] :
280+
(F.mapHomotopyCategoryPlus).IsTriangulated := by
281+
dsimp only [mapHomotopyCategoryPlus]
282+
infer_instance
283+
284+
instance [Full F] [Faithful F] : Full F.mapHomotopyCategoryPlus where
285+
map_surjective f :=
286+
⟨ObjectProperty.homMk ((F.mapHomotopyCategory _).preimage f.hom), by
287+
ext
288+
exact (F.mapHomotopyCategory _).map_preimage f.hom⟩
289+
290+
instance [Full F] [Faithful F] : Faithful F.mapHomotopyCategoryPlus where
291+
map_injective h := by
292+
ext
293+
exact (F.mapHomotopyCategory _).map_injective ((ObjectProperty.ι _).congr_map h)
294+
295+
/-- Given additive functors that are related by an isomorphism `F ⋙ G ≅ H`, this is
296+
the corresponding isomorphism on the corresponding functor between
297+
the bounded below homotopy categories. -/
298+
def mapHomotopyCategoryPlusCompIso {E : Type*} [Category* E] [Preadditive E]
299+
{F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} (e : F ⋙ G ≅ H)
300+
[F.Additive] [G.Additive] [H.Additive] :
301+
F.mapHomotopyCategoryPlus ⋙ G.mapHomotopyCategoryPlus ≅ H.mapHomotopyCategoryPlus :=
302+
((HomotopyCategory.plus _).fullyFaithfulι.whiskeringRight _).preimageIso
303+
(isoWhiskerLeft (HomotopyCategory.Plus.ι C)
304+
(mapHomotopyCategoryCompIso e (.up ℤ)))
305+
306+
end Functor
307+
308+
end CategoryTheory

0 commit comments

Comments
 (0)