Theorems · Definition · category theory
CategoryTheory.shiftEquiv
(C : Type u) →
{A : Type u_1} →
[inst : CategoryTheory.Category.{v, u} C] → [inst_1 : AddGroup A] → [CategoryTheory.HasShift C A] → A → (C ≌ C)Shifting by n and shifting by -n forms an equivalence.
- Defined in
- Mathlib.CategoryTheory.Shift.Basic
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- AddGroupstatement and proof · cited by 4,410
- CategoryTheory.HasShiftstatement and proof · cited by 1,527
- CategoryTheory.Equivalencestatement · cited by 601
- add_neg_cancelproof · cited by 213
- CategoryTheory.shiftEquiv'proof · cited by 4
Cited by22
Results whose statement or proof uses this declaration.
- CategoryTheory.Pretriangulated.Triangle.invRotateproof · cited by 38
- CategoryTheory.Pretriangulated.invRotCompRotproof · cited by 9
- CategoryTheory.Pretriangulated.rotCompInvRotproof · cited by 8
- CategoryTheory.ObjectProperty.trW_iff'proof · cited by 5
- CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁proof · cited by 4
- CategoryTheory.Triangulated.AbelianSubcategory.eq_zero_of_hom_shift_posproof · cited by 4
- CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂proof · cited by 3
- CategoryTheory.Triangulated.TStructure.isLE_of_shiftproof · cited by 2
- CategoryTheory.shiftShiftNegproof · cited by 2
- CategoryTheory.ObjectProperty.le_extensionProduct_rightproof · cited by 1
- CategoryTheory.Triangulated.TStructure.shift_geproof · cited by 1
- CategoryTheory.Triangulated.TStructure.shift_leproof · cited by 1