Scalar endomorphisms and directedness of the graded representatives

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rdGradedDirectedQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Quiver (Fin S.n)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rdGradedDirectedArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) : Fintype (x ⟶ y)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_end_scalar {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : S.StandardFormMeshCategory) (s : ℤ) (f : { obj := S.standardFormGradedVertexFunctor.obj X, degree := s } ⟶ { obj := S.standardFormGradedVertexFunctor.obj X, degree := s }) : ∃ (c : k), f = c • CategoryTheory.CategoryStruct.id { obj := S.standardFormGradedVertexFunctor.obj X, degree := s }

Every endomorphism of a shifted vertex module is scalar.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_end_isIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : S.StandardFormMeshCategory) (s : ℤ) (f : { obj := S.standardFormGradedVertexFunctor.obj X, degree := s } ⟶ { obj := S.standardFormGradedVertexFunctor.obj X, degree := s }) (hf : f ≠ 0) : CategoryTheory.IsIso f

Nonzero endomorphisms of a shifted representative are invertible.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_noniso_descent {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : S.StandardFormMeshCategory) (s t : ℤ) (f : { obj := S.standardFormGradedVertexFunctor.obj X, degree := s } ⟶ { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }) (hf : f ≠ 0) (hi : ¬CategoryTheory.IsIso f) : t < s

Every nonzero nonisomorphism between graded representatives lowers the shift.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedEdge {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : GradedCategory.DegreeObject S.standardFormIntegerHomGrading) : Prop

Nonzero nonisomorphism edges on the classified graded representatives.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_acyclic {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : GradedCategory.DegreeObject S.standardFormIntegerHomGrading) : ¬Relation.TransGen S.standardFormGradedEdge X X

The classified graded category has no cycle of nonzero nonisomorphisms.