Magnitude conjecture

MagnitudeConjecture.Algebra.StringFiniteDoubleCohookIrreducible

Irreducible double-cohook boundary sequences #

Both generic negative boundaries in the double-cohook square are upgraded to literal maximal cohooks by the sign-preserving replay construction.

source
@[simp]
theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.boundaryLetter_transportResult {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D D' : Word R} (cohook : C.CohookExtension D) (h : D = D') :
signedArrowLetter (positiveArrow (cohook.transportResult h).arrow) = signedArrowLetter (positiveArrow cohook.arrow)
source
@[simp]
theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.boundaryLetter_transportSource {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C C' D : Word R} (cohook : C.CohookExtension D) (h : C = C') :
signedArrowLetter (positiveArrow (cohook.transportSource h).arrow) = signedArrowLetter (positiveArrow cohook.arrow)
source
@[simp]
theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.boundaryLetter_rebase {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (cohook : C.CohookExtension D) {source : Q} (basePath : SignedPath source C.target) (hbase : IsString R basePath) (hfull : IsString R (Quiver.Path.comp basePath cohook.toNegativeBoundaryExtension.toRightExtension.suffixPath)) :
signedArrowLetter (positiveArrow (cohook.rebase basePath hbase hfull).rebased.arrow) = signedArrowLetter (positiveArrow cohook.arrow)
source
noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookRightCohookReplay {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.CohookExtension corner) :
cornerRight.RebaseResult (mixedBasePath left) ⋯

Replay the right cohook after deleting the left cohook prefix.

Instances For
    source
    theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookRightCohookReplay_result_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.CohookExtension corner) :
    (doubleCohookRightCohookReplay left cornerRight).result = (doubleCohookRightReplay left cornerRight.toNegativeBoundaryExtension).result
    source
    noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookRightCohook {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.CohookExtension corner) :
    D.CohookExtension (doubleCohookRightReplay left cornerRight.toNegativeBoundaryExtension).result

    The shortened core carries a literal maximal right cohook to the other middle word.

    Instances For
      source
      theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookRightCohook_boundaryLetter {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.CohookExtension corner) :
      signedArrowLetter (positiveArrow (doubleCohookRightCohook left cornerRight).arrow) = signedArrowLetter (positiveArrow cornerRight.arrow)
      source
      theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.leftCohook_result_ne_reverse_doubleCohookRight_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftCohookExtension) (cornerRight : left.result.CohookExtension corner) :
      left.result ≠ reverse R (doubleCohookRightReplay left.toLeftNegativeBoundaryExtension cornerRight.toNegativeBoundaryExtension).result

      The certified double-cohook corner rules out reversal of its two middle words.

      source
      @[simp]
      theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookRightCohook_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (left : D.LeftNegativeBoundaryExtension) (cornerRight : left.result.CohookExtension corner) :
      (doubleCohookRightCohook left cornerRight).steps = cornerRight.steps
      source
      noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookLeftCohookReplay {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.CohookExtension corner) :
      leftCohook.cohook.RebaseResult (doubleCohookReverseBasePath leftCohook.toLeftNegativeBoundaryExtension cornerRight.toNegativeBoundaryExtension) ⋯

      Replay the original left cohook after reversing the restricted right cohook word.

      Instances For
        source
        theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookLeftCohookReplay_result_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.CohookExtension corner) :
        (doubleCohookLeftCohookReplay leftCohook cornerRight).result = (doubleCohookLeftReplay leftCohook.toLeftNegativeBoundaryExtension cornerRight.toNegativeBoundaryExtension).result
        source
        noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookCornerLeftCohook {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.CohookExtension corner) :
        (doubleCohookRightReplay leftCohook.toLeftNegativeBoundaryExtension cornerRight.toNegativeBoundaryExtension).result.LeftCohookExtension

        The other middle word carries a literal maximal left cohook to the common corner.

        Instances For
          source
          @[simp]
          theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookCornerLeftCohook_result {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.CohookExtension corner) :
          (doubleCohookCornerLeftCohook leftCohook cornerRight).result = corner
          source
          @[simp]
          theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookCornerLeftCohook_steps {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.CohookExtension corner) :
          (doubleCohookCornerLeftCohook leftCohook cornerRight).steps = leftCohook.steps
          source
          noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookMaximalSquare {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.CohookExtension corner) :
          D.NegativeBoundarySquare

          The double-cohook square rebuilt from four literal maximal cohooks.

          Instances For
            source
            theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookMaximalSquare_corner {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.CohookExtension corner) :
            (doubleCohookMaximalSquare leftCohook cornerRight).corner = corner

            The common corner of the rebuilt double-cohook square is the prescribed corner word.

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

            The four-maximal-cohook complex in the finite-dimensional module category.

            Instances For
              source
              theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookMaximalFiniteShortComplex_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.CohookExtension corner) (hmono : IsMonomial R) :
              (doubleCohookMaximalFiniteShortComplex leftCohook cornerRight hmono).Exact
              source
              theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookMaximalFiniteShortComplex_f_isIrreducible_of_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] [IsAlgClosed k] {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.CohookExtension corner) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : leftCohook.result = (doubleCohookRightReplay leftCohook.toLeftNegativeBoundaryExtension cornerRight.toNegativeBoundaryExtension).result) :
              QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (doubleCohookMaximalFiniteShortComplex leftCohook cornerRight hmono).f

              In the literal repeated-middle case, the two base cohook components make the first differential irreducible.

              source
              theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookMaximalFiniteShortComplex_g_isIrreducible_of_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] [IsAlgClosed k] {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.CohookExtension corner) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : leftCohook.result = (doubleCohookRightReplay leftCohook.toLeftNegativeBoundaryExtension cornerRight.toNegativeBoundaryExtension).result) :
              QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (doubleCohookMaximalFiniteShortComplex leftCohook cornerRight hmono).g

              In the literal repeated-middle case, the two corner cohook components make the second differential irreducible.

              source
              theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookMaximalFiniteShortComplex_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.CohookExtension corner) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : ¬Nonempty (leftCohook.result.finiteRightModule hmono ≅ (doubleCohookRightReplay leftCohook.toLeftNegativeBoundaryExtension cornerRight.toNegativeBoundaryExtension).result.finiteRightModule hmono)) :
              QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (doubleCohookMaximalFiniteShortComplex leftCohook cornerRight hmono).f

              The two base cohook maps assemble to an irreducible first differential when the two middle string modules are nonisomorphic.

              source
              theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookMaximalFiniteShortComplex_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.CohookExtension corner) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : ¬Nonempty (leftCohook.result.finiteRightModule hmono ≅ (doubleCohookRightReplay leftCohook.toLeftNegativeBoundaryExtension cornerRight.toNegativeBoundaryExtension).result.finiteRightModule hmono)) :
              QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (doubleCohookMaximalFiniteShortComplex leftCohook cornerRight hmono).g

              The two corner cohook maps assemble to an irreducible second differential in the distinct-middle case.

              source
              theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookMaximalFiniteShortComplex_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.CohookExtension corner) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : ¬Nonempty (leftCohook.result.finiteRightModule hmono ≅ (doubleCohookRightReplay leftCohook.toLeftNegativeBoundaryExtension cornerRight.toNegativeBoundaryExtension).result.finiteRightModule hmono)) :
              (doubleCohookMaximalFiniteShortComplex leftCohook cornerRight hmono).ShortExact

              In the distinct-middle case, the literal finite double-cohook complex is short exact.

              source
              theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookMaximalFiniteShortComplex_shortExact_of_eq {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] [IsAlgClosed k] {D corner : Word R} (leftCohook : D.LeftCohookExtension) (cornerRight : leftCohook.result.CohookExtension corner) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) (hmiddle : leftCohook.result = (doubleCohookRightReplay leftCohook.toLeftNegativeBoundaryExtension cornerRight.toNegativeBoundaryExtension).result) :
              (doubleCohookMaximalFiniteShortComplex leftCohook cornerRight hmono).ShortExact

              In the literal repeated-middle case, the finite double-cohook complex is short exact.

              source
              theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookMaximalFiniteShortComplex_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.CohookExtension corner) :
              QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (doubleCohookMaximalFiniteShortComplex leftCohook cornerRight ⋯).f

              The first differential of the double-cohook complex is irreducible without a middle-summand case hypothesis.

              source
              theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookMaximalFiniteShortComplex_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.CohookExtension corner) :
              QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (doubleCohookMaximalFiniteShortComplex leftCohook cornerRight ⋯).g

              The second differential of the double-cohook complex is irreducible without a middle-summand case hypothesis.

              source
              theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookMaximalFiniteShortComplex_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.CohookExtension corner) :
              (doubleCohookMaximalFiniteShortComplex leftCohook cornerRight ⋯).ShortExact

              The finite double-cohook complex is short exact without a middle-summand case hypothesis. Detector classification gives literal equality or reversal of the middle words, and reducedness of the common corner excludes reversal.

              source
              def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookDeletionCornerRightCohook {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) :
              leftDeletion.toLeftCohookExtension.result.CohookExtension C

              The right cohook reattachment in the manuscript's pair of deletion inputs, transported to the literal result of the left reattachment.

              Instances For
                source
                noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookDeletionMaximalFiniteShortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {C L D : Word R} (leftDeletion : L.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) (hmono : IsMonomial R) :
                CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

                The finite four-maximal-cohook complex in the manuscript's two-deletion input form.

                Instances For
                  source
                  theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookDeletionMaximalFiniteShortComplex_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 L D : Word P.relations} (leftDeletion : L.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) :
                  QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (doubleCohookDeletionMaximalFiniteShortComplex leftDeletion rightDeletion ⋯).f

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

                  source
                  theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookDeletionMaximalFiniteShortComplex_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 L D : Word P.relations} (leftDeletion : L.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) :
                  QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (doubleCohookDeletionMaximalFiniteShortComplex leftDeletion rightDeletion ⋯).g

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

                  source
                  theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.doubleCohookDeletionMaximalFiniteShortComplex_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 L D : Word P.relations} (leftDeletion : L.LeftCohookDeletion D) (rightDeletion : C.CohookDeletion L) :
                  (doubleCohookDeletionMaximalFiniteShortComplex leftDeletion rightDeletion ⋯).ShortExact

                  Two cohook deletions give the literal finite short exact double-cohook sequence, including the repeated-middle case.