Induced morphisms that are epi or mono

Given a spectral object in an abelian category, we show that certain morphisms E^n(f₁, f₂, f₃) ⟶ E^n(f₁', f₂', f₃') are monomorphisms, epimorphisms or isomorphisms.

References

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

theorem CategoryTheory.Abelian.SpectralObject.epi_map {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₃' : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₃' : i₂ ⟶ i₃') (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁ f₂ f₃') (n₀ n₁ n₂ n₃ : ℤ) (hα₀ : α.app 0 = CategoryStruct.id ((ComposableArrows.mk₃ f₁ f₂ f₃).obj 0) := by cat_disch) (hα₁ : α.app 1 = CategoryStruct.id ((ComposableArrows.mk₃ f₁ f₂ f₃).obj 1) := by cat_disch) (hα₂ : α.app 2 = CategoryStruct.id ((ComposableArrows.mk₃ f₁ f₂ f₃).obj 2) := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) : Epi (X.map f₁ f₂ f₃ f₁ f₂ f₃' α n₀ n₁ n₂ hn₁ hn₂)

theorem CategoryTheory.Abelian.SpectralObject.mono_map {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀' i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₁' : i₀' ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (α : ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ ComposableArrows.mk₃ f₁' f₂ f₃) (n₀ n₁ n₂ n₃ : ℤ) (hα₁ : α.app 1 = CategoryStruct.id ((ComposableArrows.mk₃ f₁ f₂ f₃).obj 1) := by cat_disch) (hα₂ : α.app 2 = CategoryStruct.id ((ComposableArrows.mk₃ f₁ f₂ f₃).obj 2) := by cat_disch) (hα₃ : α.app 3 = CategoryStruct.id ((ComposableArrows.mk₃ f₁ f₂ f₃).obj 3) := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) : Mono (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) : CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (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) : CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) (CategoryStruct.comp (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃) h) = CategoryStruct.comp 0 h

instance CategoryTheory.Abelian.SpectralObject.instEpiMapFourδ₄Toδ₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ : ι} (f₁ : 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₃) : Epi (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)

theorem CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) (n₁ n₂ n₃ : ℤ) (h : (X.H n₁).map (ComposableArrows.twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0 := by cat_disch) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) : IsIso (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)

theorem CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃_of_isZero {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryStruct.comp f₃ f₄ = f₃₄) (n₁ n₂ n₃ : ℤ) (h : Limits.IsZero ((X.H n₁).obj (ComposableArrows.mk₁ f₄)) := by cat_disch) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) : IsIso (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ n₃ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) : CategoryStruct.comp (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂) (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) = 0

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d_assoc {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ n₃ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (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) : CategoryStruct.comp (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) h) = CategoryStruct.comp 0 h

instance CategoryTheory.Abelian.SpectralObject.instMonoMapFourδ₁Toδ₀ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₁ i₂ i₃ i₄ i₅ : ι} (f₂ : 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₂) : Mono (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)

