feat: the (contravariant) long exact sequence of Ext

Mathlib.lean

@@ -292,6 +292,9 @@ import Mathlib.Algebra.Homology.ComplexShapeSigns
 import Mathlib.Algebra.Homology.ConcreteCategory
 import Mathlib.Algebra.Homology.DerivedCategory.Basic
 import Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
+import Mathlib.Algebra.Homology.DerivedCategory.LargeExt
+import Mathlib.Algebra.Homology.DerivedCategory.ShortExact
+import Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
 import Mathlib.Algebra.Homology.DifferentialObject
 import Mathlib.Algebra.Homology.Embedding.Basic
 import Mathlib.Algebra.Homology.Exact
@@ -316,6 +319,7 @@ import Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
 import Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
 import Mathlib.Algebra.Homology.HomotopyCategory.Shift
 import Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
+import Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
 import Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
 import Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
 import Mathlib.Algebra.Homology.HomotopyCofiber
@@ -326,6 +330,7 @@ import Mathlib.Algebra.Homology.Localization
 import Mathlib.Algebra.Homology.ModuleCat
 import Mathlib.Algebra.Homology.Opposite
 import Mathlib.Algebra.Homology.QuasiIso
+import Mathlib.Algebra.Homology.Refinements
 import Mathlib.Algebra.Homology.ShortComplex.Ab
 import Mathlib.Algebra.Homology.ShortComplex.Abelian
 import Mathlib.Algebra.Homology.ShortComplex.Basic
@@ -1600,6 +1605,7 @@ import Mathlib.CategoryTheory.Shift.Pullback
 import Mathlib.CategoryTheory.Shift.Quotient
 import Mathlib.CategoryTheory.Shift.ShiftSequence
 import Mathlib.CategoryTheory.Shift.ShiftedHom
+import Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
 import Mathlib.CategoryTheory.Shift.SingleFunctors
 import Mathlib.CategoryTheory.Sigma.Basic
 import Mathlib.CategoryTheory.Simple
@@ -1684,6 +1690,7 @@ import Mathlib.CategoryTheory.Triangulated.Subcategory
 import Mathlib.CategoryTheory.Triangulated.TStructure.Basic
 import Mathlib.CategoryTheory.Triangulated.TriangleShift
 import Mathlib.CategoryTheory.Triangulated.Triangulated
+import Mathlib.CategoryTheory.Triangulated.Yoneda
 import Mathlib.CategoryTheory.Types
 import Mathlib.CategoryTheory.UnivLE
 import Mathlib.CategoryTheory.Whiskering

Mathlib/Algebra/Homology/DerivedCategory/Basic.lean

@@ -5,6 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
 import Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
+import Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
 import Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
 import Mathlib.Algebra.Homology.Localization
 
@@ -47,7 +48,7 @@ instance should be obtained at the beginning of the proof, using the term
 ## TODO (@joelriou)
 
 - construct the distinguished triangle associated to a short exact sequence
-of cochain complexes, and compare the associated connecting homomorphism
+of cochain complexes (done), and compare the associated connecting homomorphism
 with the one defined in `Algebra.Homology.HomologySequence`.
 - refactor the definition of Ext groups using morphisms in the derived category
 (which may be shrunk to the universe `v` at least when `C` has enough projectives
@@ -61,7 +62,7 @@ or enough injectives).
 
 universe w v u
 
-open CategoryTheory Limits
+open CategoryTheory Limits Pretriangulated
 
 variable (C : Type u) [Category.{v} C] [Abelian C]
 
@@ -131,6 +132,11 @@ instance : (Q (C := C)).IsLocalization
   dsimp only [Q, DerivedCategory]
   infer_instance
 
+instance {K L : CochainComplex C ℤ} (f : K ⟶ L) [QuasiIso f] :
+    IsIso (Q.map f) :=
+  Localization.inverts Q (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) _
+    (inferInstanceAs (QuasiIso f))
+
 /-- The localization functor `HomotopyCategory C (ComplexShape.up ℤ) ⥤ DerivedCategory C`. -/
 def Qh : HomotopyCategory C (ComplexShape.up ℤ) ⥤ DerivedCategory C :=
   HomologicalComplexUpToQuasiIso.Qh
