feat(Algebra/Homology): more API for the HomComplex from a single cochain complex (#32461)

Author: joelriou

Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

@@ -599,7 +599,7 @@ instance : Coe (Cocycle F G n) (Cochain F G n) where
   coe x := x.1
 
 @[ext]
-lemma ext (z₁ z₂ : Cocycle F G n) (h : (z₁ : Cochain F G n) = z₂) : z₁ = z₂ :=
+lemma ext {z₁ z₂ : Cocycle F G n} (h : (z₁ : Cochain F G n) = z₂) : z₁ = z₂ :=
   Subtype.ext h
 
 instance : SMul R (Cocycle F G n) where

Mathlib/Algebra/Homology/HomotopyCategory/HomComplexCohomology.lean

@@ -53,6 +53,18 @@ def coboundaries : AddSubgroup (Cocycle K L n) where
     rintro α ⟨m, hm, β, hβ⟩
     exact ⟨m, hm, -β, by aesop⟩
 
+variable {K L n} in
+lemma mem_coboundaries_iff (α : Cocycle K L n) (m : ℤ) (hm : m + 1 = n) :
+    α ∈ coboundaries K L n ↔ ∃ (β : Cochain K L m), δ m n β = α := by
+  simp only [coboundaries, exists_prop, AddSubgroup.mem_mk, AddSubmonoid.mem_mk,
+    AddSubsemigroup.mem_mk, Set.mem_setOf_eq]
+  constructor
+  · rintro ⟨m', hm', β, hβ⟩
+    obtain rfl : m = m' := by lia
+    exact ⟨β, hβ⟩
+  · rintro ⟨β, hβ⟩
+    exact ⟨m, hm, β, hβ⟩
+
 /-- The type of cohomology classes of degree `n` in the complex of morphisms
 from `K` to `L`. -/
 def CohomologyClass : Type v := Cocycle K L n ⧸ coboundaries K L n
@@ -146,6 +158,7 @@ lemma toHom_mk_eq_zero_iff (x : Cocycle K L n) :
   · rw [← mk_eq_zero_iff] at h
     rw [h, map_zero]
 
+variable (K L n) in
 lemma toHom_bijective : Function.Bijective (toHom : CohomologyClass K L n → _) := by
   refine ⟨fun x y h ↦ ?_, fun f ↦ ?_⟩
   · obtain ⟨x, rfl⟩ := x.mk_surjective
@@ -160,7 +173,7 @@ lemma toHom_bijective : Function.Bijective (toHom : CohomologyClass K L n → _)
 noncomputable def homAddEquiv :
     CohomologyClass K L n ≃+
       ((HomotopyCategory.quotient C _).obj K ⟶ (HomotopyCategory.quotient C _).obj (L⟦n⟧)) :=
-  AddEquiv.ofBijective toHom toHom_bijective
+  AddEquiv.ofBijective toHom (toHom_bijective _ _ _)
 
 end CohomologyClass
 

Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean

@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
+public import Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
 public import Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
 
 /-!
@@ -68,6 +68,40 @@ lemma δ_fromSingleMk {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q)
   · simp [δ_shape n n' (by lia), HomologicalComplex.shape K q q' (by simp; lia),
       fromSingleMk]
 
+/-- Cochains of degree `n` from `(singleFunctor C p).obj X` to `K` identify
+to `X ⟶ K.X q` when `p + n = q`. -/
+noncomputable def fromSingleEquiv {p q n : ℤ} (h : p + n = q) :
+    Cochain ((singleFunctor C p).obj X) K n ≃+ (X ⟶ K.X q) where
+  toFun α := (HomologicalComplex.singleObjXSelf (.up ℤ) p X).inv ≫ α.v p q h
+  invFun f := fromSingleMk f h
+  left_inv α := by
+    ext p' q' hpq'
+    by_cases hp : p' = p
+    · aesop
+    · exact (HomologicalComplex.isZero_single_obj_X _ _ _ _ hp).eq_of_src _ _
+  right_inv f := by simp
+  map_add' := by simp
+
+@[simp]
+lemma fromSingleMk_add {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ} (h : p + n = q) :
+    fromSingleMk (f + g) h = fromSingleMk f h + fromSingleMk g h :=
+  (fromSingleEquiv h).symm.map_add _ _
+
+@[simp]
+lemma fromSingleMk_sub {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ} (h : p + n = q) :
+    fromSingleMk (f - g) h = fromSingleMk f h - fromSingleMk g h :=
+  (fromSingleEquiv h).symm.map_sub _ _
+
+@[simp]
+lemma fromSingleMk_neg {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) :
+    fromSingleMk (-f) h = -fromSingleMk f h :=
+  (fromSingleEquiv h).symm.map_neg _
+
+lemma fromSingleMk_surjective {p n : ℤ} (α : Cochain ((singleFunctor C p).obj X) K n)
+    (q : ℤ) (h : p + n = q) :
+    ∃ (f : X ⟶ K.X q), fromSingleMk f h = α :=
+  (fromSingleEquiv h).symm.surjective α
+
 /-- Constructor for cochains to a single complex. -/
 @[nolint unusedArguments]
 noncomputable def toSingleMk {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (_ : p + n = q) :
@@ -113,6 +147,54 @@ noncomputable def fromSingleMk {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p +
     rw [Cochain.δ_fromSingleMk _ _ _ q' (by lia), hf]
     simp)
 
+lemma fromSingleMk_surjective {p n : ℤ} (α : Cocycle ((singleFunctor C p).obj X) K n)
+    (q : ℤ) (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') :
+    ∃ (f : X ⟶ K.X q) (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α := by
+  obtain ⟨f, hf⟩ := Cochain.fromSingleMk_surjective α.1 q h
+  have hα := α.δ_eq_zero (n + 1)
+  rw [← hf, Cochain.δ_fromSingleMk _ _ _ q' (by lia)] at hα
+  replace hα := Cochain.congr_v hα p q' (by lia)
+  exact ⟨f, by simpa using hα, by ext : 1; assumption⟩
+
+lemma fromSingleMk_add {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ} (h : p + n = q)
+    (q' : ℤ) (hq' : q + 1 = q') (hf : f ≫ K.d q q' = 0) (hg : g ≫ K.d q q' = 0) :
+    fromSingleMk (f + g) h q' hq' (by simp [hf, hg]) =
+      fromSingleMk f h q' hq' hf + fromSingleMk g h q' hq' hg := by
+  cat_disch
+
+lemma fromSingleMk_sub {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ} (h : p + n = q)
+    (q' : ℤ) (hq' : q + 1 = q') (hf : f ≫ K.d q q' = 0) (hg : g ≫ K.d q q' = 0) :
+    fromSingleMk (f - g) h q' hq' (by simp [hf, hg]) =
+      fromSingleMk f h q' hq' hf - fromSingleMk g h q' hq' hg := by
+  cat_disch
+
+lemma fromSingleMk_neg {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q)
+    (q' : ℤ) (hq' : q + 1 = q') (hf : f ≫ K.d q q' = 0) :
+    fromSingleMk (-f) h q' hq' (by simp [hf]) = - fromSingleMk f h q' hq' hf := by
+  cat_disch
+
+variable (X K) in
+@[simp]
+lemma fromSingleMk_zero {p q : ℤ} {n : ℤ} (h : p + n = q)
+    (q' : ℤ) (hq' : q + 1 = q') :
+    fromSingleMk (0 : X ⟶ K.X q) h q' hq' (by simp) = 0 := by
+  cat_disch
+
+lemma fromSingleMk_mem_coboundaries_iff {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q)
+    (q' : ℤ) (hq' : q + 1 = q') (hf : f ≫ K.d q q' = 0)
+    (q'' : ℤ) (hq'' : q'' + 1 = q) :
+    fromSingleMk f h q' hq' hf ∈ coboundaries _ _ _ ↔
+      ∃ (g : X ⟶ K.X q''), g ≫ K.d q'' q = f := by
+  rw [mem_coboundaries_iff _ (n - 1) (by simp)]
+  constructor
+  · rintro ⟨α, hα⟩
+    obtain ⟨g, hg⟩ := Cochain.fromSingleMk_surjective α q'' (by lia)
+    refine ⟨g, ?_⟩
+    rw [← hg, fromSingleMk_coe, Cochain.δ_fromSingleMk _ _ _ _ h] at hα
+    exact (Cochain.fromSingleEquiv h).symm.injective hα
+  · rintro ⟨g, rfl⟩
+    exact ⟨Cochain.fromSingleMk g (by lia), Cochain.δ_fromSingleMk _ _ _ _ h⟩
+
 /-- Constructor for cocycles to a single complex. -/
 @[simps!]
 noncomputable def toSingleMk {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q)