theorem CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀ {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₁ i₂ i₃ i₄ i₅ : ι} (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (h : (X.H n₂).map (ComposableArrows.twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0 := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : IsIso (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)

theorem CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀_of_isZero {C : Type u_1} {ι : Type u_2} [Category.{v_1, u_1} C] [Abelian C] [Category.{v_2, u_2} ι] (X : SpectralObject C ι) {i₁ i₂ i₃ i₄ i₅ : ι} (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X.H n₂).obj (ComposableArrows.mk₁ f₂))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : IsIso (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀' {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X'.E (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂ ⟶ X'.E (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂

For a spectral object indexed by a preorder, this is the map E^{n₁}(i₀ ≤ i₂ ≤ i₃ ≤ i₄) ⟶ E^{n₁}(i₁ ≤ i₂ ≤ i₃ ≤ i₄).

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃' {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X'.E (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE hi₂₃) n₀ n₁ n₂ hn₁ hn₂ ⟶ X'.E (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂

For a spectral object indexed by a preorder, this is the map E^{n₁}(i₀ ≤ i₁ ≤ i₂ ≤ i₃) ⟶ E^{n₁}(i₀ ≤ i₁ ≤ i₂ ≤ i₄).

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ i₅ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (hi₄₅ : i₄ ≤ i₅) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₃ i₄ i₅ hi₀₁ ⋯ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) (X'.mapFourδ₁Toδ₀' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) = X'.mapFourδ₁Toδ₀' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂

theorem CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp_assoc {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ i₅ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (hi₄₅ : i₄ ≤ i₅) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X'.E (homOfLE hi₂₃) (homOfLE hi₃₄) (homOfLE hi₄₅) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₃ i₄ i₅ hi₀₁ ⋯ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) h

theorem CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ i₅ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (hi₄₅ : i₄ ≤ i₅) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₄ i₅ hi₀₁ hi₁₂ ⋯ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) = X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂

theorem CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp_assoc {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ i₅ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (hi₄₅ : i₄ ≤ i₅) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X'.E (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₄ i₅ hi₀₁ hi₁₂ ⋯ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂) h

theorem CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃' {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ i₅ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (hi₄₅ : i₄ ≤ i₅) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) (X'.mapFourδ₄Toδ₃' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) = CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂)

theorem CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'_assoc {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ i₅ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (hi₄₅ : i₄ ≤ i₅) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : X'.E (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) h) = CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂) h)

theorem CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₁Toδ₀' {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₂).obj (ComposableArrows.mk₁ (homOfLE hi₀₁)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : IsIso (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)

noncomputable def CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀' {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₂).obj (ComposableArrows.mk₁ (homOfLE hi₀₁)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X'.E (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂ ≅ X'.E (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂

For a spectral object indexed by a preorder, this is the isomorphism E^{n₁}(i₀ ≤ i₂ ≤ i₃ ≤ i₄) ≅ E^{n₁}(i₁ ≤ i₂ ≤ i₃ ≤ i₄) when H^{n₁ + 1}(i₀ ≤ i₁) is a zero object.

Equations

• X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂ = CategoryTheory.asIso (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₂).obj (ComposableArrows.mk₁ (homOfLE hi₀₁)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).hom = X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₂).obj (ComposableArrows.mk₁ (homOfLE hi₀₁)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) (X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv = CategoryStruct.id (X'.E (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id_assoc {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₂).obj (ComposableArrows.mk₁ (homOfLE hi₀₁)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h✝ : X'.E (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv h✝) = h✝

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₂).obj (ComposableArrows.mk₁ (homOfLE hi₀₁)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) = CategoryStruct.id (X'.E (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id_assoc {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₂).obj (ComposableArrows.mk₁ (homOfLE hi₀₁)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h✝ : X'.E (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv (CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) h✝) = h✝

theorem CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₄Toδ₃' {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₀).obj (ComposableArrows.mk₁ (homOfLE hi₃₄)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : IsIso (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)

noncomputable def CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₃' {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₀).obj (ComposableArrows.mk₁ (homOfLE hi₃₄)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X'.E (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE hi₂₃) n₀ n₁ n₂ hn₁ hn₂ ≅ X'.E (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂

For a spectral object indexed by a preorder, this is the isomorphism E^{n₁}(i₀ ≤ i₁ ≤ i₂ ≤ i₃) ≅ E^{n₁}(i₀ ≤ i₁ ≤ i₂ ≤ i₄) when H^{n₁-1}(i₃ ≤ i₄) is a zero object.

Equations

• X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂ = CategoryTheory.asIso (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₃'_hom {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₀).obj (ComposableArrows.mk₁ (homOfLE hi₃₄)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).hom = X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₀).obj (ComposableArrows.mk₁ (homOfLE hi₃₄)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) (X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv = CategoryStruct.id (X'.E (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE hi₂₃) n₀ n₁ n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id_assoc {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₀).obj (ComposableArrows.mk₁ (homOfLE hi₃₄)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h✝ : X'.E (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE hi₂₃) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) (CategoryStruct.comp (X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv h✝) = h✝

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₀).obj (ComposableArrows.mk₁ (homOfLE hi₃₄)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryStruct.comp (X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) = CategoryStruct.id (X'.E (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id_assoc {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h : Limits.IsZero ((X'.H n₀).obj (ComposableArrows.mk₁ (homOfLE hi₃₄)))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h✝ : X'.E (homOfLE hi₀₁) (homOfLE hi₁₂) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z) : CategoryStruct.comp (X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv (CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) h✝) = h✝

@[reducible, inline]

noncomputable abbrev CategoryTheory.Abelian.SpectralObject.mapFourδ₂Toδ₁' {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : X'.E (homOfLE hi₀₁) (homOfLE ⋯) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂ ⟶ X'.E (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂

For a spectral object indexed by a preorder, this is the map E^{n₁}(i₀ ≤ i₁ ≤ i₃ ≤ i₄) ⟶ E^{n₁}(i₀ ≤ i₂ ≤ i₃ ≤ i₄).

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₂Toδ₁' {C : Type u_1} {ι' : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι'] (X' : SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ) (h₁ : IsIso ((X'.H n₁).map (ComposableArrows.twoδ₁Toδ₀' i₁ i₂ i₃ hi₁₂ hi₂₃))) (h₂ : IsIso ((X'.H n₂).map (ComposableArrows.twoδ₂Toδ₁' i₀ i₁ i₂ hi₀₁ hi₁₂))) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : IsIso (X'.mapFourδ₂Toδ₁' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)