Local endomorphisms and distinct shifted principal projectives

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalDegree_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) (p : PrincipalDegreeCategory R ⋯ e he0) : IsLocalRing (CategoryTheory.End p)

A one-dimensional degree-zero corner gives a local endomorphism ring at every shift of that principal projective.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalDegree_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 = ⊥) : CategoryTheory.Skeletal (PrincipalDegreeCategory R ⋯ e he0)

In a nonnegatively graded algebra with diagonal degree-zero corners, the label and shift of a principal projective are determined by its isomorphism class.