The beta bound under projective-injective socle rejection

Simultaneous rejection removes projective-injective vertices and replaces each of them by its socle quotient. At an ordinary surviving endpoint the right-mesh arity is unchanged. At a replacement endpoint the ambient middle term has one additional occurrence, but that occurrence is the deleted projective itself and hence is not counted by beta.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamily_replacement_betaAt_le_rejected_arity {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] (p : S.ProjectiveLabel) (hp : p ∈ T) : FiniteTauMatrix.betaAt S.finiteTauCategoryData.toFiniteRightTauCategoryData ↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleFamilyIdeal T hInjective)) (P.primitiveProjectiveSocleFamilyFiniteReplacementLabel T hInjective hNotSimple p hp)) ≤ FiniteTauMatrix.rightMiddleArity (S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).toFiniteRightTauCategoryData (P.primitiveProjectiveSocleFamilyFiniteReplacementLabel T hInjective hNotSimple p hp)

At a replacement endpoint, the nonprojective ambient middle occurrences fit inside the rejected middle term: the single additional ambient occurrence is the selected projective-injective itself.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.beta_le_of_primitiveProjectiveSocleFamily_rightMiddleArity_le {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] (bound : ℕ) (hbound : ∀ (j : Fin (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).n), FiniteTauMatrix.rightMiddleArity (S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).toFiniteRightTauCategoryData j ≤ bound) : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ bound

If every right-mesh middle term of the simultaneous socle quotient has arity at most bound, then the ambient beta is at most bound. Ordinary surviving endpoints keep their arity; at a replacement endpoint the one discarded occurrence is projective and therefore invisible to beta.