Commuting two-ended boundary squares for string modules

A positive boundary extension at each end of a string gives two quotient maps. When the two extensions have a common corner and their inherited position embeddings agree, the resulting square of string-module quotient maps commutes. This is the coordinate core of the two-hook canonical exact sequence; construction of the common maximal-hook corner is a separate word combinatorics step.

noncomputable def MagnitudeConjecture.BoundQuiver.functorBiprodAppLinearEquiv {k : Type u} [Field k] {D : Type u} [CategoryTheory.Category.{u, u} D] (F G : CategoryTheory.Functor D (ModuleCat k)) (X : D) : ↑((F ⊞ G).obj X) ≃ₗ[k] ↑(F.obj X) × ↑(G.obj X)

Evaluation of a functor-category biproduct is linearly equivalent to the ordinary product of the two evaluated modules. The definition uses the actual chosen biproduct projections and inclusions, so it does not depend on definitional choices for pointwise limits.

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

A common corner for positive boundary extensions at both ends of C. The coherence field says that the two ways of embedding every old word position into the corner are literally equal.

• rightResult : Word R
• right : C.PositiveBoundaryExtension self.rightResult
• left : C.LeftPositiveBoundaryExtension
• cornerLeft : self.rightResult.LeftPositiveBoundaryExtension
• cornerRight : self.left.result.PositiveBoundaryExtension self.cornerLeft.result
• position_commutes {x : Q} (i : C.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 : C.PositionAt x), self.left.position i = q ∧ self.right.toRightExtension.position i = p

def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundarySquare.ofExtensions {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.PositiveBoundaryExtension rightResult) (left : C.LeftPositiveBoundaryExtension) (cornerLeft : rightResult.LeftPositiveBoundaryExtension) (cornerRight : left.result.PositiveBoundaryExtension cornerLeft.result) (hsteps : cornerLeft.steps = left.steps) : C.PositiveBoundarySquare

Assemble a positive-boundary square from two compatible constructions of the same corner. Equality of the numbers of letters added on the left is enough to force both position commutativity and the required intersection property.

@[reducible, inline]

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

The common two-ended extension.

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

Projection from the corner after forgetting the right extension.

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

Projection from the corner after forgetting the left extension.

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

Projection from the left-extended word back to the original word.

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

Projection from the right-extended word back to the original word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundarySquare.map_commutes {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (square : C.PositiveBoundarySquare) (hmono : IsMonomial R) : CategoryTheory.CategoryStruct.comp (square.toLeftMap hmono) (square.leftToBaseMap hmono) = CategoryTheory.CategoryStruct.comp (square.toRightMap hmono) (square.rightToBaseMap hmono)

The two composites around a coherent positive-boundary square agree.

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

Projecting a right-result vector through the corner onto the left result retains exactly its coordinates inherited from the base word.

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

The symmetric cross projection formula: projecting a left-result vector through the corner onto the right result retains exactly its base-word coordinates.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundarySquare.baseToCornerSpaceInclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (square : C.PositiveBoundarySquare) (x : Q) : C.Space x →ₗ[k] square.corner.Space x

Coordinate inclusion of the base word into the common corner, using the left result and then the right extension to the corner.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundarySquare.cornerRight_projection_baseToCorner_inclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (square : C.PositiveBoundarySquare) (x : Q) (v : C.Space x) : (square.cornerRight.toRightExtension.spaceProjection x) ((square.baseToCornerSpaceInclusion x) v) = (square.left.spaceInclusion x) v

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundarySquare.cornerLeft_projection_baseToCorner_inclusion {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (square : C.PositiveBoundarySquare) (x : Q) (v : C.Space x) : (square.cornerLeft.spaceProjection x) ((square.baseToCornerSpaceInclusion x) v) = (square.right.toRightExtension.spaceInclusion x) v

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

Lift a pair of one-ended coordinate vectors to the corner. The last term corrects the overlap along the old word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundarySquare.cornerRight_projection_kernelPairLift {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (square : C.PositiveBoundarySquare) (x : Q) (v : square.left.result.Space x × square.rightResult.Space x) : (square.cornerRight.toRightExtension.spaceProjection x) ((square.kernelPairLift x) v) = v.1

The left corner projection of the corrected lift is the first component.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.PositiveBoundarySquare.cornerLeft_projection_kernelPairLift {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (square : C.PositiveBoundarySquare) (x : Q) (v : square.left.result.Space x × square.rightResult.Space x) (hv : (square.left.spaceProjection x) v.1 + (square.right.toRightExtension.spaceProjection x) v.2 = 0) : (square.cornerLeft.spaceProjection x) ((square.kernelPairLift x) v) = -v.2

On a pair killed by the sum of the two base projections, the right corner projection of the corrected lift is the negative second component.

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

The corner map written on the explicit product of the two one-ended vertex spaces.

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

The middle-to-base map written on the explicit product of vertex spaces.

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

The explicit product-space maps are exact. Surjectivity onto the kernel is witnessed by kernelPairLift.

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

The signed map from the common corner to the direct sum of the two one-ended extensions.

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

The sum of the two canonical projections from the one-ended extensions back to the original string module.

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

Commutativity of the boundary square gives the complex relation after putting the conventional minus sign on the right component.

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

Commutativity of the boundary square gives the complex relation after putting the conventional minus sign on the right component.

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

The canonical two-ended boundary short complex.

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

A coherent two-ended boundary square with no extra overlap gives an exact canonical sequence.