Deleting gaps between separated principal-projective intervals

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalDegree_bounds {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 = ⊥) (h : ℕ) (hupper : ∀ (d : ℤ), ↑h < d → R.component d = ⊥) {p q : PrincipalDegreeCategory R ⋯ e he0} (f : p ⟶ q) (hf : f ≠ 0) : q.2 ≤ p.2 ∧ p.2 - q.2 ≤ ↑h

A nonzero map between shifted principal projectives decreases degree by an amount between zero and the grading bound.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalDegree_hom_eq_zero_of_separated {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 = ⊥) (h : ℕ) (hupper : ∀ (d : ℤ), ↑h < d → R.component d = ⊥) (r : ℕ) {i j : ℕ} (hij : i ≠ j) {p q : PrincipalDegreeCategory R ⋯ e he0} (hp : GradedInterval.InBlock r h i p.2) (hq : GradedInterval.InBlock r h j q.2) (f : p ⟶ q) : f = 0

Morphisms between distinct separated blocks are zero.

def MagnitudeConjecture.Graded.FiniteGradedModule.principalSeparatedDeleted {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) (h r q : ℕ) : Set (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ

Deleted objects are precisely the degrees outside the retained blocks.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalSeparated_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 = ⊥) (h : ℕ) (hupper : ∀ (d : ℤ), ↑h < d → R.component d = ⊥) (r q : ℕ) : ObjectDeletion.NoDeletedFactorization (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (principalSeparatedDeleted R ⋯ e he0 h r q)

A nonzero composite with retained endpoints cannot pass through a gap or outside the retained block range.

def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalSeparatedDeleted {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) (h m r q : ℕ) : Set (PrincipalIntervalCategory R ⋯ e he0 m)ᵒᵖ

The gap deletion inside a finite ambient interval.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalSeparated_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 = ⊥) (h : ℕ) (hupper : ∀ (d : ℤ), ↑h < d → R.component d = ⊥) (m r q : ℕ) : ObjectDeletion.NoDeletedFactorization (PrincipalIntervalCategory R ⋯ e he0 m)ᵒᵖ (principalIntervalSeparatedDeleted R ⋯ e he0 h m r q)

The finite interval deletion ideal vanishes between retained objects.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalSeparatedDeletionEquivalence {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 = ⊥) (h : ℕ) (hupper : ∀ (d : ℤ), ↑h < d → R.component d = ⊥) (m r q : ℕ) : ObjectDeletion.SurvivingCategory (PrincipalIntervalCategory R ⋯ e he0 m)ᵒᵖ (principalIntervalSeparatedDeleted R ⋯ e he0 h m r q) ≌ ObjectDeletion.DeletionCategory (PrincipalIntervalCategory R ⋯ e he0 m)ᵒᵖ (principalIntervalSeparatedDeleted R ⋯ e he0 h m r q)

On the retained separated blocks, the literal finite deletion category is equivalent to the full subcategory: quotienting introduces no new Hom relations inside those blocks.