The finite-projective Nakayama kernel criterion

For a finitely generated projective right module P, this file constructs the concrete Nakayama object

nu P = D Hom_B(P, B).

A finite dual frame proves that the canonical map P -> Hom_B(D(B), nu P) is injective and natural in P. Consequently, if Hom_B(D(B), ker (nu d)) = 0, then a morphism d between finitely generated projectives is monic. Applied to the first differential in a minimal projective presentation, this is Ringel's projective-dimension-one argument.

Only the finite-frame construction pattern is adapted from the equidistribution formalization. The latter's Auslander-transpose and OP layers are neither imported nor copied.

structure MagnitudeConjecture.RightModule.FiniteProjectiveFrame (R P : Type u) [Semiring R] [AddCommMonoid P] [Module R P] : Type u

A finite dual frame for a finitely generated projective module.

• n : ℕ
• p : Fin self.n → P
• phi : Fin self.n → P →ₗ[R] R
• total (x : P) : ∑ i : Fin self.n, (self.phi i) x • self.p i = x

noncomputable def MagnitudeConjecture.RightModule.finiteProjectiveFrame (R P : Type u) [Semiring R] [AddCommMonoid P] [Module R P] [Module.Finite R P] [Module.Projective R P] : FiniteProjectiveFrame R P

A finite dual frame obtained from a finite free splitting.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.regularHomDualCarrier {B : Type u} [Ring B] (P : FGModuleCat Bᵐᵒᵖ) : Type u

The regular Hom-dual of a finite right module, with its natural left B-action.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.regularHomDualFGObj {B : Type u} [Ring B] (k : Type u) [Field k] [Algebra k B] [FiniteDimensional k B] (P : FGModuleCat Bᵐᵒᵖ) : FGModuleCat B

The regular Hom-dual bundled as a finitely generated left module.

def MagnitudeConjecture.RightModule.regularHomDualMap {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] {P Q : FGModuleCat Bᵐᵒᵖ} (d : P ⟶ Q) : regularHomDualFGObj k Q ⟶ regularHomDualFGObj k P

Precomposition is the contravariant map on regular Hom-duals.

def MagnitudeConjecture.RightModule.regularHomEvaluation {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P : FGModuleCat Bᵐᵒᵖ) (p : ↑P) : regularHomDualFGObj k P ⟶ leftRegularFGObj

Evaluation at p, as a left-module map from the regular Hom-dual to the left regular module.

@[simp]

theorem MagnitudeConjecture.RightModule.regularHomDualMap_comp_evaluation {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] {P Q : FGModuleCat Bᵐᵒᵖ} (d : P ⟶ Q) (p : ↑P) : CategoryTheory.CategoryStruct.comp (regularHomDualMap d) (regularHomEvaluation P p) = regularHomEvaluation Q ((ModuleCat.Hom.hom d.hom) p)

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.projectiveNakayamaFGObj {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P : FGModuleCat Bᵐᵒᵖ) : FGModuleCat Bᵐᵒᵖ

The concrete Nakayama object D Hom_B(P,B).

def MagnitudeConjecture.RightModule.projectiveNakayamaMap {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] {P Q : FGModuleCat Bᵐᵒᵖ} (d : P ⟶ Q) : projectiveNakayamaFGObj P ⟶ projectiveNakayamaFGObj Q

The covariant Nakayama map induced by a morphism of right modules.

def MagnitudeConjecture.RightModule.nakayamaUnitElement {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P : FGModuleCat Bᵐᵒᵖ) (p : ↑P) : injectiveCogeneratorFGObj ⟶ projectiveNakayamaFGObj P

An element p : P determines the corresponding morphism D(B) -> nu P.

@[simp]

theorem MagnitudeConjecture.RightModule.nakayamaUnitElement_naturality {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] {P Q : FGModuleCat Bᵐᵒᵖ} (d : P ⟶ Q) (p : ↑P) : CategoryTheory.CategoryStruct.comp (nakayamaUnitElement P p) (projectiveNakayamaMap d) = nakayamaUnitElement Q ((ModuleCat.Hom.hom d.hom) p)

@[simp]

theorem MagnitudeConjecture.RightModule.nakayamaUnitElement_zero {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P : FGModuleCat Bᵐᵒᵖ) : nakayamaUnitElement P 0 = 0

theorem MagnitudeConjecture.RightModule.nakayamaUnitElement_injective {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P : FGModuleCat Bᵐᵒᵖ) (hP : CategoryTheory.Projective P) : Function.Injective (nakayamaUnitElement P)

The element-to-Nakayama-Hom map is injective on every finite projective right module.

theorem MagnitudeConjecture.RightModule.mono_of_hom_from_injectiveCogenerator_to_nakayamaKernel_eq_zero {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {P Q : FGModuleCat Bᵐᵒᵖ} (d : P ⟶ Q) (hP : CategoryTheory.Projective P) (hzero : ∀ (q : injectiveCogeneratorFGObj ⟶ CategoryTheory.Limits.kernel (projectiveNakayamaMap d)), q = 0) : CategoryTheory.Mono d

Vanishing of maps from the standard injective cogenerator to the Nakayama kernel forces the original projective morphism to be monic.

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaDifferential {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) : RightModule.projectiveNakayamaFGObj P.syzygyPresentation.p ⟶ RightModule.projectiveNakayamaFGObj P.augmentation.p

Applying the concrete Nakayama construction to the first differential of a two-step minimal projective presentation.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaKernel {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) : FGModuleCat Bᵐᵒᵖ

Ringel's Nakayama kernel attached to the chosen minimal presentation.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.hasProjectiveDimensionLE_one_of_hom_from_injectiveCogenerator_to_nakayamaKernel_eq_zero {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (hzero : ∀ (q : RightModule.injectiveCogeneratorFGObj ⟶ P.nakayamaKernel), q = 0) : CategoryTheory.HasProjectiveDimensionLE X 1

The literal Nakayama-kernel vanishing implies projective dimension at most one.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.hasProjectiveDimensionLE_one_of_nakayamaKernelIso_of_hom_eq_zero {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) {T : FGModuleCat Bᵐᵒᵖ} (e : T ≅ P.nakayamaKernel) (hzero : ∀ (q : RightModule.injectiveCogeneratorFGObj ⟶ T), q = 0) : CategoryTheory.HasProjectiveDimensionLE X 1

It is enough to identify an external module with the Nakayama kernel and prove the cogenerator vanishing for that module. This is the interface used to connect the chosen almost-split kernel to Ringel's construction.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportEndpointFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : FinitelyGeneratedCategory (P.SupportAlgebra (S.minimalRightAlmostSplitAt ↑z).middle)

The literal support-algebra endpoint in the chosen right almost-split sequence.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportKernelFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : FinitelyGeneratedCategory (P.SupportAlgebra (S.minimalRightAlmostSplitAt ↑z).middle)

The literal selected representative of the support almost-split kernel.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportEndpoint_hasProjectiveDimensionLE_one_of_nakayamaKernelIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (Q : TwoStepMinimalProjectivePresentation (P.rightSequenceSupportEndpointFGObj hA z)) (e : P.rightSequenceSupportKernelFGObj hA z ≅ Q.nakayamaKernel) : CategoryTheory.HasProjectiveDimensionLE (P.rightSequenceSupportEndpointFGObj hA z) 1

Once the standard DTr identification is supplied for a minimal presentation of the support endpoint, the already established directed vanishing proves Ringel's projective-dimension-one conclusion.