Beta bounds after rejecting all projective-injective socles

For the family of all non-simple indecomposable projective-injective right modules, every nonprojective mesh of the simultaneous socle quotient is an unchanged ambient mesh with no projective-injective middle summand. Thus the left/right beta boundary estimate bounds its total middle arity.

This is the occurrence-level content of Auslander--Reiten, Uniserial functors, Lemma 4.2, separated from the later uniserial-functor argument.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.nonsimpleProjectiveInjectiveLabels {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : Finset S.ProjectiveLabel

The basic family of all non-simple indecomposable projective-injective right modules. Simple projective-injectives cannot occur in a nontrivial almost-split middle term, so this is the full family relevant to socle reduction.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_nonsimpleProjectiveInjectiveLabels_iff {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) : p ∈ S.nonsimpleProjectiveInjectiveLabels ↔ CategoryTheory.Injective (S.fgObj p.label) ∧ ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.nonsimpleProjectiveInjectiveLabels_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) (hp : p ∈ S.nonsimpleProjectiveInjectiveLabels) : CategoryTheory.Injective (S.fgObj p.label)

Every selected label in the all-projective-injective family is injective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.nonsimpleProjectiveInjectiveLabels_notSimple {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) (hp : p ∈ S.nonsimpleProjectiveInjectiveLabels) : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)

Every selected label in the all-projective-injective family is non-simple.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMiddleLabel_not_simple_of_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (i : (S.minimalRightAlmostSplitAt z).index.obj) (hi : CategoryTheory.Injective (S.fgObj ((S.minimalRightAlmostSplitAt z).label i))) : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj ((S.minimalRightAlmostSplitAt z).label i))

An injective occurrence in a minimal right almost-split middle term cannot be simple. Indeed, a nonzero map from a simple object is monic, and injectivity would split that irreducible component.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMiddleArity_eq_zero_of_projective_simple {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) (hsimple : IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p)) : FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData p = 0

A simple projective has zero radical, hence its projective-boundary right middle term has arity zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.nonsimpleProjectiveInjectiveSocleFamily_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) {bound : ℕ} (hbeta : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ bound) (hleft : S.leftBeta ≤ bound) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal S.nonsimpleProjectiveInjectiveLabels ⋯))ᵐᵒᵖ] (j : Fin (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleFamilyIdeal S.nonsimpleProjectiveInjectiveLabels ⋯)).n) (hjNonprojective : ¬(S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleFamilyIdeal S.nonsimpleProjectiveInjectiveLabels ⋯)).IsProjective j) : FiniteTauMatrix.rightMiddleArity (S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleFamilyIdeal S.nonsimpleProjectiveInjectiveLabels ⋯)).toFiniteRightTauCategoryData j ≤ bound

After simultaneously rejecting the socles of all non-simple projective-injective indecomposables, every nonprojective quotient mesh has total middle arity bounded by any common bound on the ambient right and left beta invariants.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.nonsimpleProjectiveInjectiveSocleFamily_rightMiddleArity_le_two {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) (hbeta : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ 2) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal S.nonsimpleProjectiveInjectiveLabels ⋯))ᵐᵒᵖ] (j : Fin (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleFamilyIdeal S.nonsimpleProjectiveInjectiveLabels ⋯)).n) : FiniteTauMatrix.rightMiddleArity (S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleFamilyIdeal S.nonsimpleProjectiveInjectiveLabels ⋯)).toFiniteRightTauCategoryData j ≤ 2

If the ambient beta invariant is at most two, then every right mesh of the simultaneous quotient by all non-simple projective-injective socles has total middle arity at most two, including the new projective replacement vertices.