A complete homogeneous idempotent family detects graded maps #
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.principalEvaluation_detect
{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}
[Fintype ι]
(e : ι → A)
(he0 : ∀ (i : ι), e i ∈ R.component 0)
(he : ∀ (i : ι), e i * e i = e i)
(hsum : ∑ i : ι, e i = 1)
{X Y : ShiftedModule}
(f : X ⟶ Y)
(hf : f ≠ 0)
:
∃ (p : PrincipalDegreeCategory R ⋯ e he0) (g : (principalDegreeInclusion R ⋯ e he0).obj p ⟶ X),
CategoryTheory.CategoryStruct.comp g f ≠ 0
A nonzero graded map remains nonzero after precomposition by some shifted projective.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.principalEvaluation_faithful
{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}
[Fintype ι]
(e : ι → A)
(he0 : ∀ (i : ι), e i ∈ R.component 0)
(he : ∀ (i : ι), e i * e i = e i)
(hsum : ∑ i : ι, e i = 1)
:
(principalEvaluationFunctor R ⋯ e he0 he).Faithful
The resulting finite contravariant representation remembers every graded module map.