Dual primitive-coordinate bounds from finite kernels

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveMultiplicity_projective_le_one_finiteKernel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) (z : Fin S.n) [CategoryTheory.Projective (S.fgObj z)] : S.primitiveMultiplicity D z ≤ 1

The dual finite-kernel argument bounds every indecomposable projective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveMultiplicity_le_one_of_rightTranslation_killed_finiteKernel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] (S : FiniteIndecomposableSkeleton k A) (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (hz : S.rightTranslationLabel z ∈ S.primitiveKilledLabels D) : S.primitiveMultiplicity D ↑z ≤ 1

If the first term of an almost-split sequence is killed, the last term has primitive-coordinate dimension at most one.