Homogeneous corner coordinates on the degree-labelled projective category

def MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeHomEquiv {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 v} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (p q : PrincipalDegreeCategory R ⋯ e he0) : (p ⟶ q) ≃ₗ[k] ↥(cornerComponent R (e p.1) (e q.1) (p.2 - q.2))

Morphisms between shifted projectives are the manuscript's homogeneous corner spaces.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeHomEquiv_id {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 v} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (p : PrincipalDegreeCategory R ⋯ e he0) : ↑((principalDegreeHomEquiv R ⋯ e he0 he p p) (CategoryTheory.CategoryStruct.id p)) = e p.1

The identity has the selected idempotent as its corner coordinate.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeHomEquiv_comp {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 v} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) {p q r : PrincipalDegreeCategory R ⋯ e he0} (f : p ⟶ q) (g : q ⟶ r) : ↑((principalDegreeHomEquiv R ⋯ e he0 he p r) (CategoryTheory.CategoryStruct.comp f g)) = ↑((principalDegreeHomEquiv R ⋯ e he0 he p q) f) * ↑((principalDegreeHomEquiv R ⋯ e he0 he q r) g)

Composition is multiplication in A, with the contravariant left-module convention.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalEvaluation_action {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 v} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) {p q : PrincipalDegreeCategory R ⋯ e he0} (f : p ⟶ q) (X : ShiftedModule) (x : (principalDegreeInclusion R ⋯ e he0).obj q ⟶ X) : ↑((principalShiftHomEquiv R ⋯ (e p.1) ⋯ ⋯ p.2 X) (CategoryTheory.CategoryStruct.comp f.hom x)) = ↑((principalDegreeHomEquiv R ⋯ e he0 he p q) f) • ↑((principalShiftHomEquiv R ⋯ (e q.1) ⋯ ⋯ q.2 X) x)

Precomposition in the representation is the action of its corner coordinate.