Two-ended negative boundary squares for string modules

The double-peak Butler--Ringel sequence is obtained by attaching a negative boundary at both ends of a shorter string. The right-module maps are inclusions. This file proves that any coherent common-corner square of those inclusions gives the canonical exact complex from the base to the two one-ended extensions and then to the common corner.

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) : Type u

A common corner for negative boundary extensions at both ends of D.

• rightResult : Word R
• right : D.NegativeBoundaryExtension self.rightResult
• left : D.LeftNegativeBoundaryExtension
• cornerLeft : self.rightResult.LeftNegativeBoundaryExtension
• cornerRight : self.left.result.NegativeBoundaryExtension self.cornerLeft.result
• steps_eq : self.cornerLeft.steps = self.left.steps
• position_commutes {x : Q} (i : D.PositionAt x) : self.cornerRight.toRightExtension.position (self.left.position i) = self.cornerLeft.position (self.right.toRightExtension.position i)
• position_intersection {x : Q} (q : self.left.result.PositionAt x) (p : self.rightResult.PositionAt x) : self.cornerRight.toRightExtension.position q = self.cornerLeft.position p → ∃ (i : D.PositionAt x), self.left.position i = q ∧ self.right.toRightExtension.position i = p

def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.ofExtensions {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D rightResult : Word R} (right : D.NegativeBoundaryExtension rightResult) (left : D.LeftNegativeBoundaryExtension) (cornerLeft : rightResult.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension cornerLeft.result) (hsteps : cornerLeft.steps = left.steps) : D.NegativeBoundarySquare

Equal left-extension lengths force the position coherence required by a negative boundary square.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.corner {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) : Word R

The common two-ended negative extension.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.baseToLeftMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) : D.rightModule hmono ⟶ square.left.result.rightModule hmono

Inclusion from the base into its left negative-boundary extension.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.baseToRightMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) : D.rightModule hmono ⟶ square.rightResult.rightModule hmono

Inclusion from the base into its right negative-boundary extension.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.leftToCornerMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) : square.left.result.rightModule hmono ⟶ square.corner.rightModule hmono

Inclusion from the left-extended word into the common corner.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.rightToCornerMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) : square.rightResult.rightModule hmono ⟶ square.corner.rightModule hmono

Inclusion from the right-extended word into the common corner.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.space_map_commutes {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) {x : Q} (v : D.Space x) : (square.cornerRight.toRightExtension.spaceInclusion x) ((square.left.spaceInclusion x) v) = (square.cornerLeft.spaceInclusion x) ((square.right.toRightExtension.spaceInclusion x) v)

The two coordinate inclusions around a negative boundary square agree.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.map_commutes {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) : CategoryTheory.CategoryStruct.comp (square.baseToLeftMap hmono) (square.leftToCornerMap hmono) = CategoryTheory.CategoryStruct.comp (square.baseToRightMap hmono) (square.rightToCornerMap hmono)

The two module inclusions around a negative boundary square commute.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.left_inclusion_projection_eq_of_corner_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) {x : Q} (l : square.left.result.Space x) (r : square.rightResult.Space x) (hcorner : (square.cornerRight.toRightExtension.spaceInclusion x) l = (square.cornerLeft.spaceInclusion x) r) : (square.left.spaceInclusion x) ((square.left.spaceProjection x) l) = l

Equality in the corner forces a left-result vector to be supported on positions inherited from the base.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.right_inclusion_projection_eq_of_corner_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) {x : Q} (l : square.left.result.Space x) (r : square.rightResult.Space x) (hcorner : (square.cornerRight.toRightExtension.spaceInclusion x) l = (square.cornerLeft.spaceInclusion x) r) : (square.right.toRightExtension.spaceInclusion x) ((square.right.toRightExtension.spaceProjection x) r) = r

Equality in the corner forces a right-result vector to be supported on positions inherited from the base.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.base_projection_eq_of_corner_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) {x : Q} (l : square.left.result.Space x) (r : square.rightResult.Space x) (hcorner : (square.cornerRight.toRightExtension.spaceInclusion x) l = (square.cornerLeft.spaceInclusion x) r) : (square.left.spaceProjection x) l = (square.right.toRightExtension.spaceProjection x) r

Equal corner inclusions have equal base-coordinate projections.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.toPairSpaceMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (x : Q) : D.Space x →ₗ[k] square.left.result.Space x × square.rightResult.Space x

The base-to-middle map on explicit vertex-space products.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.fromPairSpaceMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (x : Q) : square.left.result.Space x × square.rightResult.Space x →ₗ[k] square.corner.Space x

The signed middle-to-corner map on explicit vertex-space products.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.pairSpaceMap_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (x : Q) : Function.Exact ⇑(square.toPairSpaceMap x) ⇑(square.fromPairSpaceMap x)

The explicit double-inclusion product maps are exact.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.toMiddleMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) : D.rightModule hmono ⟶ square.left.result.rightModule hmono ⊞ square.rightResult.rightModule hmono

The base-to-middle map of the double-cohook canonical complex.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.fromMiddleMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) : square.left.result.rightModule hmono ⊞ square.rightResult.rightModule hmono ⟶ square.corner.rightModule hmono

The signed middle-to-corner map of the double-cohook canonical complex.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.toMiddleMap_fromMiddleMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) : CategoryTheory.CategoryStruct.comp (square.toMiddleMap hmono) (square.fromMiddleMap hmono) = 0

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.toMiddleMap_fromMiddleMap_assoc {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) {Z : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)} (h : square.corner.rightModule hmono ⟶ Z) : CategoryTheory.CategoryStruct.comp (square.toMiddleMap hmono) (CategoryTheory.CategoryStruct.comp (square.fromMiddleMap hmono) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.shortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) : CategoryTheory.ShortComplex (CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k))

The double-negative-boundary short complex.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.NegativeBoundarySquare.shortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.NegativeBoundarySquare) (hmono : IsMonomial R) : (square.shortComplex hmono).Exact

Every coherent negative boundary square gives an exact canonical short complex of right string modules.