Literal one-middle Butler--Ringel boundaries

The exhaustive endpoint analysis for a nonprojective string has five binary boundary shapes and two unary shapes, exchanged by word reversal. Comparing their displayed decompositions with an arbitrary one-summand minimal right almost-split source eliminates every binary shape. Thus a literal one-middle mesh is represented by a pure one-sided hook boundary.

inductive MagnitudeConjecture.BoundQuiver.StringWord.Word.FiniteUnaryBoundary {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) : Type u

The two literal unary Butler--Ringel boundary shapes at a word. The negative case is stored before reversal, so its central arrow remains an ordinary displayed arrow of the original quiver.

• positive {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} (hpure : IsPurePositive ⋯ C) (left : C.LeftHookExtension) (hresultPeak : left.result.StartsOnPeak) : FiniteUnaryBoundary P C
• negative {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} (hpure : IsPureNegative ⋯ C) (hend : C.EndsOnPeak) {D : Word P.relations} (right : C.HookExtension D) : FiniteUnaryBoundary P C

def MagnitudeConjecture.BoundQuiver.StringWord.Word.FiniteUnaryBoundary.displayedArrow {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} (B : FiniteUnaryBoundary P C) : (y : Q) × (x : Q) × (x ⟶ y)

The central displayed arrow indexing a unary boundary.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.FiniteUnaryBoundary.rightAlmostSplitDecompositionBound {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} (B : FiniteUnaryBoundary P C) : CategoryTheory.RightAlmostSplitDecompositionBound (C.finiteRightModule ⋯) 1

A literal unary boundary supplies a minimal right almost-split map with exactly one displayed middle summand.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.FiniteUnaryBoundary.kernelWord {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} (B : FiniteUnaryBoundary P C) : Word P.relations

The literal kernel word at the left end of a unary boundary sequence.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.FiniteUnaryBoundary.rawShortComplex {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} (B : FiniteUnaryBoundary P C) : CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The underlying short complex before the negative case is transported back across the canonical reversal isomorphism of its endpoint.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.FiniteUnaryBoundary.rawShortComplex_X₁ {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} (B : FiniteUnaryBoundary P C) : B.rawShortComplex.X₁ = B.kernelWord.finiteRightModule ⋯

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.FiniteUnaryBoundary.endpointIso {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} (B : FiniteUnaryBoundary P C) : B.rawShortComplex.X₃ ≅ C.finiteRightModule ⋯

The endpoint of the raw unary complex is the original word in the positive case and its reversal in the negative case.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.FiniteUnaryBoundary.rawShortComplex_shortExact {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} (B : FiniteUnaryBoundary P C) : B.rawShortComplex.ShortExact

The raw literal unary boundary complex is short exact.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.FiniteUnaryBoundary.rawShortComplex_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 : DetectorIndex.FiniteIndecomposableSkeleton) {C : Word P.relations} (B : FiniteUnaryBoundary P C) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit B.rawShortComplex.g

The raw terminal map of a unary boundary is right almost split.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.FiniteUnaryBoundary.rawShortComplex_isRightMinimal {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} (B : FiniteUnaryBoundary P C) : QuotientSubmoduleEquidistribution.IsRightMinimal B.rawShortComplex.g

The raw terminal map of a unary boundary is right minimal.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.nonempty_finiteUnaryBoundary_of_decomposition_n_eq_one {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 ⋯)) {E : CoveringHom.FiniteDimensionalModuleCategory k} (f : E ⟶ C.finiteRightModule ⋯) (d : CategoryTheory.FiniteIndecomposableDecomposition E) (hlocal : ∀ (i : Fin d.n), IsLocalRing (CategoryTheory.End (d.summand i))) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (hfmin : QuotientSubmoduleEquidistribution.IsRightMinimal f) (hd : d.n = 1) : Nonempty (FiniteUnaryBoundary P C)

If a displayed minimal right almost-split source at a nonprojective literal string has one indecomposable summand, the exhaustive endpoint classification leaves only a unary Butler--Ringel boundary.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.FiniteUnaryBoundary.kernelWord_eq_canonicalKernelWord {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} (B : FiniteUnaryBoundary P C) : B.kernelWord = HookExtension.canonicalKernelWord P.toSpecialBiserialPresentation B.displayedArrow

The literal kernel of a unary boundary depends only on its displayed central arrow.