The actual supported graded module reconstructed from interval coordinates

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.intervalReconstructedModule {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) (F : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (ModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (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 : ℕ) : Module A (intervalCoordinateSpace R ⋯ e he0 F m)

The reconstructed algebra module structure on the interval coordinate space.

def MagnitudeConjecture.Graded.FiniteGradedModule.intervalReconstructedScalarTower {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) (F : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (ModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (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 : ℕ) : IsScalarTower k A (intervalCoordinateSpace R ⋯ e he0 F m)

The reconstructed action agrees with the original field action.

def MagnitudeConjecture.Graded.FiniteGradedModule.intervalReconstructedGrading {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) (F : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (ModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (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 : ℕ) : ModuleGrading R

The degree labels grade the reconstructed algebra action.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.intervalReconstructedObject {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) (F : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (ModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (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) (hfinite : ∀ (p : (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ), FiniteDimensional k ↑(F.obj p)) (m : ℕ) : FiniteGradedModule R

An actual finite-dimensional graded module reconstructed from the interval representation.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.intervalReconstructed_supported {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) (F : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (ModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (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) (hfinite : ∀ (p : (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ), FiniteDimensional k ↑(F.obj p)) (m : ℕ) : SupportedIn m { obj := intervalReconstructedObject R ⋯ e he0 he F hneg h1 hsum horth hfinite m, degree := 0 }

No homogeneous component of the reconstructed module lies outside [0,m].

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.intervalReconstructedSupportedObject {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) (F : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (ModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (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) (hfinite : ∀ (p : (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ), FiniteDimensional k ↑(F.obj p)) (m : ℕ) : SupportedCategory m

The reconstructed object bundled in the supported graded category.