The literal retained interval category and its block coordinates

@[reducible, inline]

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

The actual surviving category inside the packed ambient interval.

def MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlockObject {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) (r h q : ℕ) (p : Fin q × ι × Fin (r + 1)) : PrincipalRetainedCategory R ⋯ e he0 r h q

A block coordinate as an actual surviving interval object.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlockObject_bijective {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 : ℕ) : Function.Bijective (principalRetainedBlockObject R ⋯ e he0 r h q)

Block coordinates enumerate the literal surviving objects without repetition.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedBlockEquiv {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 : ℕ) : Fin q × ι × Fin (r + 1) ≃ PrincipalRetainedCategory R ⋯ e he0 r h q

Finite block coordinates for the retained category.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedFintype {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 : ℕ) : Fintype (PrincipalRetainedCategory R ⋯ e he0 r h q)

The retained category is finite, including the empty packing.

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

Realize opposite retained objects by their actual principal projectives.

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

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

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedRealization_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) (r h q : ℕ) : (principalRetainedRealization R ⋯ e he0 r h q).Faithful

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedRealization_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) (r h q : ℕ) : (principalRetainedRealization R ⋯ e he0 r h q).Full

@[reducible, inline]

abbrev MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedAlgebra {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 : ℕ) : Type u

The matrix algebra of the literal retained interval category.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedAlgebraTupleEquiv {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 : ℕ) : principalRetainedAlgebra R ⋯ e he0 r h q ≃ₐ[k] CategoryTheory.End (principalSeparatedBlockTuple R ⋯ e he0 r h q)

The retained category algebra is the separated-block tuple algebra.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalRetainedAlgebraProductEquiv {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 : ℕ) : principalRetainedAlgebra R ⋯ e he0 r h q ≃ₐ[k] Fin q → principalIntervalAlgebra R ⋯ e he0 he r

The actual retained category algebra is the product of q smaller interval algebras.

@[reducible, inline]

abbrev MagnitudeConjecture.Graded.FiniteGradedModule.principalPackedDeletionAlgebra {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 : ℕ) : Type u

The matrix algebra of the literal finite category after deleting the gaps.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalPackedDeletionAlgebraProductEquiv {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 : ℕ) : principalPackedDeletionAlgebra R ⋯ e he0 r h q ≃ₐ[k] Fin q → principalIntervalAlgebra R ⋯ e he0 he r

Gap deletion gives the product of the actual smaller interval algebras.