Irreducible differentials of finite string boundary squares

This file connects the explicit boundary-square maps to the maximal hook and cohook maps whose irreducibility has already been proved.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookCornerWord_startsInDeep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : (twoHookCornerWord right left hpath).StartsInDeep

Adding a left hook does not destroy maximality of the already maximal right hook at the opposite endpoint.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookRightCornerHook {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : left.result.HookExtension (twoHookCornerWord right left hpath)

Replaying the right negative tail after a left hook gives a literal maximal right hook from the left-hook result to the common corner.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookReverseCornerWord_startsInDeep {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : (twoHookReverseCornerWord right left hpath).StartsInDeep

Adding a right hook does not destroy maximality of the already maximal left hook when the common corner is viewed in reverse orientation.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookLeftCornerHook {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : rightResult.LeftHookExtension

Replaying the left negative tail after the reversed right hook gives a literal maximal left hook from the right-hook result to the common corner.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookLeftCornerHook_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : (twoHookLeftCornerHook right left hpath).result = twoHookCornerWord right left hpath

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookLeftCornerHook_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : (twoHookLeftCornerHook right left hpath).steps = left.steps

The replayed maximal left corner adds exactly as many letters as the original left hook.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookRightCornerHookForLeftResult {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : left.result.HookExtension (twoHookLeftCornerHook right left hpath).result

Transport the maximal right-corner hook to the literal result word of the maximal left-corner hook.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalSquare {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) : C.PositiveBoundarySquare

The positive two-hook square rebuilt from four maximal hooks. All four coordinate maps are now literally hook maps, while the common corner remains the canonical two-hook word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookCorner_finiteCombinedMap_isIrreducible_of_not_iso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : ¬Nonempty (left.result.finiteRightModule hmono ≅ rightResult.finiteRightModule hmono)) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.Limits.biprod.lift ((twoHookRightCornerHookForLeftResult right left hpath).finiteModuleMap hmono) (-(twoHookLeftCornerHook right left hpath).finiteModuleMap hmono))

In the distinct-middle case, the two maximal corner hooks assemble to an irreducible first differential of the positive boundary sequence.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookCorner_finiteCombinedMap_isIrreducible_of_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] [IsAlgClosed k] {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : left.result = rightResult) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.Limits.biprod.lift ((twoHookRightCornerHookForLeftResult right left hpath).finiteModuleMap hmono) (-(twoHookLeftCornerHook right left hpath).finiteModuleMap hmono))

In the literal repeated-middle case, the two corner projections occupy different hook components. The symmetric Gaussian-elimination criterion therefore makes the first differential irreducible.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookBase_finiteCombinedMap_isIrreducible_of_not_iso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : ¬Nonempty (left.result.finiteRightModule hmono ≅ rightResult.finiteRightModule hmono)) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.Limits.biprod.desc (left.finiteModuleMap hmono) (right.finiteModuleMap hmono))

In the distinct-middle case, the original two hooks assemble to an irreducible second differential of the positive boundary sequence.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookBase_finiteCombinedMap_isIrreducible_of_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] [IsAlgClosed k] {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : left.result = rightResult) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.Limits.biprod.desc (left.finiteModuleMap hmono) (right.finiteModuleMap hmono))

When the two middle words are literally equal, the two hook components are different graph-basis vectors. Gaussian elimination on this repeated summand therefore makes the second differential irreducible.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalFiniteShortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (hmono : IsMonomial R) : CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The four-maximal-hook positive boundary complex in the finite-dimensional module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalFiniteShortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (hmono : IsMonomial R) : (twoHookMaximalFiniteShortComplex right left hpath hmono).Exact

The finite four-maximal-hook positive boundary complex is exact.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalFiniteShortComplex_f_isIrreducible_of_not_iso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : ¬Nonempty (left.result.finiteRightModule hmono ≅ rightResult.finiteRightModule hmono)) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (twoHookMaximalFiniteShortComplex right left hpath hmono).f

In the distinct-middle case, the first differential of the literal finite positive boundary complex is irreducible.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalFiniteShortComplex_g_isIrreducible_of_not_iso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : ¬Nonempty (left.result.finiteRightModule hmono ≅ rightResult.finiteRightModule hmono)) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (twoHookMaximalFiniteShortComplex right left hpath hmono).g

In the distinct-middle case, the second differential of the literal finite positive boundary complex is irreducible.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalFiniteShortComplex_f_isIrreducible_of_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] [IsAlgClosed k] {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : left.result = rightResult) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (twoHookMaximalFiniteShortComplex right left hpath hmono).f

In the literal repeated-middle case, the first differential of the finite positive boundary complex is irreducible.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalFiniteShortComplex_g_isIrreducible_of_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] [IsAlgClosed k] {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : left.result = rightResult) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (twoHookMaximalFiniteShortComplex right left hpath hmono).g

In the literal repeated-middle case, the second differential of the finite positive boundary complex is irreducible.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalFiniteShortComplex_shortExact_of_not_iso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : ¬Nonempty (left.result.finiteRightModule hmono ≅ rightResult.finiteRightModule hmono)) : (twoHookMaximalFiniteShortComplex right left hpath hmono).ShortExact

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

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalFiniteShortComplex_shortExact_of_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] [IsAlgClosed k] {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : left.result = rightResult) : (twoHookMaximalFiniteShortComplex right left hpath hmono).ShortExact

In the literal repeated-middle case, the finite positive boundary complex is short exact.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalSquare_shortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C rightResult : Word R} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString R (twoHookPath right left)) (hmono : IsMonomial R) : ((twoHookMaximalSquare right left hpath).shortComplex hmono).Exact

The four-maximal-hook positive square is exact in the raw string-module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalFiniteShortComplex_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 rightResult : Word P.relations} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString P.relations (twoHookPath right left)) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (twoHookMaximalFiniteShortComplex right left hpath ⋯).f

The first differential of the positive two-hook complex is irreducible without a middle-summand case hypothesis.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalFiniteShortComplex_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 rightResult : Word P.relations} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString P.relations (twoHookPath right left)) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (twoHookMaximalFiniteShortComplex right left hpath ⋯).g

The second differential of the positive two-hook complex is irreducible without a middle-summand case hypothesis.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.twoHookMaximalFiniteShortComplex_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 rightResult : Word P.relations} (right : C.HookExtension rightResult) (left : C.LeftHookExtension) (hpath : IsString P.relations (twoHookPath right left)) : (twoHookMaximalFiniteShortComplex right left hpath ⋯).ShortExact

The positive two-hook complex is short exact without a middle-summand case hypothesis. Detector classification turns an isomorphism of the middle modules into literal word equality, while nonisomorphic summands use the ordinary binary-biproduct criterion.