Structures · Category theory
CategoryTheory.NatTrans.CommShift
If τ : F₁ ⟶ F₂ is a natural transformation between two functors
which commute with a shift by an additive monoid A, this typeclass
asserts a compatibility of τ with these shifts.
- Defined in
- Mathlib.CategoryTheory.Shift.CommShift
- Shape
- 2 explicit arguments · adds shift_comm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- HomologicalComplex
- HomotopyCategory
- CategoryTheory.OppositeShift
- CategoryTheory.PullbackShift
- CochainComplex
How is a type an instance?
Loading the hierarchy index…
Assumed by38
- CategoryTheory.NatTrans.shift_app_comm
- CategoryTheory.Functor.mapTriangleIso
- CategoryTheory.SingleFunctors.postcompIsoOfIso
- CategoryTheory.NatTrans.shift_app
- CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap
- CategoryTheory.ShiftedHom.map_naturality_1
- CategoryTheory.NatTrans.shift_comm
- CategoryTheory.Functor.isTriangulated_iff_of_iso
- CategoryTheory.NatTrans.app_shift
- CategoryTheory.Functor.isTriangulated_of_iso
- CategoryTheory.NatTrans.CommShift.shift_comm
- CategoryTheory.ShiftedHom.map_naturality
- CategoryTheory.NatTrans.shift_app_comm_assoc
- CategoryTheory.NatTrans.CommShift.whiskerLeft
- CategoryTheory.NatTrans.commShiftPullback
- CategoryTheory.Pretriangulated.Opposite.commShift_natTrans_op_int
- CategoryTheory.NatTrans.CommShift.comp
- CategoryTheory.Functor.mapTriangleIso_hom_app_hom₂
- CategoryTheory.NatTrans.commShift_op
- CategoryTheory.Functor.mapTriangleIso_inv_app_hom₂
- CategoryTheory.Functor.isTriangulated_iff_comp_right
- CategoryTheory.SingleFunctors.postcompIsoOfIso_hom_hom_app
- CategoryTheory.Functor.isTriangulated_of_precomp_iso
- CategoryTheory.Functor.mapTriangleIso_hom_app_hom₁
- CategoryTheory.NatTrans.shift_comm_assoc
- CategoryTheory.NatTrans.app_shift_assoc
- CategoryTheory.NatTrans.CommShift.of_iso_symm
- CategoryTheory.NatTrans.CommShift.of_iso_inv
- CategoryTheory.NatTrans.CommShift.of_isIso
- CategoryTheory.NatTrans.CommShift.whiskerRight
- CategoryTheory.NatTrans.shift_app_assoc
- CategoryTheory.SingleFunctors.postcompIsoOfIso.congr_simp
- CategoryTheory.NatTrans.CommShift.verticalComposition
- CategoryTheory.ShiftedHom.map_naturality_2
- CategoryTheory.SingleFunctors.postcompIsoOfIso_inv_hom_app
- CategoryTheory.Functor.mapTriangleIso_hom_app_hom₃
- CategoryTheory.Functor.mapTriangleIso_inv_app_hom₁
- CategoryTheory.Functor.mapTriangleIso_inv_app_hom₃
Ancestors0
No ancestors.