Theorems · Theorem · category theory

CategoryTheory.DifferentialObject.d_squared

∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  (self : CategoryTheory.DifferentialObject S C),
  CategoryTheory.CategoryStruct.comp self.d ((CategoryTheory.shiftFunctor C 1).map self.d) = 0

The differential d satisfies that d² = 0.

Defined in

Mathlib.CategoryTheory.DifferentialObject

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddMonoidWithOneCategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.HasShift