Intrinsic irreducible quotients for the actual interval algebra

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalIrreducibleBaseFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : FiniteDimensional k (S.standardFormAlgebra ⋯)

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalAlgebraEquivalence_additive {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) : (S.standardFormIntervalAlgebraEquivalence m).functor.Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalAlgebraEquivalence_linear {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) : CategoryTheory.Functor.Linear k (S.standardFormIntervalAlgebraEquivalence m).functor

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterval_irreducibleEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (X Y : FGModuleCat (S.standardFormIntervalAlgebra m)ᵐᵒᵖ) : CategoricalIrreducible.Space k X Y ≃ₗ[k] CategoricalIrreducible.Space k ((S.standardFormIntervalAlgebraEquivalence m).functor.obj X) ((S.standardFormIntervalAlgebraEquivalence m).functor.obj Y)

The actual interval realization preserves the intrinsic irreducible quotient.