feat(Algebra/Homology): acyclic complexes

Mathlib/Algebra/Homology/QuasiIso.lean

@@ -79,6 +79,12 @@ lemma quasiIsoAt_iff_exactAt' (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHom
   · intro hK
     exact ⟨⟨0, IsZero.eq_of_src hK _ _, IsZero.eq_of_tgt hL _ _⟩⟩
 
+lemma exactAt_iff_of_quasiIsoAt (f : K ⟶ L) (i : ι)
+    [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] :
+    K.ExactAt i ↔ L.ExactAt i :=
+  ⟨fun hK => (quasiIsoAt_iff_exactAt f i hK).1 inferInstance,
+    fun hL => (quasiIsoAt_iff_exactAt' f i hL).1 inferInstance⟩
+
 instance (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [hf : QuasiIsoAt f i] :
     IsIso (homologyMap f i) := by
   simpa only [quasiIsoAt_iff, ShortComplex.quasiIso_iff] using hf

Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean

@@ -614,6 +614,23 @@ lemma exactAt_iff_isZero_homology [K.HasHomology i] :
   dsimp [homology]
   rw [exactAt_iff, ShortComplex.exact_iff_isZero_homology]
 
+/-- A homological complex `K` is acyclic if it is exact at `i` for any `i`. -/
+def Acyclic := ∀ i, K.ExactAt i
+
+lemma acyclic_iff :
+    K.Acyclic ↔ ∀ i, K.ExactAt i := by rfl
+
+lemma acyclic_of_isZero (hK : IsZero K) :
+    K.Acyclic := by
+  rw [acyclic_iff]
+  intro i
+  apply ShortComplex.exact_of_isZero_X₂
+  dsimp
+  rw [IsZero.iff_id_eq_zero]
+  change 𝟙 ((eval _ _ i).obj K) = 0
+  rw [← CategoryTheory.Functor.map_id, hK.eq_of_src (𝟙 K) 0]
+  simp
+
 end HomologicalComplex
 
 namespace ChainComplex

Mathlib/Algebra/Homology/ShortComplex/Homology.lean

@@ -1173,6 +1173,53 @@ instance epi_homologyMap_of_epi_cyclesMap
     Epi (homologyMap φ) :=
   epi_homologyMap_of_epi_cyclesMap' φ inferInstance
 
+/-- Given a short complex `S` such that `S.HasHomology`, this is the canonical
+left homology data for `S` whose `K` and `H` fields are
+respectively `S.cycles` and `S.homology`. -/
+@[simps!]
+noncomputable def LeftHomologyData.canonical [S.HasHomology] : S.LeftHomologyData where
+  K := S.cycles
+  H := S.homology
+  i := S.iCycles
+  π := S.homologyπ
+  wi := by simp
+  hi := S.cyclesIsKernel
+  wπ := S.toCycles_comp_homologyπ
+  hπ := S.homologyIsCokernel
+
+/-- Computation of the `f'` field of `LeftHomologyData.canonical`. -/
+@[simp]
+lemma LeftHomologyData.canonical_f' [S.HasHomology] :
+    (LeftHomologyData.canonical S).f' = S.toCycles := rfl
+
+/-- Given a short complex `S` such that `S.HasHomology`, this is the canonical
+right homology data for `S` whose `Q` and `H` fields are
+respectively `S.opcycles` and `S.homology`. -/
+@[simps!]
+noncomputable def RightHomologyData.canonical [S.HasHomology] : S.RightHomologyData where
+  Q := S.opcycles
+  H := S.homology
+  p := S.pOpcycles
+  ι := S.homologyι
+  wp := by simp
+  hp := S.opcyclesIsCokernel
+  wι := S.homologyι_comp_fromOpcycles
+  hι := S.homologyIsKernel
+
+/-- Computation of the `g'` field of `RightHomologyData.canonical`. -/
+@[simp]
+lemma RightHomologyData.canonical_g' [S.HasHomology] :
+    (RightHomologyData.canonical S).g' = S.fromOpcycles := rfl
+
+/-- Given a short complex `S` such that `S.HasHomology`, this is the canonical
+homology data for `S` whose `left.K`, `left/right.H` and `right.Q` fields are
+respectively `S.cycles`, `S.homology` and `S.opcycles`. -/
+@[simps!]
+noncomputable def HomologyData.canonical [S.HasHomology] : S.HomologyData where
+  left := LeftHomologyData.canonical S
+  right := RightHomologyData.canonical S
+  iso := Iso.refl _
+
 end ShortComplex
 
 end CategoryTheory