Kernel and cokernel of the differential of a spectral object

Let X be a spectral object indexed by the category ι in the abelian category C. In this file, we introduce the kernel X.cycles and the cokernel X.opcycles of X.δ. These are defined when f and g are composable morphisms in ι and for any integer n. In the documentation, the kernel X.cycles n f g of δ : H^n(g) ⟶ H^{n+1}(f) shall be denoted Z^n(f, g), and the cokernel X.opcycles n f g of δ : H^{n-1}(g) ⟶ H^n(f) shall be denoted opZ^n(f, g). The definitions cyclesMap and opcyclesMap give the functoriality of these definitions with respect to morphisms in ComposableArrows ι 2.

We record that Z^n(f, g) is a kernel by the lemma kernelSequenceCycles_exact and that opZ^n(f, g) is a cokernel by the lemma cokernelSequenceOpcycles_exact. We also provide a constructor X.liftCycles for morphisms to cycles and X.descOpcycles for morphisms from opcycles.

References

• [Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes, II.4][verdier1996]

noncomputable def CategoryTheory.Abelian.SpectralObject.cycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : C

The kernel of δ : H^n(g) ⟶ H^{n+1}(f). In the documentation, this may be shortened as Z^n(f, g)

noncomputable def CategoryTheory.Abelian.SpectralObject.opcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : C

The cokernel of δ : H^{n-1}(g) ⟶ H^n(g). In the documentation, this may be shortened as opZ^n₁(f, g).

noncomputable def CategoryTheory.Abelian.SpectralObject.iCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : X.cycles f g n ⟶ (X.H n).obj (ComposableArrows.mk₁ g)

The inclusion Z^n(f, g) ⟶ H^n(g) of the kernel of δ.

noncomputable def CategoryTheory.Abelian.SpectralObject.pOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : (X.H n).obj (ComposableArrows.mk₁ f) ⟶ X.opcycles f g n

The projection H^n(f) ⟶ opZ^n(f, g) to the cokernel of δ.

instance CategoryTheory.Abelian.SpectralObject.instMonoICycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : Mono (X.iCycles f g n)

instance CategoryTheory.Abelian.SpectralObject.instEpiPOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : Epi (X.pOpcycles f g n)

theorem CategoryTheory.Abelian.SpectralObject.isZero_opcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) (h : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ f))) : Limits.IsZero (X.opcycles f g n)

theorem CategoryTheory.Abelian.SpectralObject.isZero_cycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) (h : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ g))) : Limits.IsZero (X.cycles f g n)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.iCycles_δ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.iCycles f g n₀) (X.δ f g n₀ n₁ hn₁) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.iCycles_δ_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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 (ComposableArrows.mk₁ f) ⟶ Z) : CategoryStruct.comp (X.iCycles f g n₀) (CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.δ_pOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (X.pOpcycles f g n₁) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.δ_pOpcycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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) : CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) (CategoryStruct.comp (X.pOpcycles f g n₁) h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : ShortComplex C

The short complex which expresses X.cycles as the kernel of X.δ.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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.cycles f g n₀

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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₀

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_X₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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 (ComposableArrows.mk₁ g)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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 (ComposableArrows.mk₁ f)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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₁

noncomputable def CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : ShortComplex C

The short complex which expresses X.opcycles as the cokernel of X.δ.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_X₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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 (ComposableArrows.mk₁ f)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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 (ComposableArrows.mk₁ g)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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.opcycles f g n₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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₁

instance CategoryTheory.Abelian.SpectralObject.instMonoFKernelSequenceCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) : Mono (X.kernelSequenceCycles f g n₀ n₁ hn₁).f

instance CategoryTheory.Abelian.SpectralObject.instEpiGCokernelSequenceOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) : Epi (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).g

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_exact {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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₁).Exact

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_exact {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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₁).Exact

noncomputable def CategoryTheory.Abelian.SpectralObject.liftCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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 (ComposableArrows.mk₁ g)) (hx : CategoryStruct.comp x (X.δ f g n₀ n₁ hn₁) = 0) : A ⟶ X.cycles f g n₀

