Skip to content

Commit 85ca5b2

Browse files
joelrioujoelriou
committed
feat(AlgebraicTopology): model categories (#19158)
We formalize the axioms of Quillen's model categories. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
1 parent cdcfe3a commit 85ca5b2

4 files changed

Lines changed: 222 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1079,6 +1079,8 @@ import Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
10791079
import Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
10801080
import Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
10811081
import Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
1082+
import Mathlib.AlgebraicTopology.ModelCategory.Basic
1083+
import Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
10821084
import Mathlib.AlgebraicTopology.MooreComplex
10831085
import Mathlib.AlgebraicTopology.Quasicategory.Basic
10841086
import Mathlib.AlgebraicTopology.Quasicategory.Nerve

‎Mathlib/AlgebraicTopology/ModelCategory/Basic.lean‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
/-
2+
Copyright (c) 2024 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.Limits.Shapes.FiniteLimits
7+
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
8+
import Mathlib.CategoryTheory.MorphismProperty.Composition
9+
import Mathlib.CategoryTheory.MorphismProperty.Factorization
10+
import Mathlib.CategoryTheory.MorphismProperty.Retract
11+
import Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
12+
13+
/-!
14+
# Model categories
15+
16+
We introduce a typeclass `ModelCategory C` expressing that `C` is equipped with
17+
classes of morphisms named "fibrations", "cofibrations" and "weak equivalences"
18+
with satisfy the axioms of (closed) model categories.
19+
20+
As a given category `C` may have several model category structures, it is advisable
21+
to define only local instances of `ModelCategory`, or to set these instances on type synonyms.
22+
23+
## References
24+
* [Daniel G. Quillen, Homotopical algebra][Quillen1967]
25+
* [Paul G. Goerss, John F. Jardine, Simplicial Homotopy Theory][goerss-jardine-2009]
26+
27+
-/
28+
29+
universe v u
30+
31+
namespace HomotopicalAlgebra
32+
33+
open CategoryTheory Limits
34+
35+
variable (C : Type u) [Category.{v} C]
36+
37+
/-- A model category is a category equipped with classes of morphisms named cofibrations,
38+
fibrations and weak equivalences which satisfies the axioms CM1/CM2/CM3/CM4/CM5
39+
of (closed) model categories. -/
40+
class ModelCategory where
41+
categoryWithFibrations : CategoryWithFibrations C := by infer_instance
42+
categoryWithCofibrations : CategoryWithCofibrations C := by infer_instance
43+
categoryWithWeakEquivalences : CategoryWithWeakEquivalences C := by infer_instance
44+
cm1a : HasFiniteLimits C := by infer_instance
45+
cm1b : HasFiniteColimits C := by infer_instance
46+
cm2 : (weakEquivalences C).HasTwoOutOfThreeProperty := by infer_instance
47+
cm3a : (weakEquivalences C).IsStableUnderRetracts := by infer_instance
48+
cm3b : (fibrations C).IsStableUnderRetracts := by infer_instance
49+
cm3c : (cofibrations C).IsStableUnderRetracts := by infer_instance
50+
cm4a {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p] :
51+
HasLiftingProperty i p := by intros; infer_instance
52+
cm4b {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [Fibration p] [WeakEquivalence p] :
53+
HasLiftingProperty i p := by intros; infer_instance
54+
cm5a : MorphismProperty.HasFactorization (trivialCofibrations C) (fibrations C) := by
55+
infer_instance
56+
cm5b : MorphismProperty.HasFactorization (cofibrations C) (trivialFibrations C) := by
57+
infer_instance
58+
59+
namespace ModelCategory
60+
61+
attribute [instance] categoryWithFibrations categoryWithCofibrations categoryWithWeakEquivalences
62+
cm1a cm1b cm2 cm3a cm3b cm3c cm4a cm4b cm5a cm5b
63+
64+
end ModelCategory
65+
66+
end HomotopicalAlgebra

‎Mathlib/AlgebraicTopology/ModelCategory/CategoryWithCofibrations.lean‎

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
/-
2+
Copyright (c) 2024 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.MorphismProperty.Basic
7+
8+
/-!
9+
# Categories with classes of fibrations, cofibrations, weak equivalences
10+
11+
We introduce typeclasses `CategoryWithFibrations`, `CategoryWithCofibrations` and
12+
`CategoryWithWeakEquivalences` to express that a category `C` is equipped with
13+
classes of morphisms named "fibrations", "cofibrations" or "weak equivalences".
14+
15+
-/
16+
17+
universe v u
18+
19+
namespace HomotopicalAlgebra
20+
21+
open CategoryTheory
22+
23+
variable (C : Type u) [Category.{v} C]
24+
25+
/-- A category with fibrations is a category equipped with
26+
a class of morphisms named "fibrations". -/
27+
class CategoryWithFibrations where
28+
/-- the class of fibrations -/
29+
fibrations : MorphismProperty C
30+
31+
/-- A category with cofibrations is a category equipped with
32+
a class of morphisms named "cofibrations". -/
33+
class CategoryWithCofibrations where
34+
/-- the class of cofibrations -/
35+
cofibrations : MorphismProperty C
36+
37+
/-- A category with weak equivalences is a category equipped with
38+
a class of morphisms named "weak equivalences". -/
39+
class CategoryWithWeakEquivalences where
40+
/-- the class of weak equivalences -/
41+
weakEquivalences : MorphismProperty C
42+
43+
variable {X Y : C} (f : X ⟶ Y)
44+
45+
section Fib
46+
47+
variable [CategoryWithFibrations C]
48+
49+
/-- The class of fibrations in a category with fibrations. -/
50+
def fibrations : MorphismProperty C := CategoryWithFibrations.fibrations
51+
52+
variable {C}
53+
54+
/-- A morphism `f` satisfies `[Fibration f]` if it belongs to `fibrations C`. -/
55+
@[mk_iff]
56+
class Fibration : Prop where
57+
mem : fibrations C f
58+
59+
lemma mem_fibrations [Fibration f] : fibrations C f := Fibration.mem
60+
61+
end Fib
62+
63+
section Cof
64+
65+
variable [CategoryWithCofibrations C]
66+
67+
/-- The class of cofibrations in a category with cofibrations. -/
68+
def cofibrations : MorphismProperty C := CategoryWithCofibrations.cofibrations
69+
70+
variable {C}
71+
72+
/-- A morphism `f` satisfies `[Cofibration f]` if it belongs to `cofibrations C`. -/
73+
@[mk_iff]
74+
class Cofibration : Prop where
75+
mem : cofibrations C f
76+
77+
lemma mem_cofibrations [Cofibration f] : cofibrations C f := Cofibration.mem
78+
79+
end Cof
80+
81+
section W
82+
83+
variable [CategoryWithWeakEquivalences C]
84+
85+
/-- The class of weak equivalences in a category with weak equivalences. -/
86+
def weakEquivalences : MorphismProperty C := CategoryWithWeakEquivalences.weakEquivalences
87+
88+
variable {C}
89+
90+
/-- A morphism `f` satisfies `[WeakEquivalence f]` if it belongs to `weakEquivalences C`. -/
91+
@[mk_iff]
92+
class WeakEquivalence : Prop where
93+
mem : weakEquivalences C f
94+
95+
lemma mem_weakEquivalences [WeakEquivalence f] : weakEquivalences C f := WeakEquivalence.mem
96+
97+
end W
98+
99+
section TrivFib
100+
101+
variable [CategoryWithFibrations C] [CategoryWithWeakEquivalences C]
102+
103+
/-- A trivial fibration is a morphism that is both a fibration and a weak equivalence. -/
104+
def trivialFibrations : MorphismProperty C := fibrations C ⊓ weakEquivalences C
105+
106+
lemma trivialFibrations_sub_fibrations : trivialFibrations C ≤ fibrations C :=
107+
fun _ _ _ hf ↦ hf.1
108+
109+
lemma trivialFibrations_sub_weakEquivalences : trivialFibrations C ≤ weakEquivalences C :=
110+
fun _ _ _ hf ↦ hf.2
111+
112+
variable {C}
113+
114+
lemma mem_trivialFibrations [Fibration f] [WeakEquivalence f] :
115+
trivialFibrations C f :=
116+
⟨mem_fibrations f, mem_weakEquivalences f⟩
117+
118+
end TrivFib
119+
120+
section TrivCof
121+
122+
variable [CategoryWithCofibrations C] [CategoryWithWeakEquivalences C]
123+
124+
/-- A trivial cofibration is a morphism that is both a cofibration and a weak equivalence. -/
125+
def trivialCofibrations : MorphismProperty C := cofibrations C ⊓ weakEquivalences C
126+
127+
lemma trivialCofibrations_sub_cofibrations : trivialCofibrations C ≤ cofibrations C :=
128+
fun _ _ _ hf ↦ hf.1
129+
130+
lemma trivialCofibrations_sub_weakEquivalences : trivialCofibrations C ≤ weakEquivalences C :=
131+
fun _ _ _ hf ↦ hf.2
132+
133+
134+
variable {C}
135+
136+
lemma mem_trivialCofibrations [Cofibration f] [WeakEquivalence f] :
137+
trivialCofibrations C f :=
138+
⟨mem_cofibrations f, mem_weakEquivalences f⟩
139+
140+
end TrivCof
141+
142+
end HomotopicalAlgebra

‎docs/references.bib‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3122,6 +3122,18 @@ @Article{ Prielipp1970
31223122
url = {http://www.jstor.org/stable/27958492}
31233123
}
31243124

3125+
@Book{ Quillen1967,
3126+
author = {Quillen, Daniel G.},
3127+
title = {Homotopical algebra},
3128+
series = {Lecture Notes in Mathematics},
3129+
volume = {No. 43},
3130+
publisher = {Springer-Verlag, Berlin-New York},
3131+
year = {1967},
3132+
pages = {iv+156 pp. (not consecutively paged)},
3133+
mrclass = {18.20 (55.00)},
3134+
mrnumber = {223432}
3135+
}
3136+
31253137
@InCollection{ ribenboim1971,
31263138
author = {Ribenboim, Paulo},
31273139
title = {\'{E}pimorphismes de modules qui sont n\'{e}cessairement

0 commit comments

Comments
 (0)