One-middle algebra meshes as literal unary boundaries

Coefficient duality turns the selected right almost-split map at an algebra skeleton object into a left almost-split monomorphism. Rotating across its cokernel produces a literal right almost-split problem. When the original mesh has one middle occurrence, literal boundary classification gives a unary boundary, while uniqueness of kernels identifies its kernel word with the coefficient dual of the original endpoint.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.algebraSkeletonUnaryFiniteDimensional {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.algebraSkeletonUnaryNoetherian {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ᵐᵒᵖ

structure MagnitudeConjecture.BoundQuiver.StringPresentation.AlgebraOneMiddleLiteralBoundary {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) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (i : Fin T.n) : Type u

Literal data extracted from a one-middle mesh of the quotient-category algebra skeleton. Its kernel word represents the coefficient dual of the original algebra endpoint.

• word : StringWord.Word P.relations
• boundary : StringWord.Word.FiniteUnaryBoundary P self.word
• dualEndpointIso : (P.finiteCategoryDualModuleIndecomposableSkeleton T).obj i ≅ self.boundary.kernelWord.finiteRightModule ⋯

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.nonempty_algebraOneMiddleLiteralBoundary {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) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (Y : FiniteTauMatrix.OneMiddleMesh T.finiteTauCategoryData) : Nonempty (P.AlgebraOneMiddleLiteralBoundary S T ↑Y)

Every one-middle mesh on the algebra skeleton rotates to a literal unary Butler--Ringel boundary.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.oneMiddleLiteralBoundary {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) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (Y : FiniteTauMatrix.OneMiddleMesh T.finiteTauCategoryData) : P.AlgebraOneMiddleLiteralBoundary S T ↑Y

A chosen literal unary boundary representing a one-middle algebra mesh.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.oneMiddleMeshDisplayedArrow {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) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : FiniteTauMatrix.OneMiddleMesh T.finiteTauCategoryData → (y : Q) × (x : Q) × (x ⟶ y)

Send a one-middle algebra mesh to the central displayed arrow of its chosen literal unary boundary.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.oneMiddleMeshDisplayedArrow_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 : P.ArrowPolarization) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : Function.Injective (P.oneMiddleMeshDisplayedArrow S T)

Distinct one-middle meshes have distinct chosen central arrows. Equality of arrows gives equality of their canonical kernel words, hence an isomorphism between the corresponding objects of the coefficient-dual skeleton.