Structures · Category theory
CategoryTheory.HasShift
A category has a shift indexed by an additive monoid A
if there is a monoidal functor from A to C ⥤ C.
- Defined in
- Mathlib.CategoryTheory.Shift.Basic
- Shape
- 2 explicit arguments · adds shift, shiftMonoidal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances13
- CategoryTheory.ObjectProperty.FullSubcategory
- CategoryTheory.Quotient
- HomotopyCategory
- CategoryTheory.MorphismProperty.Localization
- DerivedCategory
- CategoryTheory.Pretriangulated.Triangle
- CategoryTheory.DifferentialObject
- CategoryTheory.OppositeShift
- CategoryTheory.MorphismProperty.Localization'
- CategoryTheory.PullbackShift
- CategoryTheory.TwistShiftData.Category
- CochainComplex
- CategoryTheory.GradedObjectWithShift
How is a type an instance?
Loading the hierarchy index…
Assumed by2,072
- CategoryTheory.shiftFunctor
- CategoryTheory.Pretriangulated.Triangle.obj₁
- CategoryTheory.Pretriangulated.Triangle.obj₃
- CategoryTheory.Pretriangulated.Triangle.obj₂
- CategoryTheory.Pretriangulated.Triangle.mor₁
- CategoryTheory.Pretriangulated.Triangle.mor₃
- CategoryTheory.Pretriangulated.Triangle.mor₂
- CategoryTheory.Pretriangulated.TriangleMorphism.hom₁
- CategoryTheory.Pretriangulated.TriangleMorphism.hom₂
- CategoryTheory.Pretriangulated.TriangleMorphism.hom₃
- CategoryTheory.shiftFunctorAdd'
- CategoryTheory.ShiftedHom
- CategoryTheory.Functor.mapTriangle
- CategoryTheory.Functor.shift
- CategoryTheory.Triangulated.TStructure.truncGE
- CategoryTheory.shiftFunctorZero
- CategoryTheory.Triangulated.TStructure.truncLT
- CategoryTheory.shiftFunctorCompIsoId
- CategoryTheory.SingleFunctors.functor
- CategoryTheory.Triangulated.TStructure.eTruncLT
- CategoryTheory.Pretriangulated.opShiftFunctorEquivalence
- CategoryTheory.Triangulated.TStructure.eTruncGE
- CategoryTheory.Triangulated.TStructure.truncGEπ
- CategoryTheory.shiftFunctorAdd
- CategoryTheory.ShiftedHom.comp
- CategoryTheory.ShiftedHom.mk₀
- CategoryTheory.DifferentialObject.obj
- CategoryTheory.Triangulated.TStructure.truncLTι
- CategoryTheory.Triangulated.TStructure.truncLE
- CategoryTheory.Pretriangulated.shiftFunctorOpIso
- CategoryTheory.Pretriangulated.Triangle.rotate
- CategoryTheory.Localization.HasSmallLocalizedShiftedHom
- CategoryTheory.ShiftedHom.map
- CategoryTheory.Pretriangulated.Triangle.invRotate
- CategoryTheory.SingleFunctors.Hom.hom
- CategoryTheory.ShiftedHom.comp.congr_simp
- CategoryTheory.Functor.shiftIso
- CategoryTheory.Localization.SmallShiftedHom
- CategoryTheory.Triangulated.TStructure.eTruncLTι
- CategoryTheory.Triangulated.SpectralObject.ω₁
- CategoryTheory.Pretriangulated.triangleOpEquivalence
- CategoryTheory.ObjectProperty.trW
- CategoryTheory.Pretriangulated.Triangle.shiftFunctor
- CategoryTheory.Pretriangulated.rotate
- CategoryTheory.Triangulated.TStructure.triangleLTGE
- CategoryTheory.Pretriangulated.invRotate
- CategoryTheory.shiftFunctorComm
- CategoryTheory.Triangulated.TStructure.truncLEι
- CategoryTheory.DifferentialObject.Hom.f
- CategoryTheory.Pretriangulated.contractibleTriangle
Ancestors0
No ancestors.