Constructor for morphisms to X.cycles.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.liftCycles_i {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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 (ComposableArrows.mk₁ g)) (hx : CategoryStruct.comp x (X.δ f g n₀ n₁ hn₁) = 0) : CategoryStruct.comp (X.liftCycles f g n₀ n₁ hn₁ x hx) (X.iCycles f g n₀) = x

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.liftCycles_i_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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 (ComposableArrows.mk₁ g)) (hx : CategoryStruct.comp x (X.δ f g n₀ n₁ hn₁) = 0) {Z : C} (h : (X.H n₀).obj (ComposableArrows.mk₁ g) ⟶ Z) : CategoryStruct.comp (X.liftCycles f g n₀ n₁ hn₁ x hx) (CategoryStruct.comp (X.iCycles f g n₀) h) = CategoryStruct.comp x h

noncomputable def CategoryTheory.Abelian.SpectralObject.descOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {A : C} (x : (X.H n₁).obj (ComposableArrows.mk₁ f) ⟶ A) (hx : CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) x = 0) : X.opcycles f g n₁ ⟶ A

Constructor for morphisms from X.opcycles.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.p_descOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {A : C} (x : (X.H n₁).obj (ComposableArrows.mk₁ f) ⟶ A) (hx : CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) x = 0) : CategoryStruct.comp (X.pOpcycles f g n₁) (X.descOpcycles f g n₀ n₁ hn₁ x hx) = x

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.p_descOpcycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {A : C} (x : (X.H n₁).obj (ComposableArrows.mk₁ f) ⟶ A) (hx : CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) x = 0) {Z : C} (h : A ⟶ Z) : CategoryStruct.comp (X.pOpcycles f g n₁) (CategoryStruct.comp (X.descOpcycles f g n₀ n₁ hn₁ x hx) h) = CategoryStruct.comp x h

