Skip to content

Commit b6d6921

Browse files
joelrioujoelriou
committed
feat(Algebra/Homology): the category of complexes up to quasi-isomorphisms (#8970)
In this PR, we define the category of homological complexes up to quasi-isomorphisms. The derived category of an abelian category shall be a particular case on this construction, but the additional structures on the derived category will require more work. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
1 parent e981962 commit b6d6921

File tree

3 files changed

+143
-0
lines changed

3 files changed

+143
-0
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -247,6 +247,7 @@ import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
247247
import Mathlib.Algebra.Homology.HomotopyCategory.Shift
248248
import Mathlib.Algebra.Homology.ImageToKernel
249249
import Mathlib.Algebra.Homology.LocalCohomology
250+
import Mathlib.Algebra.Homology.Localization
250251
import Mathlib.Algebra.Homology.ModuleCat
251252
import Mathlib.Algebra.Homology.Opposite
252253
import Mathlib.Algebra.Homology.QuasiIso
@@ -1147,6 +1148,7 @@ import Mathlib.CategoryTheory.Localization.CalculusOfFractions
11471148
import Mathlib.CategoryTheory.Localization.Composition
11481149
import Mathlib.CategoryTheory.Localization.Construction
11491150
import Mathlib.CategoryTheory.Localization.Equivalence
1151+
import Mathlib.CategoryTheory.Localization.HasLocalization
11501152
import Mathlib.CategoryTheory.Localization.LocalizerMorphism
11511153
import Mathlib.CategoryTheory.Localization.Opposite
11521154
import Mathlib.CategoryTheory.Localization.Pi

‎Mathlib/Algebra/Homology/Localization.lean‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
/-
2+
Copyright (c) 2023 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+
7+
import Mathlib.Algebra.Homology.HomotopyCategory
8+
import Mathlib.Algebra.Homology.QuasiIso
9+
import Mathlib.CategoryTheory.Localization.HasLocalization
10+
11+
/-! The category of homological complexes up to quasi-isomorphisms
12+
13+
Given a category `C` with homology and any complex shape `c`, we define
14+
the category `HomologicalComplexUpToQis C c` which is the localized
15+
category of `HomologicalComplex C c` with respect to quasi-isomorphisms.
16+
When `C` is abelian, this will be the derived category of `C` in the
17+
particular case of the complex shape `ComplexShape.up ℤ`.
18+
19+
Under suitable assumptions on `c` (e.g. chain or cochain complexes),
20+
we shall show that `HomologicalComplexUpToQis C c` is also the
21+
localized category of `HomotopyCategory C c` with respect to
22+
the class of quasi-isomorphisms (TODO).
23+
24+
-/
25+
26+
open CategoryTheory Limits
27+
28+
variable (C : Type*) [Category C] {ι : Type*} (c : ComplexShape ι) [HasZeroMorphisms C]
29+
[CategoryWithHomology C] [(HomologicalComplex.qis C c).HasLocalization]
30+
31+
/-- The category of homological complexes up to quasi-isomorphisms. -/
32+
abbrev HomologicalComplexUpToQis := (HomologicalComplex.qis C c).Localization'
33+
34+
variable {C c}
35+
36+
/-- The localization functor `HomologicalComplex C c ⥤ HomologicalComplexUpToQis C c`. -/
37+
abbrev HomologicalComplexUpToQis.Q :
38+
HomologicalComplex C c ⥤ HomologicalComplexUpToQis C c :=
39+
(HomologicalComplex.qis C c).Q'
40+
41+
variable (C c)
42+
43+
lemma HomologicalComplex.homologyFunctor_inverts_qis (i : ι) :
44+
(qis C c).IsInvertedBy (homologyFunctor C c i) := fun _ _ _ hf => by
45+
rw [qis_iff] at hf
46+
dsimp
47+
infer_instance
48+
49+
namespace HomologicalComplexUpToQis
50+
51+
/-- The homology functor `HomologicalComplexUpToQis C c ⥤ C` for each `i : ι`. -/
52+
noncomputable def homologyFunctor (i : ι) : HomologicalComplexUpToQis C c ⥤ C :=
53+
Localization.lift _ (HomologicalComplex.homologyFunctor_inverts_qis C c i) Q
54+
55+
/-- The homology functor on `HomologicalComplexUpToQis C c` is induced by
56+
the homology functor on `HomologicalComplex C c`. -/
57+
noncomputable def homologyFunctorFactors (i : ι) :
58+
Q ⋙ homologyFunctor C c i ≅ HomologicalComplex.homologyFunctor C c i :=
59+
Localization.fac _ (HomologicalComplex.homologyFunctor_inverts_qis C c i) Q
60+
61+
end HomologicalComplexUpToQis

‎Mathlib/CategoryTheory/Localization/HasLocalization.lean‎

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
/-
2+
Copyright (c) 2023 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+
import Mathlib.CategoryTheory.Localization.Predicate
7+
8+
/-! Morphism properties equipped with a localized category
9+
10+
If `C : Type u` is a category (with `[Category.{v} C]`), and
11+
`W : MorphismProperty C`, then the constructed localized
12+
category `W.Localization` is in `Type u` (the objects are
13+
essentially the same as that of `C`), but the morphisms
14+
are in `Type (max u v)`. In particular situations, it
15+
may happen that there is a localized category for `W`
16+
whose morphisms are in a lower universe like `v`: it shall
17+
be so for the homotopy categories of model categories (TODO),
18+
and it should also be so for the derived categories of
19+
Grothendieck abelian categories (TODO: but this shall be
20+
very technical).
21+
22+
Then, in order to allow the user to provide a localized
23+
category with specific universe parameters when it exists,
24+
we introduce a typeclass `MorphismProperty.HasLocalization.{w} W`
25+
which contains the data of a localized category `D` for `W`
26+
with `D : Type u` and `[Category.{w} D]`. Then, all
27+
definitions which involve "the" localized category
28+
for `W` should contain a `[MorphismProperty.HasLocalization.{w} W]`
29+
assumption for a suitable `w`. The functor `W.Q' : C ⥤ W.Localization'`
30+
shall be the localization functor for this fixed choice of the
31+
localized category. If the statement of a theorem does not
32+
involve the localized category, but the proof does,
33+
it is no longer necessary to use a `HasLocalization`
34+
assumption, but one may use
35+
`HasLocalization.standard` in the proof instead.
36+
37+
-/
38+
39+
universe w v u
40+
41+
namespace CategoryTheory
42+
43+
variable {C : Type u} [Category.{v} C]
44+
45+
variable (W : MorphismProperty C)
46+
47+
namespace MorphismProperty
48+
49+
/-- The data of a localized category with a given universe
50+
for the morphisms. -/
51+
class HasLocalization where
52+
/-- the objects of the localized category. -/
53+
{D : Type u}
54+
/-- the category structure. -/
55+
[hD : Category.{w} D]
56+
/-- the localization functor. -/
57+
L : C ⥤ D
58+
[hL : L.IsLocalization W]
59+
60+
variable [HasLocalization.{w} W]
61+
62+
/-- The localized category for `W : MorphismProperty C`
63+
that is fixed by the `[HasLocalization W]` instance. -/
64+
def Localization' := HasLocalization.D W
65+
66+
instance : Category W.Localization' := HasLocalization.hD
67+
68+
/-- The localization functor `C ⥤ W.Localization'`
69+
that is fixed by the `[HasLocalization W]` instance. -/
70+
def Q' : C ⥤ W.Localization' := HasLocalization.L
71+
72+
instance : W.Q'.IsLocalization W := HasLocalization.hL
73+
74+
/-- The constructed localized category. -/
75+
def HasLocalization.standard : HasLocalization.{max u v} W where
76+
L := W.Q
77+
78+
end MorphismProperty
79+
80+
end CategoryTheory

0 commit comments

Comments
 (0)