Recovering the actual supported graded module

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.supportedModuleRecoveryLinearEquiv {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) (hneg : ∀ d < 0, R.component d = ⊥) (h1 : 1 ∈ R.component 0) : ↑X.obj.obj.module ≃ₗ[A] ↑((supportedIntervalReconstructionFunctor R ⋯ e he0 he hneg h1 hsum horth m).obj ((principalSupportedEvaluationFunctor R ⋯ e he0 he m).obj X)).obj.obj.module

The coordinate equivalence is an equivalence of actual algebra modules.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.supportedModuleRecoveryMap {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) (hneg : ∀ d < 0, R.component d = ⊥) (h1 : 1 ∈ R.component 0) : X ⟶ ((principalSupportedEvaluationFunctor R ⋯ e he0 he m).comp (supportedIntervalReconstructionFunctor R ⋯ e he0 he hneg h1 hsum horth m)).obj X

The recovery map preserves physical degrees, including the external shift on the original module.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.supportedModuleRecoveryIso {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) (hneg : ∀ d < 0, R.component d = ⊥) (h1 : 1 ∈ R.component 0) : X ≅ ((principalSupportedEvaluationFunctor R ⋯ e he0 he m).comp (supportedIntervalReconstructionFunctor R ⋯ e he0 he hneg h1 hsum horth m)).obj X

Recovery is an isomorphism in the supported graded category.