Constructing the double-cohook common corner

Starting with a negative left-boundary extension and then a negative right-boundary extension, this file restricts and replays the two suffixes to construct the other one-ended word. Both routes recover the same common corner, giving the literal double-cohook Butler--Ringel square.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookRestrictedPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : SignedPath D.source corner.target

Delete the negative left extension while retaining the negative right suffix of the common corner.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookRestrictedPath_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : IsString R (doubleCohookRestrictedPath left cornerRight)

The restricted path is a contiguous subpath of the common corner.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookRightReplay {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : cornerRight.RebaseResult (mixedBasePath left) ⋯

Rebase the complete negative right boundary after deleting the left prefix.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookRightExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : D.NegativeBoundaryExtension (doubleCohookRightReplay left cornerRight).result

The negative right-boundary extension of the shortened core obtained by retaining the original right cohook.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookRightExtension_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : (doubleCohookRightExtension left cornerRight).toRightExtension.steps = cornerRight.toRightExtension.steps

Restricting across the left prefix preserves the number of right-added letters.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookReverseBasePath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : SignedPath corner.target D.source

Reverse the restricted right-cohook word before replaying the original negative left boundary.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookReverseBasePath_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : IsString R (doubleCohookReverseBasePath left cornerRight)

The reversed restricted word is again a string.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookReverseFullPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : SignedPath corner.target left.reverseResult.target

The reversed restricted word followed by the original negative left boundary suffix.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookReverseFullPath_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : doubleCohookReverseFullPath left cornerRight = (Quiver.Path.comp left.result.path cornerRight.toRightExtension.suffixPath).reverse

The explicit reverse full path is the reverse of the original common corner path.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookReverseFullPath_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : IsString R (doubleCohookReverseFullPath left cornerRight)

The reverse full path used for the second replay is a string.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookReverseBaseWord_eq_rightReverse {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : ofStringPath (doubleCohookReverseBasePath left cornerRight) ⋯ = reverse R (doubleCohookRightReplay left cornerRight).result

The reversed restricted word is the reversal of the replayed right-result word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookLeftReplay {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : left.extension.RebaseResult (doubleCohookReverseBasePath left cornerRight) ⋯

Replay the original negative left boundary after the restricted right cohook word in reverse orientation.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookCornerLeftExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : (doubleCohookRightReplay left cornerRight).result.LeftNegativeBoundaryExtension

The negative left-boundary extension of the replayed right-cohook word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookCornerLeftExtension_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : (doubleCohookCornerLeftExtension left cornerRight).steps = left.steps

The replayed negative left boundary has its original length.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookCornerLeftExtension_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : (doubleCohookCornerLeftExtension left cornerRight).result = corner

The second replay recovers the original two-cohook corner.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookBoundarySquare {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) : D.NegativeBoundarySquare

A negative extension at each endpoint forms the coherent double-cohook boundary square obtained by restricting and replaying both suffixes.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookBoundarySquare_shortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.NegativeBoundaryExtension corner) (hmono : IsMonomial R) : ((doubleCohookBoundarySquare left cornerRight).shortComplex hmono).Exact

The replayed double-cohook boundary square has an exact canonical short complex.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookDeletionSquare {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C L D : Word R} (leftDeletion : L.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) : D.NegativeBoundarySquare

The double-cohook square attached to a left cohook of the core followed by a right cohook of the resulting one-sided word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookDeletionSquare_shortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C L D : Word R} (leftDeletion : L.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) (hmono : IsMonomial R) : ((doubleCohookDeletionSquare leftDeletion rightDeletion).shortComplex hmono).Exact

Two successive endpoint cohook deletions give the literal p. 172 canonical exact complex in right-module orientation.