The actual degree-one incoming maps and their interval support

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.incomingGradedQuiver {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.incomingGradedArrowFintype {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)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedIncomingObject {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : CategoryTheory.Mat_ S.StandardFormMeshCategory

The actual incoming-arrow sum, in the raw mesh additive envelope.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedIncomingMap {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : S.standardGradedIncomingObject z ⟶ (CategoryTheory.Mat_.embedding S.StandardFormMeshCategory).obj (MeshCategory.obj S.standardFormRightMeshData z)

The literal incoming matrix, whose columns are the incoming mesh arrows.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedIncomingMap_homogeneous {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : S.standardGradedIncomingMap z ∈ (S.standardFormAdditiveHomGrading ⋯).component (S.standardGradedIncomingObject z) ((CategoryTheory.Mat_.embedding S.StandardFormMeshCategory).obj (MeshCategory.obj S.standardFormRightMeshData z)) 1

All entries of the incoming matrix have degree one.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedIncomingMap {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (t : ℤ) : { obj := S.standardFormGradedFunctor.obj (S.standardGradedIncomingObject z), degree := t + 1 } ⟶ { obj := S.standardFormGradedFamily z, degree := t }

The canonical incoming map, with its middle shifted one degree above its target.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedObject_support_control {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) (d : ℤ) (hd : d ∈ (S.standardFormGradedFunctor.obj X).grading.support) : 0 ≤ d ∧ d ≤ ↑S.standardFormIntervalControlHeight

The common mesh degree bound controls every finite sum of the actual representatives.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedObject_shifted_supported {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) (t : ℤ) (m : ℕ) (ht : 0 ≤ t) (hm : ↑S.standardFormIntervalControlHeight + t ≤ ↑m) : Graded.FiniteGradedModule.SupportedIn m { obj := S.standardFormGradedFunctor.obj X, degree := t }

Any nonnegative shift of a represented finite sum fits in the predicted interval.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedIncomingMap_supported {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (t : ℤ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : Graded.FiniteGradedModule.SupportedIn (S.standardFormIntervalControlHeight + 2) { obj := S.standardFormGradedFunctor.obj (S.standardGradedIncomingObject z), degree := t + 1 } ∧ Graded.FiniteGradedModule.SupportedIn (S.standardFormIntervalControlHeight + 2) { obj := S.standardFormGradedFamily z, degree := t }

Both the ordinary incoming map and its next shift lie in the one interval [0,h+2].