Irreducible spaces for the allowed-shift interval family

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalFamily_irreducibleEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (a b : S.standardFormSupportedLabel m) : CategoricalIrreducible.Space k ((S.standardFormIntervalAlgebraEquivalence m).inverse.obj (S.standardFormSupportedFamily m a)) ((S.standardFormIntervalAlgebraEquivalence m).inverse.obj (S.standardFormSupportedFamily m b)) ≃ₗ[k] CategoricalIrreducible.Space k (S.standardFormSupportedFamily m a) (S.standardFormSupportedFamily m b)

The quotient for the actual interval-module family is the quotient on its literal allowed-shift representatives in the supported category.