noncomputable def CategoryTheory.Abelian.SpectralObject.cyclesMap {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (n : ℤ) : X.cycles f g n ⟶ X.cycles f' g' n

The functoriality of X.cycles with respect to morphisms in ComposableArrows ι 2.

theorem CategoryTheory.Abelian.SpectralObject.cyclesMap_i {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (β : ComposableArrows.mk₁ g ⟶ ComposableArrows.mk₁ g') (n : ℤ) (hβ : β = ComposableArrows.homMk₁ (α.app 1) (α.app 2) ⋯ := by cat_disch) : CategoryStruct.comp (X.cyclesMap f g f' g' α n) (X.iCycles f' g' n) = CategoryStruct.comp (X.iCycles f g n) ((X.H n).map β)

theorem CategoryTheory.Abelian.SpectralObject.cyclesMap_i_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (β : ComposableArrows.mk₁ g ⟶ ComposableArrows.mk₁ g') (n : ℤ) (hβ : β = ComposableArrows.homMk₁ (α.app 1) (α.app 2) ⋯ := by cat_disch) {Z : C} (h : (X.H n).obj (ComposableArrows.mk₁ g') ⟶ Z) : CategoryStruct.comp (X.cyclesMap f g f' g' α n) (CategoryStruct.comp (X.iCycles f' g' n) h) = CategoryStruct.comp (X.iCycles f g n) (CategoryStruct.comp ((X.H n).map β) h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesMap_id {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : X.cyclesMap f g f g (CategoryStruct.id (ComposableArrows.mk₂ f g)) n = CategoryStruct.id (X.cycles f g n)

theorem CategoryTheory.Abelian.SpectralObject.cyclesMap_comp {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') {i'' j'' k'' : ι} (f'' : i'' ⟶ j'') (g'' : j'' ⟶ k'') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (α' : ComposableArrows.mk₂ f' g' ⟶ ComposableArrows.mk₂ f'' g'') (α'' : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f'' g'') (n : ℤ) (h : CategoryStruct.comp α α' = α'' := by cat_disch) : CategoryStruct.comp (X.cyclesMap f g f' g' α n) (X.cyclesMap f' g' f'' g'' α' n) = X.cyclesMap f g f'' g'' α'' n

theorem CategoryTheory.Abelian.SpectralObject.cyclesMap_comp_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') {i'' j'' k'' : ι} (f'' : i'' ⟶ j'') (g'' : j'' ⟶ k'') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (α' : ComposableArrows.mk₂ f' g' ⟶ ComposableArrows.mk₂ f'' g'') (α'' : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f'' g'') (n : ℤ) (h : CategoryStruct.comp α α' = α'' := by cat_disch) {Z : C} (h✝ : X.cycles f'' g'' n ⟶ Z) : CategoryStruct.comp (X.cyclesMap f g f' g' α n) (CategoryStruct.comp (X.cyclesMap f' g' f'' g'' α' n) h✝) = CategoryStruct.comp (X.cyclesMap f g f'' g'' α'' n) h✝

noncomputable def CategoryTheory.Abelian.SpectralObject.opcyclesMap {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (n : ℤ) : X.opcycles f g n ⟶ X.opcycles f' g' n

The functoriality of X.opcycles with respect to morphisms in ComposableArrows ι 2.

theorem CategoryTheory.Abelian.SpectralObject.p_opcyclesMap {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (β : ComposableArrows.mk₁ f ⟶ ComposableArrows.mk₁ f') (n : ℤ) (hβ : β = ComposableArrows.homMk₁ (α.app 0) (α.app 1) ⋯ := by cat_disch) : CategoryStruct.comp (X.pOpcycles f g n) (X.opcyclesMap f g f' g' α n) = CategoryStruct.comp ((X.H n).map β) (X.pOpcycles f' g' n)

theorem CategoryTheory.Abelian.SpectralObject.p_opcyclesMap_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (β : ComposableArrows.mk₁ f ⟶ ComposableArrows.mk₁ f') (n : ℤ) (hβ : β = ComposableArrows.homMk₁ (α.app 0) (α.app 1) ⋯ := by cat_disch) {Z : C} (h : X.opcycles f' g' n ⟶ Z) : CategoryStruct.comp (X.pOpcycles f g n) (CategoryStruct.comp (X.opcyclesMap f g f' g' α n) h) = CategoryStruct.comp ((X.H n).map β) (CategoryStruct.comp (X.pOpcycles f' g' n) h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMap_id {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : X.opcyclesMap f g f g (CategoryStruct.id (ComposableArrows.mk₂ f g)) n = CategoryStruct.id (X.opcycles f g n)

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMap_comp {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') {i'' j'' k'' : ι} (f'' : i'' ⟶ j'') (g'' : j'' ⟶ k'') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (α' : ComposableArrows.mk₂ f' g' ⟶ ComposableArrows.mk₂ f'' g'') (α'' : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f'' g'') (n : ℤ) (h : CategoryStruct.comp α α' = α'' := by cat_disch) : CategoryStruct.comp (X.opcyclesMap f g f' g' α n) (X.opcyclesMap f' g' f'' g'' α' n) = X.opcyclesMap f g f'' g'' α'' n

noncomputable def CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : Limits.cokernel ((X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)) ≅ X.cycles f g n

X.cycles also identifies to a cokernel. More precisely, Z^n(f, g) identifies to the cokernel of H^n(f) ⟶ H^n(f ≫ g)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : CategoryStruct.comp (Limits.cokernel.π ((X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h))) (CategoryStruct.comp (X.cokernelIsoCycles f g fg h n).hom (X.iCycles f g n)) = (X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h✝ : (X.H n).obj (ComposableArrows.mk₁ g) ⟶ Z) : CategoryStruct.comp (Limits.cokernel.π ((X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h))) (CategoryStruct.comp (X.cokernelIsoCycles f g fg h n).hom (CategoryStruct.comp (X.iCycles f g n) h✝)) = CategoryStruct.comp ((X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)) h✝

noncomputable def CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : X.opcycles f g n ≅ Limits.kernel ((X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h))

X.opcycles also identifies to a kernel. More precisely, opZ(f, g) identifies to the kernel of H^n(f ≫ g) ⟶ H^n(g)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : CategoryStruct.comp (X.pOpcycles f g n) (CategoryStruct.comp (X.opcyclesIsoKernel f g fg h n).hom (Limits.kernel.ι ((X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)))) = (X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h✝ : (X.H n).obj (ComposableArrows.mk₁ fg) ⟶ Z) : CategoryStruct.comp (X.pOpcycles f g n) (CategoryStruct.comp (X.opcyclesIsoKernel f g fg h n).hom (CategoryStruct.comp (Limits.kernel.ι ((X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h))) h✝)) = CategoryStruct.comp ((X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)) h✝

noncomputable def CategoryTheory.Abelian.SpectralObject.toCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.H n).obj (ComposableArrows.mk₁ fg) ⟶ X.cycles f g n

The map H^n(fg) ⟶ H^n(g) factors through Z^n(f, g).

instance CategoryTheory.Abelian.SpectralObject.instEpiToCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : Epi (X.toCycles f g fg h n)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.toCycles_i {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : CategoryStruct.comp (X.toCycles f g fg h n) (X.iCycles f g n) = (X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.toCycles_i_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h✝ : (X.H n).obj (ComposableArrows.mk₁ g) ⟶ Z) : CategoryStruct.comp (X.toCycles f g fg h n) (CategoryStruct.comp (X.iCycles f g n) h✝) = CategoryStruct.comp ((X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)) h✝

theorem CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (fg' : i' ⟶ k') (h' : CategoryStruct.comp f' g' = fg') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (β : ComposableArrows.mk₁ fg ⟶ ComposableArrows.mk₁ fg') (n : ℤ) (hβ₀ : β.app 0 = α.app 0 := by cat_disch) (hβ₁ : β.app 1 = α.app 2 := by cat_disch) : CategoryStruct.comp (X.toCycles f g fg h n) (X.cyclesMap f g f' g' α n) = CategoryStruct.comp ((X.H n).map β) (X.toCycles f' g' fg' h' n)

theorem CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (fg' : i' ⟶ k') (h' : CategoryStruct.comp f' g' = fg') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (β : ComposableArrows.mk₁ fg ⟶ 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) : CategoryStruct.comp (X.toCycles f g fg h n) (CategoryStruct.comp (X.cyclesMap f g f' g' α n) h✝) = CategoryStruct.comp ((X.H n).map β) (CategoryStruct.comp (X.toCycles f' g' fg' h' n) h✝)

noncomputable def CategoryTheory.Abelian.SpectralObject.fromOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : X.opcycles f g n ⟶ (X.H n).obj (ComposableArrows.mk₁ fg)

The map H^n(f) ⟶ H^n(f ≫ g) factors through opZ^n(f, g).

instance CategoryTheory.Abelian.SpectralObject.instMonoFromOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : Mono (X.fromOpcycles f g fg h n)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.p_fromOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : CategoryStruct.comp (X.pOpcycles f g n) (X.fromOpcycles f g fg h n) = (X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.p_fromOpcycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h✝ : (X.H n).obj (ComposableArrows.mk₁ fg) ⟶ Z) : CategoryStruct.comp (X.pOpcycles f g n) (CategoryStruct.comp (X.fromOpcycles f g fg h n) h✝) = CategoryStruct.comp ((X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)) h✝

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (fg' : i' ⟶ k') (h' : CategoryStruct.comp f' g' = fg') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (β : ComposableArrows.mk₁ fg ⟶ ComposableArrows.mk₁ fg') (n : ℤ) (hβ₀ : β.app 0 = α.app 0 := by cat_disch) (hβ₁ : β.app 1 = α.app 2 := by cat_disch) : CategoryStruct.comp (X.opcyclesMap f g f' g' α n) (X.fromOpcycles f' g' fg' h' n) = CategoryStruct.comp (X.fromOpcycles f g fg h n) ((X.H n).map β)

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (fg' : i' ⟶ k') (h' : CategoryStruct.comp f' g' = fg') (α : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g') (β : ComposableArrows.mk₁ fg ⟶ 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 (ComposableArrows.mk₁ fg') ⟶ Z) : CategoryStruct.comp (X.opcyclesMap f g f' g' α n) (CategoryStruct.comp (X.fromOpcycles f' g' fg' h' n) h✝) = CategoryStruct.comp (X.fromOpcycles f g fg h n) (CategoryStruct.comp ((X.H n).map β) h✝)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : CategoryStruct.comp ((X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)) (X.toCycles f g fg h n) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h✝ : X.cycles f g n ⟶ Z) : CategoryStruct.comp ((X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)) (CategoryStruct.comp (X.toCycles f g fg h n) h✝) = CategoryStruct.comp 0 h✝

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : CategoryStruct.comp (X.fromOpcycles f g fg h n) ((X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h✝ : (X.H n).obj (ComposableArrows.mk₁ g) ⟶ Z) : CategoryStruct.comp (X.fromOpcycles f g fg h n) (CategoryStruct.comp ((X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)) h✝) = CategoryStruct.comp 0 h✝

noncomputable def CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : ShortComplex C

The short complex expressing Z^n(f, g) as a cokernel of the map H^n(f) ⟶ H^n(f ≫ g).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.cokernelSequenceCycles f g fg h n).X₁ = (X.H n).obj (ComposableArrows.mk₁ f)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.cokernelSequenceCycles f g fg h n).f = (X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_X₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.cokernelSequenceCycles f g fg h n).X₂ = (X.H n).obj (ComposableArrows.mk₁ fg)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.cokernelSequenceCycles f g fg h n).g = X.toCycles f g fg h n

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.cokernelSequenceCycles f g fg h n).X₃ = X.cycles f g n

noncomputable def CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : ShortComplex C

The short complex expressing opZ^n(f, g) as a kernel of the map H^n(f ≫ g) ⟶ H^n(g).

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_f {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.kernelSequenceOpcycles f g fg h n).f = X.fromOpcycles f g fg h n

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_g {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.kernelSequenceOpcycles f g fg h n).g = (X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_X₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.kernelSequenceOpcycles f g fg h n).X₃ = (X.H n).obj (ComposableArrows.mk₁ g)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_X₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.kernelSequenceOpcycles f g fg h n).X₂ = (X.H n).obj (ComposableArrows.mk₁ fg)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_X₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.kernelSequenceOpcycles f g fg h n).X₁ = X.opcycles f g n

instance CategoryTheory.Abelian.SpectralObject.instEpiGCokernelSequenceCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : Epi (X.cokernelSequenceCycles f g fg h n).g

instance CategoryTheory.Abelian.SpectralObject.instMonoFKernelSequenceOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : Mono (X.kernelSequenceOpcycles f g fg h n).f

theorem CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_exact {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.cokernelSequenceCycles f g fg h n).Exact

Z^n(f, g) identifies to a cokernel of the H^n(f) ⟶ H^n(f ≫ g).

theorem CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_exact {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) : (X.kernelSequenceOpcycles f g fg h n).Exact

opZ^n(f, g) identifies to the kernel of H^n(f ≫ g) ⟶ H^n(g).

theorem CategoryTheory.Abelian.SpectralObject.isIso_toCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) (hf : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ f))) : IsIso (X.toCycles f g fg h n)

theorem CategoryTheory.Abelian.SpectralObject.isIso_fromOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) (n : ℤ) (hg : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ g))) : IsIso (X.fromOpcycles f g fg h n)

