Magnitude conjecture

MagnitudeConjecture.CategoryTheory.GradedShiftFunctor

Simultaneous translation of graded shift labels #

source
def MagnitudeConjecture.GradedCategory.HomGrading.shiftFunctor {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (s : ℤ) :
CategoryTheory.Functor (DegreeObject G) (DegreeObject G)

Translate all shift labels by the same integer.

Instances For
    source
    instance MagnitudeConjecture.GradedCategory.HomGrading.instFullDegreeObjectShiftFunctor {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (s : ℤ) :
    (G.shiftFunctor s).Full
    source
    instance MagnitudeConjecture.GradedCategory.HomGrading.instFaithfulDegreeObjectShiftFunctor {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (s : ℤ) :
    (G.shiftFunctor s).Faithful
    source
    instance MagnitudeConjecture.GradedCategory.HomGrading.instAdditiveDegreeObjectShiftFunctor {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (s : ℤ) :
    (G.shiftFunctor s).Additive
    source
    instance MagnitudeConjecture.GradedCategory.HomGrading.instLinearDegreeObjectShiftFunctor {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (s : ℤ) :
    CategoryTheory.Functor.Linear k (G.shiftFunctor s)