Repeated middle words for the negative cohook square #
The finite detector classification reduces an isomorphism between the two middle string modules to literal equality or reversal. In the reversal branch, cancellation of equally long cohook prefixes shows that the original word has length zero. The reverse double-cohook path then contains an adjacent inverse pair, contradicting its reducedness.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.not_isReduced_positiveArrow_comp_zero_comp_negativeArrow_of_letter_eq
{Q : Type u}
[Quiver Q]
{a b c d : Q}
(leftArrow : a ⟶ b)
(middle : SignedPath b c)
(rightArrow : d ⟶ c)
(hmiddle : Quiver.Path.length middle = 0)
(hletter : signedArrowLetter (positiveArrow leftArrow) = signedArrowLetter (positiveArrow rightArrow))
:
¬IsReduced
((Quiver.Hom.toPath (positiveArrow leftArrow)).comp
(Quiver.Path.comp middle (Quiver.Hom.toPath (negativeArrow rightArrow))))
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.length_eq_zero_and_boundaryLetter_eq_of_leftCohook_result_eq_reverse_rightCohook_result
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{D rightResult : Word R}
(right : D.CohookExtension rightResult)
(left : D.LeftCohookExtension)
(hmiddle : left.result = reverse R rightResult)
:
length R D = 0 ∧ signedArrowLetter (positiveArrow left.cohook.arrow) = signedArrowLetter (positiveArrow right.arrow)
If a left-cohook result is the reverse of a right-cohook result, then the base has length zero and the two boundary letters coincide.
def
MagnitudeConjecture.BoundQuiver.StringWord.Word.twoCohookReversePath
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{D rightResult : Word R}
(right : D.CohookExtension rightResult)
(left : D.LeftCohookExtension)
:
SignedPath rightResult.target left.reverseResult.target
The reverse-oriented path obtained by adjoining maximal cohooks at both ends of a word.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.leftCohook_result_ne_reverse_rightCohook_result_of_twoCohookReversePath_isString
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
{D rightResult : Word R}
(right : D.CohookExtension rightResult)
(left : D.LeftCohookExtension)
(hpath : IsString R (twoCohookReversePath right left))
:
A valid two-cohook corner rules out reversal of its two middle words.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.leftCohook_result_eq_of_finiteRightModule_iso_of_twoCohookReversePath_isString
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
(S : P.ArrowPolarization)
{D rightResult : Word P.relations}
(right : D.CohookExtension rightResult)
(left : D.LeftCohookExtension)
(hpath : IsString P.relations (twoCohookReversePath right left))
(e : left.result.finiteRightModule ⋯ ≅ rightResult.finiteRightModule ⋯)
:
left.result = rightResult
For a valid two-cohook square, isomorphism of the two middle modules forces literal equality of their words.