Theorems · Theorem · category theory

CategoryTheory.ShortComplex.homMk.congr_simp

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (τ₁ τ₁_1 : S₁.X₁ ⟶ S₂.X₁) (e_τ₁ : τ₁ = τ₁_1) (τ₂ τ₂_1 : S₁.X₂ ⟶ S₂.X₂)
  (e_τ₂ : τ₂ = τ₂_1) (τ₃ τ₃_1 : S₁.X₃ ⟶ S₂.X₃) (e_τ₃ : τ₃ = τ₃_1)
  (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂)
  (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃),
  CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃ = CategoryTheory.ShortComplex.homMk τ₁_1 τ₂_1 τ₃_1 ⋯ ⋯

Defined in

Mathlib.Algebra.Homology.ShortComplex.Basic

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms