The grading interface on the primitive factor skeleton

The representation-directed standardness step in the frozen manuscript gives the surviving indecomposable skeleton a positive path-length grading. This file records the exact output needed by the poset-space argument and proves all subsequent concentration statements from it.

The chosen maps P ⟶ P_t need not be included as extra homogeneous data: their Hom spaces are one-dimensional, so internal direct-sum uniqueness makes each chosen nonzero map homogeneous in a unique degree.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : Type u

A positive internal grading on the Hom spaces between surviving selected indecomposables. Composition adds degrees, and distinct skeleton objects have no degree-zero morphisms.

• component (x y : S.SurvivingLabel K) : ℕ → Submodule k (S.factorObject K x ⟶ S.factorObject K y)
• isInternal (x y : S.SurvivingLabel K) : DirectSum.IsInternal (self.component x y)
• comp_mem {x y z : S.SurvivingLabel K} {i j : ℕ} {f : S.factorObject K x ⟶ S.factorObject K y} {g : S.factorObject K y ⟶ S.factorObject K z} : f ∈ self.component x y i → g ∈ self.component y z j → CategoryTheory.CategoryStruct.comp f g ∈ self.component x z (i + j)
• id_mem_zero (x : S.SurvivingLabel K) : CategoryTheory.CategoryStruct.id (S.factorObject K x) ∈ self.component x x 0
• degreeZero_eq_bot_of_ne {x y : S.SurvivingLabel K} : x ≠ y → self.component x y 0 = ⊥

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.source_projective_finrank_eq_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (t : T) : Module.finrank k (S.factorObject K D.source ⟶ S.factorObject K (R.label t)) = 1

The represented Hom space Hom(P,P_t) is one-dimensional.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.unitDegree {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) (t : T) : ℕ

The unique homogeneous degree of the chosen nonzero map P ⟶ P_t.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.unit_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) (t : T) : R.unit t ∈ G.component D.source (R.label t) (G.unitDegree R t)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.precomposition_shiftsDegree {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) (t : T) (x : S.SurvivingLabel K) : GradedLinear.ShiftsDegree (G.component (R.label t) x) (G.component D.source x) (R.representableData.precomposition t (S.factorObject K x)) (G.unitDegree R t)

Precomposition by the chosen map P ⟶ P_t shifts the skeleton grading by the uniquely determined degree of that map.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.objInternalGrading {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) (x : S.SurvivingLabel K) : PosetSpace.InternalGrading (R.representableData.obj (S.factorObject K x))

The represented poset space of a surviving indecomposable inherits the internal grading on Hom(P,X).

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.map_homogeneousOfDegree {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) {x y : S.SurvivingLabel K} {f : S.factorObject K x ⟶ S.factorObject K y} {d : ℕ} (hf : f ∈ G.component x y d) : (G.objInternalGrading R x).HomogeneousOfDegree (G.objInternalGrading R y) (R.representableData.map f) d

A homogeneous factor morphism induces a homogeneous map of represented poset spaces of the same degree.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.objLevel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] [IsAlgClosed k] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (hsink : D.multiplicity ↑D.sink = 1) (x : S.SurvivingLabel K) : ℕ

The concentration level of a surviving indecomposable under the completed primitive poset-space realization.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.obj_component_level_eq_top {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] [IsAlgClosed k] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (hsink : D.multiplicity ↑D.sink = 1) (x : S.SurvivingLabel K) : G.component D.source x (G.objLevel R H hsink x) = ⊤

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.objLevel_source_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] [IsAlgClosed k] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (hsink : D.multiplicity ↑D.sink = 1) : G.objLevel R H hsink D.source = 0

The primitive source is concentrated in degree zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.objLevel_add_degree_eq_of_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] [IsAlgClosed k] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (hsink : D.multiplicity ↑D.sink = 1) {x y : S.SurvivingLabel K} {f : S.factorObject K x ⟶ S.factorObject K y} {d : ℕ} (hf : f ≠ 0) (hfd : f ∈ G.component x y d) : G.objLevel R H hsink x + d = G.objLevel R H hsink y

A nonzero homogeneous factor morphism raises concentration level by exactly its homogeneous degree.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.homogeneousComponent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} (G : S.SkeletonHomGrading K) {x y : S.SurvivingLabel K} (f : S.factorObject K x ⟶ S.factorObject K y) (d : ℕ) : S.factorObject K x ⟶ S.factorObject K y

The degree-d homogeneous component of a factor morphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.homogeneousComponent_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} (G : S.SkeletonHomGrading K) {x y : S.SurvivingLabel K} (f : S.factorObject K x ⟶ S.factorObject K y) (d : ℕ) : G.homogeneousComponent f d ∈ G.component x y d

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.exists_homogeneousComponent_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} (G : S.SkeletonHomGrading K) {x y : S.SurvivingLabel K} {f : S.factorObject K x ⟶ S.factorObject K y} (hf : f ≠ 0) : ∃ (d : ℕ), G.homogeneousComponent f d ≠ 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.exists_degree_mem_and_objLevel_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] [IsAlgClosed k] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (hsink : D.multiplicity ↑D.sink = 1) {x y : S.SurvivingLabel K} {f : S.factorObject K x ⟶ S.factorObject K y} (hf : f ≠ 0) : ∃ (d : ℕ), f ∈ G.component x y d ∧ G.objLevel R H hsink x + d = G.objLevel R H hsink y

Every nonzero factor morphism is homogeneous in one degree, and that degree is the difference of the concentration levels of its endpoints.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.existsUnique_degree_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] [IsAlgClosed k] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (hsink : D.multiplicity ↑D.sink = 1) {x y : S.SurvivingLabel K} {f : S.factorObject K x ⟶ S.factorObject K y} (hf : f ≠ 0) : ∃! d : ℕ, f ∈ G.component x y d

The homogeneous degree of a nonzero factor morphism is unique.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.objLevel_lt_of_nonzero_not_isIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] [IsAlgClosed k] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (hsink : D.multiplicity ↑D.sink = 1) {x y : S.SurvivingLabel K} (f : S.factorObject K x ⟶ S.factorObject K y) (hf : f ≠ 0) (hniso : ¬CategoryTheory.IsIso f) : G.objLevel R H hsink x < G.objLevel R H hsink y

A nonzero nonisomorphism between surviving indecomposables strictly raises the concentration level.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.SkeletonHomGrading.objLevel_le_sink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] [IsAlgClosed k] (G : S.SkeletonHomGrading K) (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (hsink : D.multiplicity ↑D.sink = 1) (x : S.SurvivingLabel K) : G.objLevel R H hsink x ≤ G.objLevel R H hsink D.sink

Every surviving indecomposable has level at most the level of the distinguished sink.