A finite interval algebra realizing supported graded modules

@[instance_reducible]

def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalFintype {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) (m : ℕ) : Fintype (PrincipalIntervalCategory R ⋯ e he0 m)

@[instance_reducible]

def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpFintype {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) (m : ℕ) : Fintype (PrincipalIntervalCategory R ⋯ e he0 m)ᵒᵖ

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalFiniteRepresentables {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) (m : ℕ) (X : (PrincipalIntervalCategory R ⋯ e he0 m)ᵒᵖ) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)

Every representable on the finite interval has finite dimension and finite support.

@[reducible, inline]

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

The finite matrix algebra of the interval of actual shifted principal projectives.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalAlgebraRepresentableEquiv {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) (m : ℕ) : principalIntervalAlgebra R ⋯ e he0 he m ≃ₐ[k] CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯

The matrix model is algebra-isomorphic to the existing representable generator model.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalAlgebra_finiteDimensional {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) (m : ℕ) : FiniteDimensional k (principalIntervalAlgebra R ⋯ e he0 he m)

The interval algebra is finite dimensional over the original field.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalAlgebraGradedModuleEquivalence {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 = ⊥) (h1 : 1 ∈ R.component 0) (hsum : ∑ i : ι, e i = 1) (horth : Pairwise fun (i j : ι) => e i * e j = 0) (m : ℕ) : FGModuleCat (principalIntervalAlgebra R ⋯ e he0 he m)ᵐᵒᵖ ≌ SupportedCategory m

Right modules over the finite interval algebra are actual graded modules supported on that interval.