Theorems · Theorem · category theory

CategoryTheory.Abelian.SpectralObject.EIsoH_hom_naturality

∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) {i' j' : ι} (f' : i' ⟶ j')
  (α : CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ f')
  (β :
    CategoryTheory.ComposableArrows.mk₃ (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) ⟶
      CategoryTheory.ComposableArrows.mk₃ (CategoryTheory.CategoryStruct.id i') f'
        (CategoryTheory.CategoryStruct.id j'))
  (n₀ n₁ n₂ : ℤ),
  autoParam (β = CategoryTheory.ComposableArrows.homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯)
      CategoryTheory.Abelian.SpectralObject.EIsoH_hom_naturality._auto_1 →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.EIsoH_hom_naturality._auto_3)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.EIsoH_hom_naturality._auto_5),
      CategoryTheory.CategoryStruct.comp
          (X.map (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j)
            (CategoryTheory.CategoryStruct.id i') f' (CategoryTheory.CategoryStruct.id j') β n₀ n₁ n₂ hn₁ hn₂)
          (X.EIsoH f' n₀ n₁ n₂ hn₁ hn₂).hom =
        CategoryTheory.CategoryStruct.comp (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ((X.H n₁).map α)

Defined in

Mathlib.Algebra.Homology.SpectralObject.Page

Cited by

0 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Abelian