The exact simple-module count of a finite graded interval

@[instance_reducible]

def MagnitudeConjecture.Graded.FiniteGradedModule.intervalSimpleCountFintype {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.intervalSimpleCountOpFintype {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.intervalSimpleCountFinite {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)

theorem MagnitudeConjecture.Graded.FiniteGradedModule.intervalSimpleCountNoetherian {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 : ℕ) : IsNoetherianRing (principalIntervalAlgebra R ⋯ e he0 he m)ᵐᵒᵖ

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOp_end_isLocalRing {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) (hdiag : ∀ (i : ι), Module.finrank k ↥(cornerComponent R (e i) (e i) 0) = 1) (m : ℕ) (p : (PrincipalIntervalCategory R ⋯ e he0 m)ᵒᵖ) : IsLocalRing (CategoryTheory.End p)

The interval's opposite category has local endomorphism rings.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOp_skeletal {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) (hdiag : ∀ (i : ι), Module.finrank k ↥(cornerComponent R (e i) (e i) 0) = 1) (hneg : ∀ d < 0, R.component d = ⊥) (hoff : ∀ (i j : ι), i ≠ j → cornerComponent R (e i) (e j) 0 = ⊥) (m : ℕ) : CategoryTheory.Skeletal (PrincipalIntervalCategory R ⋯ e he0 m)ᵒᵖ

Restricting the skeletal degree category to a finite interval and taking the opposite preserves distinct labels.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalAlgebra_simpleCount {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) (hdiag : ∀ (i : ι), Module.finrank k ↥(cornerComponent R (e i) (e i) 0) = 1) (hneg : ∀ d < 0, R.component d = ⊥) (hoff : ∀ (i j : ι), i ≠ j → cornerComponent R (e i) (e j) 0 = ⊥) (m : ℕ) (S : RightModule.FiniteIndecomposableSkeleton k (principalIntervalAlgebra R ⋯ e he0 he m)) : S.simpleCount = Fintype.card ι * (m + 1)

Each primitive label contributes exactly one simple class in each degree of the interval, independently of the widths of the indecomposable modules.