Functoriality of the pages of spectral objects

Let φ : X ⟶ Y be a morphism of spectral objects in an abelian category. We define the induced maps on the objects E^n(f₁, f₂, f₃) (CategoryTheory.Abelian.SpectralObject.EMap), on the cycles Z^n(f, g) (CategoryTheory.Abelian.SpectralObject.cyclesMapOfHom), and show that they are functorial in φ (EMap_id, EMap_comp, cyclesMapOfHom_id, cyclesMapOfHom_comp) and compatible with the projections πE, the maps toCycles, the functoriality maps X.map in the indices, and the differentials X.d (CategoryTheory.Abelian.SpectralObject.d_EMap). These are the ingredients of the morphism of spectral sequences induced by φ.

Main definitions

• CategoryTheory.Abelian.SpectralObject.EMap φ f₁ f₂ f₃ n₀ n₁ n₂: the map X.E f₁ f₂ f₃ n₀ n₁ n₂ ⟶ Y.E f₁ f₂ f₃ n₀ n₁ n₂.
• CategoryTheory.Abelian.SpectralObject.cyclesMapOfHom φ f g n: the map on cycles.
• CategoryTheory.Abelian.SpectralObject.opcyclesMapOfHom φ f g n: the map on opcycles, with isIso_opcyclesMapOfHom_of_isIso (three-lemma on Mathlib's short exact sequences 0 ⟶ opZ^n(f₁, f₂ ≫ f₃) ⟶ opZ^n(f₁ ≫ f₂, f₃) ⟶ E^n(f₁, f₂, f₃) ⟶ 0).

Main results

• CategoryTheory.Abelian.SpectralObject.EMap_id, EMap_comp: functoriality.
• CategoryTheory.Abelian.SpectralObject.map_EMap: compatibility with X.map.
• CategoryTheory.Abelian.SpectralObject.d_EMap: compatibility with the differentials.

References

• The constructions adapt to morphisms of spectral objects those of Joël Riou's Mathlib files Mathlib/Algebra/Homology/SpectralObject/{Page,Cycles,Differentials}.lean (shortComplexMap, map, cyclesMap, πE_map), which are functorial in the indices.
• J.-L. Verdier, Des catégories dérivées des catégories abéliennes, Astérisque 239 (1996), II.4.

def CategoryTheory.Abelian.SpectralObject.shortComplexMapOfHom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Y.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

The morphism of short complexes X.shortComplex f₁ f₂ f₃ ⟶ Y.shortComplex f₁ f₂ f₃ induced by a morphism of spectral objects.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMapOfHom_τ₁ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : (shortComplexMapOfHom φ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).τ₁ = (φ.hom n₀).app (ComposableArrows.mk₁ f₃)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMapOfHom_τ₂ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : (shortComplexMapOfHom φ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).τ₂ = (φ.hom n₁).app (ComposableArrows.mk₁ f₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMapOfHom_τ₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : (shortComplexMapOfHom φ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).τ₃ = (φ.hom n₂).app (ComposableArrows.mk₁ f₁)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMapOfHom_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 l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : shortComplexMapOfHom (CategoryStruct.id X) f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ = CategoryStruct.id (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)

@[simp]

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

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMapOfHom_comp_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y Z : SpectralObject C ι} (φ : X ⟶ Y) (ψ : Y ⟶ Z) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {Z✝ : ShortComplex C} (h : Z.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Z✝) : CategoryStruct.comp (shortComplexMapOfHom (CategoryStruct.comp φ ψ) f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h = CategoryStruct.comp (shortComplexMapOfHom φ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (shortComplexMapOfHom ψ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h)

noncomputable def CategoryTheory.Abelian.SpectralObject.EMap {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Y.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂

The morphism X.E f₁ f₂ f₃ n₀ n₁ n₂ ⟶ Y.E f₁ f₂ f₃ n₀ n₁ n₂ induced by a morphism of spectral objects.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.EMap_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 l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : EMap (CategoryStruct.id X) f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ = CategoryStruct.id (X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)

@[simp]

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

theorem CategoryTheory.Abelian.SpectralObject.EMap_comp_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y Z : SpectralObject C ι} (φ : X ⟶ Y) (ψ : Y ⟶ Z) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {Z✝ : C} (h : Z.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Z✝) : CategoryStruct.comp (EMap (CategoryStruct.comp φ ψ) f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h = CategoryStruct.comp (EMap φ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (EMap ψ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h)

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMap_shortComplexMapOfHom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i' j' k' l' : ι} {f₁' : i' ⟶ j'} {f₂' : j' ⟶ k'} {f₃' : k' ⟶ l'} (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') : CategoryStruct.comp (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) (shortComplexMapOfHom φ f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂) = CategoryStruct.comp (shortComplexMapOfHom φ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (Y.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)

The morphisms shortComplexMapOfHom commute with the functoriality maps X.shortComplexMap in the indices.

theorem CategoryTheory.Abelian.SpectralObject.shortComplexMap_shortComplexMapOfHom_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i' j' k' l' : ι} {f₁' : i' ⟶ j'} {f₂' : j' ⟶ k'} {f₃' : k' ⟶ l'} (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') {Z : ShortComplex C} (h : Y.shortComplex f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (shortComplexMapOfHom φ f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp (shortComplexMapOfHom φ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (Y.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) h)

The morphisms shortComplexMapOfHom commute with the functoriality maps X.shortComplexMap in the indices.

theorem CategoryTheory.Abelian.SpectralObject.map_EMap {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i' j' k' l' : ι} {f₁' : i' ⟶ j'} {f₂' : j' ⟶ k'} {f₃' : k' ⟶ l'} (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') : CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) (EMap φ f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂) = CategoryStruct.comp (EMap φ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (Y.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)

The maps EMap commute with the functoriality maps X.map in the indices.

theorem CategoryTheory.Abelian.SpectralObject.map_EMap_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i' j' k' l' : ι} {f₁' : i' ⟶ j'} {f₂' : j' ⟶ k'} {f₃' : k' ⟶ l'} (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂' f₃') {Z : C} (h : Y.E f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (EMap φ f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp (EMap φ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (Y.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) h)

The maps EMap commute with the functoriality maps X.map in the indices.

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

The morphism X.cycles f g n ⟶ Y.cycles f g n induced by a morphism of spectral objects.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesMapOfHom_i {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : CategoryStruct.comp (cyclesMapOfHom φ f g n) (Y.iCycles f g n) = CategoryStruct.comp (X.iCycles f g n) ((φ.hom n).app (ComposableArrows.mk₁ g))

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesMapOfHom_i_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) {Z : C} (h : (Y.H n).obj (ComposableArrows.mk₁ g) ⟶ Z) : CategoryStruct.comp (cyclesMapOfHom φ f g n) (CategoryStruct.comp (Y.iCycles f g n) h) = CategoryStruct.comp (X.iCycles f g n) (CategoryStruct.comp ((φ.hom n).app (ComposableArrows.mk₁ g)) h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesMapOfHom_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 : ℤ) : cyclesMapOfHom (CategoryStruct.id X) f g n = CategoryStruct.id (X.cycles f g n)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.cyclesMapOfHom_comp {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y Z : SpectralObject C ι} (φ : X ⟶ Y) (ψ : Y ⟶ Z) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : cyclesMapOfHom (CategoryStruct.comp φ ψ) f g n = CategoryStruct.comp (cyclesMapOfHom φ f g n) (cyclesMapOfHom ψ f g n)

theorem CategoryTheory.Abelian.SpectralObject.cyclesMapOfHom_comp_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y Z : SpectralObject C ι} (φ : X ⟶ Y) (ψ : Y ⟶ Z) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) {Z✝ : C} (h : Z.cycles f g n ⟶ Z✝) : CategoryStruct.comp (cyclesMapOfHom (CategoryStruct.comp φ ψ) f g n) h = CategoryStruct.comp (cyclesMapOfHom φ f g n) (CategoryStruct.comp (cyclesMapOfHom ψ f g n) h)

theorem CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMapOfHom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) : CategoryStruct.comp (X.toCycles f g fg h n) (cyclesMapOfHom φ f g n) = CategoryStruct.comp ((φ.hom n).app (ComposableArrows.mk₁ fg)) (Y.toCycles f g fg h n)

theorem CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMapOfHom_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) {Z : C} (h✝ : Y.cycles f g n ⟶ Z) : CategoryStruct.comp (X.toCycles f g fg h n) (CategoryStruct.comp (cyclesMapOfHom φ f g n) h✝) = CategoryStruct.comp ((φ.hom n).app (ComposableArrows.mk₁ fg)) (CategoryStruct.comp (Y.toCycles f g fg h n) h✝)

theorem CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_cyclesMap_shortComplexMapOfHom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) {l : ι} (f₃ : k ⟶ l) (n₀ n₂ : ℤ) (hn₁ : n₀ + 1 = n) (hn₂ : n + 1 = n₂) : CategoryStruct.comp (X.cyclesIso f g f₃ n₀ n n₂ hn₁ hn₂).inv (ShortComplex.cyclesMap (shortComplexMapOfHom φ f g f₃ n₀ n n₂ hn₁ hn₂)) = CategoryStruct.comp (cyclesMapOfHom φ f g n) (Y.cyclesIso f g f₃ n₀ n n₂ hn₁ hn₂).inv

Through the identifications cyclesIso, the map on cycles of shortComplexMapOfHom is cyclesMapOfHom.

theorem CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_cyclesMap_shortComplexMapOfHom_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) {l : ι} (f₃ : k ⟶ l) (n₀ n₂ : ℤ) (hn₁ : n₀ + 1 = n) (hn₂ : n + 1 = n₂) {Z : C} (h : (Y.shortComplex f g f₃ n₀ n n₂ hn₁ hn₂).cycles ⟶ Z) : CategoryStruct.comp (X.cyclesIso f g f₃ n₀ n n₂ hn₁ hn₂).inv (CategoryStruct.comp (ShortComplex.cyclesMap (shortComplexMapOfHom φ f g f₃ n₀ n n₂ hn₁ hn₂)) h) = CategoryStruct.comp (cyclesMapOfHom φ f g n) (CategoryStruct.comp (Y.cyclesIso f g f₃ n₀ n n₂ hn₁ hn₂).inv h)

