The concrete right-module Auslander transpose copresentation

For a two-step minimal projective presentation P₁ ⟶ P₀ ⟶ X, the Nakayama kernel ker(nu P₁ ⟶ nu P₀) embeds in the injective module nu P₁. This file packages the resulting short injective presentation and its pullback-natural quotient description of degree-one Ext.

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

The inclusion of the Nakayama kernel in nu P₁, packaged as an injective presentation.

@[reducible, inline]

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

The actual quotient of nu P₁ by the Nakayama kernel.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaCokernelπ {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 ⟶ P.nakayamaCokernel

The quotient map nu P₁ ⟶ C_P.

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

The Nakayama differential descends to an embedding C_P ⟶ nu P₀.

@[simp]

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaCokernelπ_comp_ι {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) : CategoryTheory.CategoryStruct.comp P.nakayamaCokernelπ P.nakayamaCokernelι = P.nakayamaDifferential

instance MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaCokernelι_mono {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) : CategoryTheory.Mono P.nakayamaCokernelι

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaKernel_isZero_of_injective_retract {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) {I : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.Injective I] (r : CategoryTheory.Retract I P.nakayamaKernel) : CategoryTheory.Limits.IsZero I

Minimality of the projective presentation rules out nonzero injective retracts of its Nakayama kernel.

@[reducible, inline]

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

The short exact sequence computing Ext¹(-,ker(nu d)).

@[reducible, inline]

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

Coboundaries in the short injective presentation.

@[simp]

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.mem_nakayamaExtPresentationRange_iff {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) (f : Y ⟶ P.nakayamaCokernel) : f ∈ P.nakayamaExtPresentationRange Y ↔ ∃ (a : Y ⟶ RightModule.projectiveNakayamaFGObj P.syzygyPresentation.p), CategoryTheory.CategoryStruct.comp a P.nakayamaCokernelπ = f

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaExtOneQuotientLinearEquiv {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (Y : FGModuleCat Bᵐᵒᵖ) : ((Y ⟶ P.nakayamaCokernel) ⧸ P.nakayamaExtPresentationRange Y) ≃ₗ[k] CategoryTheory.Abelian.Ext Y P.nakayamaKernel 1

The sound presentation quotient for Ext¹(Y,ker(nu d)).

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaPrecompQuotient {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) {Y Z : FGModuleCat Bᵐᵒᵖ} (g : Y ⟶ Z) : (Z ⟶ P.nakayamaCokernel) ⧸ P.nakayamaExtPresentationRange Z →ₗ[k] (Y ⟶ P.nakayamaCokernel) ⧸ P.nakayamaExtPresentationRange Y

Pullback on the Nakayama presentation quotient.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaExtOneQuotientLinearEquiv_symm_pullback {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) {Y Z : FGModuleCat Bᵐᵒᵖ} (g : Y ⟶ Z) (xi : CategoryTheory.Abelian.Ext Z P.nakayamaKernel 1) : (P.nakayamaExtOneQuotientLinearEquiv Y).symm ((CategoryTheory.Abelian.Ext.mk₀ g).comp xi ⋯) = (P.nakayamaPrecompQuotient g) ((P.nakayamaExtOneQuotientLinearEquiv Z).symm xi)

Inverse-form pullback naturality of the Ext quotient.