Simple socles in almost-split sources

If the source of a right almost-split sequence has simple socle, some displayed component of its monic left map must itself be monic. Otherwise every component kills the socle, contradicting monicity of the total map.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_rightSequenceLeftComponent_mono_of_simpleSocle {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (hsocle : IsSimpleModule Aᵐᵒᵖ ↥(moduleSocle Aᵐᵒᵖ ↑(S.fgObj (S.rightTranslationLabel z)))) : ∃ (i : (S.minimalRightAlmostSplitAt ↑z).index.obj), CategoryTheory.Mono (QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalLeftAlmostSplitDecomposition.component S.almostSplitSkeleton (S.rightSequenceLeftDecomposition z) i)

A simple socle in the source of a chosen right almost-split sequence forces at least one displayed left component to be monic.