Beta bounds at a projective radical boundary

For a noninjective indecomposable projective P, every irreducible map into P has noninjective source: an irreducible map from an injective object to a projective object would split whether it were monic or epic. Simultaneous inverse Auslander--Reiten translation therefore identifies all incoming arrow occurrences at P with the nonprojective occurrences in the right mesh ending at τ⁻¹P. Consequently the number of indecomposable summands of rad P is bounded by the ordinary beta invariant.

This is the decomposition-count part of Auslander--Reiten's projective radical argument. The later uniseriality of the resulting one or two summands is not asserted here.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.arrowMultiplicity_eq_zero_of_injective_source_of_projective_target {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source target : Fin S.n) (hsource : CategoryTheory.Injective (S.fgObj source)) (htarget : CategoryTheory.Projective (S.fgObj target)) : FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData source target = 0

There is no irreducible map from an injective selected indecomposable to a projective selected indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projective_rightMiddleArity_eq_betaAt_inverseTranslation {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)) (hpNotInjective : ¬CategoryTheory.Injective (S.fgObj p)) : FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData p = FiniteTauMatrix.betaAt S.finiteTauCategoryData.toFiniteRightTauCategoryData ↑(S.rightTranslationEquiv.symm ⟨p, hpNotInjective⟩)

At a noninjective projective boundary, total incoming middle arity is the beta count at the inverse translate.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projective_rightMiddleArity_le_beta {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)) (hpNotInjective : ¬CategoryTheory.Injective (S.fgObj p)) : FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData p ≤ FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData

The projective-boundary arity of a noninjective projective is bounded by the global beta invariant.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_projectiveBoundaryRadical_decomposition_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 : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) (hpNotInjective : ¬CategoryTheory.Injective (S.fgObj p)) (hbeta : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ 2) : ∃ (d : CategoryTheory.FiniteIndecomposableDecomposition (S.projectiveBoundaryRadical p)), d.n ≤ 2

Under beta ≤ 2, the radical of a noninjective indecomposable projective admits an indecomposable decomposition with at most two occurrences.