Theorems · Inductive type · category theory

CategoryTheory.DifferentialObject

(S : Type u_1) →
  [inst : AddMonoidWithOne S] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [CategoryTheory.Limits.HasZeroMorphisms C] → [CategoryTheory.HasShift C S] → Type (max u v)

A differential object in a category with zero morphisms and a shift is an object obj equipped with a morphism d : obj ⟶ obj⟦1⟧, such that d^2 = 0.

Defined in

Mathlib.CategoryTheory.DifferentialObject

Cited by

61 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

AddMonoidWithOneCategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.HasShift