Arity bounds for literal string almost-split sequences

The Butler--Ringel boundary complexes have either one literal string in the middle or a binary biproduct of literal strings. This file records their displayed indecomposable decompositions and packages the resulting minimal right almost-split maps with the uniform bound two.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteRightModuleSingletonDecomposition {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) (C : Word P.relations) : CategoryTheory.FiniteIndecomposableDecomposition (C.finiteRightModule ⋯)

A literal finite string module, displayed as its one indecomposable summand.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteRightModuleBiprodDecomposition {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) (C D : Word P.relations) : CategoryTheory.FiniteIndecomposableDecomposition (C.finiteRightModule ⋯ ⊞ D.finiteRightModule ⋯)

A binary biproduct of literal finite string modules, displayed as its two indecomposable summands.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteRightModuleSingletonDecomposition_n {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) (C : Word P.relations) : (finiteRightModuleSingletonDecomposition P C).n = 1

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteRightModuleBiprodDecomposition_n {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) (C D : Word P.relations) : (finiteRightModuleBiprodDecomposition P C D).n = 2

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalFiniteRightAlmostSplitDecompositionBound {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 : P.ArrowPolarization) (V : DetectorIndex.FiniteIndecomposableSkeleton) {C rightResult : Word P.relations} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString P.relations (twoHookPath right left)) : CategoryTheory.RightAlmostSplitDecompositionBound (C.finiteRightModule ⋯) 2

A positive two-hook boundary square gives a minimal right almost-split map whose source has two displayed string summands.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.purePositiveLeftHookResultPeakFiniteRightAlmostSplitDecompositionBound {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 : P.ArrowPolarization) (V : DetectorIndex.FiniteIndecomposableSkeleton) {C : Word P.relations} (hpure : IsPurePositive ⋯ C) (left : C.LeftHookExtension) (hresultPeak : left.result.StartsOnPeak) : CategoryTheory.RightAlmostSplitDecompositionBound (C.finiteRightModule ⋯) 1

The unary pure-positive boundary complex gives a minimal right almost-split map with one displayed string summand.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.purePositiveLeftHookFiniteRightAlmostSplitDecompositionBound {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 : P.ArrowPolarization) (V : DetectorIndex.FiniteIndecomposableSkeleton) {C : Word P.relations} (hpure : IsPurePositive ⋯ C) (hstart : C.StartsOnPeak) (left : C.LeftHookExtension) : CategoryTheory.RightAlmostSplitDecompositionBound (C.finiteRightModule ⋯) 1

The usual pure-positive endpoint hypothesis specializes the unary result-peak witness.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.pureNegativeRightHookReverseFiniteRightAlmostSplitDecompositionBound {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 : P.ArrowPolarization) (V : DetectorIndex.FiniteIndecomposableSkeleton) {C D : Word P.relations} (hpure : IsPureNegative ⋯ C) (hend : C.EndsOnPeak) (right : C.HookExtension D) : CategoryTheory.RightAlmostSplitDecompositionBound (C.finiteRightModule ⋯) 1

The reversed pure-negative unary sequence has the same one-summand middle bound after returning its endpoint to the original word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.leftCohookDeletionRightHookFiniteRightAlmostSplitDecompositionBound {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 : P.ArrowPolarization) (V : DetectorIndex.FiniteIndecomposableSkeleton) {C D corner : Word P.relations} (deletion : C.LeftCohookDeletion D) (right : C.HookExtension corner) : CategoryTheory.RightAlmostSplitDecompositionBound (C.finiteRightModule ⋯) 2

A left cohook deletion and a right hook give a two-summand minimal right almost-split source at the original string.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookReverseFiniteRightAlmostSplitDecompositionBound {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 : P.ArrowPolarization) (V : DetectorIndex.FiniteIndecomposableSkeleton) {C D : Word P.relations} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) : CategoryTheory.RightAlmostSplitDecompositionBound (C.finiteRightModule ⋯) 2

A right cohook deletion and a left hook give the reversed two-summand minimal right almost-split source at the original string.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookDeletionFiniteRightAlmostSplitDecompositionBound {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 : P.ArrowPolarization) (V : DetectorIndex.FiniteIndecomposableSkeleton) {C L D : Word P.relations} (leftDeletion : L.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) : CategoryTheory.RightAlmostSplitDecompositionBound (C.finiteRightModule ⋯) 2

Two compatible cohook deletions give a two-summand minimal right almost-split source at the original string.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.exists_finiteRightAlmostSplitDecompositionBound_two_of_not_projective {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 : P.ArrowPolarization) (V : DetectorIndex.FiniteIndecomposableSkeleton) (C : Word P.relations) (hnonprojective : ¬CategoryTheory.Projective (C.finiteRightModule ⋯)) : Nonempty (CategoryTheory.RightAlmostSplitDecompositionBound (C.finiteRightModule ⋯) 2)

Every nonprojective literal finite string module admits a minimal right almost-split map whose source is displayed as at most two indecomposable literal string modules.