feat(algebraic_topology/dold_kan): N₂ reflects isomorphisms (#17577)

This PR shows that `N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ))` reflects isomorphisms.

src/algebra/homology/additive.lean

@@ -110,6 +110,17 @@ def functor.map_homological_complex (F : V ⥤ W) [F.additive] (c : complex_shap
 instance functor.map_homogical_complex_additive
   (F : V ⥤ W) [F.additive] (c : complex_shape ι) : (F.map_homological_complex c).additive := {}
 
+instance functor.map_homological_complex_reflects_iso
+  (F : V ⥤ W) [F.additive] [reflects_isomorphisms F] (c : complex_shape ι) :
+  reflects_isomorphisms (F.map_homological_complex c) :=
+⟨λ X Y f, begin
+  introI,
+  haveI : ∀ (n : ι), is_iso (F.map (f.f n)) := λ n, is_iso.of_iso
+    ((homological_complex.eval W c n).map_iso (as_iso ((F.map_homological_complex c).map f))),
+  haveI := λ n, is_iso_of_reflects_iso (f.f n) F,
+  exact homological_complex.hom.is_iso_of_components f,
+end⟩
+
 /--
 A natural transformation between functors induces a natural transformation
 between those functors applied to homological complexes.

src/algebra/homology/homological_complex.lean

@@ -428,6 +428,14 @@ def iso_of_components (f : Π i, C₁.X i ≅ C₂.X i)
   iso_app (iso_of_components f hf) i = f i :=
 by { ext, simp, }
 
+lemma is_iso_of_components (f : C₁ ⟶ C₂) [∀ (n : ι), is_iso (f.f n)] : is_iso f :=
+begin
+  convert is_iso.of_iso (homological_complex.hom.iso_of_components (λ n, as_iso (f.f n))
+    (by tidy)),
+  ext n,
+  refl,
+end
+
 /-! Lemmas relating chain maps and `d_to`/`d_from`. -/
 
 /-- `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

@@ -8,6 +8,7 @@ import algebra.homology.additive
 import algebraic_topology.Moore_complex
 import algebra.big_operators.fin
 import category_theory.preadditive.opposite
+import category_theory.idempotents.functor_categories
 import tactic.equiv_rw
 
 /-!
@@ -34,7 +35,7 @@ when `A` is an abelian category.
 -/
 
 open category_theory category_theory.limits category_theory.subobject
-open category_theory.preadditive category_theory.category
+open category_theory.preadditive category_theory.category category_theory.idempotents
 open opposite
 
 open_locale big_operators
@@ -204,6 +205,15 @@ begin
       refl, }, },
 end
 
+lemma karoubi_alternating_face_map_complex_d (P : karoubi (simplicial_object C)) (n : ℕ) :
+  (((alternating_face_map_complex.obj (karoubi_functor_category_embedding.obj P)).d (n+1) n).f) =
+    P.p.app (op [n+1]) ≫ ((alternating_face_map_complex.obj P.X).d (n+1) n) :=
+begin
+  dsimp,
+  simpa only [alternating_face_map_complex.obj_d_eq, karoubi.sum_hom,
+    preadditive.comp_sum, karoubi.zsmul_hom, preadditive.comp_zsmul],
+end
+
 namespace alternating_face_map_complex
 
 /-- The natural transformation which gives the augmentation of the alternating face map

src/algebraic_topology/dold_kan/n_reflects_iso.lean

@@ -7,17 +7,16 @@ Authors: Joël Riou
 import algebraic_topology.dold_kan.functor_n
 import algebraic_topology.dold_kan.decomposition
 import category_theory.idempotents.homological_complex
+import category_theory.idempotents.karoubi_karoubi
 
 /-!
 
 # N₁ and N₂ reflects isomorphisms
 
-In this file, it is shown that the functor
-`N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)`
-reflects isomorphisms for any preadditive category `C`.
-
-TODO @joelriou: deduce that `N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ)`
-also reflects isomorphisms.
+In this file, it is shown that the functors
+`N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)` and
+`N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ))`
+reflect isomorphisms for any preadditive category `C`.
 
 -/
 
@@ -69,6 +68,56 @@ instance : reflects_isomorphisms (N₁ : simplicial_object C ⥤ karoubi (chain_
     tauto, },
 end⟩
 
+lemma compatibility_N₂_N₁_karoubi :
+  N₂ ⋙ (karoubi_chain_complex_equivalence C ℕ).functor =
+  karoubi_functor_category_embedding simplex_categoryᵒᵖ C ⋙ N₁ ⋙
+  (karoubi_chain_complex_equivalence (karoubi C) ℕ).functor ⋙
+  functor.map_homological_complex (karoubi_karoubi.equivalence C).inverse _ :=
+begin
+  refine category_theory.functor.ext (λ P, _) (λ P Q f, _),
+  { refine homological_complex.ext _ _,
+    { ext n,
+      { dsimp,
+        simp only [karoubi_P_infty_f, comp_id, P_infty_f_naturality, id_comp], },
+      { refl, }, },
+    { rintros _ n (rfl : n+1 = _),
+      ext,
+      have h := (alternating_face_map_complex.map P.p).comm (n+1) n,
+      dsimp [N₂, karoubi_chain_complex_equivalence, karoubi_karoubi.inverse,
+        karoubi_homological_complex_equivalence.functor.obj] at ⊢ h,
+      simp only [karoubi.comp_f, assoc, karoubi.eq_to_hom_f, eq_to_hom_refl, id_comp, comp_id,
+        karoubi_alternating_face_map_complex_d, karoubi_P_infty_f,
+        ← homological_complex.hom.comm_assoc, ← h, app_idem_assoc], }, },
+  { ext n,
+    dsimp [karoubi_karoubi.inverse, karoubi_functor_category_embedding,
+      karoubi_functor_category_embedding.map],
+    simp only [karoubi.comp_f, karoubi_P_infty_f, homological_complex.eq_to_hom_f,
+      karoubi.eq_to_hom_f, assoc, comp_id, P_infty_f_naturality, app_p_comp,
+      karoubi_chain_complex_equivalence_functor_obj_X_p, N₂_obj_p_f, eq_to_hom_refl,
+      P_infty_f_naturality_assoc, app_comp_p, P_infty_f_idem_assoc], },
+end
+
+/-- We deduce that `N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ))`
+reflects isomorphisms from the fact that
+`N₁ : simplicial_object (karoubi C) ⥤ karoubi (chain_complex (karoubi C) ℕ)` does. -/
+instance : reflects_isomorphisms
+  (N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ)) := ⟨λ X Y f,
+begin
+  introI,
+  -- The following functor `F` reflects isomorphism because it is
+  -- a composition of four functors which reflects isomorphisms.
+  -- Then, it suffices to show that `F.map f` is an isomorphism.
+  let F := karoubi_functor_category_embedding simplex_categoryᵒᵖ C ⋙ N₁ ⋙
+    (karoubi_chain_complex_equivalence (karoubi C) ℕ).functor ⋙
+    functor.map_homological_complex (karoubi_karoubi.equivalence C).inverse
+      (complex_shape.down ℕ),
+  haveI : is_iso (F.map f),
+  { dsimp only [F],
+    rw [← compatibility_N₂_N₁_karoubi, functor.comp_map],
+    apply functor.map_is_iso, },
+  exact is_iso_of_reflects_iso f F,
+end⟩
+
 end dold_kan
 
 end algebraic_topology

src/category_theory/idempotents/karoubi.lean

@@ -246,6 +246,11 @@ lemma decomp_id_p_naturality {P Q : karoubi C} (f : P ⟶ Q) : decomp_id_p P ≫
   (⟨f.f, by erw [comp_id, id_comp]⟩ : (P.X : karoubi C) ⟶ Q.X) ≫ decomp_id_p Q :=
 by { ext, simp only [comp_f, decomp_id_p_f, karoubi.comp_p, karoubi.p_comp], }
 
+@[simp]
+lemma zsmul_hom [preadditive C] {P Q : karoubi C} (n : ℤ) (f : P ⟶ Q) :
+  (n • f).f = n • f.f :=
+map_zsmul (inclusion_hom P Q) n f
+
 end karoubi
 
 end idempotents