Naturality of the evaluation–reconstruction coordinate comparison #
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionCoefficient_of_morphism
{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 : ℕ)
(p q : ι × Fin (m + 1))
(f : intervalProjectiveLabel R ⋯ e he0 m p ⟶ intervalProjectiveLabel R ⋯ e he0 m q)
:
(intervalActionCoefficient R ⋯ e he0 he m p q)
↑((principalDegreeHomEquiv R ⋯ e he0 he (intervalProjectiveLabel R ⋯ e he0 m p)
(intervalProjectiveLabel R ⋯ e he0 m q))
f) = f
A homogeneous projective map is recovered from its own corner coefficient.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionMap_singleCoordinate
{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]
(m : ℕ)
(p q : ι × Fin (m + 1))
(f : intervalProjectiveLabel R ⋯ e he0 m p ⟶ intervalProjectiveLabel R ⋯ e he0 m q)
(x : intervalCoordinateSpace R ⋯ e he0 F m)
(hx :
x ∈ singleCoordinate (fun (z : ι × Fin (m + 1)) => ↑(F.obj (Opposite.op (intervalProjectiveLabel R ⋯ e he0 m z)))) q)
:
(intervalActionMap R ⋯ e he0 he F m
↑((principalDegreeHomEquiv R ⋯ e he0 he (intervalProjectiveLabel R ⋯ e he0 m p)
(intervalProjectiveLabel R ⋯ e he0 m q))
f))
x p = (ModuleCat.Hom.hom (F.map f.op)) (x q)
On a single coordinate, the reconstructed action is the original representation map.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.intervalEvaluationCoordinate_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 : 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 : ℕ)
(p q : ι × Fin (m + 1))
(f : intervalProjectiveLabel R ⋯ e he0 m p ⟶ intervalProjectiveLabel R ⋯ e he0 m q)
(g :
(principalDegreeInclusion R ⋯ e he0).obj (intervalProjectiveLabel R ⋯ e he0 m q) ⟶ (intervalReconstructedSupportedObject R ⋯ e he0 he F hneg h1 hsum horth hfinite m).obj)
:
(intervalEvaluationCoordinateEquiv R ⋯ e he0 he F hneg h1 hsum horth hfinite m p)
(CategoryTheory.CategoryStruct.comp f.hom g) = (ModuleCat.Hom.hom (F.map f.op)) ((intervalEvaluationCoordinateEquiv R ⋯ e he0 he F hneg h1 hsum horth hfinite m q) g)
Evaluation after reconstruction intertwines every morphism between interval projectives.