Theorems · Theorem · category theory

CategoryTheory.Abelian.SpectralObject.opcyclesToE_map

∀ {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₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁')
  (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (f₁₂' : i₀' ⟶ i₂') (h₁₂' : CategoryTheory.CategoryStruct.comp f₁' f₂' = f₁₂')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (β : CategoryTheory.ComposableArrows.mk₂ f₁₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₂ f₁₂' f₃') (n₀ n₁ n₂ : ℤ),
  autoParam (β.app 0 = α.app 0) CategoryTheory.Abelian.SpectralObject.opcyclesToE_map._auto_1 →
    autoParam (β.app 1 = α.app 2) CategoryTheory.Abelian.SpectralObject.opcyclesToE_map._auto_3 →
      ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesToE_map._auto_5)
        (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesToE_map._auto_7),
        CategoryTheory.CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)
            (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) =
          CategoryTheory.CategoryStruct.comp (X.opcyclesMap f₁₂ f₃ f₁₂' f₃' β n₁)
            (X.opcyclesToE f₁' f₂' f₃' f₁₂' h₁₂' n₀ n₁ n₂ hn₁ hn₂)

Defined in

Mathlib.Algebra.Homology.SpectralObject.Page

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Abelian