Theorems · Theorem · category theory

CategoryTheory.DifferentialObject.objEqToHom_d

∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x y : β} (h : x = y),
  CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (X.d y) =
    CategoryTheory.CategoryStruct.comp (X.d x) (X.objEqToHom ⋯)

Defined in

Mathlib.Algebra.Homology.DifferentialObject

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupCategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms