Theorems · Theorem · category theory

ChainComplex.mk_d

∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0)
  (n : ℕ),
  (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 3) (n + 2) =
    CategoryTheory.CategoryStruct.comp (ChainComplex.mkXIso X₀ X₁ X₂ d₀ d₁ s succ n).hom
      (succ
            { X₁ := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2),
              X₂ := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
              X₃ := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X n,
              f := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
              g := (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).snd.fst

Defined in

Mathlib.Algebra.Homology.HomologicalComplex

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms