Supported graded modules and supported projective representations #
noncomputable def
MagnitudeConjecture.Graded.FiniteGradedModule.supportedProjectiveRepresentationEquivalence
{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)
(hsum : ∑ i : ι, e i = 1)
(horth : Pairwise fun (i j : ι) => e i * e j = 0)
(m : ℕ)
(hneg : ∀ d < 0, R.component d = ⊥)
(h1 : 1 ∈ R.component 0)
:
SupportedCategory m ≌ ObjectDeletion.VanishingFiniteModuleCategory (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ
(principalOutsideInterval R ⋯ e he0 m)
Actual graded modules supported in [0,m] are equivalent to supported projective representations.
Instances For
instance
MagnitudeConjecture.Graded.FiniteGradedModule.supportedProjectiveRepresentationEquivalence_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}
[Fintype ι]
(e : ι → A)
(he0 : ∀ (i : ι), e i ∈ R.component 0)
(he : ∀ (i : ι), e i * e i = e i)
(hsum : ∑ i : ι, e i = 1)
(horth : Pairwise fun (i j : ι) => e i * e j = 0)
(m : ℕ)
(hneg : ∀ d < 0, R.component d = ⊥)
(h1 : 1 ∈ R.component 0)
:
(supportedProjectiveRepresentationEquivalence R ⋯ e he0 he hsum horth m hneg h1).functor.Additive
instance
MagnitudeConjecture.Graded.FiniteGradedModule.supportedProjectiveRepresentationEquivalence_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}
[Fintype ι]
(e : ι → A)
(he0 : ∀ (i : ι), e i ∈ R.component 0)
(he : ∀ (i : ι), e i * e i = e i)
(hsum : ∑ i : ι, e i = 1)
(horth : Pairwise fun (i j : ι) => e i * e j = 0)
(m : ℕ)
(hneg : ∀ d < 0, R.component d = ⊥)
(h1 : 1 ∈ R.component 0)
:
CategoryTheory.Functor.Linear k (supportedProjectiveRepresentationEquivalence R ⋯ e he0 he hsum horth m hneg h1).functor