Magnitude conjecture

MagnitudeConjecture.Algebra.StringFinitePureOneSidedHook

Unary boundary complexes for pure string endpoints #

A pure-positive string which is maximal at its right endpoint but has a left hook has a one-middle Butler--Ringel boundary complex. The kernel of the left-hook projection is the positive arm before its first negative letter; its inclusion is a maximal right cohook. This file constructs that kernel word, proves the resulting coordinate sequence short exact, and proves both differentials irreducible in the finite module category.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.spaceProjection_spaceInclusion_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {K C : Word R} (left : C.LeftPositiveBoundaryExtension) (cohook : K.CohookExtension left.result) (hcutoff : length R K + 1 = left.steps) (x : Q) :

left.spaceProjection x ∘ₗ cohook.toNegativeBoundaryExtension.toRightExtension.spaceInclusion x = 0

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.moduleMap_comp_leftBoundaryModuleMap_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {K C : Word R} (left : C.LeftPositiveBoundaryExtension) (cohook : K.CohookExtension left.result) (hcutoff : length R K + 1 = left.steps) (hmono : IsMonomial R) :

CategoryTheory.CategoryStruct.comp (cohook.moduleMap hmono) (left.moduleMap hmono) = 0

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.prefixSuffixSpaceMap_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {K C : Word R} (left : C.LeftPositiveBoundaryExtension) (cohook : K.CohookExtension left.result) (hcutoff : length R K + 1 = left.steps) (x : Q) :

Function.Exact ⇑(cohook.toNegativeBoundaryExtension.toRightExtension.spaceInclusion x) ⇑(left.spaceProjection x)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.prefixSuffixShortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {K C : Word R} (left : C.LeftPositiveBoundaryExtension) (cohook : K.CohookExtension left.result) (hcutoff : length R K + 1 = left.steps) (hmono : IsMonomial R) :

CategoryTheory.ShortComplex (CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k))

Instances For

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.prefixSuffixShortComplex_exact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {K C : Word R} (left : C.LeftPositiveBoundaryExtension) (cohook : K.CohookExtension left.result) (hcutoff : length R K + 1 = left.steps) (hmono : IsMonomial R) :

(prefixSuffixShortComplex left cohook hcutoff hmono).Exact

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.prefixSuffixShortComplex_shortExact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {K C : Word R} (left : C.LeftPositiveBoundaryExtension) (cohook : K.CohookExtension left.result) (hcutoff : length R K + 1 = left.steps) (hmono : IsMonomial R) :

(prefixSuffixShortComplex left cohook hcutoff hmono).ShortExact

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.PurePositiveKernelData {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (left : C.LeftHookExtension) :

kernel : Word R
cohook : self.kernel.CohookExtension left.toLeftPositiveBoundaryExtension.result
cutoff : length R self.kernel + 1 = left.toLeftPositiveBoundaryExtension.steps

Instances For

def MagnitudeConjecture.BoundQuiver.StringWord.Word.HookExtension.toReverseLeftHook {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C D : Word R} (hook : C.HookExtension D) :

(reverse R C).LeftHookExtension

Regard a right hook on C as a left hook on the reversed word.

Instances For

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.result_startsOnPeak_of_startsOnPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {C : Word R} (left : C.LeftHookExtension) (hstart : C.StartsOnPeak) :

left.result.StartsOnPeak

Extending a word at its left endpoint preserves a peak at its right endpoint.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.purePositiveKernelDataOfResultPeak {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) {C : Word R} (hpure : IsPurePositive hR C) (left : C.LeftHookExtension) (hresultPeak : left.result.StartsOnPeak) :

PurePositiveKernelData C left

Construct the cohook kernel of a pure-positive left-hook projection when the hooked result is maximal at its right endpoint.

Instances For

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.purePositiveKernelData {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) {C : Word R} (hpure : IsPurePositive hR C) (hstart : C.StartsOnPeak) (left : C.LeftHookExtension) :

PurePositiveKernelData C left

The kernel data in the common one-sided case where the original pure word is already maximal at its right endpoint.

Instances For

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.prefixSuffixFiniteShortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {K C : Word R} (left : C.LeftPositiveBoundaryExtension) (cohook : K.CohookExtension left.result) (hcutoff : length R K + 1 = left.steps) (hmono : IsMonomial R) :

CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

Instances For

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.CohookExtension.prefixSuffixFiniteShortComplex_shortExact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] {K C : Word R} (left : C.LeftPositiveBoundaryExtension) (cohook : K.CohookExtension left.result) (hcutoff : length R K + 1 = left.steps) (hmono : IsMonomial R) :

(prefixSuffixFiniteShortComplex left cohook hcutoff hmono).ShortExact

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.purePositiveResultPeakFiniteShortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (hR : IsAdmissible R) {C : Word R} (hpure : IsPurePositive hR C) (left : C.LeftHookExtension) (hresultPeak : left.result.StartsOnPeak) (hmono : IsMonomial R) :

CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

The unary finite complex whenever the pure-positive hook result is a peak at its right endpoint.

Instances For

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.purePositiveResultPeakFiniteShortComplex_shortExact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (hR : IsAdmissible R) {C : Word R} (hpure : IsPurePositive hR C) (left : C.LeftHookExtension) (hresultPeak : left.result.StartsOnPeak) (hmono : IsMonomial R) :

(purePositiveResultPeakFiniteShortComplex hR hpure left ⋯ hmono).ShortExact

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.purePositiveResultPeakFiniteShortComplex_f_isIrreducible {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (hR : IsAdmissible R) {C : Word R} (hpure : IsPurePositive hR C) (left : C.LeftHookExtension) (hresultPeak : left.result.StartsOnPeak) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) :

QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (purePositiveResultPeakFiniteShortComplex hR hpure left ⋯ hmono).f

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.purePositiveResultPeakFiniteShortComplex_g_isIrreducible {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (hR : IsAdmissible R) {C : Word R} (hpure : IsPurePositive hR C) (left : C.LeftHookExtension) (hresultPeak : left.result.StartsOnPeak) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) :

QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (purePositiveResultPeakFiniteShortComplex hR hpure left ⋯ hmono).g

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.purePositiveFiniteShortComplex {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (hR : IsAdmissible R) {C : Word R} (hpure : IsPurePositive hR C) (hstart : C.StartsOnPeak) (left : C.LeftHookExtension) (hmono : IsMonomial R) :

CategoryTheory.ShortComplex (CoveringHom.FiniteDimensionalModuleCategory k)

Instances For

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.purePositiveFiniteShortComplex_shortExact {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (hR : IsAdmissible R) {C : Word R} (hpure : IsPurePositive hR C) (hstart : C.StartsOnPeak) (left : C.LeftHookExtension) (hmono : IsMonomial R) :

(purePositiveFiniteShortComplex hR hpure ⋯ left hmono).ShortExact

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.purePositiveFiniteShortComplex_f_isIrreducible {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (hR : IsAdmissible R) {C : Word R} (hpure : IsPurePositive hR C) (hstart : C.StartsOnPeak) (left : C.LeftHookExtension) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) :

QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (purePositiveFiniteShortComplex hR hpure ⋯ left hmono).f

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.LeftHookExtension.purePositiveFiniteShortComplex_g_isIrreducible {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (hR : IsAdmissible R) {C : Word R} (hpure : IsPurePositive hR C) (hstart : C.StartsOnPeak) (left : C.LeftHookExtension) (hmono : IsMonomial R) (hcover : EveryFiniteModuleIsFiniteStringSum hmono) :

QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (purePositiveFiniteShortComplex hR hpure ⋯ left hmono).g