Projective boundary summands in Auslander--Reiten meshes

If one summand of a right almost-split middle term is projective, the corresponding left component is monic. Exactness then makes every other right component monic, so none of the other middle summands can be injective. This is the boundary-counting step used in the comparison of the left and right beta invariants and in projective-injective socle rejection.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.leftBetaAt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source : Fin S.n) : ℕ

Number of noninjective indecomposable occurrences leaving a selected label. Under contragredient duality this is the ordinary betaAt for the opposite-algebra skeleton.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.leftBeta {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : ℕ

Maximum number of noninjective occurrences leaving a noninjective label. This is the right-module realization of the classical left beta invariant.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.leftBeta_le_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (bound : ℕ) : S.leftBeta ≤ bound ↔ ∀ (source : Fin S.n), ¬CategoryTheory.Injective (S.fgObj source) → S.leftBetaAt source ≤ bound

A bound on left beta is exactly a bound on the outgoing noninjective occurrences at every noninjective source.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredient_betaAt_eq_leftBetaAt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] (x : { i : Fin S.n // ¬CategoryTheory.Injective (S.fgObj i) }) : FiniteTauMatrix.betaAt S.contragredientSkeleton.finiteTauCategoryData.toFiniteRightTauCategoryData ↑(S.contragredientNonprojectiveLabel x) = S.leftBetaAt ↑x

Contragredient duality identifies opposite betaAt with the original outgoing noninjective-occurrence count.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredient_beta_eq_leftBeta {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] : FiniteTauMatrix.beta S.contragredientSkeleton.finiteTauCategoryData.toFiniteRightTauCategoryData = S.leftBeta

The beta invariant of the label-aligned contragredient skeleton is the original left beta invariant.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.nonprojectiveOutgoingAt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source : Fin S.n) : ℕ

Number of nonprojective indecomposable occurrences leaving a selected label. Unlike betaAt, this is an outgoing count.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.arrowMultiplicity_inverseTranslation_pair {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x y : { i : Fin S.n // ¬CategoryTheory.Injective (S.fgObj i) }) : FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData ↑(S.rightTranslationEquiv.symm x) ↑(S.rightTranslationEquiv.symm y) = FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData ↑x ↑y

Simultaneous inverse Auslander--Reiten translation preserves arrow multiplicity between noninjective labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.leftBetaAt_eq_nonprojectiveOutgoingAt_inverseTranslation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x : { i : Fin S.n // ¬CategoryTheory.Injective (S.fgObj i) }) : S.leftBetaAt ↑x = S.nonprojectiveOutgoingAt ↑(S.rightTranslationEquiv.symm x)

Inverse translation identifies the noninjective outgoing count at x with the nonprojective outgoing count at tauMinus x.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.nonprojectiveOutgoingAt_eq_betaAt_inverseTranslation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x : { i : Fin S.n // ¬CategoryTheory.Injective (S.fgObj i) }) : S.nonprojectiveOutgoingAt ↑x = FiniteTauMatrix.betaAt S.finiteTauCategoryData.toFiniteRightTauCategoryData ↑(S.rightTranslationEquiv.symm x)

At a noninjective source, the nonprojective outgoing count is the ordinary betaAt count at its inverse translate.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.leftBetaAt_le_beta_of_inverseTranslation_not_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x : { i : Fin S.n // ¬CategoryTheory.Injective (S.fgObj i) }) (hx : ¬CategoryTheory.Injective (S.fgObj ↑(S.rightTranslationEquiv.symm x))) : S.leftBetaAt ↑x ≤ FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData

A left-beta count can exceed the global right beta only at the terminal injective boundary of inverse translation.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.inverseTranslation_injective_of_beta_lt_leftBetaAt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x : { i : Fin S.n // ¬CategoryTheory.Injective (S.fgObj i) }) (hx : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData < S.leftBetaAt ↑x) : CategoryTheory.Injective (S.fgObj ↑(S.rightTranslationEquiv.symm x))

Under a right-beta bound, any larger left-beta count is forced to sit at an injective inverse translate.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_injective_inverseTranslation_of_beta_lt_leftBeta {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (hbeta : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData < S.leftBeta) : ∃ (x : { i : Fin S.n // ¬CategoryTheory.Injective (S.fgObj i) }), FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData < S.leftBetaAt ↑x ∧ CategoryTheory.Injective (S.fgObj ↑(S.rightTranslationEquiv.symm x))

If the global left beta is strictly larger than the global right beta, the excess is witnessed by a noninjective source whose inverse translate is injective. Thus simultaneous translation eliminates every non-boundary case of the one-sided beta comparison.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_injective_nonprojective_boundary_of_beta_le_of_not_leftBeta_le {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] {bound : ℕ} (hbeta : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ bound) (hleft : ¬S.leftBeta ≤ bound) : ∃ (z : { i : Fin S.n // ¬CategoryTheory.Projective (S.fgObj i) }), CategoryTheory.Injective (S.fgObj ↑z) ∧ bound < S.nonprojectiveOutgoingAt ↑z

If a proposed common bound holds for right beta but fails for left beta, the whole failure is concentrated at an injective nonprojective label: more than bound nonprojective arrow occurrences leave that label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_injective_nonprojective_boundary_of_beta_le_two {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (hbeta : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ 2) (hleft : ¬S.leftBeta ≤ 2) : ∃ (z : { i : Fin S.n // ¬CategoryTheory.Projective (S.fgObj i) }), CategoryTheory.Injective (S.fgObj ↑z) ∧ 3 ≤ S.nonprojectiveOutgoingAt ↑z

In particular, failure of the desired left-beta-two bound under the right-beta-two hypothesis produces an injective nonprojective boundary label with at least three nonprojective outgoing occurrences.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.betaAt_eq_natCard_nonprojective_minimalRightMiddle {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { i : Fin S.n // ¬CategoryTheory.Projective (S.fgObj i) }) : have B := S.minimalRightAlmostSplitAt ↑z; FiniteTauMatrix.betaAt S.finiteTauCategoryData.toFiniteRightTauCategoryData ↑z = Nat.card { i : B.index.obj // ¬CategoryTheory.Projective (S.fgObj (B.label i)) }

The ordinary betaAt count may be read directly from the skeleton's displayed minimal right almost-split decomposition, whose index is a finite category rather than a chosen finite ordinal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.leftBetaAt_eq_natCard_noninjective_rightMiddle {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x : { i : Fin S.n // ¬CategoryTheory.Injective (S.fgObj i) }) : have z := S.rightTranslationEquiv.symm x; have B := S.minimalRightAlmostSplitAt ↑z; S.leftBetaAt ↑x = Nat.card { i : B.index.obj // ¬CategoryTheory.Injective (S.fgObj (B.label i)) }

leftBetaAt counts the noninjective occurrences in the displayed right almost-split middle term whose left endpoint is the specified source. This is the occurrence-level form of translation invariance.

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

If one displayed summand of a nonprojective right almost-split middle term is projective, every different displayed summand is noninjective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMiddle_natCard_le_leftBetaAt_add_one_of_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (x : { i : Fin S.n // ¬CategoryTheory.Injective (S.fgObj i) }) (i : (S.minimalRightAlmostSplitAt ↑(S.rightTranslationEquiv.symm x)).index.obj) (hi : CategoryTheory.Projective (S.fgObj ((S.minimalRightAlmostSplitAt ↑(S.rightTranslationEquiv.symm x)).label i))) : Nat.card (S.minimalRightAlmostSplitAt ↑(S.rightTranslationEquiv.symm x)).index.obj ≤ S.leftBetaAt ↑x + 1

If the right almost-split middle term attached to a noninjective left endpoint contains a projective occurrence, all but that occurrence are counted by leftBetaAt.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMiddle_natCard_le_of_no_projectiveInjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] {bound : ℕ} (hbeta : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ bound) (hleft : S.leftBeta ≤ bound) (z : { i : Fin S.n // ¬CategoryTheory.Projective (S.fgObj i) }) (hnoPI : ∀ (i : (S.minimalRightAlmostSplitAt ↑z).index.obj), CategoryTheory.Projective (S.fgObj ((S.minimalRightAlmostSplitAt ↑z).label i)) → ¬CategoryTheory.Injective (S.fgObj ((S.minimalRightAlmostSplitAt ↑z).label i))) : Nat.card (S.minimalRightAlmostSplitAt ↑z).index.obj ≤ bound

If a nonprojective right almost-split middle term contains no projective-injective occurrence, its total arity is bounded by the maximum of the right and left beta bounds. With no projective occurrence, right beta counts the whole middle; with one, the boundary lemma makes left beta count the whole middle.