Actual almost-split maps and nonprojective targets in the control interval

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalIncomingQuiver {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.intervalIncomingArrowFintype {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.standardFormGradedIncomingMap_underlyingFG_epi {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) (hz : ¬CategoryTheory.Projective (S.fgObj z)) (t : ℤ) : CategoryTheory.Epi (Graded.FiniteGradedModule.underlyingFG.map ↑(S.standardFormGradedIncomingMap z t))

At a nonprojective original label the actual incoming map is epic after forgetting its grading, in the finitely generated standard-form category.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIncomingSource {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.SupportedCategory (S.standardFormIntervalControlHeight + 2)

The middle of the incoming map, placed in the single control interval.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIncomingTarget {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.SupportedCategory (S.standardFormIntervalControlHeight + 2)

The target representative at shift zero or one in the same interval.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIncomingMap {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) : S.standardFormIntervalIncomingSource z t ht0 ht1 ⟶ S.standardFormIntervalIncomingTarget z t ht0 ht1

The literal degree-one incoming map in the finite interval.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIncomingMap_rightAlmostSplit {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) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (S.standardFormIntervalIncomingMap z t ht0 ht1)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIncomingMap_rightMinimal {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) : QuotientSubmoduleEquidistribution.IsRightMinimal (S.standardFormIntervalIncomingMap z t ht0 ht1)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalIncomingTarget_not_projective {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) (hz : ¬CategoryTheory.Projective (S.fgObj z)) (t : ℤ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : ¬CategoryTheory.Projective (S.standardFormIntervalIncomingTarget z t ht0 ht1)

The second shift preserves nonprojectivity inside the control interval: the shifted incoming map is an actual nonsplit epimorphism there.