Gradings carried by a representable poset-space realization

The frozen manuscript grades the factor category by path length and then grades each represented total space Hom(P, X) by the same homogeneous Hom components. The chosen maps P ⟶ P_t are homogeneous. Composition therefore makes every distinguished subspace

image (Hom(P_t, X) ⟶ Hom(P, X))

homogeneous, so the represented poset space acquires the compatible internal grading used in the concentration argument.

structure MagnitudeConjecture.PosetSpace.RepresentableData.HomGrading {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) : Type (max u v)

An internal grading on every Hom space, compatible with composition and with the chosen maps defining a representable poset-space realization.

• component (X Y : C) : ℕ → Submodule k (X ⟶ Y)
• isInternal (X Y : C) : DirectSum.IsInternal (self.component X Y)
• comp_mem {X Y Z : C} {i j : ℕ} {f : X ⟶ Y} {g : Y ⟶ Z} : f ∈ self.component X Y i → g ∈ self.component Y Z j → CategoryTheory.CategoryStruct.comp f g ∈ self.component X Z (i + j)
• unitDegree : T → ℕ
• unit_mem (t : T) : D.unit t ∈ self.component D.source (D.projective t) (self.unitDegree t)

theorem MagnitudeConjecture.PosetSpace.RepresentableData.HomGrading.precomposition_shiftsDegree {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : RepresentableData k T C} (G : D.HomGrading) (t : T) (X : C) : GradedLinear.ShiftsDegree (G.component (D.projective t) X) (G.component D.source X) (D.precomposition t X) (G.unitDegree t)

Precomposition by a chosen homogeneous map P ⟶ P_t shifts degree by the degree of that map.

theorem MagnitudeConjecture.PosetSpace.RepresentableData.HomGrading.subspace_isHomogeneous {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : RepresentableData k T C} (G : D.HomGrading) (X : C) (t : T) : DirectSum.SetLike.IsHomogeneous (G.component D.source X) ((D.obj X).subspace t)

Every distinguished subspace in the represented poset space is homogeneous for the grading inherited from Hom(P, X).

def MagnitudeConjecture.PosetSpace.RepresentableData.HomGrading.objInternalGrading {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : RepresentableData k T C} (G : D.HomGrading) (X : C) : InternalGrading (D.obj X)

The grading on Hom(P, X) is a compatible internal grading of the represented poset space F(X).

theorem MagnitudeConjecture.PosetSpace.RepresentableData.HomGrading.map_homogeneousOfDegree {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : RepresentableData k T C} (G : D.HomGrading) {X Y : C} {f : X ⟶ Y} {d : ℕ} (hf : f ∈ G.component X Y d) : (G.objInternalGrading X).HomogeneousOfDegree (G.objInternalGrading Y) (D.map f) d

A homogeneous categorical morphism induces a homogeneous morphism of the represented poset spaces, of the same degree.

theorem MagnitudeConjecture.PosetSpace.RepresentableData.HomGrading.objLevel_add_degree_eq {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : RepresentableData k T C} (G : D.HomGrading) {X Y : C} (hX : IsSchur k T (D.obj X)) (hY : IsSchur k T (D.obj Y)) {f : X ⟶ Y} {d : ℕ} (hf : D.map f ≠ 0) (hfd : f ∈ G.component X Y d) : (G.objInternalGrading X).level hX + d = (G.objInternalGrading Y).level hY

A nonzero homogeneous morphism between objects whose represented poset spaces are Schur raises their concentration levels by exactly its degree.