The Nakayama kernel is the support Auslander--Reiten translate

At a literal middle-support endpoint, directedness makes the endomorphism ring scalar. The stable-socle realization of the Nakayama kernel is therefore minimal right almost split, so uniqueness identifies its kernel with the selected support almost-split kernel. This discharges the DTr identification used in Ringel's projective-dimension-one argument.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightTranslation_strictly_precedes {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : S.rightTranslationLabel z < ↑z

Auslander--Reiten translation points strictly backwards in the directed order.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.hom_to_rightTranslation_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (f : S.fgObj ↑z ⟶ S.fgObj (S.rightTranslationLabel z)) : f = 0

Directedness rules out every morphism from a nonprojective endpoint to its Auslander--Reiten translate.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightTranslationIso_nakayamaKernel_of_targetIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) {X : FGModuleCat Aᵐᵒᵖ} (e : X ≅ S.fgObj ↑z) (Q : TwoStepMinimalProjectivePresentation X) (hTind : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑Q.nakayamaKernel) : Nonempty (S.fgObj (S.rightTranslationLabel z) ≅ Q.nakayamaKernel)

If the Nakayama kernel of a minimal presentation is indecomposable, it is the chosen Auslander--Reiten translate of any selected skeleton endpoint isomorphic to the presented module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightTranslationIso_nakayamaKernel_of_isIndecomposableModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (Q : TwoStepMinimalProjectivePresentation (S.fgObj ↑z)) (hTind : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑Q.nakayamaKernel) : Nonempty (S.fgObj (S.rightTranslationLabel z) ≅ Q.nakayamaKernel)

If the Nakayama kernel of a minimal presentation is indecomposable, it is the chosen Auslander--Reiten translate of the endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightTranslationIso_nakayamaKernel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (Q : TwoStepMinimalProjectivePresentation (S.fgObj ↑z)) : Nonempty (S.fgObj (S.rightTranslationLabel z) ≅ Q.nakayamaKernel)

For any nonprojective vertex of a directed finite module skeleton, the Nakayama kernel of a minimal two-step presentation is its chosen Auslander--Reiten translate.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_nonzero_hom_inverseTranslation_of_extOne_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] [CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)] (H : S.HasAcyclicNonzeroNonisomorphisms) (x : { x : Fin S.n // ¬CategoryTheory.Injective (S.fgObj x) }) (Y : FGModuleCat Aᵐᵒᵖ) (xi : CategoryTheory.Abelian.Ext Y (S.fgObj ↑x) 1) (hxi : xi ≠ 0) : ∃ (f : S.fgObj ↑(S.rightTranslationEquiv.symm x) ⟶ Y), f ≠ 0

A nonzero degree-one extension into a noninjective selected module gives a nonzero ordinary morphism from its inverse Auslander--Reiten translate. This is the nonvanishing direction of stable Auslander--Reiten duality used by the source-marker sign test.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.extOne_self_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] [CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)] (H : S.HasAcyclicNonzeroNonisomorphisms) (x : Fin S.n) (xi : CategoryTheory.Abelian.Ext (S.fgObj x) (S.fgObj x) 1) : xi = 0

Every selected indecomposable over a directed algebra has vanishing degree-one self-Ext. For a noninjective object, rotate to the corresponding right Auslander--Reiten sequence and use stable Hom--Ext duality together with the absence of maps from its endpoint back to its translate.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportKernelIso_nakayamaKernel {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] (hA : IsRepresentationFinite k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (Q : TwoStepMinimalProjectivePresentation (P.rightSequenceSupportEndpointFGObj hA z)) : Nonempty (P.rightSequenceSupportKernelFGObj hA z ≅ Q.nakayamaKernel)

For a minimal two-step presentation of a literal middle-support endpoint, its Nakayama kernel is the kernel selected by the transported almost-split sequence.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportEndpoint_hasProjectiveDimensionLE_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] (hA : IsRepresentationFinite k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (Q : TwoStepMinimalProjectivePresentation (P.rightSequenceSupportEndpointFGObj hA z)) : CategoryTheory.HasProjectiveDimensionLE (P.rightSequenceSupportEndpointFGObj hA z) 1

Ringel's endpoint projective-dimension bound in the literal support quotient, with the Nakayama/AR identification discharged internally.