Theorems · Definition · category theory

CategoryTheory.DifferentialObject.shiftZero

{S : Type u_1} →
  [inst : AddCommGroupWithOne S] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            CategoryTheory.DifferentialObject.shiftFunctor C 0 ≅
              CategoryTheory.Functor.id (CategoryTheory.DifferentialObject S C)

The shift by zero is naturally isomorphic to the identity.

Defined in: Mathlib.CategoryTheory.DifferentialObject
Cited by: 2 results in Mathlib
Foundations: Depth 47 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommGroupWithOne CategoryTheory.Category CategoryTheory.Limits.HasZeroMorphisms CategoryTheory.HasShift

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Functorstatement · cited by 16,252
CategoryTheory.Isostatement · cited by 3,963
CategoryTheory.Functor.idstatement · cited by 3,333
CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
CategoryTheory.HasShiftstatement and proof · cited by 1,527
CategoryTheory.Iso.appproof · cited by 253
CategoryTheory.NatIso.ofComponentsproof · cited by 178
CategoryTheory.shiftFunctorZeroproof · cited by 82
CategoryTheory.DifferentialObjectstatement and proof · cited by 61
AddCommGroupWithOnestatement and proof · cited by 61
CategoryTheory.DifferentialObject.objproof · cited by 50

Cited by2

Results whose statement or proof uses this declaration.

CategoryTheory.DifferentialObject.shiftZero_hom_app_fstatement and proof · cited by 0
CategoryTheory.DifferentialObject.shiftZero_inv_app_fstatement and proof · cited by 0