Each literal retained block is a translated small interval

@[reducible, inline]

abbrev MagnitudeConjecture.Graded.FiniteGradedModule.PrincipalRetainedBlockCategory {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) (r h q : ℕ) (j : Fin q) : Type

The full subcategory of retained objects in one specified block.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlock_blockObject {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) (r h q : ℕ) (j : Fin q) (p : ι × Fin (r + 1)) : principalRetainedBlock R ⋯ e he0 r h q (principalRetainedBlockObject R ⋯ e he0 r h q (j, p)) = j

A block coordinate belongs to its specified block.

def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalRetainedBlockObj {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) (r h q : ℕ) (j : Fin q) (p : PrincipalIntervalCategory R ⋯ e he0 r) : (PrincipalRetainedBlockCategory R ⋯ e he0 r h q j)ᵒᵖ

Small interval labels as positive objects of the corresponding retained block.

def MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlockRealization {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) (r h q : ℕ) (j : Fin q) : CategoryTheory.Functor (PrincipalRetainedBlockCategory R ⋯ e he0 r h q j)ᵒᵖ (PrincipalDegreeCategory R ⋯ e he0)

Realize a single retained block inside the whole principal degree category.

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlockRealization_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} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (r h q : ℕ) (j : Fin q) : (principalRetainedBlockRealization R ⋯ e he0 r h q j).Full

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlockRealization_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} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (r h q : ℕ) (j : Fin q) : (principalRetainedBlockRealization R ⋯ e he0 r h q j).Faithful

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlockRealization_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) (r h q : ℕ) (j : Fin q) : (principalRetainedBlockRealization R ⋯ e he0 r h q j).Additive

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlockRealization_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) (r h q : ℕ) (j : Fin q) : CategoryTheory.Functor.Linear k (principalRetainedBlockRealization R ⋯ e he0 r h q j)

def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalRetainedBlockObjIso {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) (r h q : ℕ) (j : Fin q) (p : PrincipalIntervalCategory R ⋯ e he0 r) : (principalRetainedBlockRealization R ⋯ e he0 r h q j).obj (principalIntervalRetainedBlockObj R ⋯ e he0 r h q j p) ≅ (principalDegreeShift R ⋯ e he0 he (↑↑j * (↑r + ↑h + 1))).obj (intervalProjectiveLabel R ⋯ e he0 r p)

The two realizations of a block point agree after common degree translation.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalToRetainedBlock {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) (r h q : ℕ) (j : Fin q) : CategoryTheory.Functor (PrincipalIntervalCategory R ⋯ e he0 r) (PrincipalRetainedBlockCategory R ⋯ e he0 r h q j)ᵒᵖ

Common degree translation lifted into the literal retained block category.

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalToRetainedBlock_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} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (r h q : ℕ) (j : Fin q) : (principalIntervalToRetainedBlock R ⋯ e he0 he r h q j).Full

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalToRetainedBlock_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} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (r h q : ℕ) (j : Fin q) : (principalIntervalToRetainedBlock R ⋯ e he0 he r h q j).Faithful

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalToRetainedBlock_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) (r h q : ℕ) (j : Fin q) : (principalIntervalToRetainedBlock R ⋯ e he0 he r h q j).Additive

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalToRetainedBlock_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) (r h q : ℕ) (j : Fin q) : CategoryTheory.Functor.Linear k (principalIntervalToRetainedBlock R ⋯ e he0 he r h q j)

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalRetainedBlockObj_surjective {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) (r h q : ℕ) (j : Fin q) : Function.Surjective (principalIntervalRetainedBlockObj R ⋯ e he0 r h q j)

Every object of the literal retained block has small-interval coordinates.

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalToRetainedBlock_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} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (r h q : ℕ) (j : Fin q) : (principalIntervalToRetainedBlock R ⋯ e he0 he r h q j).EssSurj

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalToRetainedBlock_leftOp_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) (r h q : ℕ) (j : Fin q) : CategoryTheory.Functor.Linear k (principalIntervalToRetainedBlock R ⋯ e he0 he r h q j).leftOp

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpRetainedBlockEquivalence {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) (r h q : ℕ) (j : Fin q) : (PrincipalIntervalCategory R ⋯ e he0 r)ᵒᵖ ≌ PrincipalRetainedBlockCategory R ⋯ e he0 r h q j

In the module variance, the small interval is equivalent to the retained block.

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpRetainedBlockEquivalence_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) (r h q : ℕ) (j : Fin q) : (principalIntervalOpRetainedBlockEquivalence R ⋯ e he0 he r h q j).functor.Additive

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpRetainedBlockEquivalence_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) (r h q : ℕ) (j : Fin q) : CategoryTheory.Functor.Linear k (principalIntervalOpRetainedBlockEquivalence R ⋯ e he0 he r h q j).functor

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlockDeletionEquivalence {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 : ℕ) (j : Fin q) : ObjectDeletion.DeletionCategory (PrincipalRetainedCategory R ⋯ e he0 r h q) (CoveringHom.blockComplement (principalRetainedBlock R ⋯ e he0 r h q) j) ≌ (PrincipalIntervalCategory R ⋯ e he0 r)ᵒᵖ

Deleting all other retained blocks gives precisely the small interval category.

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlockDeletionEquivalence_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 = ⊥) (h : ℕ) (hupper : ∀ (d : ℤ), ↑h < d → R.component d = ⊥) (r q : ℕ) (j : Fin q) : (principalRetainedBlockDeletionEquivalence R ⋯ e he0 he hneg h hupper r q j).functor.Additive

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlockDeletionEquivalence_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 = ⊥) (h : ℕ) (hupper : ∀ (d : ℤ), ↑h < d → R.component d = ⊥) (r q : ℕ) (j : Fin q) : CategoryTheory.Functor.Linear k (principalRetainedBlockDeletionEquivalence R ⋯ e he0 he hneg h hupper r q j).functor