Incoming indecomposables at interior targets remain supported

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.interiorSupportQuiver {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.interiorSupportArrowFintype {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_interior_source_supported {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (i j : Fin S.n) (s t : ℤ) (ht0 : 0 ≤ t) (htm : t ≤ ↑m - 2 * ↑S.standardFormIntervalControlHeight) (f : { obj := S.standardFormGradedFamily i, degree := s } ⟶ { obj := S.standardFormGradedFamily j, degree := t }) (hf : f ≠ 0) : Graded.FiniteGradedModule.SupportedIn m { obj := S.standardFormGradedFamily i, degree := s }

Every shifted representative mapping nontrivially to an interior target has its whole support in the finite interval.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_interior_indecomposable_supported {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (j : Fin S.n) (t : ℤ) (ht0 : 0 ≤ t) (htm : t ≤ ↑m - 2 * ↑S.standardFormIntervalControlHeight) (M : Graded.FiniteGradedModule.ShiftedModule) (hM : CategoryTheory.Indecomposable M) (f : M ⟶ { obj := S.standardFormGradedFamily j, degree := t }) (hf : f ≠ 0) : Graded.FiniteGradedModule.SupportedIn m M

The interior support statement applies to every graded indecomposable, not just the chosen representatives.