The Coxeter vector of a Nakayama kernel

This file proves the coordinate calculation in Ringel Section 2.4(4) for the right-module convention used by the manuscript. A finite projective is first decomposed into the selected indecomposable projectives. The two exact sequences attached to a length-one projective presentation then identify the Nakayama kernel vector with the Coxeter transform of the endpoint vector.

theorem MagnitudeConjecture.projectiveColumn_vecMul_inverseTranspose_mul {I : Type u} [Fintype I] [DecidableEq I] (C Cinv : Matrix I I ℤ) (hinv : Cinv * C = 1) (p : I) : Matrix.vecMul (C.col p) (Cinv.transpose * C) = C.row p

A Cartan column, viewed as a row vector, is carried to the corresponding Cartan row by Cinvᵀ C.

theorem MagnitudeConjecture.projectiveColumnSum_vecMul_inverseTranspose_mul {I : Type u} [Fintype I] [DecidableEq I] {J : Type u} [Fintype J] (C Cinv : Matrix I I ℤ) (hinv : Cinv * C = 1) (label : J → I) : Matrix.vecMul (∑ j : J, C.col (label j)) (Cinv.transpose * C) = ∑ j : J, C.row (label j)

The same Cartan identity summed over a finite family of projective summands.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveHomVectorFGObj {k B : Type u} [Field k] [Ring B] [Algebra k B] (S : FiniteIndecomposableSkeleton k B) (M : FGModuleCat Bᵐᵒᵖ) : S.ProjectiveLabel → ℤ

The projective-Hom dimension vector of an arbitrary finite module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveCohomVectorFGObj {k B : Type u} [Field k] [Ring B] [Algebra k B] (S : FiniteIndecomposableSkeleton k B) (M : FGModuleCat Bᵐᵒᵖ) : S.ProjectiveLabel → ℤ

The opposite Hom vector of an arbitrary finite module, evaluated on the selected indecomposable projectives.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveHomVectorFGObj_fgObj {k B : Type u} [Field k] [Ring B] [Algebra k B] (S : FiniteIndecomposableSkeleton k B) (x : Fin S.n) : S.projectiveHomVectorFGObj (S.fgObj x) = S.projectiveHomVector x

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveHomVectorFGObj_projectiveNakayama {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : S.projectiveHomVectorFGObj (projectiveNakayamaFGObj P) = S.projectiveCohomVectorFGObj P

Nakayama--Hom duality exchanges the two projective Hom vectors.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveHomVectorFGObj_iso {k B : Type u} [Field k] [Ring B] [Algebra k B] (S : FiniteIndecomposableSkeleton k B) {M N : FGModuleCat Bᵐᵒᵖ} (e : M ≅ N) : S.projectiveHomVectorFGObj M = S.projectiveHomVectorFGObj N

Projective-Hom vectors are invariant under isomorphism of their target module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveHomVectorFGObj_vecMul_inverseTranspose_mul {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : Matrix.vecMul (S.projectiveHomVectorFGObj P) (S.projectiveCartanInverse.transpose * S.projectiveCartanMatrix) = S.projectiveCohomVectorFGObj P

For every finite projective, multiplication by Cinvᵀ C exchanges its incoming and outgoing projective Hom vectors.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.regularHomDualMap_mono_of_hom_to_regular_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 : X ⟶ RightModule.rightRegularFGObj), q = 0) : CategoryTheory.Mono (RightModule.regularHomDualMap P.differential)

If the presented module has no map to the regular module, precomposition by the first projective differential is injective on regular-valued Hom.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaDifferential_epi_of_hom_to_regular_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 : X ⟶ RightModule.rightRegularFGObj), q = 0) : CategoryTheory.Epi P.nakayamaDifferential

