Coordinates of actual supported graded modules #
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.supportedModule_degree_cover
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
(R : VectorGrading k A)
(m : ℕ)
(X : SupportedCategory m)
(d : ℤ)
(hd : X.obj.obj.grading.component d ≠ ⊥)
:
∃ (r : Fin (m + 1)), ↑↑r - X.obj.degree = d
The interval labels cover every nonzero degree of a supported shifted module.
noncomputable def
MagnitudeConjecture.Graded.FiniteGradedModule.supportedModuleCoordinateEquiv
{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 : ℕ)
(X : SupportedCategory m)
:
↑X.obj.obj.module ≃ₗ[k] intervalCoordinateSpace R ⋯ e he0 (CoveringHom.restrictedLinearYoneda (principalDegreeInclusion R ⋯ e he0) X.obj) m
Evaluate all interval projectives to express the actual underlying vector space in reconstruction coordinates.
Instances For
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.supportedModuleCoordinateEquiv_evaluation
{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 : ℕ)
(X : SupportedCategory m)
(x : ↑X.obj.obj.module)
(p : ι × Fin (m + 1))
:
(principalShiftHomEquiv R ⋯ (e p.1) ⋯ ⋯ (↑↑p.2) X.obj)
((supportedModuleCoordinateEquiv R ⋯ e he0 he hsum horth m X) x p) = ⟨(X.obj.obj.grading.idempotentProjection (e p.1) (↑↑p.2 - X.obj.degree)) x, ⋯⟩
Reading a reconstructed coordinate recovers the corresponding homogeneous idempotent projection.