Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 88bca0c

Browse files
joelrioujoelriou
committed
feat(algebraic_topology/dold_kan): N₂ reflects isomorphisms (#17577)
This PR shows that `N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ))` reflects isomorphisms.
1 parent c0dd3fc commit 88bca0c

5 files changed

Lines changed: 90 additions & 7 deletions

File tree

‎src/algebra/homology/additive.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,17 @@ def functor.map_homological_complex (F : V ⥤ W) [F.additive] (c : complex_shap
110110
instance functor.map_homogical_complex_additive
111111
(F : V ⥤ W) [F.additive] (c : complex_shape ι) : (F.map_homological_complex c).additive := {}
112112

113+
instance functor.map_homological_complex_reflects_iso
114+
(F : V ⥤ W) [F.additive] [reflects_isomorphisms F] (c : complex_shape ι) :
115+
reflects_isomorphisms (F.map_homological_complex c) :=
116+
⟨λ X Y f, begin
117+
introI,
118+
haveI : ∀ (n : ι), is_iso (F.map (f.f n)) := λ n, is_iso.of_iso
119+
((homological_complex.eval W c n).map_iso (as_iso ((F.map_homological_complex c).map f))),
120+
haveI := λ n, is_iso_of_reflects_iso (f.f n) F,
121+
exact homological_complex.hom.is_iso_of_components f,
122+
end⟩
123+
113124
/--
114125
A natural transformation between functors induces a natural transformation
115126
between those functors applied to homological complexes.

‎src/algebra/homology/homological_complex.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -428,6 +428,14 @@ def iso_of_components (f : Π i, C₁.X i ≅ C₂.X i)
428428
iso_app (iso_of_components f hf) i = f i :=
429429
by { ext, simp, }
430430

431+
lemma is_iso_of_components (f : C₁ ⟶ C₂) [∀ (n : ι), is_iso (f.f n)] : is_iso f :=
432+
begin
433+
convert is_iso.of_iso (homological_complex.hom.iso_of_components (λ n, as_iso (f.f n))
434+
(by tidy)),
435+
ext n,
436+
refl,
437+
end
438+
431439
/-! Lemmas relating chain maps and `d_to`/`d_from`. -/
432440

433441
/-- `f.prev j` is `f.f i` if there is some `r i j`, and `f.f j` otherwise. -/

‎src/algebraic_topology/alternating_face_map_complex.lean‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ import algebra.homology.additive
88
import algebraic_topology.Moore_complex
99
import algebra.big_operators.fin
1010
import category_theory.preadditive.opposite
11+
import category_theory.idempotents.functor_categories
1112
import tactic.equiv_rw
1213

1314
/-!
@@ -34,7 +35,7 @@ when `A` is an abelian category.
3435
-/
3536

3637
open category_theory category_theory.limits category_theory.subobject
37-
open category_theory.preadditive category_theory.category
38+
open category_theory.preadditive category_theory.category category_theory.idempotents
3839
open opposite
3940

4041
open_locale big_operators
@@ -204,6 +205,15 @@ begin
204205
refl, }, },
205206
end
206207

208+
lemma karoubi_alternating_face_map_complex_d (P : karoubi (simplicial_object C)) (n : ℕ) :
209+
(((alternating_face_map_complex.obj (karoubi_functor_category_embedding.obj P)).d (n+1) n).f) =
210+
P.p.app (op [n+1]) ≫ ((alternating_face_map_complex.obj P.X).d (n+1) n) :=
211+
begin
212+
dsimp,
213+
simpa only [alternating_face_map_complex.obj_d_eq, karoubi.sum_hom,
214+
preadditive.comp_sum, karoubi.zsmul_hom, preadditive.comp_zsmul],
215+
end
216+
207217
namespace alternating_face_map_complex
208218

209219
/-- The natural transformation which gives the augmentation of the alternating face map

‎src/algebraic_topology/dold_kan/n_reflects_iso.lean‎

Lines changed: 55 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -7,17 +7,16 @@ Authors: Joël Riou
77
import algebraic_topology.dold_kan.functor_n
88
import algebraic_topology.dold_kan.decomposition
99
import category_theory.idempotents.homological_complex
10+
import category_theory.idempotents.karoubi_karoubi
1011

1112
/-!
1213
1314
# N₁ and N₂ reflects isomorphisms
1415
15-
In this file, it is shown that the functor
16-
`N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)`
17-
reflects isomorphisms for any preadditive category `C`.
18-
19-
TODO @joelriou: deduce that `N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ)`
20-
also reflects isomorphisms.
16+
In this file, it is shown that the functors
17+
`N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)` and
18+
`N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ))`
19+
reflect isomorphisms for any preadditive category `C`.
2120
2221
-/
2322

