feat(Algebra/Homology/SpectralObject): kernel and cokernel of differentials (#35359)

Author: joelriou

Mathlib.lean

@@ -662,6 +662,7 @@ public import Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
 public import Mathlib.Algebra.Homology.Single
 public import Mathlib.Algebra.Homology.SingleHomology
 public import Mathlib.Algebra.Homology.SpectralObject.Basic
+public import Mathlib.Algebra.Homology.SpectralObject.Cycles
 public import Mathlib.Algebra.Homology.SpectralSequence.Basic
 public import Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
 public import Mathlib.Algebra.Homology.Square

Mathlib/Algebra/Homology/SpectralObject/Basic.lean

@@ -59,16 +59,17 @@ variable {C ι} (X : SpectralObject C ι)
 
 section
 
-variable (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k)
-
 /-- The connecting homomorphism of the spectral object. -/
-def δ : (X.H n₀).obj (mk₁ g) ⟶ (X.H n₁).obj (mk₁ f) :=
+def δ {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) :
+    (X.H n₀).obj (mk₁ g) ⟶ (X.H n₁).obj (mk₁ f) :=
   (X.δ' n₀ n₁ hn₁).app (mk₂ f g)
 
 @[reassoc]
-lemma δ_naturality {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k')
-    (α : mk₁ f ⟶ mk₁ f') (β : mk₁ g ⟶ mk₁ g') (hαβ : α.app 1 = β.app 0 := by cat_disch) :
-    (X.H n₀).map β ≫ X.δ n₀ n₁ hn₁ f' g' = X.δ n₀ n₁ hn₁ f g ≫ (X.H n₁).map α := by
+lemma δ_naturality {i j k : ι} (f : i ⟶ j) (g : j ⟶ k)
+    {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k')
+    (α : mk₁ f ⟶ mk₁ f') (β : mk₁ g ⟶ mk₁ g')
+    (n₀ n₁ : ℤ) (hαβ : α.app 1 = β.app 0 := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) :
+    (X.H n₀).map β ≫ X.δ f' g' n₀ n₁ hn₁ = X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map α := by
   have h := (X.δ' n₀ n₁ hn₁).naturality
     (homMk₂ (α.app 0) (α.app 1) (β.app 1) (naturality' α 0 1)
       (by simpa only [hαβ] using naturality' β 0 1) : mk₂ f g ⟶ mk₂ f' g')
@@ -79,90 +80,94 @@ end
 
 section
 
-variable (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k)
+variable {i j k : ι} (f : i ⟶ j) (g : j ⟶ k)
   (fg : i ⟶ k) (h : f ≫ g = fg)
 
 @[reassoc (attr := simp)]
-lemma zero₁ :
-    X.δ n₀ n₁ hn₁ f g ≫ (X.H n₁).map (twoδ₂Toδ₁ f g fg h) = 0 := by
+lemma zero₁ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) :
+    X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f g fg h) = 0 := by
   subst h
   exact (X.exact₁' n₀ n₁ hn₁ (mk₂ f g)).zero 0
 
 @[reassoc (attr := simp)]
-lemma zero₂ (fg : i ⟶ k) (h : f ≫ g = fg) :
+lemma zero₂ (fg : i ⟶ k) (h : f ≫ g = fg) (n₀ : ℤ) :
     (X.H n₀).map (twoδ₂Toδ₁ f g fg h) ≫ (X.H n₀).map (twoδ₁Toδ₀ f g fg h) = 0 := by
   subst h
   exact (X.exact₂' n₀ (mk₂ f g)).zero 0
 
 @[reassoc (attr := simp)]
-lemma zero₃ :
-    (X.H n₀).map (twoδ₁Toδ₀ f g fg h) ≫ X.δ n₀ n₁ hn₁ f g = 0 := by
+lemma zero₃ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) :
+    (X.H n₀).map (twoδ₁Toδ₀ f g fg h) ≫ X.δ f g n₀ n₁ hn₁ = 0 := by
   subst h
   exact (X.exact₃' n₀ n₁ hn₁ (mk₂ f g)).zero 0
 
 /-- The (exact) short complex `H^n₀(g) ⟶ H^n₁(f) ⟶ H^n₁(fg)` of a
 spectral object, when `f ≫ g = fg` and `n₀ + 1 = n₁`. -/
 @[simps]
-def sc₁ : ShortComplex C :=
-  ShortComplex.mk _ _ (X.zero₁ n₀ n₁ hn₁ f g fg h)
+def sc₁ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : ShortComplex C :=
+  ShortComplex.mk _ _ (X.zero₁ f g fg h n₀ n₁ hn₁)
 
 /-- The (exact) short complex `H^n₀(f) ⟶ H^n₀(fg) ⟶ H^n₀(g)` of a
 spectral object, when `f ≫ g = fg`. -/
 @[simps]
-def sc₂ : ShortComplex C :=
-  ShortComplex.mk _ _ (X.zero₂ n₀ f g fg h)
+def sc₂ (n₀ : ℤ) : ShortComplex C :=
+  ShortComplex.mk _ _ (X.zero₂ f g fg h n₀)
 
 /-- The (exact) short complex `H^n₀(fg) ⟶ H^n₀(g) ⟶ H^n₁(f)`
 of a spectral object, when `f ≫ g = fg` and `n₀ + 1 = n₁`. -/
 @[simps]
-def sc₃ : ShortComplex C :=
-  ShortComplex.mk _ _ (X.zero₃ n₀ n₁ hn₁ f g fg h)
+def sc₃ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : ShortComplex C :=
+  ShortComplex.mk _ _ (X.zero₃ f g fg h n₀ n₁ hn₁)
 
-lemma exact₁ : (X.sc₁ n₀ n₁ hn₁ f g fg h).Exact := by
+lemma exact₁ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) :
+    (X.sc₁ f g fg h n₀ n₁ hn₁ ).Exact := by
   subst h
   exact (X.exact₁' n₀ n₁ hn₁ (mk₂ f g)).exact 0
 
-lemma exact₂ : (X.sc₂ n₀ f g fg h).Exact := by
+lemma exact₂ (n₀ : ℤ) :
+    (X.sc₂ f g fg h n₀).Exact := by
   subst h
   exact (X.exact₂' n₀ (mk₂ f g)).exact 0
 
-lemma exact₃ : (X.sc₃ n₀ n₁ hn₁ f g fg h).Exact := by
+lemma exact₃ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) :
+    (X.sc₃ f g fg h n₀ n₁ hn₁).Exact := by
   subst h
   exact ((X.exact₃' n₀ n₁ hn₁ (mk₂ f g))).exact 0
 
 /-- The (exact) sequence
 `H^n₀(f) ⟶ H^n₀(fg) ⟶ H^n₀(g) ⟶ H^n₁(f) ⟶ H^n₁(fg) ⟶ H^n₁(g)`
 of a spectral object, when `f ≫ g = fg` and `n₀ + 1 = n₁`. -/
-abbrev composableArrows₅ : ComposableArrows C 5 :=
+abbrev composableArrows₅ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) :
+    ComposableArrows C 5 :=
   mk₅ ((X.H n₀).map (twoδ₂Toδ₁ f g fg h)) ((X.H n₀).map (twoδ₁Toδ₀ f g fg h))
-    (X.δ n₀ n₁ hn₁ f g) ((X.H n₁).map (twoδ₂Toδ₁ f g fg h))
+    (X.δ f g n₀ n₁ hn₁) ((X.H n₁).map (twoδ₂Toδ₁ f g fg h))
     ((X.H n₁).map (twoδ₁Toδ₀ f g fg h))
 
-lemma composableArrows₅_exact :
-    (X.composableArrows₅ n₀ n₁ hn₁ f g fg h).Exact :=
-  exact_of_δ₀ (X.exact₂ n₀ _ _ _ h).exact_toComposableArrows
-    (exact_of_δ₀ (X.exact₃ n₀ n₁ hn₁ _ _ _ h).exact_toComposableArrows
-      (exact_of_δ₀ (X.exact₁ n₀ n₁ hn₁ _ _ _ h).exact_toComposableArrows
-        ((X.exact₂ n₁ _ _ _ h).exact_toComposableArrows)))
+lemma composableArrows₅_exact (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) :
+    (X.composableArrows₅ f g fg h n₀ n₁ hn₁).Exact :=
+  exact_of_δ₀ (X.exact₂ _ _ _ h n₀).exact_toComposableArrows
+    (exact_of_δ₀ (X.exact₃ _ _ _ h n₀ n₁ hn₁).exact_toComposableArrows
+      (exact_of_δ₀ (X.exact₁ _ _ _ h n₀ n₁ hn₁).exact_toComposableArrows
+        ((X.exact₂ _ _ _ h n₁).exact_toComposableArrows)))
 
 end
 
 @[reassoc (attr := simp)]
-lemma δ_δ (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂)
-    {i j k l : ι} (f : i ⟶ j) (g : j ⟶ k) (h : k ⟶ l) :
-    X.δ n₀ n₁ hn₁ g h ≫ X.δ n₁ n₂ hn₂ f g = 0 := by
-  have eq := X.δ_naturality n₁ n₂ hn₂ f g f (g ≫ h) (𝟙 _) (twoδ₂Toδ₁ g h _ rfl)
+lemma δ_δ {i j k l : ι} (f : i ⟶ j) (g : j ⟶ k) (h : k ⟶ l)
+    (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
+    X.δ g h n₀ n₁ hn₁ ≫ X.δ f g n₁ n₂ hn₂ = 0 := by
+  have eq := X.δ_naturality f g f (g ≫ h) (𝟙 _) (twoδ₂Toδ₁ g h _ rfl) n₁ n₂
   rw [Functor.map_id, comp_id] at eq
-  rw [← eq, X.zero₁_assoc n₀ n₁ hn₁ g h _ rfl, zero_comp]
+  rw [← eq, X.zero₁_assoc g h _ rfl n₀ n₁ hn₁, zero_comp]
 
 /-- The type of morphisms between spectral objects in abelian categories. -/
 @[ext]
 structure Hom (X' : SpectralObject C ι) where
   /-- The natural transformation that is part of a morphism between spectral objects. -/
   hom (n : ℤ) : X.H n ⟶ X'.H n
   comm (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) :
-    X.δ n₀ n₁ hn₁ f g ≫ (hom n₁).app (mk₁ f) =
-    (hom n₀).app (mk₁ g) ≫ X'.δ n₀ n₁ hn₁ f g := by cat_disch
+    X.δ f g n₀ n₁ hn₁ ≫ (hom n₁).app (mk₁ f) =
+    (hom n₀).app (mk₁ g) ≫ X'.δ f g n₀ n₁ hn₁ := by cat_disch
 
 attribute [reassoc (attr := simp)] Hom.comm
 
@@ -183,7 +188,7 @@ lemma isZero_H_map_mk₁_of_isIso (n : ℤ) {i₀ i₁ : ι} (f : i₀ ⟶ i₁)
     constructor <;> dsimp [φ] <;> infer_instance
   rw [IsZero.iff_id_eq_zero]
   rw [← cancel_mono ((X.H n).map φ), Category.id_comp, zero_comp,
-    ← X.zero₂ n f (inv f) (𝟙 _) (by simp), ← Functor.map_comp]
+    ← X.zero₂ f (inv f) (𝟙 _) (by simp), ← Functor.map_comp]
 
 section
 
@@ -193,11 +198,11 @@ variable (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i₀ i₁ i₂ : ι}
 
 include h₁ in
 lemma mono_H_map_twoδ₁Toδ₀ : Mono ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg)) :=
-  (X.exact₂ n₀ f g fg hfg).mono_g (h₁.eq_of_src _ _)
+  (X.exact₂ f g fg hfg n₀).mono_g (h₁.eq_of_src _ _)
 
 include h₂ hn₁ in
 lemma epi_H_map_twoδ₁Toδ₀ : Epi ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg)) :=
-  (X.exact₃ n₀ n₁ hn₁ f g fg hfg).epi_f (h₂.eq_of_tgt _ _)
+  (X.exact₃ f g fg hfg n₀ n₁ hn₁).epi_f (h₂.eq_of_tgt _ _)
 
 include h₁ h₂ hn₁ in
 lemma isIso_H_map_twoδ₁Toδ₀ : IsIso ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg)) := by