Through the identifications cyclesIso, the map on cycles of shortComplexMapOfHom is cyclesMapOfHom.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.πE_EMap {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) {l : ι} (f₃ : k ⟶ l) (n₀ n₂ : ℤ) (hn₁ : n₀ + 1 = n) (hn₂ : n + 1 = n₂) : CategoryStruct.comp (X.πE f g f₃ n₀ n n₂ hn₁ hn₂) (EMap φ f g f₃ n₀ n n₂ hn₁ hn₂) = CategoryStruct.comp (cyclesMapOfHom φ f g n) (Y.πE f g f₃ n₀ n n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.πE_EMap_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) {l : ι} (f₃ : k ⟶ l) (n₀ n₂ : ℤ) (hn₁ : n₀ + 1 = n) (hn₂ : n + 1 = n₂) {Z : C} (h : Y.E f g f₃ n₀ n n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X.πE f g f₃ n₀ n n₂ hn₁ hn₂) (CategoryStruct.comp (EMap φ f g f₃ n₀ n n₂ hn₁ hn₂) h) = CategoryStruct.comp (cyclesMapOfHom φ f g n) (CategoryStruct.comp (Y.πE f g f₃ n₀ n n₂ hn₁ hn₂) h)

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

The morphism X.opcycles f g n ⟶ Y.opcycles f g n induced by a morphism of spectral objects.

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.p_opcyclesMapOfHom {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : CategoryStruct.comp (X.pOpcycles f g n) (opcyclesMapOfHom φ f g n) = CategoryStruct.comp ((φ.hom n).app (ComposableArrows.mk₁ f)) (Y.pOpcycles f g n)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.p_opcyclesMapOfHom_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) {Z : C} (h : Y.opcycles f g n ⟶ Z) : CategoryStruct.comp (X.pOpcycles f g n) (CategoryStruct.comp (opcyclesMapOfHom φ f g n) h) = CategoryStruct.comp ((φ.hom n).app (ComposableArrows.mk₁ f)) (CategoryStruct.comp (Y.pOpcycles f g n) h)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMapOfHom_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 : ℤ) : opcyclesMapOfHom (CategoryStruct.id X) f g n = CategoryStruct.id (X.opcycles f g n)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMapOfHom_comp {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y Z : SpectralObject C ι} (φ : X ⟶ Y) (ψ : Y ⟶ Z) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) : opcyclesMapOfHom (CategoryStruct.comp φ ψ) f g n = CategoryStruct.comp (opcyclesMapOfHom φ f g n) (opcyclesMapOfHom ψ f g n)

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMapOfHom_comp_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y Z : SpectralObject C ι} (φ : X ⟶ Y) (ψ : Y ⟶ Z) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) {Z✝ : C} (h : Z.opcycles f g n ⟶ Z✝) : CategoryStruct.comp (opcyclesMapOfHom (CategoryStruct.comp φ ψ) f g n) h = CategoryStruct.comp (opcyclesMapOfHom φ f g n) (CategoryStruct.comp (opcyclesMapOfHom ψ f g n) h)

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMapOfHom_fromOpcycles {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) : CategoryStruct.comp (opcyclesMapOfHom φ f g n) (Y.fromOpcycles f g fg h n) = CategoryStruct.comp (X.fromOpcycles f g fg h n) ((φ.hom n).app (ComposableArrows.mk₁ fg))

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMapOfHom_fromOpcycles_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) {Z : C} (h✝ : (Y.H n).obj (ComposableArrows.mk₁ fg) ⟶ Z) : CategoryStruct.comp (opcyclesMapOfHom φ f g n) (CategoryStruct.comp (Y.fromOpcycles f g fg h n) h✝) = CategoryStruct.comp (X.fromOpcycles f g fg h n) (CategoryStruct.comp ((φ.hom n).app (ComposableArrows.mk₁ fg)) h✝)

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

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

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMapOfHom_opcyclesToE {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) : CategoryStruct.comp (opcyclesMapOfHom φ f₁₂ f₃ n₁) (Y.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) = CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) (EMap φ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)

