Irreducible mixed hook--cohook boundary sequences

The generic mixed boundary square retains only the signs of its four boundary maps. Here an actual left cohook deletion and right hook are replayed with their maximal arms intact, so all four maps are literal hook or cohook maps.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookDeletion.toLeftCohookExtension {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.LeftCohookDeletion D) : D.LeftCohookExtension

A left cohook deletion is literally the left cohook extension which reattaches the deleted prefix.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftCohookDeletion.toLeftCohookExtension_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (deletion : C.LeftCohookDeletion D) : deletion.toLeftCohookExtension.result = C

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

Sign-preserving replay of the right hook after deleting the left cohook prefix.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedRightHookReplay_result_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.HookExtension corner) : (mixedRightHookReplay left cornerRight).result = (mixedRightReplay left cornerRight.toPositiveBoundaryExtension).result

The sign-preserving hook replay and the generic positive-boundary replay produce the same word.

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

The shortened word carries a literal maximal right hook to the mixed square's right result.

@[simp]

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

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedLeftCohookReplay {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) : leftCohook.cohook.RebaseResult (mixedReverseBasePath leftCohook.toLeftNegativeBoundaryExtension cornerRight.toPositiveBoundaryExtension) ⋯

Sign-preserving replay of the deleted left cohook after the restricted right-hook word is reversed.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedLeftCohookReplay_result_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) : (mixedLeftCohookReplay leftCohook cornerRight).result = (mixedLeftReplay leftCohook.toLeftNegativeBoundaryExtension cornerRight.toPositiveBoundaryExtension).result

The sign-preserving cohook replay and the generic negative-boundary replay produce the same reversed corner word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedCornerLeftCohook {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) : (mixedRightReplay leftCohook.toLeftNegativeBoundaryExtension cornerRight.toPositiveBoundaryExtension).result.LeftCohookExtension

The restricted right-hook word carries a literal maximal left cohook to the common corner.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedCornerLeftCohook_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) : (mixedCornerLeftCohook leftCohook cornerRight).result = corner

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedCornerLeftCohook_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) : (mixedCornerLeftCohook leftCohook cornerRight).steps = leftCohook.steps

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedMaximalSquare {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) : D.MixedBoundarySquare

The mixed boundary square rebuilt from four literal maximal maps: the replayed right hook, the original left cohook, the replayed left cohook, and the original right hook.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.leftCohookDeletionRightHookMaximalSquare {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 manuscript input of a left cohook deletion and a right hook, rebuilt as the literal four-maximal-map mixed square.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedMaximalFiniteShortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) (hmono : IsMonomial R) : CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The four-maximal-map mixed boundary complex in the finite-dimensional module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedMaximalFiniteShortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) (hmono : IsMonomial R) : (mixedMaximalFiniteShortComplex leftCohook cornerRight hmono).Exact

The finite four-maximal-map mixed boundary complex is exact.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedMaximalFiniteShortComplex_f_isIrreducible_of_not_iso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : ¬Nonempty (D.finiteRightModule hmono ≅ corner.finiteRightModule hmono)) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (mixedMaximalFiniteShortComplex leftCohook cornerRight hmono).f

In the distinct-middle case, the replayed right hook and left cohook assemble to the irreducible first differential of the mixed sequence.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedMaximalFiniteShortComplex_g_isIrreducible_of_not_iso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : ¬Nonempty (D.finiteRightModule hmono ≅ corner.finiteRightModule hmono)) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (mixedMaximalFiniteShortComplex leftCohook cornerRight hmono).g

In the distinct-middle case, the original left cohook and transported right hook assemble to the irreducible second differential.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedMaximalFiniteShortComplex_shortExact_of_not_iso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : ¬Nonempty (D.finiteRightModule hmono ≅ corner.finiteRightModule hmono)) : (mixedMaximalFiniteShortComplex leftCohook cornerRight hmono).ShortExact

