refactor(Algebra/Homology): remove single₀ (#8208)

This PR removes the special definitions of `single₀` for chain and cochain complexes, so as to avoid duplication of code with `HomologicalComplex.single` which is the functor constructing the complex that is supported by a single arbitrary degree. `single₀` was supposed to have better definitional properties, but it turns out that in Lean4, it is no longer true (at least for the action of this functor on objects). The computation of the homology of these single complexes is generalized for `HomologicalComplex.single` using the new homology API: this result is moved to a separate file `Algebra.Homology.SingleHomology`.

Author: joelriou

Mathlib.lean

@@ -259,6 +259,7 @@ import Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
 import Mathlib.Algebra.Homology.ShortExact.Abelian
 import Mathlib.Algebra.Homology.ShortExact.Preadditive
 import Mathlib.Algebra.Homology.Single
+import Mathlib.Algebra.Homology.SingleHomology
 import Mathlib.Algebra.IndicatorFunction
 import Mathlib.Algebra.Invertible.Basic
 import Mathlib.Algebra.Invertible.Defs

Mathlib/Algebra/Homology/Additive.lean

@@ -21,10 +21,6 @@ TODO: similarly for `R`-linear.
 
 universe v u
 
-open Classical
-
-noncomputable section
-
 open CategoryTheory CategoryTheory.Category CategoryTheory.Limits HomologicalComplex
 
 variable {ι : Type*}
@@ -276,12 +272,11 @@ variable [HasZeroObject V] {W : Type*} [Category W] [Preadditive W] [HasZeroObje
 
 namespace HomologicalComplex
 
-attribute [local simp] eqToHom_map
-
 /-- Turning an object into a complex supported at `j` then applying a functor is
 the same as applying the functor then forming the complex.
 -/
-def singleMapHomologicalComplex (F : V ⥤ W) [F.Additive] (c : ComplexShape ι) (j : ι) :
+noncomputable def singleMapHomologicalComplex (F : V ⥤ W) [F.Additive] (c : ComplexShape ι)
+    [DecidableEq ι] (j : ι) :
     single V c j ⋙ F.mapHomologicalComplex _ ≅ F ⋙ single W c j :=
   NatIso.ofComponents
     (fun X =>
@@ -292,27 +287,30 @@ def singleMapHomologicalComplex (F : V ⥤ W) [F.Additive] (c : ComplexShape ι)
           dsimp
           split_ifs with h
           · simp [h]
-          · rw [zero_comp, if_neg h]
-            exact (zero_of_source_iso_zero _ F.mapZeroObject).symm
+          · rw [zero_comp, ← F.map_id,
+              (isZero_single_obj_X c j X _ h).eq_of_src (𝟙 _) 0, F.map_zero]
         inv_hom_id := by
           ext i
           dsimp
           split_ifs with h
           · simp [h]
-          · rw [zero_comp, if_neg h]
-            simp })
+          · apply (isZero_single_obj_X c j _ _ h).eq_of_src })
     fun f => by
-    ext i
-    dsimp
-    split_ifs with h <;> simp [h]
+      ext i
+      dsimp
+      split_ifs with h
+      · subst h
+        simp [single_map_f_self, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]
+      · apply (isZero_single_obj_X c j _ _ h).eq_of_tgt
 #align homological_complex.single_map_homological_complex HomologicalComplex.singleMapHomologicalComplex
 
-variable (F : V ⥤ W) [Functor.Additive F] (c)
+variable (F : V ⥤ W) [Functor.Additive F] (c) [DecidableEq ι]
 
 @[simp]
 theorem singleMapHomologicalComplex_hom_app_self (j : ι) (X : V) :
-    ((singleMapHomologicalComplex F c j).hom.app X).f j = eqToHom (by simp) := by
-  simp [singleMapHomologicalComplex]
+    ((singleMapHomologicalComplex F c j).hom.app X).f j =
+      F.map (singleObjXSelf c j X).hom ≫ (singleObjXSelf c j (F.obj X)).inv := by
+  simp [singleMapHomologicalComplex, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]
 #align homological_complex.single_map_homological_complex_hom_app_self HomologicalComplex.singleMapHomologicalComplex_hom_app_self
 
 @[simp]
@@ -323,8 +321,9 @@ theorem singleMapHomologicalComplex_hom_app_ne {i j : ι} (h : i ≠ j) (X : V)
 
 @[simp]
 theorem singleMapHomologicalComplex_inv_app_self (j : ι) (X : V) :
