-
Notifications
You must be signed in to change notification settings - Fork 259
/
Normalized.lean
146 lines (120 loc) · 6.01 KB
/
Normalized.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
/-
Copyright (c) 2022 Joël Riou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joël Riou
-/
import Mathlib.AlgebraicTopology.DoldKan.FunctorN
/-!
# Comparison with the normalized Moore complex functor
In this file, we show that when the category `A` is abelian,
there is an isomorphism `N₁_iso_normalizedMooreComplex_comp_toKaroubi` between
the functor `N₁ : SimplicialObject A ⥤ Karoubi (ChainComplex A ℕ)`
defined in `FunctorN.lean` and the composition of
`normalizedMooreComplex A` with the inclusion
`ChainComplex A ℕ ⥤ Karoubi (ChainComplex A ℕ)`.
This isomorphism shall be used in `Equivalence.lean` in order to obtain
the Dold-Kan equivalence
`CategoryTheory.Abelian.DoldKan.equivalence : SimplicialObject A ≌ ChainComplex A ℕ`
with a functor (definitionally) equal to `normalizedMooreComplex A`.
(See `Equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
-/
open CategoryTheory CategoryTheory.Category CategoryTheory.Limits
CategoryTheory.Subobject CategoryTheory.Idempotents DoldKan
noncomputable section
namespace AlgebraicTopology
namespace DoldKan
universe v
variable {A : Type*} [Category A] [Abelian A] {X : SimplicialObject A}
theorem HigherFacesVanish.inclusionOfMooreComplexMap (n : ℕ) :
HigherFacesVanish (n + 1) ((inclusionOfMooreComplexMap X).f (n + 1)) := fun j _ => by
dsimp [AlgebraicTopology.inclusionOfMooreComplexMap, NormalizedMooreComplex.objX]
rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j
(by simp only [Finset.mem_univ])), assoc, kernelSubobject_arrow_comp, comp_zero]
theorem factors_normalizedMooreComplex_PInfty (n : ℕ) :
Subobject.Factors (NormalizedMooreComplex.objX X n) (PInfty.f n) := by
rcases n with _|n
· apply top_factors
· rw [PInfty_f, NormalizedMooreComplex.objX, finset_inf_factors]
intro i _
apply kernelSubobject_factors
exact (HigherFacesVanish.of_P (n + 1) n) i le_add_self
/-- `PInfty` factors through the normalized Moore complex -/
@[simps!]
def PInftyToNormalizedMooreComplex (X : SimplicialObject A) : K[X] ⟶ N[X] :=
ChainComplex.ofHom _ _ _ _ _ _
(fun n => factorThru _ _ (factors_normalizedMooreComplex_PInfty n)) fun n => by
rw [← cancel_mono (NormalizedMooreComplex.objX X n).arrow, assoc, assoc, factorThru_arrow,
← inclusionOfMooreComplexMap_f, ← normalizedMooreComplex_objD,
← (inclusionOfMooreComplexMap X).comm (n + 1) n, inclusionOfMooreComplexMap_f,
factorThru_arrow_assoc, ← alternatingFaceMapComplex_obj_d]
exact PInfty.comm (n + 1) n
@[reassoc (attr := simp)]
theorem PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap (X : SimplicialObject A) :
PInftyToNormalizedMooreComplex X ≫ inclusionOfMooreComplexMap X = PInfty := by aesop_cat
@[reassoc (attr := simp)]
theorem PInftyToNormalizedMooreComplex_naturality {X Y : SimplicialObject A} (f : X ⟶ Y) :
AlternatingFaceMapComplex.map f ≫ PInftyToNormalizedMooreComplex Y =
PInftyToNormalizedMooreComplex X ≫ NormalizedMooreComplex.map f := by
aesop_cat
@[reassoc (attr := simp)]
theorem PInfty_comp_PInftyToNormalizedMooreComplex (X : SimplicialObject A) :
PInfty ≫ PInftyToNormalizedMooreComplex X = PInftyToNormalizedMooreComplex X := by aesop_cat
@[reassoc (attr := simp)]
theorem inclusionOfMooreComplexMap_comp_PInfty (X : SimplicialObject A) :
inclusionOfMooreComplexMap X ≫ PInfty = inclusionOfMooreComplexMap X := by
ext (_|n)
· dsimp
simp only [comp_id]
· exact (HigherFacesVanish.inclusionOfMooreComplexMap n).comp_P_eq_self
instance : Mono (inclusionOfMooreComplexMap X) :=
⟨fun _ _ hf => by
ext n
dsimp
ext
exact HomologicalComplex.congr_hom hf n⟩
/-- `inclusionOfMooreComplexMap X` is a split mono. -/
def splitMonoInclusionOfMooreComplexMap (X : SimplicialObject A) :
SplitMono (inclusionOfMooreComplexMap X) where
retraction := PInftyToNormalizedMooreComplex X
id := by
simp only [← cancel_mono (inclusionOfMooreComplexMap X), assoc, id_comp,
PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
inclusionOfMooreComplexMap_comp_PInfty]
variable (A)
/-- When the category `A` is abelian,
the functor `N₁ : SimplicialObject A ⥤ Karoubi (ChainComplex A ℕ)` defined
using `PInfty` identifies to the composition of the normalized Moore complex functor
and the inclusion in the Karoubi envelope. -/
def N₁_iso_normalizedMooreComplex_comp_toKaroubi : N₁ ≅ normalizedMooreComplex A ⋙ toKaroubi _ where
hom :=
{ app := fun X =>
{ f := PInftyToNormalizedMooreComplex X
comm := by erw [comp_id, PInfty_comp_PInftyToNormalizedMooreComplex] }
naturality := fun X Y f => by
simp only [Functor.comp_map, normalizedMooreComplex_map,
PInftyToNormalizedMooreComplex_naturality, Karoubi.hom_ext_iff, Karoubi.comp_f, N₁_map_f,
PInfty_comp_PInftyToNormalizedMooreComplex_assoc, toKaroubi_map_f, assoc] }
inv :=
{ app := fun X =>
{ f := inclusionOfMooreComplexMap X
comm := by erw [inclusionOfMooreComplexMap_comp_PInfty, id_comp] }
naturality := fun X Y f => by
ext
simp only [Functor.comp_map, normalizedMooreComplex_map, Karoubi.comp_f, toKaroubi_map_f,
HomologicalComplex.comp_f, NormalizedMooreComplex.map_f,
inclusionOfMooreComplexMap_f, factorThru_arrow, N₁_map_f,
inclusionOfMooreComplexMap_comp_PInfty_assoc, AlternatingFaceMapComplex.map_f] }
hom_inv_id := by
ext X : 3
simp only [PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
NatTrans.comp_app, Karoubi.comp_f, N₁_obj_p, NatTrans.id_app, Karoubi.id_f]
inv_hom_id := by
ext X : 3
rw [← cancel_mono (inclusionOfMooreComplexMap X)]
simp only [NatTrans.comp_app, Karoubi.comp_f, assoc, NatTrans.id_app, Karoubi.id_f,
PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
inclusionOfMooreComplexMap_comp_PInfty]
dsimp only [Functor.comp_obj, toKaroubi]
erw [id_comp]
end DoldKan
end AlgebraicTopology