Structures · Category theory
CategoryTheory.Functor.CommShift
A functor F commutes with the shift by a monoid A if it is equipped with
commutation isomorphisms with the shifts by all a : A, and these isomorphisms
satisfy coherence properties with respect to 0 : A and the addition in A.
- Defined in
- Mathlib.CategoryTheory.Shift.CommShift
- Shape
- 2 explicit arguments · adds commShiftIso, commShiftIso_zero, commShiftIso_add
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances11
- HomologicalComplex
- CategoryTheory.ObjectProperty.FullSubcategory
- CategoryTheory.Quotient
- HomotopyCategory
- DerivedCategory
- CategoryTheory.Pretriangulated.Triangle
- CategoryTheory.OppositeShift
- CategoryTheory.PullbackShift
- CochainComplex
- HomotopyCategory.Plus
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by355
- CategoryTheory.Functor.CommShift.commShiftIso
- CategoryTheory.Functor.mapTriangle
- CategoryTheory.ShiftedHom.map
- CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt
- CategoryTheory.Localization.SmallShiftedHom.equiv
- CategoryTheory.SingleFunctors.postcomp
- CategoryTheory.Functor.map_distinguished
- CategoryTheory.Functor.commShiftIso_comp_hom_app
- CategoryTheory.NatTrans.shift_app_comm
- CategoryTheory.Functor.mapTriangleCompIso
- CategoryTheory.Localization.SmallShiftedHom.equiv_comp
- CategoryTheory.Functor.mapTriangleRotateIso
- CategoryTheory.Functor.mapTriangleIso
- CategoryTheory.Functor.mapTriangleCommShiftIso
- CategoryTheory.Functor.mapTriangleInvRotateIso
- CategoryTheory.Functor.essImageDistTriang
- CategoryTheory.Adjunction.RightAdjointCommShift.iso
- CategoryTheory.Equivalence.CommShift
- CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀
- CategoryTheory.Functor.CommShift.OfComp.iso
- CategoryTheory.Functor.ShiftSequence.induced
- CategoryTheory.Adjunction.LeftAdjointCommShift.iso
- CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp
- CategoryTheory.LocalizerMorphism.smallShiftedHomMap
- CategoryTheory.SingleFunctors.lift
- CategoryTheory.Functor.CommShift.commShiftIso_zero
- CategoryTheory.ShiftedHom.map_comp
- CategoryTheory.LocalizerMorphism.commShift
- CategoryTheory.Functor.commShiftOfLocalization.iso
- CategoryTheory.ShiftedHom.map_mk₀
- CategoryTheory.Functor.commShiftIso_hom_naturality
- CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀Inv
- CategoryTheory.Functor.commShiftIso_comp_inv_app
- CategoryTheory.SingleFunctors.postcompIsoOfIso
- CategoryTheory.Functor.commShiftIso_add'
- CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app
- CategoryTheory.NatTrans.shift_app
- CategoryTheory.Adjunction.isTriangulated_rightAdjoint
- CategoryTheory.NatTrans.CommShiftCore.shift_comm
- CategoryTheory.Functor.ShiftSequence.leftComp
- CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app
- CategoryTheory.SingleFunctors.postcompPostcompIso
- CategoryTheory.Functor.CommShift.ofIso
- CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap
- CategoryTheory.Quotient.LiftCommShift.iso
- CategoryTheory.Functor.ShiftSequence.induced_shiftMap
- CategoryTheory.Functor.ShiftSequence.induced_shiftIso_hom_app_obj
- CategoryTheory.SingleFunctors.postcompFunctor
- CategoryTheory.Functor.map_distinguished_iff
- CategoryTheory.Functor.CommShift.commShiftIso_add
Ancestors0
No ancestors.