The exceptional Auslander--Reiten mesh under socle rejection

Let P be a non-simple indecomposable projective-injective right module and let Q = P / soc(P). This file identifies the ambient Auslander--Reiten sequence ending at Q: the endpoint Q is nonprojective and its Auslander--Reiten translate is rad(P). Thus the canonical kernel of the chosen right almost-split map ending at Q is isomorphic to the literal radical boundary object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientReplacementLabel_not_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) (hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) : ¬CategoryTheory.Projective (S.fgObj ↑(P.socleQuotientReplacementLabel p hpInjective hnotSimple))

Although P / soc(P) becomes projective after socle rejection, it is not projective as an ambient A-module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientReplacementNonprojectiveLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) (hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }

The replacement label bundled with its ambient nonprojectivity.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_projectiveInjectiveMiddleOccurrence_at_socleQuotient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) (hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) : ∃ (t : (S.minimalRightAlmostSplitAt ↑(P.socleQuotientReplacementNonprojectiveLabel p hpInjective hnotSimple)).index.obj), (S.minimalRightAlmostSplitAt ↑(P.socleQuotientReplacementNonprojectiveLabel p hpInjective hnotSimple)).label t = p.label

The selected projective-injective occurs in the middle term of the ambient right almost-split sequence ending at P / soc(P).

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.card_projectiveInjectiveMiddleOccurrence_at_socleQuotient_eq_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) [IsAlgClosed k] (p : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) (hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) : Nat.card (S.almostSplitSkeleton.RightAROccurrence (S.minimalRightAlmostSplitAt ↑(P.socleQuotientReplacementNonprojectiveLabel p hpInjective hnotSimple)) p.label) = 1

Over an algebraically closed field, the selected projective-injective occurs exactly once in the ambient right almost-split middle term ending at P / soc(P). This is the single incoming boundary arrow removed from that mesh by socle rejection.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightTranslationLabel_socleQuotientReplacement {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) (hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) : S.rightTranslationLabel (P.socleQuotientReplacementNonprojectiveLabel p hpInjective hnotSimple) = projectiveInjectiveBoundaryRadicalLabel p hpInjective hnotSimple

The ambient Auslander--Reiten translate of P / soc(P) is the chosen skeletal representative of rad(P).

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientReplacementKernelIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) (hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) : CategoryTheory.Limits.kernel (S.minimalRightAlmostSplitAt ↑(P.socleQuotientReplacementNonprojectiveLabel p hpInjective hnotSimple)).map ≅ S.projectiveBoundaryRadical p.label

The kernel of the chosen ambient right almost-split map ending at P / soc(P) is the literal radical rad(P).