In the distinct-middle case, the literal finite mixed boundary complex is short exact.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.not_nonempty_finiteRightModule_iso_of_leftCohook_rightHook {k Q : Type u} [Field k] [Quiver Q] [Fintype Q] {A : Type u} [Ring A] [Algebra k A] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} (S : P.ArrowPolarization) {D corner : Word P.relations} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) : ¬Nonempty (D.finiteRightModule ⋯ ≅ corner.finiteRightModule ⋯)

The two middle modules of a mixed cohook--hook square cannot be isomorphic: the common corner is strictly longer than the base word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedMaximalFiniteShortComplex_f_isIrreducible {k Q : Type u} [Field k] [Quiver Q] [Fintype Q] {A : Type u} [Ring A] [Algebra k A] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} [IsAlgClosed k] (S : P.ArrowPolarization) [Fintype (DetectorIndex S)] {D corner : Word P.relations} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (mixedMaximalFiniteShortComplex leftCohook cornerRight ⋯).f

The first differential of the mixed cohook--hook complex is unconditionally irreducible.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedMaximalFiniteShortComplex_g_isIrreducible {k Q : Type u} [Field k] [Quiver Q] [Fintype Q] {A : Type u} [Ring A] [Algebra k A] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} [IsAlgClosed k] (S : P.ArrowPolarization) [Fintype (DetectorIndex S)] {D corner : Word P.relations} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (mixedMaximalFiniteShortComplex leftCohook cornerRight ⋯).g

The second differential of the mixed cohook--hook complex is unconditionally irreducible.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mixedMaximalFiniteShortComplex_shortExact {k Q : Type u} [Field k] [Quiver Q] [Fintype Q] {A : Type u} [Ring A] [Algebra k A] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} [IsAlgClosed k] (S : P.ArrowPolarization) [Fintype (DetectorIndex S)] {D corner : Word P.relations} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.HookExtension corner) : (mixedMaximalFiniteShortComplex leftCohook cornerRight ⋯).ShortExact

The literal mixed cohook--hook complex is unconditionally short exact.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.leftCohookDeletionRightHookMaximalFiniteShortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C D corner : Word R} (deletion : C.LeftCohookDeletion D) (right : C.HookExtension corner) (hmono : IsMonomial R) : CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The finite literal mixed complex in the manuscript's deletion--hook input form.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.leftCohookDeletionRightHookMaximalFiniteShortComplex_f_isIrreducible {k Q : Type u} [Field k] [Quiver Q] [Fintype Q] {A : Type u} [Ring A] [Algebra k A] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} [IsAlgClosed k] (S : P.ArrowPolarization) [Fintype (DetectorIndex S)] {C D corner : Word P.relations} (deletion : C.LeftCohookDeletion D) (right : C.HookExtension corner) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (leftCohookDeletionRightHookMaximalFiniteShortComplex deletion right ⋯).f

The first differential in the deletion--hook input form is irreducible.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.leftCohookDeletionRightHookMaximalFiniteShortComplex_g_isIrreducible {k Q : Type u} [Field k] [Quiver Q] [Fintype Q] {A : Type u} [Ring A] [Algebra k A] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} [IsAlgClosed k] (S : P.ArrowPolarization) [Fintype (DetectorIndex S)] {C D corner : Word P.relations} (deletion : C.LeftCohookDeletion D) (right : C.HookExtension corner) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (leftCohookDeletionRightHookMaximalFiniteShortComplex deletion right ⋯).g

The second differential in the deletion--hook input form is irreducible.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.leftCohookDeletionRightHookMaximalFiniteShortComplex_shortExact {k Q : Type u} [Field k] [Quiver Q] [Fintype Q] {A : Type u} [Ring A] [Algebra k A] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} [IsAlgClosed k] (S : P.ArrowPolarization) [Fintype (DetectorIndex S)] {C D corner : Word P.relations} (deletion : C.LeftCohookDeletion D) (right : C.HookExtension corner) : (leftCohookDeletionRightHookMaximalFiniteShortComplex deletion right ⋯).ShortExact

A left cohook deletion and a right hook give the literal short exact mixed boundary sequence.