Finite contravariant representations obtained from graded projective evaluation

def MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeObject {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) (p : ι × ℤ) : ShiftedModule

All shifts of the selected homogeneous principal projectives.

@[reducible, inline]

abbrev MagnitudeConjecture.Graded.FiniteGradedModule.PrincipalDegreeCategory {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) : Type v

def MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeInclusion {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) : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0) ShiftedModule

The full inclusion of the degree-labelled projective family.

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeInclusion_additive {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) : (principalDegreeInclusion R ⋯ e he0).Additive

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalDegreeInclusion_linear {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) : CategoryTheory.Functor.Linear k (principalDegreeInclusion R ⋯ e he0)

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalEvaluation_finiteSupport {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) [Fintype ι] (he : ∀ (i : ι), e i * e i = e i) (X : ShiftedModule) : {p : (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ | Nontrivial ((principalDegreeInclusion R ⋯ e he0).obj (Opposite.unop p) ⟶ X)}.Finite

Only finitely many shifted projectives see any fixed finite graded module.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalEvaluation_finite {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) [Fintype ι] (he : ∀ (i : ι), e i * e i = e i) (X : ShiftedModule) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.restrictedLinearYonedaLinearModule (principalDegreeInclusion R ⋯ e he0) X)

def MagnitudeConjecture.Graded.FiniteGradedModule.principalEvaluationFunctor {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) [Fintype ι] (he : ∀ (i : ι), e i * e i = e i) : CategoryTheory.Functor ShiftedModule (CoveringHom.FiniteDimensionalModuleCategory k)

A graded module gives a finite-dimensional contravariant representation on shifted projectives.

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalEvaluationFunctor_additive {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) [Fintype ι] (he : ∀ (i : ι), e i * e i = e i) : (principalEvaluationFunctor R ⋯ e he0 he).Additive

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalEvaluationFunctor_linear {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) [Fintype ι] (he : ∀ (i : ι), e i * e i = e i) : CategoryTheory.Functor.Linear k (principalEvaluationFunctor R ⋯ e he0 he)

theorem MagnitudeConjecture.Graded.FiniteGradedModule.principalEvaluation_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)) {ι : Type v} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) [Fintype ι] (he : ∀ (i : ι), e i * e i = e i) {m : ℕ} (X : ShiftedModule) (hX : SupportedIn m X) (p : PrincipalDegreeCategory R ⋯ e he0) (hp : p.2 < 0 ∨ ↑m < p.2) : CategoryTheory.Limits.IsZero (((principalEvaluationFunctor R ⋯ e he0 he).obj X).obj.obj.obj (Opposite.op p))

A supported module evaluates to zero on projective degrees outside the interval.