-    ((singleMapHomologicalComplex F c j).inv.app X).f j = eqToHom (by simp) := by
-  simp [singleMapHomologicalComplex]
+    ((singleMapHomologicalComplex F c j).inv.app X).f j =
+      (singleObjXSelf c j (F.obj X)).hom ≫ F.map (singleObjXSelf c j X).inv := by
+  simp [singleMapHomologicalComplex, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]
 #align homological_complex.single_map_homological_complex_inv_app_self HomologicalComplex.singleMapHomologicalComplex_inv_app_self
 
 @[simp]
@@ -334,115 +333,3 @@ theorem singleMapHomologicalComplex_inv_app_ne {i j : ι} (h : i ≠ j) (X : V)
 #align homological_complex.single_map_homological_complex_inv_app_ne HomologicalComplex.singleMapHomologicalComplex_inv_app_ne
 
 end HomologicalComplex
-
-namespace ChainComplex
-
-/-- Turning an object into a chain complex supported at zero then applying a functor is
-the same as applying the functor then forming the complex.
--/
-def single₀MapHomologicalComplex (F : V ⥤ W) [F.Additive] :
-    single₀ V ⋙ F.mapHomologicalComplex _ ≅ F ⋙ single₀ W :=
-  NatIso.ofComponents
-    (fun X =>
-      { hom :=
-          { f := fun i =>
-              match i with
-              | 0 => 𝟙 _
-              | _ + 1 => F.mapZeroObject.hom }
-        inv :=
-          { f := fun i =>
-              match i with
-              | 0 => 𝟙 _
-              | _ + 1 => F.mapZeroObject.inv }
-        hom_inv_id := by
-          ext (_|_)
-          · simp
-          · exact IsZero.eq_of_src (IsZero.of_iso (isZero_zero _) F.mapZeroObject) _ _
-        inv_hom_id := by
-          ext (_|_)
-          · simp
-          · exact IsZero.eq_of_src (isZero_zero _) _ _ })
-    fun f => by ext (_|_) <;> simp
-#align chain_complex.single₀_map_homological_complex ChainComplex.single₀MapHomologicalComplex
-
-@[simp]
-theorem single₀MapHomologicalComplex_hom_app_zero (F : V ⥤ W) [F.Additive] (X : V) :
-    ((single₀MapHomologicalComplex F).hom.app X).f 0 = 𝟙 _ :=
-  rfl
-#align chain_complex.single₀_map_homological_complex_hom_app_zero ChainComplex.single₀MapHomologicalComplex_hom_app_zero
-
-@[simp]
-theorem single₀MapHomologicalComplex_hom_app_succ (F : V ⥤ W) [F.Additive] (X : V) (n : ℕ) :
-    ((single₀MapHomologicalComplex F).hom.app X).f (n + 1) = 0 :=
-  rfl
-#align chain_complex.single₀_map_homological_complex_hom_app_succ ChainComplex.single₀MapHomologicalComplex_hom_app_succ
-
-@[simp]
-theorem single₀MapHomologicalComplex_inv_app_zero (F : V ⥤ W) [F.Additive] (X : V) :
-    ((single₀MapHomologicalComplex F).inv.app X).f 0 = 𝟙 _ :=
-  rfl
-#align chain_complex.single₀_map_homological_complex_inv_app_zero ChainComplex.single₀MapHomologicalComplex_inv_app_zero
-
-@[simp]
-theorem single₀MapHomologicalComplex_inv_app_succ (F : V ⥤ W) [F.Additive] (X : V) (n : ℕ) :
-    ((single₀MapHomologicalComplex F).inv.app X).f (n + 1) = 0 :=
-  rfl
-#align chain_complex.single₀_map_homological_complex_inv_app_succ ChainComplex.single₀MapHomologicalComplex_inv_app_succ
-
-end ChainComplex
-
-namespace CochainComplex
-
-/-- Turning an object into a cochain complex supported at zero then applying a functor is
-the same as applying the functor then forming the cochain complex.
--/
-def single₀MapHomologicalComplex (F : V ⥤ W) [F.Additive] :
-    single₀ V ⋙ F.mapHomologicalComplex _ ≅ F ⋙ single₀ W :=
-  NatIso.ofComponents
-    (fun X =>
-      { hom :=
-          { f := fun i =>
-              match i with
-              | 0 => 𝟙 _
-              | _ + 1 => F.mapZeroObject.hom }
-        inv :=
-          { f := fun i =>
-              match i with
-              | 0 => 𝟙 _
-              | _ + 1 => F.mapZeroObject.inv }
-        hom_inv_id := by
-          ext (_|_)
-          · simp
-          · exact IsZero.eq_of_src (IsZero.of_iso (isZero_zero _) F.mapZeroObject) _ _
-        inv_hom_id := by
-          ext (_|_)
-          · simp
-          · exact IsZero.eq_of_src (isZero_zero _) _ _ })
-    fun f => by ext (_|_) <;> simp
-#align cochain_complex.single₀_map_homological_complex CochainComplex.single₀MapHomologicalComplex
-
-@[simp]
-theorem single₀MapHomologicalComplex_hom_app_zero (F : V ⥤ W) [F.Additive] (X : V) :
-    ((single₀MapHomologicalComplex F).hom.app X).f 0 = 𝟙 _ :=
-  rfl
-#align cochain_complex.single₀_map_homological_complex_hom_app_zero CochainComplex.single₀MapHomologicalComplex_hom_app_zero
-
-@[simp]
-theorem single₀MapHomologicalComplex_hom_app_succ (F : V ⥤ W) [F.Additive] (X : V) (n : ℕ) :
-    ((single₀MapHomologicalComplex F).hom.app X).f (n + 1) = 0 :=
-  rfl
-#align cochain_complex.single₀_map_homological_complex_hom_app_succ CochainComplex.single₀MapHomologicalComplex_hom_app_succ
-
-@[simp]
-theorem single₀MapHomologicalComplex_inv_app_zero (F : V ⥤ W) [F.Additive] (X : V) :
-    ((single₀MapHomologicalComplex F).inv.app X).f 0 = 𝟙 _ :=
-  rfl
-#align cochain_complex.single₀_map_homological_complex_inv_app_zero CochainComplex.single₀MapHomologicalComplex_inv_app_zero
-
-@[simp]
-theorem single₀MapHomologicalComplex_inv_app_succ (F : V ⥤ W) [F.Additive] (X : V) (n : ℕ) :
-    ((single₀MapHomologicalComplex F).inv.app X).f (n + 1) = 0 :=
-  rfl
-#align cochain_complex.single₀_map_homological_complex_inv_app_succ CochainComplex.single₀MapHomologicalComplex_inv_app_succ
-
-end CochainComplex