@@ -167,6 +173,12 @@ noncomputable instance : HasShift (DerivedCategory C) ℤ :=
 noncomputable instance : (Qh (C := C)).CommShift ℤ :=
   Functor.CommShift.localized Qh (HomotopyCategory.subcategoryAcyclic C).W ℤ
 
+noncomputable instance : (Q (C := C)).CommShift ℤ :=
+  Functor.CommShift.ofIso (quotientCompQhIso C) ℤ
+
+instance : NatTrans.CommShift (quotientCompQhIso C).hom ℤ :=
+  Functor.CommShift.ofIso_compatibility (quotientCompQhIso C) ℤ
+
 instance (n : ℤ) : (shiftFunctor (DerivedCategory C) n).Additive := by
   rw [Localization.functor_additive_iff
     Qh (HomotopyCategory.subcategoryAcyclic C).W]
@@ -195,4 +207,53 @@ instance {D : Type*} [Category D] : ((whiskeringLeft _ _ D).obj (Qh (C := C))).F
   inferInstanceAs
     (Localization.whiskeringLeftFunctor' _ (HomotopyCategory.quasiIso _ _) D).Faithful
 
+variable {C}
+
+lemma mem_distTriang_iff (T : Triangle (DerivedCategory C)) :
+    (T ∈ distTriang (DerivedCategory C)) ↔ ∃ (X Y : CochainComplex C ℤ) (f : X ⟶ Y),
+      Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f)) := by
+  constructor
+  · rintro ⟨T', e, ⟨X, Y, f, ⟨e'⟩⟩⟩
+    refine ⟨_, _, f, ⟨?_⟩⟩
+    exact e ≪≫ Qh.mapTriangle.mapIso e' ≪≫
+      (Functor.mapTriangleCompIso (HomotopyCategory.quotient C _) Qh).symm.app _ ≪≫
+      (Functor.mapTriangleIso (quotientCompQhIso C)).app _
+  · rintro ⟨X, Y, f, ⟨e⟩⟩
+    refine isomorphic_distinguished _ (Qh.map_distinguished _ ?_) _
+      (e ≪≫ (Functor.mapTriangleIso (quotientCompQhIso C)).symm.app _ ≪≫
+      (Functor.mapTriangleCompIso (HomotopyCategory.quotient C _) Qh).app _)
+    exact ⟨_, _, f, ⟨Iso.refl _⟩⟩
+
+variable (C)
+
+/-- The single functors `C ⥤ DerivedCategory C` for all `n : ℤ` along with
+their compatibilities with shifts. -/
+noncomputable def singleFunctors : SingleFunctors C (DerivedCategory C) ℤ :=
+  (HomotopyCategory.singleFunctors C).postcomp Qh
+
+/-- The shift functor `C ⥤ DerivedCategory C` which sends `X : C` to the
+single cochain complex with `X` sitting in degree `n : ℤ`. -/
+noncomputable abbrev singleFunctor (n : ℤ) := (singleFunctors C).functor n
+
+instance (n : ℤ) : (singleFunctor C n).Additive := by
+  dsimp [singleFunctor, singleFunctors]
+  infer_instance
+
+/-- The isomorphism
+`DerivedCategory.singleFunctors C ≅ (HomotopyCategory.singleFunctors C).postcomp Qh` given
+by the definition of `DerivedCategory.singleFunctors`. -/
+noncomputable def singleFunctorsPostcompQhIso :
+    singleFunctors C ≅ (HomotopyCategory.singleFunctors C).postcomp Qh :=
+  Iso.refl _
+
+/-- The isomorphism
+`DerivedCategory.singleFunctors C ≅ (CochainComplex.singleFunctors C).postcomp Q`. -/
+noncomputable def singleFunctorsPostcompQIso :
+    singleFunctors C ≅ (CochainComplex.singleFunctors C).postcomp Q :=
+  (SingleFunctors.postcompFunctor C ℤ (Qh : _ ⥤ DerivedCategory C)).mapIso
+    (HomotopyCategory.singleFunctorsPostcompQuotientIso C) ≪≫
+      (CochainComplex.singleFunctors C).postcompPostcompIso (HomotopyCategory.quotient _ _) Qh ≪≫
+      SingleFunctors.postcompIsoOfIso
+        (CochainComplex.singleFunctors C) (quotientCompQhIso C)
+
 end DerivedCategory