Kupisch uniseriality for selected projectives

The primitive-corner finite-ideal theorem gives comparability on literal corners. This file transports it through the fully faithful coordinate functor to the selected-projective category and applies the generic Kupisch classification, producing condition (K)(2) in the exact module orientation used by the Skowroński--Waschbüsch correction.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.finiteIdeal_projectiveHom_homSubbimodule_comparable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) {X Y : S.ProjectiveCategory} (T U : Submodule k (X ⟶ Y)) (hT : IsHomSubbimodule T) (hU : IsHomSubbimodule U) : T ≤ U ∨ U ≤ T

Representation-finite primitive-corner comparability transported to the literal selected-projective category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.finiteIdeal_projectiveHom_uniserialAlternative {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (X Y : S.ProjectiveCategory) : IsUniserialModule (CategoryTheory.End Y) (X ⟶ Y) ∨ IsUniserialModule (CategoryTheory.End X)ᵐᵒᵖ (X ⟶ Y)

Representation-finiteness gives Kupisch's exact target-side or opposite-source-side uniserial alternative on every selected-projective Hom space.