The category of degree-labelled objects

For a linear category with graded Hom spaces, the objects (X,s) have morphisms to (Y,t) given by the degree s-t part of Hom(X,Y). This is the shift convention of the graded interval proof. Restricting the objects to projectives and a finite interval gives its finite category algebra.

structure MagnitudeConjecture.GradedCategory.HomGrading (k : Type u) [Field k] (C : Type v) [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : Type (max v w)

An internal grading of the Hom spaces, with composition adding degrees.

• component (X Y : C) : ℤ → Submodule k (X ⟶ Y)
• internal (X Y : C) : DirectSum.IsInternal (self.component X Y)
• id_mem (X : C) : CategoryTheory.CategoryStruct.id X ∈ self.component X X 0
• comp_mem {X Y Z : C} {i j : ℤ} {f : X ⟶ Y} {g : Y ⟶ Z} : f ∈ self.component X Y i → g ∈ self.component Y Z j → CategoryTheory.CategoryStruct.comp f g ∈ self.component X Z (i + j)

structure MagnitudeConjecture.GradedCategory.DegreeObject {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) : Type v

An object together with its integer shift.

• obj : C
• degree : ℤ

def MagnitudeConjecture.GradedCategory.HomGrading.ofNat {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (A : (X Y : C) → ℕ → Submodule k (X ⟶ Y)) (hinternal : ∀ (X Y : C), DirectSum.IsInternal (A X Y)) (hid : ∀ (X : C), CategoryTheory.CategoryStruct.id X ∈ A X X 0) (hcomp : ∀ {X Y Z : C} {i j : ℕ} {f : X ⟶ Y} {g : Y ⟶ Z}, f ∈ A X Y i → g ∈ A Y Z j → CategoryTheory.CategoryStruct.comp f g ∈ A X Z (i + j)) : HomGrading k C

Convert the natural path-length grading into an integer Hom grading.

@[instance_reducible]

instance MagnitudeConjecture.GradedCategory.HomGrading.instCategoryDegreeObject {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) : CategoryTheory.Category.{w, v} (DegreeObject G)

@[instance_reducible]

instance MagnitudeConjecture.GradedCategory.HomGrading.instPreadditiveDegreeObject {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) : CategoryTheory.Preadditive (DegreeObject G)

@[instance_reducible]

instance MagnitudeConjecture.GradedCategory.HomGrading.instModuleHomDegreeObject {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (X Y : DegreeObject G) : Module k (X ⟶ Y)

@[instance_reducible]

instance MagnitudeConjecture.GradedCategory.HomGrading.instLinearDegreeObject {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) : CategoryTheory.Linear k (DegreeObject G)

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

Forget the shift and include the homogeneous component into its Hom space.

instance MagnitudeConjecture.GradedCategory.HomGrading.instFaithfulDegreeObjectForget {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) : G.forget.Faithful

instance MagnitudeConjecture.GradedCategory.HomGrading.instAdditiveDegreeObjectForget {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) : G.forget.Additive

instance MagnitudeConjecture.GradedCategory.HomGrading.instLinearDegreeObjectForget {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) : CategoryTheory.Functor.Linear k G.forget

theorem MagnitudeConjecture.GradedCategory.HomGrading.degree_bounds_of_ne_zero {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (h : ℕ) (hbound : ∀ (X Y : C) (d : ℤ), d < 0 ∨ ↑h < d → G.component X Y d = ⊥) {X Y : DegreeObject G} (f : X ⟶ Y) (hf : f ≠ 0) : Y.degree ≤ X.degree ∧ X.degree ≤ Y.degree + ↑h

A nonzero homogeneous map cannot have degree outside the grading bound.

theorem MagnitudeConjecture.GradedCategory.HomGrading.degree_strict_of_ne_zero_of_ne {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (h : ℕ) (hbound : ∀ (X Y : C) (d : ℤ), d < 0 ∨ ↑h < d → G.component X Y d = ⊥) (hzero : ∀ (X Y : C), X ≠ Y → G.component X Y 0 = ⊥) {X Y : DegreeObject G} (f : X ⟶ Y) (hf : f ≠ 0) (hXY : X ≠ Y) : Y.degree < X.degree

For a skeletal degree-zero category, a nonzero map between distinct degree-labelled objects strictly decreases their shift.