Magnitude conjecture

MagnitudeConjecture.Algebra.StringDetectorFiniteIndex

Finiteness of the detector index in finite representation type #

The literal string module attached to a detector index is indecomposable. A finite complete indecomposable skeleton therefore assigns it a skeleton label. The diagonal/off-diagonal detector calculation shows that two indices with the same label must coincide. Thus the full family of finite-string detectors is finite in the representation-finite setting.

source
@[reducible, inline]
abbrev MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.FiniteIndecomposableSkeleton {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} :
Type (u + 1)
Instances For
    source
    noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteSkeletonLabel {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} {S : P.ArrowPolarization} (T : FiniteIndecomposableSkeleton) (i : DetectorIndex S) :
    Fin T.n

    A chosen skeleton label for the literal string module represented by a detector index.

    Instances For
      source
      noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteSkeletonIso {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} {S : P.ArrowPolarization} (T : FiniteIndecomposableSkeleton) (i : DetectorIndex S) :
      i.endpointWord.word.finiteRightModule ⋯ ≅ T.obj (finiteSkeletonLabel T i)

      The chosen isomorphism from a literal string module to its finite-skeleton representative.

      Instances For
        source
        theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteSkeletonLabel_injective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} {S : P.ArrowPolarization} (T : FiniteIndecomposableSkeleton) :
        Function.Injective (finiteSkeletonLabel T)

        Distinct detector indices have distinct labels in any complete indecomposable skeleton.

        source
        theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finite_of_finiteIndecomposableSkeleton {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} {S : P.ArrowPolarization} (T : FiniteIndecomposableSkeleton) :
        Finite (DetectorIndex S)

        In finite representation type, the entire inversion-class index of finite-string detectors is finite.

        source
        theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finite_word_of_finite_detectorIndex {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} [Finite (DetectorIndex S)] :
        Finite (Word P.relations)

        If the inversion classes of finite string words are finite, then the literal string words themselves are finite. Each inversion class contains at most the chosen representative and its formal inverse.

        source
        theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finite_endpointWord_of_finite_detectorIndex {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} [Finite (DetectorIndex S)] (u : Q) (t : Bool) :
        Finite (EndpointWord S u t)

        Finiteness of literal words also gives finiteness of every fixed endpoint-polarized word family.

        source
        theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.exists_word_length_bound_of_finite_detectorIndex {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} [Finite (DetectorIndex S)] :
        ∃ (L : ℕ), ∀ (C : Word P.relations), Word.length P.relations C ≤ L

        A finite detector index supplies a uniform bound on the length of every literal string word.

        source
        theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.natCard_le_skeleton {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} {S : P.ArrowPolarization} (T : FiniteIndecomposableSkeleton) :
        Nat.card (DetectorIndex S) ≤ T.n

        The number of finite-string detector indices is bounded by the number of indecomposable representatives in a complete finite skeleton.