Exactly which standard-form indecomposables are supported in an interval

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalShiftsQuiver {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.intervalShiftsArrowFintype {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.standardFormGradedFamily_support_nonempty {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : (S.standardFormGradedFamily i).grading.support.Nonempty

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportWindow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : GradedInterval.SupportWindow (S.standardFormGradedFamily i).grading.support

Exact least and greatest nonzero degrees of each standard-form representative.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportHeight {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : ℕ

A common positive upper bound for every representative's support.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportWindow_upper_le {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : (S.standardFormSupportWindow i).upper ≤ S.standardFormSupportHeight

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_supported_iff {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) (s : ℤ) (m : ℕ) : Graded.FiniteGradedModule.SupportedIn m { obj := S.standardFormGradedFamily i, degree := s } ↔ s ∈ GradedInterval.allowedShifts m (S.standardFormSupportWindow i).lower (S.standardFormSupportWindow i).upper

A shifted representative lies in [0,m] exactly at the explicitly counted shifts.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_supported_classification {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (M : Graded.FiniteGradedModule.ShiftedModule) (hM : CategoryTheory.Indecomposable M) (hs : Graded.FiniteGradedModule.SupportedIn m M) : ∃ (i : Fin S.n), ∃ s ∈ GradedInterval.allowedShifts m (S.standardFormSupportWindow i).lower (S.standardFormSupportWindow i).upper, Nonempty (M ≅ { obj := S.standardFormGradedFamily i, degree := s })

Every indecomposable supported graded module occurs at one of the allowed shifts.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_supported_label_count {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (hm : S.standardFormSupportHeight ≤ m) : ∑ i : Fin S.n, ↑(GradedInterval.allowedShifts m (S.standardFormSupportWindow i).lower (S.standardFormSupportWindow i).upper).card = ↑S.n * (↑m + 1) - ∑ i : Fin S.n, (↑(S.standardFormSupportWindow i).upper - ↑(S.standardFormSupportWindow i).lower)

The exact number of allowed labelled representatives has constant width correction.