Finite interval representations of actual graded modules #
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalOpDeletion_obj_bijective
{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}
[Fintype ι]
(e : ι → A)
(he0 : ∀ (i : ι), e i ∈ R.component 0)
(he : ∀ (i : ι), e i * e i = e i)
(hneg : ∀ d < 0, R.component d = ⊥)
(m : ℕ)
:
Function.Bijective (principalIntervalOpDeletionEquivalence R ⋯ e he0 he hneg m).functor.obj
The deletion comparison preserves literal object support by a bijection.
noncomputable def
MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalSupportedRepresentationEquivalence
{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}
[Fintype ι]
(e : ι → A)
(he0 : ∀ (i : ι), e i ∈ R.component 0)
(he : ∀ (i : ι), e i * e i = e i)
(hneg : ∀ d < 0, R.component d = ⊥)
(m : ℕ)
:
CoveringHom.FiniteDimensionalModuleCategory k ≌ ObjectDeletion.VanishingFiniteModuleCategory (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ
(principalOutsideInterval R ⋯ e he0 m)
Finite interval representations are precisely supported representations of all shifted projectives.
Instances For
noncomputable def
MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalGradedModuleEquivalence
{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}
[Fintype ι]
(e : ι → A)
(he0 : ∀ (i : ι), e i ∈ R.component 0)
(he : ∀ (i : ι), e i * e i = e i)
(hneg : ∀ d < 0, R.component d = ⊥)
(h1 : 1 ∈ R.component 0)
(hsum : ∑ i : ι, e i = 1)
(horth : Pairwise fun (i j : ι) => e i * e j = 0)
(m : ℕ)
:
The finite projective interval represents actual supported graded modules.