Almost-split sequences ending in string-arrow cokernels

For a displayed arrow a : x ⟶ y, the Auslander--Reiten translate of V(a) is the kernel of νP(x) ⟶ νP(y). The source projective P(x) is indecomposable, hence its Nakayama image is an indecomposable injective with simple socle. The nonzero Nakayama kernel therefore also has simple socle. This is the homological input for proving that the almost-split middle term of V(a) is indecomposable.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowAlmostSplitAlgebraFiniteDimensional {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : FiniteDimensional k P.quotientCategoryAlgebra

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowAlmostSplitAlgebraOppositeIsNoetherian {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : IsNoetherianRing P.quotientCategoryAlgebraᵐᵒᵖ

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowAlmostSplitEnoughProjectives {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : CategoryTheory.EnoughProjectives (FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ)

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelNakayamaKernel_moduleSocle_isSimple {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : IsSimpleModule P.quotientCategoryAlgebraᵐᵒᵖ ↥(moduleSocle P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.arrowCokernelTwoStepMinimalProjectivePresentation a).nakayamaKernel)

The Nakayama kernel associated to P(x) ⟶ P(y) ⟶ V(a) has simple socle.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelNakayamaKernel_isIndecomposableModule {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.arrowCokernelTwoStepMinimalProjectivePresentation a).nakayamaKernel

The Nakayama kernel associated to a displayed arrow is indecomposable as a module.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelSkeletonIndex {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) {x y : Q} (a : x ⟶ y) : Fin S.n

The chosen complete-skeleton label of an arrow cokernel.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelSkeletonIso {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) {x y : Q} (a : x ⟶ y) : P.arrowCokernelFGObj a ≅ S.fgObj (P.arrowCokernelSkeletonIndex S a)

The literal arrow cokernel represented by its selected skeleton label.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelNonprojectiveLabel {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) {x y : Q} (a : x ⟶ y) : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }

The selected nonprojective skeleton label represented by a displayed arrow cokernel.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelRightTranslation_moduleSocle_isSimple {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) {x y : Q} (a : x ⟶ y) : IsSimpleModule P.quotientCategoryAlgebraᵐᵒᵖ ↥(moduleSocle P.quotientCategoryAlgebraᵐᵒᵖ ↑(S.fgObj (S.rightTranslationLabel (P.arrowCokernelNonprojectiveLabel S a))))

The selected Auslander--Reiten source ending at an arrow cokernel has simple socle.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.exists_arrowCokernelRightSequenceLeftComponent_mono {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) {x y : Q} (a : x ⟶ y) : ∃ (i : (S.minimalRightAlmostSplitAt ↑(P.arrowCokernelNonprojectiveLabel S a)).index.obj), CategoryTheory.Mono (QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalLeftAlmostSplitDecomposition.component S.almostSplitSkeleton (S.rightSequenceLeftDecomposition (P.arrowCokernelNonprojectiveLabel S a)) i)

Some displayed left component of the chosen Auslander--Reiten sequence ending at an arrow cokernel is monic.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelRightMiddleIndex_unique {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) {x y : Q} (a : x ⟶ y) : ∃ (i : (S.minimalRightAlmostSplitAt ↑(P.arrowCokernelNonprojectiveLabel S a)).index.obj), ∀ (j : (S.minimalRightAlmostSplitAt ↑(P.arrowCokernelNonprojectiveLabel S a)).index.obj), j = i

The middle term of the chosen right almost-split sequence ending at an arrow cokernel has a unique displayed indecomposable summand.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelRightMiddleDecomposition {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) {x y : Q} (a : x ⟶ y) : CategoryTheory.FiniteIndecomposableDecomposition (S.minimalRightAlmostSplitAt ↑(P.arrowCokernelNonprojectiveLabel S a)).middle

The chosen right almost-split middle term ending at an arrow cokernel, reindexed as a Fin-indexed indecomposable decomposition.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.rightMiddleArity_arrowCokernelNonprojectiveLabel {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) {x y : Q} (a : x ⟶ y) : FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData ↑(P.arrowCokernelNonprojectiveLabel S a) = 1

Every displayed arrow contributes a one-summand right Auslander--Reiten middle term.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.displayedArrowOneMiddleMesh {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (a : DisplayedArrow Q) : FiniteTauMatrix.OneMiddleMesh S.finiteTauCategoryData

The one-middle mesh selected by the Butler--Ringel arrow cokernel.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.displayedArrowOneMiddleMesh_injective {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : Function.Injective (P.displayedArrowOneMiddleMesh S)

Distinct displayed arrows select distinct one-middle meshes. This is the injective half of the Butler--Ringel correspondence, expressed on the chosen finite indecomposable skeleton.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.natCard_displayedArrow_le_oneMiddleMeshCount {k A Q : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : Nat.card (DisplayedArrow Q) ≤ FiniteTauMatrix.oneMiddleMeshCount S.finiteTauCategoryData

The displayed-arrow family gives a lower bound for the number of one-middle meshes.