Mixed cohook-hook boundary squares

The peak/non-peak cases of Butler--Ringel's canonical sequences combine a cohook deletion at one endpoint with a hook at the other. In the right-module convention this is a commuting square with horizontal monomorphisms and vertical epimorphisms. Its associated short complex has the upper-right word as source, the lower-left and upper-right-corner words as middle terms, and the cohook-extended word as target.

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

A commuting boundary square with a negative extension on the left and a positive extension on the right.

• rightResult : Word R
• right : D.PositiveBoundaryExtension self.rightResult
• left : D.LeftNegativeBoundaryExtension
• cornerLeft : self.rightResult.LeftNegativeBoundaryExtension
• cornerRight : self.left.result.PositiveBoundaryExtension 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.MixedBoundarySquare.ofExtensions {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D rightResult : Word R} (right : D.PositiveBoundaryExtension rightResult) (left : D.LeftNegativeBoundaryExtension) (cornerLeft : rightResult.LeftNegativeBoundaryExtension) (cornerRight : left.result.PositiveBoundaryExtension cornerLeft.result) (hsteps : cornerLeft.steps = left.steps) : D.MixedBoundarySquare

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

@[reducible, inline]

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

The common corner word.

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

Projection from the right-hook result back to the shortened word.

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

Inclusion from the right-hook result into the common corner.

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

Inclusion from the shortened word into the cohook-extended word.

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

Projection from the common corner onto the cohook-extended word.

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

The coordinate square commutes on every vertex space.

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

The two module maps around the mixed square commute.

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

Projecting through the two sides of the square gives the same base-word coordinates.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.MixedBoundarySquare.cornerLeft_inclusion_projection_eq_of_kernel {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.MixedBoundarySquare) {x : Q} (d : D.Space x) (c : square.corner.Space x) (hkernel : (square.left.spaceInclusion x) d + (square.cornerRight.toRightExtension.spaceProjection x) c = 0) : (square.cornerLeft.spaceInclusion x) ((square.cornerLeft.spaceProjection x) c) = c

A vector in the common corner whose projection cancels an included base vector has no coordinates outside the upper-right word.

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

The mixed square maps written on the product of the two middle vertex spaces.

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

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

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

The explicit mixed-square product maps are exact.

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

The signed source-to-middle map of the mixed canonical complex.

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

The sum of the inclusion and projection from the two middle terms to the cohook-extended target.

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

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.MixedBoundarySquare.toMiddleMap_fromMiddleMap_assoc {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.MixedBoundarySquare) (hmono : IsMonomial R) {Z : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)} (h : square.left.result.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.MixedBoundarySquare.shortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (square : D.MixedBoundarySquare) (hmono : IsMonomial R) : CategoryTheory.ShortComplex (CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k))

The mixed cohook-hook boundary short complex.

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

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