Almost-split string boundary complexes

The positive, mixed, and negative Butler--Ringel boundary complexes are short exact with irreducible differentials. A complete finite indecomposable skeleton therefore identifies each one with the almost-split sequence at its literal string endpoint.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.finiteStringSkeletonLabel {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 : StringWord.DetectorIndex.FiniteIndecomposableSkeleton) (C : StringWord.Word P.relations) : Fin V.n

The label of the fixed finite indecomposable skeleton belonging to a literal string word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.finiteStringSkeletonIso {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 : StringWord.DetectorIndex.FiniteIndecomposableSkeleton) (C : StringWord.Word P.relations) : C.finiteRightModule ⋯ ≅ V.obj (P.finiteStringSkeletonLabel S V C)

A literal string module is isomorphic to the selected skeleton object with the same inversion-class detector index.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.finiteStringBoundaryEnoughProjectives {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 (CoveringHom.FiniteDimensionalModuleCategory k)

Admissibility makes the contravariant finite string-module category have enough projectives.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.twoHookMaximalFiniteShortComplex_isRightAlmostSplit {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 : StringWord.DetectorIndex.FiniteIndecomposableSkeleton) {C rightResult : StringWord.Word P.relations} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : StringWord.IsString P.relations (StringWord.Word.twoHookPath right left)) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (StringWord.Word.twoHookMaximalFiniteShortComplex right left hpath ⋯).g

The positive two-hook complex is the right almost-split sequence ending at its base string.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.purePositiveLeftHookResultPeakFiniteShortComplex_isRightAlmostSplit {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 : StringWord.DetectorIndex.FiniteIndecomposableSkeleton) {C : StringWord.Word P.relations} (hpure : StringWord.Word.IsPurePositive ⋯ C) (left : C.LeftHookExtension) (hresultPeak : left.result.StartsOnPeak) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (StringWord.Word.LeftHookExtension.purePositiveResultPeakFiniteShortComplex ⋯ hpure left ⋯ ⋯).g

A pure-positive left-hook projection is right almost split whenever its hooked result is maximal at the opposite endpoint.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.purePositiveLeftHookFiniteShortComplex_isRightAlmostSplit {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 : StringWord.DetectorIndex.FiniteIndecomposableSkeleton) {C : StringWord.Word P.relations} (hpure : StringWord.Word.IsPurePositive ⋯ C) (hstart : C.StartsOnPeak) (left : C.LeftHookExtension) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (StringWord.Word.LeftHookExtension.purePositiveFiniteShortComplex ⋯ hpure ⋯ left ⋯).g

A pure-positive string which is maximal at the right endpoint and has a left hook has a one-middle right almost-split sequence.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.pureNegativeRightHookReverseFiniteMap_isRightAlmostSplit {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 : StringWord.DetectorIndex.FiniteIndecomposableSkeleton) {C D : StringWord.Word P.relations} (hpure : StringWord.Word.IsPureNegative ⋯ C) (hend : C.EndsOnPeak) (right : C.HookExtension D) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (CategoryTheory.CategoryStruct.comp (StringWord.Word.LeftHookExtension.purePositiveFiniteShortComplex ⋯ hpure ⋯ right.toReverseLeftHook ⋯).g C.finiteReverseRightModuleIso.symm.hom)

The reversed pure-negative form: a pure-negative string maximal at its left endpoint with a right hook has a one-middle right almost-split map.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.leftCohookDeletionRightHookMaximalFiniteShortComplex_isRightAlmostSplit {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 : StringWord.DetectorIndex.FiniteIndecomposableSkeleton) {C D corner : StringWord.Word P.relations} (deletion : C.LeftCohookDeletion D) (right : C.HookExtension corner) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (StringWord.Word.leftCohookDeletionRightHookMaximalFiniteShortComplex deletion right ⋯).g

A left cohook deletion and a right hook give the right almost-split sequence ending at the original string.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.rightCohookDeletionLeftHookReverseTargetIso {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 : StringWord.Word P.relations} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) : (StringWord.Word.leftCohookDeletionRightHookMaximalFiniteShortComplex deletion.toReverseLeftCohookDeletion left.hook ⋯).X₃ ≅ C.finiteRightModule ⋯

The target of the reversed asymmetric finite complex, returned to the original literal string module.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.rightCohookDeletionLeftHookReverseMaximalFiniteShortComplex_isRightAlmostSplit {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 : StringWord.DetectorIndex.FiniteIndecomposableSkeleton) {C D : StringWord.Word P.relations} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (CategoryTheory.CategoryStruct.comp (StringWord.Word.leftCohookDeletionRightHookMaximalFiniteShortComplex deletion.toReverseLeftCohookDeletion left.hook ⋯).g (P.rightCohookDeletionLeftHookReverseTargetIso deletion left).hom)

A right cohook deletion and a left hook give the opposite asymmetric right almost-split sequence. The existing mixed complex is constructed on the reversed word; the canonical reversal isomorphism returns its endpoint to the original literal string module.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.doubleCohookDeletionMaximalFiniteShortComplex_isRightAlmostSplit {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 : StringWord.DetectorIndex.FiniteIndecomposableSkeleton) {C L D : StringWord.Word P.relations} (leftDeletion : L.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (StringWord.Word.doubleCohookDeletionMaximalFiniteShortComplex leftDeletion rightDeletion ⋯).g

Two cohook deletions give the right almost-split sequence ending at the original string.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.exists_doubleCohookDeletion_rightAlmostSplit_of_steps_add_le {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 : StringWord.DetectorIndex.FiniteIndecomposableSkeleton) {C L D : StringWord.Word P.relations} (leftDeletion : C.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) (hnonoverlap : leftDeletion.steps + rightDeletion.steps ≤ StringWord.Word.length P.relations C) : ∃ (E : StringWord.Word P.relations) (leftAfter : L.LeftCohookDeletion E), QuotientSubmoduleEquidistribution.IsRightAlmostSplit (StringWord.Word.doubleCohookDeletionMaximalFiniteShortComplex leftAfter rightDeletion ⋯).g

Nonoverlapping cohook deletions at the two endpoints can be ordered into the double-cohook right almost-split sequence ending at the original word.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.doubleCohookDeletion_rightAlmostSplit_or_overlap {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 : StringWord.DetectorIndex.FiniteIndecomposableSkeleton) {C L D : StringWord.Word P.relations} (leftDeletion : C.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) : (∃ (E : StringWord.Word P.relations) (leftAfter : L.LeftCohookDeletion E), QuotientSubmoduleEquidistribution.IsRightAlmostSplit (StringWord.Word.doubleCohookDeletionMaximalFiniteShortComplex leftAfter rightDeletion ⋯).g) ∨ leftDeletion.steps + rightDeletion.steps = StringWord.Word.length P.relations C + 2 ∧ StringWord.signedPathSigns C.path = List.replicate rightDeletion.cohook.tail.steps false ++ List.replicate leftDeletion.cohook.tail.steps true

Two cohook deletions either give the double-cohook right almost-split sequence, or lie in the rigid two-letter overlap boundary.