Evaluation from supported graded modules to supported projective representations #
def
MagnitudeConjecture.Graded.FiniteGradedModule.principalOutsideInterval
{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)
(m : ℕ)
:
Set (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ
Projective degrees deleted when retaining [0,m].
Instances For
def
MagnitudeConjecture.Graded.FiniteGradedModule.principalSupportedEvaluationFunctor
{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)
(m : ℕ)
:
CategoryTheory.Functor (SupportedCategory m)
(ObjectDeletion.VanishingFiniteModuleCategory (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ
(principalOutsideInterval R ⋯ e he0 m))
The forward representation functor with both interval-support conditions bundled.
Instances For
instance
MagnitudeConjecture.Graded.FiniteGradedModule.principalSupportedEvaluationFunctor_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}
[Fintype ι]
(e : ι → A)
(he0 : ∀ (i : ι), e i ∈ R.component 0)
(he : ∀ (i : ι), e i * e i = e i)
(m : ℕ)
:
(principalSupportedEvaluationFunctor R ⋯ e he0 he m).Additive
instance
MagnitudeConjecture.Graded.FiniteGradedModule.principalSupportedEvaluationFunctor_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}
[Fintype ι]
(e : ι → A)
(he0 : ∀ (i : ι), e i ∈ R.component 0)
(he : ∀ (i : ι), e i * e i = e i)
(m : ℕ)
:
CategoryTheory.Functor.Linear k (principalSupportedEvaluationFunctor R ⋯ e he0 he m)
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.principalSupportedEvaluation_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)
(m : ℕ)
:
(principalSupportedEvaluationFunctor R ⋯ e he0 he m).Faithful
A complete idempotent family still detects maps after imposing interval support.