The same regular-module vanishing makes the Nakayama differential epic.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.projectiveHomVectorFGObj_eq_sub_of_mono_differential {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (S : RightModule.FiniteIndecomposableSkeleton k B) (P : TwoStepMinimalProjectivePresentation X) (hmono : CategoryTheory.Mono P.differential) : S.projectiveHomVectorFGObj X = S.projectiveHomVectorFGObj P.augmentation.p - S.projectiveHomVectorFGObj P.syzygyPresentation.p

A monic first differential gives the dimension-vector equation for the projective presentation.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaKernel_projectiveHomVector_eq_sub {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} (S : RightModule.FiniteIndecomposableSkeleton k B) (P : TwoStepMinimalProjectivePresentation X) (hzero : ∀ (q : X ⟶ RightModule.rightRegularFGObj), q = 0) : S.projectiveHomVectorFGObj P.nakayamaKernel = S.projectiveHomVectorFGObj (RightModule.projectiveNakayamaFGObj P.syzygyPresentation.p) - S.projectiveHomVectorFGObj (RightModule.projectiveNakayamaFGObj P.augmentation.p)

The regular-module vanishing gives the exact Nakayama-kernel vector equation.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.nakayamaKernel_projectiveHomVector_eq_coxeter {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {X : FGModuleCat Bᵐᵒᵖ} [IsAlgClosed k] (S : RightModule.FiniteIndecomposableSkeleton k B) (H : S.HasAcyclicNonzeroNonisomorphisms) (P : TwoStepMinimalProjectivePresentation X) (hmono : CategoryTheory.Mono P.differential) (hzero : ∀ (q : X ⟶ RightModule.rightRegularFGObj), q = 0) : S.projectiveHomVectorFGObj P.nakayamaKernel = Matrix.vecMul (S.projectiveHomVectorFGObj X) (CartanCoordinate.coxeterMatrix S.projectiveCartanMatrix S.projectiveCartanInverse)

Ringel Section 2.4(4) in the manuscript's row-vector convention: under the length-one and regular-Hom vanishings, the Nakayama kernel vector is the Coxeter transform of the presented module vector.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSourceSupportObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : SupportSubcategory (S.minimalRightAlmostSplitAt ↑z).middle

The translated source of the chosen sequence, as an object of the full middle-support subcategory.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportSourceKernelMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : rightSequenceSourceSupportObj z ⟶ rightSequenceMiddleSupportObj z

The chosen kernel inclusion inside the full middle-support subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportSourceKernelMap_comp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : CategoryTheory.CategoryStruct.comp (rightSequenceSupportSourceKernelMap z) (rightSequenceSupportMap z) = 0

The supported source map followed by the supported almost-split map is zero.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportSourceKernelIsLimit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (rightSequenceSupportSourceKernelMap z) ⋯)

The supported translated source is the actual kernel of the supported almost-split map.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportKernelIsoSource {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) }) : (P.rightSequenceMiddleSupportSkeleton hA z).fgObj (P.rightSequenceSupportKernelLabel hA z) ≅ (P.rightSequenceMiddleSupportSkeleton hA z).fgObj (P.rightSequenceSupportSourceLabel hA z)

The skeleton representative of the supported translated source is the selected representative of the support almost-split kernel.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportKernel_coxeter_translate {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)) : let T := P.rightSequenceMiddleSupportSkeleton hA z; T.projectiveHomVector (P.rightSequenceSupportKernelLabel hA z) = Matrix.vecMul (T.projectiveHomVector (P.rightSequenceSupportTargetLabel hA z)) (CartanCoordinate.coxeterMatrix T.projectiveCartanMatrix T.projectiveCartanInverse)

The selected literal support kernel has the Coxeter transform of the support endpoint's projective-Hom vector.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportSource_coxeter_translate {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) }) : let T := P.rightSequenceMiddleSupportSkeleton hA z; T.projectiveHomVector (P.rightSequenceSupportSourceLabel hA z) = Matrix.vecMul (T.projectiveHomVector (P.rightSequenceSupportTargetLabel hA z)) (CartanCoordinate.coxeterMatrix T.projectiveCartanMatrix T.projectiveCartanInverse)

Ringel Section 2.4(4) for the literal middle-support quotient: the projective-Hom vector of the translated source is the Coxeter transform of the endpoint vector.