noncomputable def CategoryTheory.Abelian.SpectralObject.descCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) {A : C} {n : ℤ} (x : (X.H n).obj (ComposableArrows.mk₁ fg) ⟶ A) (hx : CategoryStruct.comp ((X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)) x = 0) : X.cycles f g n ⟶ A

Constructor for morphisms from X.cycles.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.toCycles_descCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) {A : C} {n : ℤ} (x : (X.H n).obj (ComposableArrows.mk₁ fg) ⟶ A) (hx : CategoryStruct.comp ((X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)) x = 0) : CategoryStruct.comp (X.toCycles f g fg h n) (X.descCycles f g fg h x hx) = x

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.toCycles_descCycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) {A : C} {n : ℤ} (x : (X.H n).obj (ComposableArrows.mk₁ fg) ⟶ A) (hx : CategoryStruct.comp ((X.H n).map (ComposableArrows.twoδ₂Toδ₁ f g fg h)) x = 0) {Z : C} (h✝ : A ⟶ Z) : CategoryStruct.comp (X.toCycles f g fg h n) (CategoryStruct.comp (X.descCycles f g fg h x hx) h✝) = CategoryStruct.comp x h✝

noncomputable def CategoryTheory.Abelian.SpectralObject.liftOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) {A : C} {n : ℤ} (x : A ⟶ (X.H n).obj (ComposableArrows.mk₁ fg)) (hx : CategoryStruct.comp x ((X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0) : A ⟶ X.opcycles f g n

Constructor for morphisms to X.opcycles.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.liftOpcycles_fromOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) {A : C} {n : ℤ} (x : A ⟶ (X.H n).obj (ComposableArrows.mk₁ fg)) (hx : CategoryStruct.comp x ((X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0) : CategoryStruct.comp (X.liftOpcycles f g fg h x hx) (X.fromOpcycles f g fg h n) = x

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.liftOpcycles_fromOpcycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) {A : C} {n : ℤ} (x : A ⟶ (X.H n).obj (ComposableArrows.mk₁ fg)) (hx : CategoryStruct.comp x ((X.H n).map (ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0) {Z : C} (h✝ : (X.H n).obj (ComposableArrows.mk₁ fg) ⟶ Z) : CategoryStruct.comp (X.liftOpcycles f g fg h x hx) (CategoryStruct.comp (X.fromOpcycles f g fg h n) h✝) = CategoryStruct.comp x h✝

noncomputable def CategoryTheory.Abelian.SpectralObject.δToCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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 (ComposableArrows.mk₁ f₃) ⟶ X.cycles f₁ f₂ n₁

The morphism H^{n₀}(f₃) ⟶ Z^{n₁}(f₁, f₂) induced by δ when f₁, f₂, f₃ are composable morphisms and n₀ + 1 = n₁.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.δToCycles_iCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) : CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (X.iCycles f₁ f₂ n₁) = X.δ f₂ f₃ n₀ n₁ hn₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.δToCycles_iCycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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 (ComposableArrows.mk₁ f₂) ⟶ Z) : CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (CategoryStruct.comp (X.iCycles f₁ f₂ n₁) h) = CategoryStruct.comp (X.δ f₂ f₃ n₀ n₁ hn₁) h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.δ_toCycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) = X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.δ_toCycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : X.cycles f₁ f₂ n₁ ⟶ Z) : CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) (CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₁) h) = CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) h

