Functorial reconstruction from interval representation coordinates

def MagnitudeConjecture.Graded.FiniteGradedModule.intervalCoordinateMap {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} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) {F G : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (ModuleCat k)} (m : ℕ) (α : F ⟶ G) : intervalCoordinateSpace R ⋯ e he0 F m →ₗ[k] intervalCoordinateSpace R ⋯ e he0 G m

A natural transformation acts componentwise on the reconstructed vector spaces.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionMap_naturality {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 G : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (ModuleCat k)} [F.Additive] [CategoryTheory.Functor.Linear k F] [G.Additive] [CategoryTheory.Functor.Linear k G] (m : ℕ) (α : F ⟶ G) (a : A) (x : intervalCoordinateSpace R ⋯ e he0 F m) : (intervalCoordinateMap R ⋯ e he0 m α) ((intervalActionMap R ⋯ e he0 he F m a) x) = (intervalActionMap R ⋯ e he0 he G m a) ((intervalCoordinateMap R ⋯ e he0 m α) x)

Naturality is precisely compatibility with the reconstructed algebra action.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.intervalReconstructedMap {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 G : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (ModuleCat k)} [F.Additive] [CategoryTheory.Functor.Linear k F] [G.Additive] [CategoryTheory.Functor.Linear k G] (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) (hF : ∀ (p : (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ), FiniteDimensional k ↑(F.obj p)) (hG : ∀ (p : (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ), FiniteDimensional k ↑(G.obj p)) (m : ℕ) (α : F ⟶ G) : intervalReconstructedSupportedObject R ⋯ e he0 he F hneg h1 hsum horth hF m ⟶ intervalReconstructedSupportedObject R ⋯ e he0 he G hneg h1 hsum horth hG m

The induced degree-zero map between the actual reconstructed modules.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.intervalReconstructionFunctor {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 : ℕ) : CategoryTheory.Functor (CoveringHom.FiniteDimensionalModuleCategory k) (SupportedCategory m)

Reconstructing the supported graded module is functorial in the finite representation.

instance MagnitudeConjecture.Graded.FiniteGradedModule.intervalReconstructionFunctor_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) (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 : ℕ) : (intervalReconstructionFunctor R ⋯ e he0 he hneg h1 hsum horth m).Additive

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.supportedIntervalReconstructionFunctor {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 : ℕ) : CategoryTheory.Functor (ObjectDeletion.VanishingFiniteModuleCategory (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (principalOutsideInterval R ⋯ e he0 m)) (SupportedCategory m)

The candidate inverse to supported projective evaluation, with its support domain bundled.

instance MagnitudeConjecture.Graded.FiniteGradedModule.supportedIntervalReconstructionFunctor_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) (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).Additive