Restricting a hook across a left cohook deletion

This file supplies the word-combinatorics part of the asymmetric Butler--Ringel square. A negative left-boundary extension and a positive right-boundary extension have a common subword obtained by deleting the left extension while retaining the complete right suffix.

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

The shorter base path, with its right endpoint cast to the endpoint of a negative left extension.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedBasePath_isString {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (left : D.LeftNegativeBoundaryExtension) : IsString R (mixedBasePath left)

Endpoint casting preserves the string condition on the shorter base.

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

Delete the negative left extension while retaining an arbitrary positive right-boundary suffix.

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

The mixed restricted path is a contiguous subpath of the common corner, so it is automatically a string.

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

Rebase the complete positive boundary after deleting the left prefix.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedBaseWord_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D : Word R} (left : D.LeftNegativeBoundaryExtension) : ofStringPath (mixedBasePath left) ⋯ = D

Bundling the cast shorter path gives the original shorter word.

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

The positive-boundary extension of the shortened word obtained by retaining the original complete right suffix.

@[simp]

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

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

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

Reverse the restricted right-hook word before replaying the original negative left boundary in reverse orientation.

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

The reversed restricted word is again a string.

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

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

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedReverseFullPath_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.PositiveBoundaryExtension corner) : mixedReverseFullPath 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 written as base plus right suffix.

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

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

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedReverseBaseWord_eq_rightReverse {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.PositiveBoundaryExtension corner) : ofStringPath (mixedReverseBasePath left cornerRight) ⋯ = reverse R (mixedRightReplay left cornerRight).result

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

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

Replay the original negative left boundary after the reversed restricted right-result word.

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

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

@[simp]

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

The replayed negative boundary adds the same number of letters as the original negative left boundary.

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

The second replay recovers the original common corner in forward orientation.

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

A negative left extension followed by a positive right extension forms the coherent mixed boundary square obtained by restricting and replaying both suffixes.

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

The replayed mixed boundary square has an exact canonical short complex.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.leftCohookDeletionRightHookSquare {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D corner : Word R} (deletion : C.LeftCohookDeletion D) (right : C.HookExtension corner) : D.MixedBoundarySquare

The mixed square attached to an actual left cohook deletion and a right hook of the original word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.leftCohookDeletionRightHookSquare_shortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D corner : Word R} (deletion : C.LeftCohookDeletion D) (right : C.HookExtension corner) (hmono : IsMonomial R) : ((leftCohookDeletionRightHookSquare deletion right).shortComplex hmono).Exact

A left cohook deletion and a right hook give the asymmetric canonical exact complex.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookReverseSquare {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) : (reverse R D).MixedBoundarySquare

The opposite asymmetric case, expressed on reversed words: a right cohook deletion becomes a left cohook deletion and a left hook becomes its stored right hook.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookReverseSquare_shortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) (hmono : IsMonomial R) : ((rightCohookDeletionLeftHookReverseSquare deletion left).shortComplex hmono).Exact

The reversed square for a right cohook deletion and a left hook has an exact canonical short complex. This is the intermediate exactness result transported back to the original orientation below.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookReverseSquare_corner {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) : (rightCohookDeletionLeftHookReverseSquare deletion left).corner = left.reverseResult

The common corner of the reversed asymmetric square is the stored result of the original left hook.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookReverseSquare_left_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) : (rightCohookDeletionLeftHookReverseSquare deletion left).left.result = reverse R C

The target of the reversed asymmetric square is the reverse of the original word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookSourceWord {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) : Word R

The source word of the right-cohook/left-hook sequence, returned to the original orientation.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookReverseCorner_eq_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) : reverse R (rightCohookDeletionLeftHookReverseSquare deletion left).corner = left.result

Reversing the square corner recovers the original left-hook result.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookReverseTarget_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) : reverse R (rightCohookDeletionLeftHookReverseSquare deletion left).left.result = C

Reversing the square target recovers the original word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookSourceIso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) (hmono : IsMonomial R) : (rightCohookDeletionLeftHookReverseSquare deletion left).rightResult.rightModule hmono ≅ (rightCohookDeletionLeftHookSourceWord deletion left).rightModule hmono

Reversal identifies the source of the reversed square with the source word in the original orientation.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookMiddleIso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) (hmono : IsMonomial R) : (reverse R D).rightModule hmono ⊞ (rightCohookDeletionLeftHookReverseSquare deletion left).corner.rightModule hmono ≅ D.rightModule hmono ⊞ left.result.rightModule hmono

Reversal identifies the two middle terms with the shortened word and the original left-hook result.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookTargetIso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) (hmono : IsMonomial R) : (rightCohookDeletionLeftHookReverseSquare deletion left).left.result.rightModule hmono ≅ C.rightModule hmono

Reversal identifies the target of the reversed square with the original word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookShortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) (hmono : IsMonomial R) : CategoryTheory.ShortComplex (CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k))

The complete right-cohook/left-hook canonical complex in the original right-module orientation. Both differentials are transported, together with all three objects, through the canonical word-reversal isomorphisms.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookShortComplexIso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) (hmono : IsMonomial R) : (rightCohookDeletionLeftHookReverseSquare deletion left).shortComplex hmono ≅ rightCohookDeletionLeftHookShortComplex deletion left hmono

The original-orientation canonical complex is isomorphic to the exact reversed mixed square.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightCohookDeletionLeftHookShortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.CohookDeletion D) (left : C.LeftHookExtension) (hmono : IsMonomial R) : (rightCohookDeletionLeftHookShortComplex deletion left hmono).Exact

A right cohook deletion and a left hook give the asymmetric canonical exact complex in the original right-module orientation.