Interval restriction as object deletion

Nonnegative degrees prevent a nonzero factorization between interval objects from leaving the interval. Thus the finite interval category agrees with the object-deletion quotient, allowing use of the proved extension-by-zero module equivalence. This uses degree monotonicity, not a covering or averaging theorem.

def MagnitudeConjecture.GradedCategory.HomGrading.outsideInterval {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 : ℕ) : Set (DegreeObject G)

The objects outside the closed degree interval.

theorem MagnitudeConjecture.GradedCategory.HomGrading.noDeletedFactorization_outsideInterval {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 : ℕ) : ObjectDeletion.NoDeletedFactorization (DegreeObject G) (G.outsideInterval m)

Between retained objects, factoring through a deleted degree gives zero.

def MagnitudeConjecture.GradedCategory.HomGrading.intervalToSurviving {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) (ObjectDeletion.SurvivingCategory (DegreeObject G) (G.outsideInterval m))

The finite degree coordinates identify with the surviving objects.

instance MagnitudeConjecture.GradedCategory.HomGrading.instFullIntervalSurvivingCategoryDegreeObjectOutsideIntervalIntervalToSurviving {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.intervalToSurviving m).Full

instance MagnitudeConjecture.GradedCategory.HomGrading.instFaithfulIntervalSurvivingCategoryDegreeObjectOutsideIntervalIntervalToSurviving {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.intervalToSurviving m).Faithful

instance MagnitudeConjecture.GradedCategory.HomGrading.instAdditiveIntervalSurvivingCategoryDegreeObjectOutsideIntervalIntervalToSurviving {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.intervalToSurviving m).Additive

instance MagnitudeConjecture.GradedCategory.HomGrading.instLinearIntervalSurvivingCategoryDegreeObjectOutsideIntervalIntervalToSurviving {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.Linear k (G.intervalToSurviving m)

instance MagnitudeConjecture.GradedCategory.HomGrading.instEssSurjIntervalSurvivingCategoryDegreeObjectOutsideIntervalIntervalToSurviving {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.intervalToSurviving m).EssSurj

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.intervalSurvivingEquivalence {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.Interval m ≌ ObjectDeletion.SurvivingCategory (DegreeObject G) (G.outsideInterval m)

The interval category is equivalent to the full subcategory on surviving degree-labelled objects.

instance MagnitudeConjecture.GradedCategory.HomGrading.instAdditiveIntervalSurvivingCategoryDegreeObjectOutsideIntervalFunctorIntervalSurvivingEquivalence {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.intervalSurvivingEquivalence m).functor.Additive

instance MagnitudeConjecture.GradedCategory.HomGrading.instLinearIntervalSurvivingCategoryDegreeObjectOutsideIntervalFunctorIntervalSurvivingEquivalence {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.Linear k (G.intervalSurvivingEquivalence m).functor

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.intervalDeletionEquivalence {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 : ℕ) : G.Interval m ≌ ObjectDeletion.DeletionCategory (DegreeObject G) (G.outsideInterval m)

Nonnegative bounded Hom degrees identify the interval with deletion of all degrees outside it.

instance MagnitudeConjecture.GradedCategory.HomGrading.instAdditiveIntervalDeletionCategoryDegreeObjectOutsideIntervalFunctorIntervalDeletionEquivalence {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 : ℕ) : (G.intervalDeletionEquivalence h hbound m).functor.Additive

instance MagnitudeConjecture.GradedCategory.HomGrading.instLinearIntervalDeletionCategoryDegreeObjectOutsideIntervalFunctorIntervalDeletionEquivalence {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 : ℕ) : CategoryTheory.Functor.Linear k (G.intervalDeletionEquivalence h hbound m).functor