@@ -69,6 +68,56 @@ instance : reflects_isomorphisms (N₁ : simplicial_object C ⥤ karoubi (chain_
6968
tauto, },
7069
end⟩
7170

71+
lemma compatibility_N₂_N₁_karoubi :
72+
N₂ ⋙ (karoubi_chain_complex_equivalence C ℕ).functor =
73+
karoubi_functor_category_embedding simplex_categoryᵒᵖ C ⋙ N₁ ⋙
74+
(karoubi_chain_complex_equivalence (karoubi C) ℕ).functor ⋙
75+
functor.map_homological_complex (karoubi_karoubi.equivalence C).inverse _ :=
76+
begin
77+
refine category_theory.functor.ext (λ P, _) (λ P Q f, _),
78+
{ refine homological_complex.ext _ _,
79+
{ ext n,
80+
{ dsimp,
81+
simp only [karoubi_P_infty_f, comp_id, P_infty_f_naturality, id_comp], },
82+
{ refl, }, },
83+
{ rintros _ n (rfl : n+1 = _),
84+
ext,
85+
have h := (alternating_face_map_complex.map P.p).comm (n+1) n,
86+
dsimp [N₂, karoubi_chain_complex_equivalence, karoubi_karoubi.inverse,
87+
karoubi_homological_complex_equivalence.functor.obj] at ⊢ h,
88+
simp only [karoubi.comp_f, assoc, karoubi.eq_to_hom_f, eq_to_hom_refl, id_comp, comp_id,
89+
karoubi_alternating_face_map_complex_d, karoubi_P_infty_f,
90+
← homological_complex.hom.comm_assoc, ← h, app_idem_assoc], }, },
91+
{ ext n,
92+
dsimp [karoubi_karoubi.inverse, karoubi_functor_category_embedding,
93+
karoubi_functor_category_embedding.map],
94+
simp only [karoubi.comp_f, karoubi_P_infty_f, homological_complex.eq_to_hom_f,
95+
karoubi.eq_to_hom_f, assoc, comp_id, P_infty_f_naturality, app_p_comp,
96+
karoubi_chain_complex_equivalence_functor_obj_X_p, N₂_obj_p_f, eq_to_hom_refl,
97+
P_infty_f_naturality_assoc, app_comp_p, P_infty_f_idem_assoc], },
98+
end
99+
100+
/-- We deduce that `N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ))`
101+
reflects isomorphisms from the fact that
102+
`N₁ : simplicial_object (karoubi C) ⥤ karoubi (chain_complex (karoubi C) ℕ)` does. -/
103+
instance : reflects_isomorphisms
104+
(N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ)) := ⟨λ X Y f,
105+
begin
106+
introI,
107+
-- The following functor `F` reflects isomorphism because it is
108+
-- a composition of four functors which reflects isomorphisms.
109+
-- Then, it suffices to show that `F.map f` is an isomorphism.
110+
let F := karoubi_functor_category_embedding simplex_categoryᵒᵖ C ⋙ N₁ ⋙
111+
(karoubi_chain_complex_equivalence (karoubi C) ℕ).functor ⋙
112+
functor.map_homological_complex (karoubi_karoubi.equivalence C).inverse
113+
(complex_shape.down ℕ),
114+
haveI : is_iso (F.map f),
115+
{ dsimp only [F],
116+
rw [← compatibility_N₂_N₁_karoubi, functor.comp_map],
117+
apply functor.map_is_iso, },
118+
exact is_iso_of_reflects_iso f F,
119+
end⟩
120+
72121
end dold_kan
73122

74123
end algebraic_topology

‎src/category_theory/idempotents/karoubi.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -246,6 +246,11 @@ lemma decomp_id_p_naturality {P Q : karoubi C} (f : P ⟶ Q) : decomp_id_p P ≫
246246
(⟨f.f, by erw [comp_id, id_comp]⟩ : (P.X : karoubi C) ⟶ Q.X) ≫ decomp_id_p Q :=
247247
by { ext, simp only [comp_f, decomp_id_p_f, karoubi.comp_p, karoubi.p_comp], }
248248

249+
@[simp]
250+
lemma zsmul_hom [preadditive C] {P Q : karoubi C} (n : ℤ) (f : P ⟶ Q) :
251+
(n • f).f = n • f.f :=
252+
map_zsmul (inclusion_hom P Q) n f
253+
249254
end karoubi
250255

251256
end idempotents

0 commit comments

Comments
 (0)