feat: port AlgebraicTopology.DoldKan.NReflectsIso (#3548)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

Mathlib.lean

@@ -303,6 +303,7 @@ import Mathlib.AlgebraicTopology.DoldKan.Decomposition
 import Mathlib.AlgebraicTopology.DoldKan.Faces
 import Mathlib.AlgebraicTopology.DoldKan.FunctorN
 import Mathlib.AlgebraicTopology.DoldKan.Homotopies
+import Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
 import Mathlib.AlgebraicTopology.DoldKan.Notations
 import Mathlib.AlgebraicTopology.DoldKan.PInfty
 import Mathlib.AlgebraicTopology.DoldKan.Projections

Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean

@@ -0,0 +1,127 @@
+/-
+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
+
+! This file was ported from Lean 3 source module algebraic_topology.dold_kan.n_reflects_iso
+! leanprover-community/mathlib commit 88bca0ce5d22ebfd9e73e682e51d60ea13b48347
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.AlgebraicTopology.DoldKan.FunctorN
+import Mathlib.AlgebraicTopology.DoldKan.Decomposition
+import Mathlib.CategoryTheory.Idempotents.HomologicalComplex
+import Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
+
+/-!
+
+# N₁ and N₂ reflects isomorphisms
+
+In this file, it is shown that the functors
+`N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)` and
+`N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ))`
+reflect isomorphisms for any preadditive category `C`.
+
+-/
+
+
+open CategoryTheory CategoryTheory.Category CategoryTheory.Idempotents Opposite Simplicial
+
+namespace AlgebraicTopology
+
+namespace DoldKan
+
+variable {C : Type _} [Category C] [Preadditive C]
+
+open MorphComponents
+
+instance : ReflectsIsomorphisms (N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)) :=
+  ⟨fun {X Y} f => by
+    intro
+    -- restating the result in a way that allows induction on the degree n
+    suffices ∀ n : ℕ, IsIso (f.app (op [n])) by
+      haveI : ∀ Δ : SimplexCategoryᵒᵖ, IsIso (f.app Δ) := fun Δ => this Δ.unop.len
+      apply NatIso.isIso_of_isIso_app
+    -- restating the assumption in a more practical form
+    have h₁ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.hom_inv_id (N₁.map f)))
+    have h₂ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.inv_hom_id (N₁.map f)))
+    have h₃ := fun n =>
+      Karoubi.HomologicalComplex.p_comm_f_assoc (inv (N₁.map f)) n (f.app (op [n]))
+    simp only [N₁_map_f, Karoubi.comp_f, HomologicalComplex.comp_f,
+      AlternatingFaceMapComplex.map_f, N₁_obj_p, Karoubi.id_eq, assoc] at h₁ h₂ h₃
+    -- we have to construct an inverse to f in degree n, by induction on n
+    intro n
+    induction' n with n hn
+    -- degree 0
+    · use (inv (N₁.map f)).f.f 0
+      have h₁₀ := h₁ 0
+      have h₂₀ := h₂ 0
+      dsimp at h₁₀ h₂₀
+      simp only [id_comp, comp_id] at h₁₀ h₂₀
+      tauto
+    · haveI := hn
+      use φ { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
+              b := fun i => inv (f.app (op [n])) ≫ X.σ i }
+      simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp,
+        PInfty_f_naturality_assoc, IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc,
+        SimplicialObject.σ_naturality, h₁, h₂, h₃]⟩
+
+theorem compatibility_N₂_N₁_karoubi :
+    N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor =
+      karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
+        N₁ ⋙ (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor ⋙
+            Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse _ := by
+  refine' CategoryTheory.Functor.ext (fun P => _) fun P Q f => _
+  · refine' HomologicalComplex.ext _ _
+    · ext n
+      · dsimp
+        simp only [karoubi_PInfty_f, comp_id, PInfty_f_naturality, id_comp, eqToHom_refl]
+      . rfl
+    · rintro _ n (rfl : n + 1 = _)
+      ext
+      have h := (AlternatingFaceMapComplex.map P.p).comm (n + 1) n
+      dsimp [N₂, karoubiChainComplexEquivalence,
+        KaroubiHomologicalComplexEquivalence.Functor.obj] at h ⊢
+      simp only [assoc, Karoubi.eqToHom_f, eqToHom_refl, comp_id,
+        karoubi_alternatingFaceMapComplex_d, karoubi_PInfty_f,
+        ← HomologicalComplex.Hom.comm_assoc, ← h, app_idem_assoc]
+  · ext n
+    dsimp [KaroubiKaroubi.inverse, Functor.mapHomologicalComplex]
+    simp only [karoubi_PInfty_f, HomologicalComplex.eqToHom_f, Karoubi.eqToHom_f,
+      assoc, comp_id, PInfty_f_naturality, app_p_comp,
+      karoubiChainComplexEquivalence_functor_obj_X_p, N₂_obj_p_f, eqToHom_refl,
+      PInfty_f_naturality_assoc, app_comp_p, PInfty_f_idem_assoc]
+set_option linter.uppercaseLean3 false in
+#align algebraic_topology.dold_kan.compatibility_N₂_N₁_karoubi AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi
+
+/-- We deduce that `N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ))`
+reflects isomorphisms from the fact that
+`N₁ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ)` does. -/
+instance : ReflectsIsomorphisms (N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ)) :=
+  ⟨fun f => by
+    intro
+    -- 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₁ := karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
+    let F₂ : SimplicialObject (Karoubi C) ⥤ _ := N₁
+    let F₃ := (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
+    let F₄ := Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse
+      (ComplexShape.down ℕ)
+    let F := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
+    -- porting note: we have to help Lean4 find the `ReflectsIsomorphisms` instances
+    -- could this be fixed by setting better instance priorities?
+    haveI : ReflectsIsomorphisms F₁ := reflectsIsomorphisms_of_full_and_faithful _
+    haveI : ReflectsIsomorphisms F₂ := by infer_instance
+    haveI : ReflectsIsomorphisms F₃ := reflectsIsomorphisms_of_full_and_faithful _
+    haveI : ReflectsIsomorphisms ((KaroubiKaroubi.equivalence C).inverse) :=
+      reflectsIsomorphisms_of_full_and_faithful _
+    have : IsIso (F.map f) := by
+      simp only
+      rw [← compatibility_N₂_N₁_karoubi, Functor.comp_map]
+      apply Functor.map_isIso
+    exact isIso_of_reflects_iso f F⟩
+
+end DoldKan
+
+end AlgebraicTopology

Mathlib/CategoryTheory/Functor/ReflectsIso.lean

@@ -52,13 +52,15 @@ theorem isIso_of_reflects_iso {A B : C} (f : A ⟶ B) (F : C ⥤ D) [IsIso (F.ma
   ReflectsIsomorphisms.reflects F f
 #align category_theory.is_iso_of_reflects_iso CategoryTheory.isIso_of_reflects_iso
 
-instance (priority := 100) of_full_and_faithful (F : C ⥤ D) [Full F] [Faithful F] :
+instance (priority := 100) reflectsIsomorphisms_of_full_and_faithful
+    (F : C ⥤ D) [Full F] [Faithful F] :
     ReflectsIsomorphisms F
     where reflects f i :=
     ⟨⟨F.preimage (inv (F.map f)), ⟨F.map_injective (by simp), F.map_injective (by simp)⟩⟩⟩
-#align category_theory.of_full_and_faithful CategoryTheory.of_full_and_faithful
+#align category_theory.of_full_and_faithful CategoryTheory.reflectsIsomorphisms_of_full_and_faithful
 
-instance (F : C ⥤ D) (G : D ⥤ E) [ReflectsIsomorphisms F] [ReflectsIsomorphisms G] :
+instance reflectsIsomorphisms_of_comp (F : C ⥤ D) (G : D ⥤ E)
+    [ReflectsIsomorphisms F] [ReflectsIsomorphisms G] :
     ReflectsIsomorphisms (F ⋙ G) :=
   ⟨fun f (hf : IsIso (G.map _)) => by
     haveI := isIso_of_reflects_iso (F.map f) G