Primitive-coordinate boundary bounds from finite kernels

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveMultiplicity_rightTranslation_le_one_of_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 : ↑z ∈ S.primitiveKilledLabels D) : S.primitiveMultiplicity D (S.rightTranslationLabel z) ≤ 1

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveMultiplicity_injective_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.Injective (S.fgObj z)] : S.primitiveMultiplicity D z ≤ 1

Every indecomposable injective has primitive-coordinate dimension at most one, by the finite-kernel argument.