The Auslander--Reiten boundary at a projective-injective module

Let P be a non-simple indecomposable projective-injective right module. The two canonical boundary maps

• rad(P) ⟶ P, and
• P ⟶ P / soc(P)

are respectively minimal right and minimal left almost split. Their middle objects are indecomposable. Consequently each chosen almost-split decomposition incident with P has exactly one summand. This is the categorical form of the two-arrow boundary used in projective-injective socle rejection.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveInjectiveBoundaryRadical_isIndecomposableModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (p : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) (hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑(S.projectiveBoundaryRadical p.label)

The radical of a non-simple indecomposable projective-injective has a simple socle, hence is indecomposable.

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

The radical boundary object is categorically indecomposable.

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

A skeletal label for the indecomposable radical of the selected projective-injective.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveInjectiveBoundaryRadicalIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (p : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) (hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) : S.projectiveBoundaryRadical p.label ≅ S.fgObj (projectiveInjectiveBoundaryRadicalLabel p hpInjective hnotSimple)

The radical boundary object is isomorphic to its chosen skeletal representative.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientAmbientIso {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)) : P.primitiveProjectiveSocleQuotientFGObj p ≅ S.fgObj ↑(P.socleQuotientReplacementLabel p hpInjective hnotSimple)

Viewed again as an ambient A-module, the literal socle quotient is isomorphic to the ambient representative underlying its intrinsic quotient label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveLeftMiddleIso {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)) : (S.minimalLeftAlmostSplitAt p.label).middle ≅ P.primitiveProjectiveSocleQuotientFGObj p

The chosen minimal left almost-split middle term out of P is the literal quotient P / soc(P).

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveRightMiddleIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (p : S.ProjectiveLabel) : (S.minimalRightAlmostSplitAt p.label).middle ≅ S.projectiveBoundaryRadical p.label

The chosen minimal right almost-split middle term ending at P is rad(P).

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveLeftMiddleDecomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (p : S.ProjectiveLabel) : CategoryTheory.FiniteIndecomposableDecomposition (S.minimalLeftAlmostSplitAt p.label).middle

The displayed decomposition of the chosen left almost-split middle term, reindexed by a finite ordinal.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveRightMiddleDecomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (p : S.ProjectiveLabel) : CategoryTheory.FiniteIndecomposableDecomposition (S.minimalRightAlmostSplitAt p.label).middle

The displayed decomposition of the chosen right almost-split middle term, reindexed by a finite ordinal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveLeftMiddle_card_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) (p : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) (hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) : Fintype.card (S.minimalLeftAlmostSplitAt p.label).index.obj = 1

Exactly one indecomposable summand occurs in the chosen minimal left almost-split middle term out of P.

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

Exactly one indecomposable summand occurs in the chosen minimal right almost-split middle term ending at P.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveLeftMiddle_label_eq_replacement {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.minimalLeftAlmostSplitAt p.label).index.obj) : (S.minimalLeftAlmostSplitAt p.label).label t = ↑(P.socleQuotientReplacementLabel p hpInjective hnotSimple)

Every summand of the chosen left almost-split middle term out of P has the ambient label of P / soc(P).

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

Every summand of the chosen right almost-split middle term ending at P has the ambient label of rad(P).

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.hasIrreducibleMorphism_from_projectiveInjective_iff {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) : QuotientSubmoduleEquidistribution.HasIrreducibleMorphism (S.fgObj p.label) (S.fgObj x) ↔ x = ↑(P.socleQuotientReplacementLabel p hpInjective hnotSimple)

The only ambient indecomposable target of an irreducible map out of the selected projective-injective is its socle-quotient replacement.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.hasIrreducibleMorphism_to_projectiveInjective_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (p : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) (hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (x : Fin S.n) : QuotientSubmoduleEquidistribution.HasIrreducibleMorphism (S.fgObj x) (S.fgObj p.label) ↔ x = projectiveInjectiveBoundaryRadicalLabel p hpInjective hnotSimple

The only ambient indecomposable source of an irreducible map into the selected projective-injective is its radical.