Mathlib/Algebra/Homology/QuasiIso.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Joël Riou
 -/
 import Mathlib.Algebra.Homology.Homotopy
-import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
+import Mathlib.Algebra.Homology.SingleHomology
 import Mathlib.CategoryTheory.Abelian.Homology
 
 #align_import algebra.homology.quasi_iso from "leanprover-community/mathlib"@"956af7c76589f444f2e1313911bad16366ea476d"
@@ -20,9 +20,7 @@ Define the derived category as the localization at quasi-isomorphisms? (TODO @jo
 -/
 
 
-open CategoryTheory
-
-open CategoryTheory.Limits
+open CategoryTheory Limits
 
 universe v u
 
@@ -133,8 +131,7 @@ theorem to_single₀_epi_at_zero [hf : QuasiIso' f] : Epi (f.f 0) := by
 
 theorem to_single₀_exact_d_f_at_zero [hf : QuasiIso' f] : Exact (X.d 1 0) (f.f 0) := by
   rw [Preadditive.exact_iff_homology'_zero]
-  have h : X.d 1 0 ≫ f.f 0 = 0 := by
-    simp only [← f.2 1 0 rfl, ChainComplex.single₀_obj_X_d, comp_zero]
+  have h : X.d 1 0 ≫ f.f 0 = 0 := by simp only [← f.comm 1 0, single_obj_d, comp_zero]
   refine' ⟨h, Nonempty.intro (homology'IsoKernelDesc _ _ _ ≪≫ _)⟩
   suffices IsIso (cokernel.desc _ _ h) by apply kernel.ofMono
   rw [← toSingle₀CokernelAtZeroIso_hom_eq]
@@ -186,8 +183,7 @@ theorem from_single₀_mono_at_zero [hf : QuasiIso' f] : Mono (f.f 0) := by
 
 theorem from_single₀_exact_f_d_at_zero [hf : QuasiIso' f] : Exact (f.f 0) (X.d 0 1) := by
   rw [Preadditive.exact_iff_homology'_zero]
-  have h : f.f 0 ≫ X.d 0 1 = 0 := by
-    simp only [HomologicalComplex.Hom.comm, CochainComplex.single₀_obj_X_d, zero_comp]
+  have h : f.f 0 ≫ X.d 0 1 = 0 := by simp
   refine' ⟨h, Nonempty.intro (homology'IsoCokernelLift _ _ _ ≪≫ _)⟩
   suffices IsIso (kernel.lift (X.d 0 1) (f.f 0) h) by apply cokernel.ofEpi
   rw [← fromSingle₀KernelAtZeroIso_inv_eq f]