noncomputable def CategoryTheory.Abelian.SpectralObject.δFromOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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 (ComposableArrows.mk₁ f₁)

The morphism opZ^{n₀}(f₂, f₃) ⟶ H^{n₁}(f₁) induced by δ when f₁, f₂, f₃ are composable morphisms and n₀ + 1 = n₁.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.pOpcycles_δFromOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) : CategoryStruct.comp (X.pOpcycles f₂ f₃ n₀) (X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁) = X.δ f₁ f₂ n₀ n₁ hn₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.pOpcycles_δFromOpcycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : 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 (ComposableArrows.mk₁ f₁) ⟶ Z) : CategoryStruct.comp (X.pOpcycles f₂ f₃ n₀) (CategoryStruct.comp (X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁) h) = CategoryStruct.comp (X.δ f₁ f₂ n₀ n₁ hn₁) h

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : CategoryStruct.comp (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀) (X.δ f₁ f₂₃ n₀ n₁ hn₁) = X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] (X : SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) {Z : C} (h : (X.H n₁).obj (ComposableArrows.mk₁ f₁) ⟶ Z) : CategoryStruct.comp (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀) (CategoryStruct.comp (X.δ f₁ f₂₃ n₀ n₁ hn₁) h) = CategoryStruct.comp (X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁) h