Compatibility of actual module coordinates with the reconstructed action

theorem MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionMap_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) (m : ℕ) (X : SupportedCategory m) (a : A) (y : intervalCoordinateSpace R ⋯ e he0 (CoveringHom.restrictedLinearYoneda (principalDegreeInclusion R ⋯ e he0) X.obj) m) (p : ι × Fin (m + 1)) : ↑((principalShiftHomEquiv R ⋯ (e p.1) ⋯ ⋯ (↑↑p.2) X.obj) ((intervalActionMap R ⋯ e he0 he (CoveringHom.restrictedLinearYoneda (principalDegreeInclusion R ⋯ e he0) X.obj) m a) y p)) = ∑ q : ι × Fin (m + 1), intervalCorner R e m p q a • ↑((principalShiftHomEquiv R ⋯ (e q.1) ⋯ ⋯ (↑↑q.2) X.obj) (y q))

Evaluation turns the reconstructed matrix action into the same action on coordinate vectors.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.supportedModuleCoordinateEquiv_smul {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) (a : A) (x : ↑X.obj.obj.module) : (supportedModuleCoordinateEquiv R ⋯ e he0 he hsum horth m X) (a • x) = (intervalActionMap R ⋯ e he0 he (CoveringHom.restrictedLinearYoneda (principalDegreeInclusion R ⋯ e he0) X.obj) m a) ((supportedModuleCoordinateEquiv R ⋯ e he0 he hsum horth m X) x)

The vector-space coordinate equivalence intertwines the actual algebra action with reconstruction.