Finite intervals in a graded category

The interval category has objects (X,r) for 0 ≤ r ≤ m and morphisms the degree r-s part of Hom(X,Y). When C is the category of projectives of the standard form, this is the finite category defining the manuscript's interval algebra. Here we construct the category and its Hom coordinates; the equivalence of its modules with supported graded modules is separate.

def MagnitudeConjecture.GradedCategory.HomGrading.intervalObject {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (m : ℕ) (X : C × Fin (m + 1)) : DegreeObject G

Include the finite range of degree coordinates in all integer shifts.

@[reducible, inline]

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

The full category on objects with degrees from zero to m.

@[instance_reducible]

instance MagnitudeConjecture.GradedCategory.HomGrading.instFintypeInterval {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (m : ℕ) [Fintype C] : Fintype (G.Interval m)

theorem MagnitudeConjecture.GradedCategory.HomGrading.card_interval {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (m : ℕ) [Fintype C] : Fintype.card (G.Interval m) = (m + 1) * Fintype.card C

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

Include the interval as a full subcategory of the degree category.

instance MagnitudeConjecture.GradedCategory.HomGrading.instFullIntervalDegreeObjectIntervalInclusion {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (m : ℕ) : (G.intervalInclusion m).Full

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

def MagnitudeConjecture.GradedCategory.HomGrading.intervalHomEquiv {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (m : ℕ) (X Y : G.Interval m) : (X ⟶ Y) ≃ₗ[k] ↥(G.component X.1 Y.1 (↑↑X.2 - ↑↑Y.2))

The defining Hom-coordinate equivalence of the finite interval.

instance MagnitudeConjecture.GradedCategory.HomGrading.instFiniteDimensionalHomIntervalOfFstFinHAddNatOfNat {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (m : ℕ) (X Y : G.Interval m) [FiniteDimensional k (X.1 ⟶ Y.1)] : FiniteDimensional k (X ⟶ Y)

theorem MagnitudeConjecture.GradedCategory.HomGrading.intervalHomEquiv_id {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (m : ℕ) (X : G.Interval m) : ↑((G.intervalHomEquiv m X X) (CategoryTheory.CategoryStruct.id X)) = CategoryTheory.CategoryStruct.id X.1

The Hom coordinate of an interval identity is the original identity.

theorem MagnitudeConjecture.GradedCategory.HomGrading.intervalHomEquiv_comp {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (m : ℕ) {X Y Z : G.Interval m} (f : X ⟶ Y) (g : Y ⟶ Z) : ↑((G.intervalHomEquiv m X Z) (CategoryTheory.CategoryStruct.comp f g)) = CategoryTheory.CategoryStruct.comp ↑((G.intervalHomEquiv m X Y) f) ↑((G.intervalHomEquiv m Y Z) g)

Composition in the interval is the original homogeneous composition.

theorem MagnitudeConjecture.GradedCategory.HomGrading.interval_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 = ⊥) (m : ℕ) {X Y : G.Interval m} (f : X ⟶ Y) (hf : f ≠ 0) : ↑Y.2 ≤ ↑X.2 ∧ ↑X.2 ≤ ↑Y.2 + h

A nonzero interval morphism decreases degree by at most the common Hom-degree bound. This also controls every factor in a nonzero composite.