The principal-projective interval as object deletion

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalDegree_nonincreasing {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (hneg : ∀ d < 0, R.component d = ⊥) {p q : PrincipalDegreeCategory R ⋯ e he0} (f : p ⟶ q) (hf : f ≠ 0) : q.2 ≤ p.2

A nonzero map between the shifted principal projectives cannot increase degree.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalInterval_noDeletedFactorization {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (hneg : ∀ d < 0, R.component d = ⊥) (m : ℕ) : ObjectDeletion.NoDeletedFactorization (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (principalOutsideInterval R ⋯ e he0 m)

A factorization through an omitted degree vanishes between interval objects.

def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpToSurviving {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (m : ℕ) : CategoryTheory.Functor (PrincipalIntervalCategory R ⋯ e he0 m)ᵒᵖ (ObjectDeletion.SurvivingCategory (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (principalOutsideInterval R ⋯ e he0 m))

Finite interval coordinates viewed as surviving opposite degree objects.

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpToSurviving_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (m : ℕ) : (principalIntervalOpToSurviving R ⋯ e he0 m).Full

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpToSurviving_faithful {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (m : ℕ) : (principalIntervalOpToSurviving R ⋯ e he0 m).Faithful

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpToSurviving_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (m : ℕ) : (principalIntervalOpToSurviving R ⋯ e he0 m).Additive

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpToSurviving_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (m : ℕ) : CategoryTheory.Functor.Linear k (principalIntervalOpToSurviving R ⋯ e he0 m)

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpToSurviving_essSurj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (m : ℕ) : (principalIntervalOpToSurviving R ⋯ e he0 m).EssSurj

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpSurvivingEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (m : ℕ) : (PrincipalIntervalCategory R ⋯ e he0 m)ᵒᵖ ≌ ObjectDeletion.SurvivingCategory (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (principalOutsideInterval R ⋯ e he0 m)

The interval and surviving full categories are equivalent.

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpSurvivingEquivalence_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (m : ℕ) : (principalIntervalOpSurvivingEquivalence R ⋯ e he0 m).functor.Additive

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpSurvivingEquivalence_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (m : ℕ) : CategoryTheory.Functor.Linear k (principalIntervalOpSurvivingEquivalence R ⋯ e he0 m).functor

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpDeletionEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (hneg : ∀ d < 0, R.component d = ⊥) (m : ℕ) : (PrincipalIntervalCategory R ⋯ e he0 m)ᵒᵖ ≌ ObjectDeletion.DeletionCategory (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (principalOutsideInterval R ⋯ e he0 m)

Interval restriction agrees with deletion because no nonzero factorization leaves the interval.

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpDeletionEquivalence_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (hneg : ∀ d < 0, R.component d = ⊥) (m : ℕ) : (principalIntervalOpDeletionEquivalence R ⋯ e he0 he hneg m).functor.Additive

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpDeletionEquivalence_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (hneg : ∀ d < 0, R.component d = ⊥) (m : ℕ) : CategoryTheory.Functor.Linear k (principalIntervalOpDeletionEquivalence R ⋯ e he0 he hneg m).functor