Indecomposability of the finite-representable Nakayama kernel

For a minimal two-step presentation of an indecomposable endpoint, an idempotent of the associated Nakayama kernel or its complement factors through an injective. Minimality rules out injective retracts, so the kernel has only trivial idempotents and is indecomposable.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaKernel_idempotent_factorsThroughInjective_or_complement {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hMind : CategoryTheory.Indecomposable M) (a : nakayamaKernel hI P ⟶ nakayamaKernel hI P) (haa : CategoryTheory.CategoryStruct.comp a a = a) : Nonempty (InjectiveStable.FactorsThroughInjective a) ∨ Nonempty (InjectiveStable.FactorsThroughInjective (CategoryTheory.CategoryStruct.id (nakayamaKernel hI P) - a))

For an idempotent of the Nakayama kernel, either it or its complementary idempotent factors through an injective. Only indecomposability of the endpoint is needed: the induced endpoint endomorphism is idempotent modulo maps through projectives, and its local endomorphism ring decides which of it and its complement is stably zero.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaKernel_not_isZero {k : Type v} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hM : ¬CategoryTheory.Projective M) (hMind : CategoryTheory.Indecomposable M) : ¬CategoryTheory.Limits.IsZero (nakayamaKernel hI P)

The distinguished stable socle class prevents the Nakayama kernel from being zero.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaKernel_idempotent_eq_zero_or_one {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hMind : CategoryTheory.Indecomposable M) (a : nakayamaKernel hI P ⟶ nakayamaKernel hI P) (haa : CategoryTheory.CategoryStruct.comp a a = a) : a = 0 ∨ a = CategoryTheory.CategoryStruct.id (nakayamaKernel hI P)

Every idempotent endomorphism of the Nakayama kernel is zero or the identity.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaKernel_indecomposable {k : Type v} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hM : ¬CategoryTheory.Projective M) (hMind : CategoryTheory.Indecomposable M) : CategoryTheory.Indecomposable (nakayamaKernel hI P)

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

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.stableSocleClass_realization_isRightMinimal {k : Type v} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hM : ¬CategoryTheory.Projective M) (hMind : CategoryTheory.Indecomposable M) {E : FiniteDimensionalModuleCategory k} (i : nakayamaKernel hI P ⟶ E) (q : E ⟶ M) (zero : CategoryTheory.CategoryStruct.comp i q = 0) (hS : { X₁ := nakayamaKernel hI P, X₂ := E, X₃ := M, f := i, g := q, zero := zero }.ShortExact) (hqAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q) {N : FiniteDimensionalModuleCategory k} (m : N ⟶ M) (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.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nonempty_nakayamaKernelIso_kernel_of_minimalRightAlmostSplit {k : Type v} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hM : ¬CategoryTheory.Projective M) (hMind : CategoryTheory.Indecomposable M) {E : FiniteDimensionalModuleCategory k} (i : nakayamaKernel hI P ⟶ E) (q : E ⟶ M) (zero : CategoryTheory.CategoryStruct.comp i q = 0) (hS : { X₁ := nakayamaKernel hI P, X₂ := E, X₃ := M, f := i, g := q, zero := zero }.ShortExact) (hqAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q) {N : FiniteDimensionalModuleCategory k} (m : N ⟶ M) (hmAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit m) (hmMin : QuotientSubmoduleEquidistribution.IsRightMinimal m) : Nonempty (nakayamaKernel hI P ≅ CategoryTheory.Limits.kernel m)

The Nakayama kernel is the kernel of every minimal right almost-split map to the same endpoint.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nonempty_nakayamaKernelIso_kernel {k : Type v} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} [CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)] (P : TwoStepMinimalFiniteRepresentablePresentation hP M) (hM : ¬CategoryTheory.Projective M) (hMind : CategoryTheory.Indecomposable M) {N : FiniteDimensionalModuleCategory k} (m : N ⟶ M) (hmAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit m) (hmMin : QuotientSubmoduleEquidistribution.IsRightMinimal m) : Nonempty (nakayamaKernel hI P ≅ CategoryTheory.Limits.kernel m)

The Nakayama kernel is the kernel of a chosen minimal right almost-split map, without retaining the auxiliary realization of the distinguished stable socle class in the statement.