Recovery of supported representations by actual graded modules #
noncomputable def
MagnitudeConjecture.Graded.FiniteGradedModule.supportedEvaluationReconstructionObjectIso
{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 : ℕ)
(F :
ObjectDeletion.VanishingFiniteModuleCategory (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ
(principalOutsideInterval R ⋯ e he0 m))
:
((supportedIntervalReconstructionFunctor R ⋯ e he0 he hneg h1 hsum horth m).comp
(principalSupportedEvaluationFunctor R ⋯ e he0 he m)).obj
F ≅ F
The recovered representation is isomorphic in the supported finite module category.
Instances For
noncomputable def
MagnitudeConjecture.Graded.FiniteGradedModule.supportedEvaluationReconstructionCounit
{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 : ℕ)
:
(supportedIntervalReconstructionFunctor R ⋯ e he0 he hneg h1 hsum horth m).comp
(principalSupportedEvaluationFunctor R ⋯ e he0 he m) ≅ CategoryTheory.Functor.id
(ObjectDeletion.VanishingFiniteModuleCategory (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ
(principalOutsideInterval R ⋯ e he0 m))
Reconstruction followed by evaluation is naturally isomorphic to the identity.
Instances For
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.principalSupportedEvaluation_essSurj
{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 : ℕ)
:
(principalSupportedEvaluationFunctor R ⋯ e he0 he m).EssSurj
Every supported finite representation is the evaluation of an actual supported graded module.