Loogle!

Result

Found 273 declarations mentioning CategoryTheory.Abelian.SpectralObject.H. Of these, only the first 200 are shown.

• CategoryTheory.Abelian.SpectralObject.H 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (self : CategoryTheory.Abelian.SpectralObject C ι) (n : ℤ) : CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C
• CategoryTheory.Abelian.SpectralObject.isZero_H_map_mk₁_of_isIso 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) (n : ℤ) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) [CategoryTheory.IsIso f] : CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ f))
• CategoryTheory.Abelian.SpectralObject.sc₂_X₁ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ) : (X.sc₂ f g fg h n₀).X₁ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.sc₂_X₂ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ) : (X.sc₂ f g fg h n₀).X₂ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ fg)
• CategoryTheory.Abelian.SpectralObject.sc₂_X₃ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ) : (X.sc₂ f g fg h n₀).X₃ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)
• CategoryTheory.Abelian.SpectralObject.sc₁_X₁ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₁ f g fg h n₀ n₁ hn₁).X₁ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)
• CategoryTheory.Abelian.SpectralObject.sc₁_X₂ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₁ f g fg h n₀ n₁ hn₁).X₂ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.sc₁_X₃ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₁ f g fg h n₀ n₁ hn₁).X₃ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ fg)
• CategoryTheory.Abelian.SpectralObject.sc₃_X₁ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₃ f g fg h n₀ n₁ hn₁).X₁ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ fg)
• CategoryTheory.Abelian.SpectralObject.sc₃_X₂ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₃ f g fg h n₀ n₁ hn₁).X₂ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)
• CategoryTheory.Abelian.SpectralObject.sc₃_X₃ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₃ f g fg h n₀ n₁ hn₁).X₃ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.δ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶ (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.sc₁_f 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₁ f g fg h n₀ n₁ hn₁).f = X.δ f g n₀ n₁ hn₁
• CategoryTheory.Abelian.SpectralObject.sc₃_g 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₃ f g fg h n₀ n₁ hn₁).g = X.δ f g n₀ n₁ hn₁
• CategoryTheory.Abelian.SpectralObject.Hom.hom 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] {X X' : CategoryTheory.Abelian.SpectralObject C ι} (self : X.Hom X') (n : ℤ) : X.H n ⟶ X'.H n
• CategoryTheory.Abelian.SpectralObject.sc₂_f 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ) : (X.sc₂ f g fg h n₀).f = (X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)
• CategoryTheory.Abelian.SpectralObject.sc₂_g 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ) : (X.sc₂ f g fg h n₀).g = (X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)
• CategoryTheory.Abelian.SpectralObject.Hom.ext 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} {inst✝ : CategoryTheory.Category.{u_3, u_1} C} {inst✝¹ : CategoryTheory.Category.{u_4, u_2} ι} {inst✝² : CategoryTheory.Abelian C} {X X' : CategoryTheory.Abelian.SpectralObject C ι} {x y : X.Hom X'} (hom : x.hom = y.hom) : x = y
• CategoryTheory.Abelian.SpectralObject.Hom.ext_iff 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} {inst✝ : CategoryTheory.Category.{u_3, u_1} C} {inst✝¹ : CategoryTheory.Category.{u_4, u_2} ι} {inst✝² : CategoryTheory.Abelian C} {X X' : CategoryTheory.Abelian.SpectralObject C ι} {x y : X.Hom X'} : x = y ↔ x.hom = y.hom
• CategoryTheory.Abelian.SpectralObject.sc₁_g 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₁ f g fg h n₀ n₁ hn₁).g = (X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)
• CategoryTheory.Abelian.SpectralObject.sc₃_f 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.sc₃ f g fg h n₀ n₁ hn₁).f = (X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)
• CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ : ℤ) {i₀ i₁ i₂ : ι} (f : i₀ ⟶ i₁) (g : i₁ ⟶ i₂) (fg : i₀ ⟶ i₂) (hfg : CategoryTheory.CategoryStruct.comp f g = fg) (h₁ : CategoryTheory.Limits.IsZero ((X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f))) : CategoryTheory.Mono ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg hfg))
• CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i₀ i₁ i₂ : ι} (f : i₀ ⟶ i₁) (g : i₁ ⟶ i₂) (fg : i₀ ⟶ i₂) (hfg : CategoryTheory.CategoryStruct.comp f g = fg) (h₂ : CategoryTheory.Limits.IsZero ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))) : CategoryTheory.Epi ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg hfg))
• CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀' 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Abelian C] {ι' : Type u_3} [Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (n₀ : ℤ) (i₀ i₁ i₂ : ι') (h₀₁ : i₀ ≤ i₁) (h₁₂ : i₁ ≤ i₂) (h₁ : CategoryTheory.Limits.IsZero ((X'.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE h₀₁)))) : CategoryTheory.Mono ((X'.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))
• CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀' 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Abelian C] {ι' : Type u_3} [Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) (i₀ i₁ i₂ : ι') (h₀₁ : i₀ ≤ i₁) (h₁₂ : i₁ ≤ i₂) (h₂ : CategoryTheory.Limits.IsZero ((X'.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE h₀₁)))) : CategoryTheory.Epi ((X'.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))
• CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i₀ i₁ i₂ : ι} (f : i₀ ⟶ i₁) (g : i₁ ⟶ i₂) (fg : i₀ ⟶ i₂) (hfg : CategoryTheory.CategoryStruct.comp f g = fg) (h₁ : CategoryTheory.Limits.IsZero ((X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f))) (h₂ : CategoryTheory.Limits.IsZero ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))) : CategoryTheory.IsIso ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg hfg))
• CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀' 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Abelian C] {ι' : Type u_3} [Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) (i₀ i₁ i₂ : ι') (h₀₁ : i₀ ≤ i₁) (h₁₂ : i₁ ≤ i₂) (h₁ : CategoryTheory.Limits.IsZero ((X'.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE h₀₁)))) (h₂ : CategoryTheory.Limits.IsZero ((X'.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE h₀₁)))) : CategoryTheory.IsIso ((X'.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))
• CategoryTheory.Abelian.SpectralObject.id_hom 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) (x✝ : ℤ) : (CategoryTheory.CategoryStruct.id X).hom x✝ = CategoryTheory.CategoryStruct.id (X.H x✝)
• CategoryTheory.Abelian.SpectralObject.comp_hom 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] {X✝ Y✝ Z✝ : CategoryTheory.Abelian.SpectralObject C ι} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (n : ℤ) : (CategoryTheory.CategoryStruct.comp f g).hom n = CategoryTheory.CategoryStruct.comp (f.hom n) (g.hom n)
• CategoryTheory.Abelian.SpectralObject.δ' 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (self : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : (CategoryTheory.ComposableArrows.functorArrows ι 1 2 2 CategoryTheory.Abelian.SpectralObject._proof_2 CategoryTheory.Abelian.SpectralObject._proof_4).comp (self.H n₀) ⟶ (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_2).comp (self.H n₁)
• CategoryTheory.Abelian.SpectralObject.Hom.comm 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] {X X' : CategoryTheory.Abelian.SpectralObject C ι} (self : X.Hom X') (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((self.hom n₁).app (CategoryTheory.ComposableArrows.mk₁ f)) = CategoryTheory.CategoryStruct.comp ((self.hom n₀).app (CategoryTheory.ComposableArrows.mk₁ g)) (X'.δ f g n₀ n₁ hn₁)
• CategoryTheory.Abelian.SpectralObject.δ_δ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {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) : CategoryTheory.CategoryStruct.comp (X.δ g h n₀ n₁ hn₁) (X.δ f g n₁ n₂ hn₂) = 0
• CategoryTheory.Abelian.SpectralObject.zero₁ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) = 0
• CategoryTheory.Abelian.SpectralObject.zero₃ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryTheory.CategoryStruct.comp ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) (X.δ f g n₀ n₁ hn₁) = 0
• CategoryTheory.Abelian.SpectralObject.Hom.comm_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] {X X' : CategoryTheory.Abelian.SpectralObject C ι} (self : X.Hom X') (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {Z : C} (h : (X'.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (CategoryTheory.CategoryStruct.comp ((self.hom n₁).app (CategoryTheory.ComposableArrows.mk₁ f)) h) = CategoryTheory.CategoryStruct.comp ((self.hom n₀).app (CategoryTheory.ComposableArrows.mk₁ g)) (CategoryTheory.CategoryStruct.comp (X'.δ f g n₀ n₁ hn₁) h)
• CategoryTheory.Abelian.SpectralObject.zero₂ 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ) : CategoryTheory.CategoryStruct.comp ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0
• CategoryTheory.Abelian.SpectralObject.Hom.mk 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] {X X' : CategoryTheory.Abelian.SpectralObject C ι} (hom : (n : ℤ) → X.H n ⟶ X'.H n) (comm : ∀ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k), CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((hom n₁).app (CategoryTheory.ComposableArrows.mk₁ f)) = CategoryTheory.CategoryStruct.comp ((hom n₀).app (CategoryTheory.ComposableArrows.mk₁ g)) (X'.δ f g n₀ n₁ hn₁) := by cat_disch) : X.Hom X'
• CategoryTheory.Abelian.SpectralObject.δ_δ_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {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) {Z : C} (h✝ : (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ g h n₀ n₁ hn₁) (CategoryTheory.CategoryStruct.comp (X.δ f g n₁ n₂ hn₂) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
• CategoryTheory.Abelian.SpectralObject.zero₁_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h✝ : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (CategoryTheory.CategoryStruct.comp ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
• CategoryTheory.Abelian.SpectralObject.zero₃_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h✝ : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) (CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
• CategoryTheory.Abelian.SpectralObject.comp_hom_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] {X✝ Y✝ Z✝ : CategoryTheory.Abelian.SpectralObject C ι} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (n : ℤ) {Z : CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C} (h : Z✝.H n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).hom n) h = CategoryTheory.CategoryStruct.comp (f.hom n) (CategoryTheory.CategoryStruct.comp (g.hom n) h)
• CategoryTheory.Abelian.SpectralObject.zero₂_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ) {Z : C} (h✝ : (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) (CategoryTheory.CategoryStruct.comp ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
• CategoryTheory.Abelian.SpectralObject.δ_naturality 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ f') (β : CategoryTheory.ComposableArrows.mk₁ g ⟶ CategoryTheory.ComposableArrows.mk₁ g') (n₀ n₁ : ℤ) (hαβ : α.app 1 = β.app 0 := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryTheory.CategoryStruct.comp ((X.H n₀).map β) (X.δ f' g' n₀ n₁ hn₁) = CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((X.H n₁).map α)
• CategoryTheory.Abelian.SpectralObject.δ_naturality_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ f') (β : CategoryTheory.ComposableArrows.mk₁ g ⟶ CategoryTheory.ComposableArrows.mk₁ g') (n₀ n₁ : ℤ) (hαβ : α.app 1 = β.app 0 := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f') ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.H n₀).map β) (CategoryTheory.CategoryStruct.comp (X.δ f' g' n₀ n₁ hn₁) h) = CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (CategoryTheory.CategoryStruct.comp ((X.H n₁).map α) h)
• CategoryTheory.Abelian.SpectralObject.exact₁' 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (self : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : CategoryTheory.ComposableArrows ι 2) : (CategoryTheory.ComposableArrows.mk₂ ((self.δ' n₀ n₁ h).app D) ((self.H n₁).map ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2 CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_8 CategoryTheory.Abelian.SpectralObject._proof_10 CategoryTheory.Abelian.SpectralObject._proof_2 CategoryTheory.Abelian.SpectralObject._proof_4).app D))).Exact
• CategoryTheory.Abelian.SpectralObject.exact₃' 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (self : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : CategoryTheory.ComposableArrows ι 2) : (CategoryTheory.ComposableArrows.mk₂ ((self.H n₀).map ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2 CategoryTheory.Abelian.SpectralObject._proof_8 CategoryTheory.Abelian.SpectralObject._proof_2 CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_4 CategoryTheory.Abelian.SpectralObject._proof_4).app D)) ((self.δ' n₀ n₁ h).app D)).Exact
• CategoryTheory.Abelian.SpectralObject.exact₂' 📋 Mathlib.Algebra.Homology.SpectralObject.Basic
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} ι] [CategoryTheory.Abelian C] (self : CategoryTheory.Abelian.SpectralObject C ι) (n : ℤ) (D : CategoryTheory.ComposableArrows ι 2) : (CategoryTheory.ComposableArrows.mk₂ ((self.H n).map ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2 CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_8 CategoryTheory.Abelian.SpectralObject._proof_10 CategoryTheory.Abelian.SpectralObject._proof_2 CategoryTheory.Abelian.SpectralObject._proof_4).app D)) ((self.H n).map ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2 CategoryTheory.Abelian.SpectralObject._proof_8 CategoryTheory.Abelian.SpectralObject._proof_2 CategoryTheory.Abelian.SpectralObject._proof_6 CategoryTheory.Abelian.SpectralObject._proof_4 CategoryTheory.Abelian.SpectralObject._proof_4).app D))).Exact
• CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctor_H 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {A : Type u_4} [CategoryTheory.Category.{v_4, u_4} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (n : ℤ) : (X.mapHomologicalFunctor F).H n = X.ω₁.comp (F.shift n)
• CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctor_δ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {A : Type u_4} [CategoryTheory.Category.{v_4, u_4} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁ := by lia) : (X.mapHomologicalFunctor F).δ f g n₀ n₁ h = F.homologySequenceδ (X.triangle f g) n₀ n₁ h
• CategoryTheory.Abelian.SpectralObject.isZero_cycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) (h : CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g))) : CategoryTheory.Limits.IsZero (X.cycles f g n)
• CategoryTheory.Abelian.SpectralObject.isZero_opcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) (h : CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ f))) : CategoryTheory.Limits.IsZero (X.opcycles f g n)
• CategoryTheory.Abelian.SpectralObject.iCycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : X.cycles f g n ⟶ (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g)
• CategoryTheory.Abelian.SpectralObject.pOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ X.opcycles f g n
• CategoryTheory.Abelian.SpectralObject.instEpiPOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : CategoryTheory.Epi (X.pOpcycles f g n)
• CategoryTheory.Abelian.SpectralObject.instMonoICycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : CategoryTheory.Mono (X.iCycles f g n)
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_X₁ 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).X₁ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_X₂ 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).X₂ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_X₂ 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.kernelSequenceCycles f g n₀ n₁ hn₁).X₂ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)
• CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_X₃ 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.kernelSequenceCycles f g n₀ n₁ hn₁).X₃ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.δFromOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : X.opcycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁)
• CategoryTheory.Abelian.SpectralObject.δToCycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f₃) ⟶ X.cycles f₁ f₂ n₁
• CategoryTheory.Abelian.SpectralObject.fromOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : X.opcycles f g n ⟶ (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg)
• CategoryTheory.Abelian.SpectralObject.toCycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ X.cycles f g n
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_X₁ 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : (X.cokernelSequenceCycles f g fg h n).X₁ = (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_X₂ 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : (X.cokernelSequenceCycles f g fg h n).X₂ = (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg)
• CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_X₂ 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : (X.kernelSequenceOpcycles f g fg h n).X₂ = (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg)
• CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_X₃ 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : (X.kernelSequenceOpcycles f g fg h n).X₃ = (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g)
• CategoryTheory.Abelian.SpectralObject.instEpiToCycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : CategoryTheory.Epi (X.toCycles f g fg h n)
• CategoryTheory.Abelian.SpectralObject.instMonoFromOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : CategoryTheory.Mono (X.fromOpcycles f g fg h n)
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_g 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).g = X.pOpcycles f g n₁
• CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_f 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.kernelSequenceCycles f g n₀ n₁ hn₁).f = X.iCycles f g n₀
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_g 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : (X.cokernelSequenceCycles f g fg h n).g = X.toCycles f g fg h n
• CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_f 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : (X.kernelSequenceOpcycles f g fg h n).f = X.fromOpcycles f g fg h n
• CategoryTheory.Abelian.SpectralObject.isIso_fromOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) (hg : CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g))) : CategoryTheory.IsIso (X.fromOpcycles f g fg h n)
• CategoryTheory.Abelian.SpectralObject.isIso_toCycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) (hf : CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ f))) : CategoryTheory.IsIso (X.toCycles f g fg h n)
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_f 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).f = X.δ f g n₀ n₁ hn₁
• CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_g 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.kernelSequenceCycles f g n₀ n₁ hn₁).g = X.δ f g n₀ n₁ hn₁
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_f 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : (X.cokernelSequenceCycles f g fg h n).f = (X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)
• CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_g 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : (X.kernelSequenceOpcycles f g fg h n).g = (X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)
• CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryTheory.CategoryStruct.comp (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀) (X.δ f₁ f₂₃ n₀ n₁ hn₁) = X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁
• CategoryTheory.Abelian.SpectralObject.δ_toCycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryTheory.CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
• CategoryTheory.Abelian.SpectralObject.pOpcycles_δFromOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f₂ f₃ n₀) (X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁) = X.δ f₁ f₂ n₀ n₁ hn₁
• CategoryTheory.Abelian.SpectralObject.δToCycles_iCycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) : CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (X.iCycles f₁ f₂ n₁) = X.δ f₂ f₃ n₀ n₁ hn₁
• CategoryTheory.Abelian.SpectralObject.p_fromOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n) (X.fromOpcycles f g fg h n) = (X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)
• CategoryTheory.Abelian.SpectralObject.toCycles_i 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n) (X.iCycles f g n) = (X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)
• CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀) (CategoryTheory.CategoryStruct.comp (X.δ f₁ f₂₃ n₀ n₁ hn₁) h) = CategoryTheory.CategoryStruct.comp (X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁) h
• CategoryTheory.Abelian.SpectralObject.δ_toCycles_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : X.cycles f₁ f₂ n₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) (CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) h) = CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) h
• CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : CategoryTheory.Limits.cokernel ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) ≅ X.cycles f g n
• CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : X.opcycles f g n ≅ CategoryTheory.Limits.kernel ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h))
• CategoryTheory.Abelian.SpectralObject.pOpcycles_δFromOpcycles_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {Z : C} (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f₂ f₃ n₀) (CategoryTheory.CategoryStruct.comp (X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁) h) = CategoryTheory.CategoryStruct.comp (X.δ f₁ f₂ n₀ n₁ hn₁) h
• CategoryTheory.Abelian.SpectralObject.δToCycles_iCycles_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {Z : C} (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂ n₁) h) = CategoryTheory.CategoryStruct.comp (X.δ f₂ f₃ n₀ n₁ hn₁) h
• CategoryTheory.Abelian.SpectralObject.iCycles_δ 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryTheory.CategoryStruct.comp (X.iCycles f g n₀) (X.δ f g n₀ n₁ hn₁) = 0
• CategoryTheory.Abelian.SpectralObject.δ_pOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (X.pOpcycles f g n₁) = 0
• CategoryTheory.Abelian.SpectralObject.descOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {A : C} (x : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ A) (hx : CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) x = 0) : X.opcycles f g n₁ ⟶ A
• CategoryTheory.Abelian.SpectralObject.liftCycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {A : C} (x : A ⟶ (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)) (hx : CategoryTheory.CategoryStruct.comp x (X.δ f g n₀ n₁ hn₁) = 0) : A ⟶ X.cycles f g n₀
• CategoryTheory.Abelian.SpectralObject.p_fromOpcycles_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h✝ : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n) (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f g fg h n) h✝) = CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) h✝
• CategoryTheory.Abelian.SpectralObject.toCycles_i_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h✝ : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n) (CategoryTheory.CategoryStruct.comp (X.iCycles f g n) h✝) = CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) h✝
• CategoryTheory.Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) (X.toCycles f g fg h n) = 0
• CategoryTheory.Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀ 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : CategoryTheory.CategoryStruct.comp (X.fromOpcycles f g fg h n) ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0
• CategoryTheory.Abelian.SpectralObject.descCycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) {A : C} {n : ℤ} (x : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ A) (hx : CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) x = 0) : X.cycles f g n ⟶ A
• CategoryTheory.Abelian.SpectralObject.liftOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) {A : C} {n : ℤ} (x : A ⟶ (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg)) (hx : CategoryTheory.CategoryStruct.comp x ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0) : A ⟶ X.opcycles f g n
• CategoryTheory.Abelian.SpectralObject.iCycles_δ_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.iCycles f g n₀) (CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Abelian.SpectralObject.δ_pOpcycles_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : X.opcycles f g n₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n₁) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Abelian.SpectralObject.liftCycles_i 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {A : C} (x : A ⟶ (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)) (hx : CategoryTheory.CategoryStruct.comp x (X.δ f g n₀ n₁ hn₁) = 0) : CategoryTheory.CategoryStruct.comp (X.liftCycles f g n₀ n₁ hn₁ x hx) (X.iCycles f g n₀) = x
• CategoryTheory.Abelian.SpectralObject.p_descOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {A : C} (x : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ A) (hx : CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) x = 0) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n₁) (X.descOpcycles f g n₀ n₁ hn₁ x hx) = x
• CategoryTheory.Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h✝ : X.cycles f g n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) (CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
• CategoryTheory.Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h✝ : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.fromOpcycles f g fg h n) (CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
• CategoryTheory.Abelian.SpectralObject.liftOpcycles_fromOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) {A : C} {n : ℤ} (x : A ⟶ (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg)) (hx : CategoryTheory.CategoryStruct.comp x ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0) : CategoryTheory.CategoryStruct.comp (X.liftOpcycles f g fg h x hx) (X.fromOpcycles f g fg h n) = x
• CategoryTheory.Abelian.SpectralObject.toCycles_descCycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) {A : C} {n : ℤ} (x : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ A) (hx : CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) x = 0) : CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n) (X.descCycles f g fg h x hx) = x
• CategoryTheory.Abelian.SpectralObject.liftCycles_i_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {A : C} (x : A ⟶ (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)) (hx : CategoryTheory.CategoryStruct.comp x (X.δ f g n₀ n₁ hn₁) = 0) {Z : C} (h : (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.liftCycles f g n₀ n₁ hn₁ x hx) (CategoryTheory.CategoryStruct.comp (X.iCycles f g n₀) h) = CategoryTheory.CategoryStruct.comp x h
• CategoryTheory.Abelian.SpectralObject.p_descOpcycles_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {A : C} (x : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ A) (hx : CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) x = 0) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n₁) (CategoryTheory.CategoryStruct.comp (X.descOpcycles f g n₀ n₁ hn₁ x hx) h) = CategoryTheory.CategoryStruct.comp x h
• CategoryTheory.Abelian.SpectralObject.liftOpcycles_fromOpcycles_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) {A : C} {n : ℤ} (x : A ⟶ (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg)) (hx : CategoryTheory.CategoryStruct.comp x ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0) {Z : C} (h✝ : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.liftOpcycles f g fg h x hx) (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f g fg h n) h✝) = CategoryTheory.CategoryStruct.comp x h✝
• CategoryTheory.Abelian.SpectralObject.toCycles_descCycles_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) {A : C} {n : ℤ} (x : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ A) (hx : CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) x = 0) {Z : C} (h✝ : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n) (CategoryTheory.CategoryStruct.comp (X.descCycles f g fg h x hx) h✝) = CategoryTheory.CategoryStruct.comp x h✝
• CategoryTheory.Abelian.SpectralObject.cyclesMap_i 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') (β : CategoryTheory.ComposableArrows.mk₁ g ⟶ CategoryTheory.ComposableArrows.mk₁ g') (n : ℤ) (hβ : β = CategoryTheory.ComposableArrows.homMk₁ (α.app 1) (α.app 2) ⋯ := by cat_disch) : CategoryTheory.CategoryStruct.comp (X.cyclesMap f g f' g' α n) (X.iCycles f' g' n) = CategoryTheory.CategoryStruct.comp (X.iCycles f g n) ((X.H n).map β)
• CategoryTheory.Abelian.SpectralObject.p_opcyclesMap 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') (β : CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ f') (n : ℤ) (hβ : β = CategoryTheory.ComposableArrows.homMk₁ (α.app 0) (α.app 1) ⋯ := by cat_disch) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n) (X.opcyclesMap f g f' g' α n) = CategoryTheory.CategoryStruct.comp ((X.H n).map β) (X.pOpcycles f' g' n)
• CategoryTheory.Abelian.SpectralObject.cyclesMap_i_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') (β : CategoryTheory.ComposableArrows.mk₁ g ⟶ CategoryTheory.ComposableArrows.mk₁ g') (n : ℤ) (hβ : β = CategoryTheory.ComposableArrows.homMk₁ (α.app 1) (α.app 2) ⋯ := by cat_disch) {Z : C} (h : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g') ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.cyclesMap f g f' g' α n) (CategoryTheory.CategoryStruct.comp (X.iCycles f' g' n) h) = CategoryTheory.CategoryStruct.comp (X.iCycles f g n) (CategoryTheory.CategoryStruct.comp ((X.H n).map β) h)
• CategoryTheory.Abelian.SpectralObject.p_opcyclesMap_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') (β : CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ f') (n : ℤ) (hβ : β = CategoryTheory.ComposableArrows.homMk₁ (α.app 0) (α.app 1) ⋯ := by cat_disch) {Z : C} (h : X.opcycles f' g' n ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n) (CategoryTheory.CategoryStruct.comp (X.opcyclesMap f g f' g' α n) h) = CategoryTheory.CategoryStruct.comp ((X.H n).map β) (CategoryTheory.CategoryStruct.comp (X.pOpcycles f' g' n) h)
• CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (fg' : i' ⟶ k') (h' : CategoryTheory.CategoryStruct.comp f' g' = fg') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') (β : CategoryTheory.ComposableArrows.mk₁ fg ⟶ CategoryTheory.ComposableArrows.mk₁ fg') (n : ℤ) (hβ₀ : β.app 0 = α.app 0 := by cat_disch) (hβ₁ : β.app 1 = α.app 2 := by cat_disch) : CategoryTheory.CategoryStruct.comp (X.opcyclesMap f g f' g' α n) (X.fromOpcycles f' g' fg' h' n) = CategoryTheory.CategoryStruct.comp (X.fromOpcycles f g fg h n) ((X.H n).map β)
• CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (fg' : i' ⟶ k') (h' : CategoryTheory.CategoryStruct.comp f' g' = fg') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') (β : CategoryTheory.ComposableArrows.mk₁ fg ⟶ CategoryTheory.ComposableArrows.mk₁ fg') (n : ℤ) (hβ₀ : β.app 0 = α.app 0 := by cat_disch) (hβ₁ : β.app 1 = α.app 2 := by cat_disch) : CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n) (X.cyclesMap f g f' g' α n) = CategoryTheory.CategoryStruct.comp ((X.H n).map β) (X.toCycles f' g' fg' h' n)
• CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (fg' : i' ⟶ k') (h' : CategoryTheory.CategoryStruct.comp f' g' = fg') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') (β : CategoryTheory.ComposableArrows.mk₁ fg ⟶ CategoryTheory.ComposableArrows.mk₁ fg') (n : ℤ) (hβ₀ : β.app 0 = α.app 0 := by cat_disch) (hβ₁ : β.app 1 = α.app 2 := by cat_disch) {Z : C} (h✝ : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg') ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.opcyclesMap f g f' g' α n) (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f' g' fg' h' n) h✝) = CategoryTheory.CategoryStruct.comp (X.fromOpcycles f g fg h n) (CategoryTheory.CategoryStruct.comp ((X.H n).map β) h✝)
• CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (fg' : i' ⟶ k') (h' : CategoryTheory.CategoryStruct.comp f' g' = fg') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') (β : CategoryTheory.ComposableArrows.mk₁ fg ⟶ CategoryTheory.ComposableArrows.mk₁ fg') (n : ℤ) (hβ₀ : β.app 0 = α.app 0 := by cat_disch) (hβ₁ : β.app 1 = α.app 2 := by cat_disch) {Z : C} (h✝ : X.cycles f' g' n ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n) (CategoryTheory.CategoryStruct.comp (X.cyclesMap f g f' g' α n) h✝) = CategoryTheory.CategoryStruct.comp ((X.H n).map β) (CategoryTheory.CategoryStruct.comp (X.toCycles f' g' fg' h' n) h✝)
• CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n) (CategoryTheory.CategoryStruct.comp (X.opcyclesIsoKernel f g fg h n).hom (CategoryTheory.Limits.kernel.ι ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)))) = (X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)
• CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h))) (CategoryTheory.CategoryStruct.comp (X.cokernelIsoCycles f g fg h n).hom (X.iCycles f g n)) = (X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)
• CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h✝ : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h))) (CategoryTheory.CategoryStruct.comp (X.cokernelIsoCycles f g fg h n).hom (CategoryTheory.CategoryStruct.comp (X.iCycles f g n) h✝)) = CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) h✝
• CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Cycles
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h✝ : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n) (CategoryTheory.CategoryStruct.comp (X.opcyclesIsoKernel f g fg h n).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h))) h✝)) = CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) h✝
• CategoryTheory.Abelian.SpectralObject.isZero_H_obj_of_isIso 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (hf : CategoryTheory.IsIso f) (n : ℤ) : CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ f))
• CategoryTheory.Abelian.SpectralObject.cyclesIsoH 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : X.cycles (CategoryTheory.CategoryStruct.id i₀) f n₀ ≅ (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.opcyclesIsoH 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : X.opcycles f (CategoryTheory.CategoryStruct.id i₁) n₁ ≅ (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.EIsoH 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X.E (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂ ≅ (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_X₁ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f₃)
• CategoryTheory.Abelian.SpectralObject.isZero_E_of_isZero_H 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (h : CategoryTheory.Limits.IsZero ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryTheory.Limits.IsZero (X.E f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
• CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_X₃ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₁)
• CategoryTheory.Abelian.SpectralObject.shortComplex_X₁ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f₃)
• CategoryTheory.Abelian.SpectralObject.shortComplex_X₂ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂)
• CategoryTheory.Abelian.SpectralObject.shortComplex_X₃ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₁)
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_X₂ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₂ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁₂)
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_X₁ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁)
• CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_X₃ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₃)
• CategoryTheory.Abelian.SpectralObject.kernelSequenceE_X₂ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂₃)
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_f 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁
• CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_g 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
• CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_H 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left.H = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_K 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left.K = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_H 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).right.H = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_Q 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).right.Q = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_i 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).i = X.iCycles f₁ f₂ n₁
• CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_p 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).p = X.pOpcycles f₂ f₃ n₁
• CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_H 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).H = CategoryTheory.Limits.cokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)
• CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_H 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).H = CategoryTheory.Limits.kernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯)
• CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.cyclesIsoH f n₀ n₁ hn₁).inv = X.toCycles (CategoryTheory.CategoryStruct.id i₀) f f ⋯ n₀
• CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : (X.opcyclesIsoH f n₀ n₁ hn₁).hom = X.fromOpcycles f (CategoryTheory.CategoryStruct.id i₁) f ⋯ n₁
• CategoryTheory.Abelian.SpectralObject.shortComplex_f 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f = X.δ f₂ f₃ n₀ n₁ ⋯
• CategoryTheory.Abelian.SpectralObject.shortComplex_g 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = X.δ f₁ f₂ n₁ n₂ ⋯
• CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_i 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left.i = CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
• CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_π 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left.π = CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
• CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_p 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).right.p = CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
• CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_ι 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).right.ι = CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
• CategoryTheory.Abelian.SpectralObject.πE_ιE 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) = CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂ n₁) (X.pOpcycles f₂ f₃ n₁)
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_X₁ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁ = ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁) ⊞ (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f₃))
• CategoryTheory.Abelian.SpectralObject.kernelSequenceE_X₃ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₃ = ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₃) ⊞ (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₁))
• CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_inv_id 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryTheory.CategoryStruct.comp (X.cyclesIsoH f n₀ n₁ hn₁).hom (X.toCycles (CategoryTheory.CategoryStruct.id i₀) f f ⋯ n₀) = CategoryTheory.CategoryStruct.id (X.cycles (CategoryTheory.CategoryStruct.id i₀) f n₀)
• CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom_inv_id 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryTheory.CategoryStruct.comp (X.fromOpcycles f (CategoryTheory.CategoryStruct.id i₁) f ⋯ n₁) (X.opcyclesIsoH f n₀ n₁ hn₁).inv = CategoryTheory.CategoryStruct.id (X.opcycles f (CategoryTheory.CategoryStruct.id i₁) n₁)
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_g 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g = CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
• CategoryTheory.Abelian.SpectralObject.kernelSequenceE_f 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f = CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁)
• CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_π 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).π = CategoryTheory.Limits.cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)
• CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_ι 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).ι = CategoryTheory.Limits.kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯)
• CategoryTheory.Abelian.SpectralObject.πE_ιE_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.opcycles f₂ f₃ n₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂ n₁) (CategoryTheory.CategoryStruct.comp (X.pOpcycles f₂ f₃ n₁) h)
• CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_inv_id_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : X.cycles (CategoryTheory.CategoryStruct.id i₀) f n₀ ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.cyclesIsoH f n₀ n₁ hn₁).hom (CategoryTheory.CategoryStruct.comp (X.toCycles (CategoryTheory.CategoryStruct.id i₀) f f ⋯ n₀) h) = h
• CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom_inv_id_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : X.opcycles f (CategoryTheory.CategoryStruct.id i₁) n₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.fromOpcycles f (CategoryTheory.CategoryStruct.id i₁) f ⋯ n₁) (CategoryTheory.CategoryStruct.comp (X.opcyclesIsoH f n₀ n₁ hn₁).inv h) = h
• CategoryTheory.Abelian.SpectralObject.EIsoH_hom_opcyclesIsoH_inv 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i j : ι} (f : i ⟶ j) : CategoryTheory.CategoryStruct.comp (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom (X.opcyclesIsoH f n₀ n₁ hn₁).inv = X.ιE (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂
• CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_EIsoH_inv 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i j : ι} (f : i ⟶ j) : CategoryTheory.CategoryStruct.comp (X.cyclesIsoH f n₁ n₂ hn₂).hom (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).inv = X.πE (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂
• CategoryTheory.Abelian.SpectralObject.EToCycles_i 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryTheory.CategoryStruct.comp (X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂) (X.iCycles f₁ f₂₃ n₁) = CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁)
• CategoryTheory.Abelian.SpectralObject.p_opcyclesToE 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f₁₂ f₃ n₁) (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) = CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_f 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f = CategoryTheory.CategoryStruct.comp ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) (X.pOpcycles f₁₂ f₃ n₁)
• CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_g 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g = CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂₃ n₁) ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃))
• CategoryTheory.Abelian.SpectralObject.EToCycles_i_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂₃) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂₃ n₁) h) = CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) h)
• CategoryTheory.Abelian.SpectralObject.p_opcyclesToE_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f₁₂ f₃ n₁) (CategoryTheory.CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) (CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h)
• CategoryTheory.Abelian.SpectralObject.homologyDataIdId_iso_hom 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).iso.hom = CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
• CategoryTheory.Abelian.SpectralObject.homologyDataIdId_iso_inv 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).iso.inv = CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
• CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.toCycles (CategoryTheory.CategoryStruct.id i₀) f f ⋯ n₀) (CategoryTheory.CategoryStruct.comp (X.cyclesIsoH f n₀ n₁ hn₁).hom h) = h
• CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_inv_hom_id_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.opcyclesIsoH f n₀ n₁ hn₁).inv (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f (CategoryTheory.CategoryStruct.id i₁) f ⋯ n₁) h) = h
• CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryTheory.CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom (X.iCycles f₁ f₂ n₁) = (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).iCycles
• CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f₂ f₃ n₁) (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv = (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles
• CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryTheory.CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂) = (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles
• CategoryTheory.Abelian.SpectralObject.δToCycles_cyclesIso_inv 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv = (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).toCycles
• CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryTheory.CategoryStruct.comp (X.toCycles (CategoryTheory.CategoryStruct.id i₀) f f ⋯ n₀) (X.cyclesIsoH f n₀ n₁ hn₁).hom = CategoryTheory.CategoryStruct.id ((X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f))
• CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_inv_hom_id 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryTheory.CategoryStruct.comp (X.opcyclesIsoH f n₀ n₁ hn₁).inv (X.fromOpcycles f (CategoryTheory.CategoryStruct.id i₁) f ⋯ n₁) = CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
• CategoryTheory.Abelian.SpectralObject.EIsoH_hom_opcyclesIsoH_inv_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i j : ι} (f : i ⟶ j) {Z : C} (h : X.opcycles f (CategoryTheory.CategoryStruct.id j) n₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom (CategoryTheory.CategoryStruct.comp (X.opcyclesIsoH f n₀ n₁ hn₁).inv h) = CategoryTheory.CategoryStruct.comp (X.ιE (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂) h
• CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_EIsoH_inv_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i j : ι} (f : i ⟶ j) {Z : C} (h : X.E (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.cyclesIsoH f n₁ n₂ hn₂).hom (CategoryTheory.CategoryStruct.comp (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).inv h) = CategoryTheory.CategoryStruct.comp (X.πE (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂) h
• CategoryTheory.Abelian.SpectralObject.δToCycles_πE 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) = 0
• CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂) = 0
• CategoryTheory.Abelian.SpectralObject.δ_eq_zero_of_isIso₁ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (hf : CategoryTheory.IsIso f) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : X.δ f g n₀ n₁ hn₁ = 0
• CategoryTheory.Abelian.SpectralObject.δ_eq_zero_of_isIso₂ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (hg : CategoryTheory.IsIso g) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : X.δ f g n₀ n₁ hn₁ = 0
• CategoryTheory.Abelian.SpectralObject.δToCycles_πE_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₁) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryTheory.CategoryStruct.comp (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_f 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f = CategoryTheory.Limits.biprod.desc ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) (X.δ f₁₂ f₃ n₀ n₁ ⋯)
• CategoryTheory.Abelian.SpectralObject.kernelSequenceE_g 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g = CategoryTheory.Limits.biprod.lift ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯)
• CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom (CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂ n₁) h) = CategoryTheory.CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).iCycles h
• CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv_assoc 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).opcycles ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.pOpcycles f₂ f₃ n₁) (CategoryTheory.CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv h) = CategoryTheory.CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles h
• CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₁ 📋 Mathlib.Algebra.Homology.SpectralObject.Page
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Abelian C] (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι} (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃') (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂).τ₁ = (X.H n₀).map (CategoryTheory.ComposableArrows.homMk₁ (α.app 2) (α.app 3) ⋯)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59