theorem CategoryTheory.Abelian.SpectralObject.opcyclesMapOfHom_opcyclesToE_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {Z : C} (h : Y.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (opcyclesMapOfHom φ f₁₂ f₃ n₁) (CategoryStruct.comp (Y.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (EMap φ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h)

theorem CategoryTheory.Abelian.SpectralObject.isIso_opcyclesMapOfHom_of_isIso {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) [IsIso (opcyclesMapOfHom φ f₁ f₂₃ n₁)] [IsIso (EMap φ f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)] : IsIso (opcyclesMapOfHom φ f₁₂ f₃ n₁)

A morphism of spectral objects which is an isomorphism on opZ^n(f₁, f₂ ≫ f₃) and on E^n(f₁, f₂, f₃) is an isomorphism on opZ^n(f₁ ≫ f₂, f₃).

theorem CategoryTheory.Abelian.SpectralObject.d_EMap {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (n₀ n₁ n₂ n₃ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) (hn₃ : n₂ + 1 = n₃) : CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) (EMap φ f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) = CategoryStruct.comp (EMap φ f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂) (Y.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)

The maps EMap commute with the differentials.

theorem CategoryTheory.Abelian.SpectralObject.d_EMap_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} ι] [Abelian C] {X Y : SpectralObject C ι} (φ : X ⟶ Y) {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (n₀ n₁ n₂ n₃ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) (hn₃ : n₂ + 1 = n₃) {Z : C} (h : Y.E f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ ⟶ Z) : CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) (CategoryStruct.comp (EMap φ f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) h) = CategoryStruct.comp (EMap φ f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (Y.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) h)

The maps EMap commute with the differentials.