Projective evaluation in the actual category of shifted graded modules

def MagnitudeConjecture.Graded.FiniteGradedModule.regularObject {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)) : FiniteGradedModule R

The graded regular module with the canonical bundled field action.

def MagnitudeConjecture.Graded.FiniteGradedModule.principalObject {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)) (e : A) (he0 : e ∈ R.component 0) : FiniteGradedModule R

The actual graded module Ae attached to a homogeneous idempotent.

def MagnitudeConjecture.Graded.FiniteGradedModule.regularShiftHomEquiv {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)) (h1 : 1 ∈ R.component 0) (r : ℤ) (X : ShiftedModule) : ({ obj := regularObject R ⋯, degree := r } ⟶ X) ≃ₗ[k] ↥(X.obj.grading.component (r - X.degree))

Evaluation at one identifies maps from a shifted regular module with the target degree.

def MagnitudeConjecture.Graded.FiniteGradedModule.principalShiftHomEquiv {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)) (e : A) (he : e * e = e) (he0 : e ∈ R.component 0) (r : ℤ) (X : ShiftedModule) : ({ obj := principalObject R ⋯ e he0, degree := r } ⟶ X) ≃ₗ[k] ↥(idempotentComponent R X.obj.grading e (r - X.degree))

Evaluation at e gives the idempotent coordinate of the physical target degree.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.regularHom_eq_zero_outside {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)) (h1 : 1 ∈ R.component 0) {m : ℕ} (X : ShiftedModule) (hX : SupportedIn m X) (r : ℤ) (hr : r < 0 ∨ ↑m < r) (f : { obj := regularObject R ⋯, degree := r } ⟶ X) : f = 0

Projective evaluation on a module supported in [0,m] vanishes outside that interval.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalHom_eq_zero_of_not_mem {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)) (e : A) (he : e * e = e) (he0 : e ∈ R.component 0) (X : ShiftedModule) (r : ℤ) (hr : r ∉ shiftedSupport X) (f : { obj := principalObject R ⋯ e he0, degree := r } ⟶ X) : f = 0

A projective evaluation is zero at every degree outside the actual support.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalHom_eq_zero_outside {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)) (e : A) (he : e * e = e) (he0 : e ∈ R.component 0) {m : ℕ} (X : ShiftedModule) (hX : SupportedIn m X) (r : ℤ) (hr : r < 0 ∨ ↑m < r) (f : { obj := principalObject R ⋯ e he0, degree := r } ⟶ X) : f = 0

The same vanishing holds for every degree-zero idempotent coordinate.