The algebra action reconstructed from an interval representation

@[reducible, inline]

abbrev MagnitudeConjecture.Graded.FiniteGradedModule.intervalCoordinateSpace {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 v} (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (F : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (ModuleCat k)) (m : ℕ) : Type (max u v)

The underlying vector space assembled from all coordinates in [0,m].

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionMap {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 v} [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)) (m : ℕ) (a : A) : intervalCoordinateSpace R ⋯ e he0 F m →ₗ[k] intervalCoordinateSpace R ⋯ e he0 F m

An algebra element acts through its matrix of homogeneous projective morphisms.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionLinear {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 v} [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] (m : ℕ) : A →ₗ[k] Module.End k (intervalCoordinateSpace R ⋯ e he0 F m)

The reconstructed action is linear in the algebra element as well.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionMap_mul {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 v} [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 = ⊥) (hsum : ∑ i : ι, e i = 1) (m : ℕ) (a b : A) : intervalActionMap R ⋯ e he0 he F m (a * b) = intervalActionMap R ⋯ e he0 he F m a ∘ₗ intervalActionMap R ⋯ e he0 he F m b

The interval action respects multiplication.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionMap_one {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 v} [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] (h1 : 1 ∈ R.component 0) (horth : Pairwise fun (i j : ι) => e i * e j = 0) (m : ℕ) : intervalActionMap R ⋯ e he0 he F m 1 = LinearMap.id

Orthogonal complete coordinates make the action of 1 the identity.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionAlgHom {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 v} [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 : ℕ) : A →ₐ[k] Module.End k (intervalCoordinateSpace R ⋯ e he0 F m)

The reconstructed module action, packaged as an algebra homomorphism.