Right-module variance for interval deletion

Right modules are contravariant on projectives. We therefore identify the opposite interval category with deletion from the opposite degree category, so the existing covariant module machinery applies with the correct variance.

def MagnitudeConjecture.GradedCategory.HomGrading.outsideIntervalOp {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)ᵒᵖ

theorem MagnitudeConjecture.GradedCategory.HomGrading.noDeletedFactorization_outsideIntervalOp {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.outsideIntervalOp m)

def MagnitudeConjecture.GradedCategory.HomGrading.intervalOpToSurviving {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.outsideIntervalOp m))

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

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

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

instance MagnitudeConjecture.GradedCategory.HomGrading.instLinearOppositeIntervalSurvivingCategoryDegreeObjectOutsideIntervalOpIntervalOpToSurviving {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.intervalOpToSurviving m)

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

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.intervalOpSurvivingEquivalence {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.outsideIntervalOp m)

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

instance MagnitudeConjecture.GradedCategory.HomGrading.instLinearOppositeIntervalSurvivingCategoryDegreeObjectOutsideIntervalOpFunctorIntervalOpSurvivingEquivalence {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.intervalOpSurvivingEquivalence m).functor

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.intervalOpDeletionEquivalence {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.outsideIntervalOp m)

instance MagnitudeConjecture.GradedCategory.HomGrading.instAdditiveOppositeIntervalDeletionCategoryDegreeObjectOutsideIntervalOpFunctorIntervalOpDeletionEquivalence {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.intervalOpDeletionEquivalence h hbound m).functor.Additive

instance MagnitudeConjecture.GradedCategory.HomGrading.instLinearOppositeIntervalDeletionCategoryDegreeObjectOutsideIntervalOpFunctorIntervalOpDeletionEquivalence {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.intervalOpDeletionEquivalence h hbound m).functor