Indecomposability of the Nakayama kernel

For a minimal two-step projective presentation of a Schur object, every endomorphism of the associated Nakayama kernel is scalar modulo a morphism factoring through an injective. Minimality rules out injective summands, so idempotents of the kernel are trivial.

structure MagnitudeConjecture.FactorsThroughInjective {B : Type u} [Ring B] {U V : FGModuleCat Bᵐᵒᵖ} (f : U ⟶ V) : Type (u + 1)

A morphism of finite modules factors through an injective finite module.

• middle : FGModuleCat Bᵐᵒᵖ
• injective : CategoryTheory.Injective self.middle
• left : U ⟶ self.middle
• right : self.middle ⟶ V
• fac : CategoryTheory.CategoryStruct.comp self.left self.right = f

theorem MagnitudeConjecture.idempotent_eq_zero_of_factorsThroughInjective {B : Type u} [Ring B] {T : FGModuleCat Bᵐᵒᵖ} (a : T ⟶ T) (haa : CategoryTheory.CategoryStruct.comp a a = a) (hfac : Nonempty (FactorsThroughInjective a)) (hzero : ∀ {I : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.Injective I] (a : CategoryTheory.Retract I T), CategoryTheory.Limits.IsZero I) : a = 0

An idempotent which factors through an injective has injective image. If every injective retract of its source is zero, the idempotent vanishes.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaKernel_endomorphism_factorsThroughInjective_sub_smul_id {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] [IsAlgClosed k] {X : FGModuleCat Bᵐᵒᵖ} (P : TwoStepMinimalProjectivePresentation X) (hscalar : ∀ (r : X ⟶ X), ∃ (c : k), c • CategoryTheory.CategoryStruct.id X = r) (a : P.nakayamaKernel ⟶ P.nakayamaKernel) : ∃ (c : k), Nonempty (FactorsThroughInjective (a - c • CategoryTheory.CategoryStruct.id P.nakayamaKernel))

At a scalar-endomorphism endpoint, every endomorphism of the Nakayama kernel differs from a scalar by a map through an injective.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaKernel_nontrivial {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] [IsAlgClosed k] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (hX : ¬CategoryTheory.Projective X) (hXind : CategoryTheory.Indecomposable X) : Nontrivial ↑P.nakayamaKernel

The Nakayama kernel of a minimal presentation of a nonprojective indecomposable object is nonzero.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaKernel_isIndecomposableModule {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] [IsAlgClosed k] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (hX : ¬CategoryTheory.Projective X) (hXind : CategoryTheory.Indecomposable X) (hscalar : ∀ (r : X ⟶ X), ∃ (c : k), c • CategoryTheory.CategoryStruct.id X = r) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Bᵐᵒᵖ ↑P.nakayamaKernel

The Nakayama kernel of a minimal presentation of a nonprojective Schur object is indecomposable.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.stableSocleClass_realization_isRightMinimal {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] [IsAlgClosed k] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (hTind : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Bᵐᵒᵖ ↑P.nakayamaKernel) {E : FGModuleCat Bᵐᵒᵖ} (i : P.nakayamaKernel ⟶ E) (q : E ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i q = 0) (hS : { X₁ := P.nakayamaKernel, X₂ := E, X₃ := X, f := i, g := q, zero := zero }.ShortExact) (hqAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q) {M : FGModuleCat Bᵐᵒᵖ} (m : M ⟶ X) (hmAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit m) (hmMin : QuotientSubmoduleEquidistribution.IsRightMinimal m) : QuotientSubmoduleEquidistribution.IsRightMinimal q

A right almost-split realization with indecomposable Nakayama kernel is already right minimal, by comparison with any minimal right almost-split map to the same endpoint.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nonempty_nakayamaKernelIso_kernel_of_minimalRightAlmostSplit {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] [IsAlgClosed k] {X : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.HasExt (FGModuleCat Bᵐᵒᵖ)] (P : TwoStepMinimalProjectivePresentation X) (hTind : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Bᵐᵒᵖ ↑P.nakayamaKernel) {E : FGModuleCat Bᵐᵒᵖ} (i : P.nakayamaKernel ⟶ E) (q : E ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i q = 0) (hS : { X₁ := P.nakayamaKernel, X₂ := E, X₃ := X, f := i, g := q, zero := zero }.ShortExact) (hqAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q) {M : FGModuleCat Bᵐᵒᵖ} (m : M ⟶ X) (hmAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit m) (hmMin : QuotientSubmoduleEquidistribution.IsRightMinimal m) : Nonempty (P.nakayamaKernel ≅ CategoryTheory.Limits.kernel m)

The kernel of a stable-socle realization is the kernel of every minimal right almost-split map to the same endpoint.