Indices for finite-string detectors

Butler--Ringel choose one representative of string words modulo formal inversion. This file packages the endpoint-polarized words, defines that equivalence relation through their underlying literal words, and attaches the already constructed detector functor to a chosen representative of each quotient class.

The quotient identifies the two polarized length-zero words at a vertex, since they are formal inverses in the source convention. No band indices are needed: finite detector reconstruction directly proves object coverage in the representation-finite branch.

def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.ofWord {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) (C : Word P.relations) : EndpointWord S C.target (signedPathTargetSignOr S false C.path)

Give an arbitrary literal word its intrinsic target sign. For the empty word we choose false; the quotient index below identifies this choice with the oppositely polarized trivial word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.ofWord_word {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) (C : Word P.relations) : (ofWord S C).word = C

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.word_injective {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) {u : Q} {t : Bool} : Function.Injective word

Forgetting a fixed endpoint polarization is injective on endpoint words.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringWord.DetectorWord {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) : Type u

All endpoint-polarized finite string words.

def MagnitudeConjecture.BoundQuiver.StringWord.DetectorWord.underlying {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} (C : DetectorWord S) : Word P.relations

Forget the endpoint and sign indices.

def MagnitudeConjecture.BoundQuiver.StringWord.DetectorWord.ofWord {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) (C : Word P.relations) : DetectorWord S

Regard an arbitrary literal word as a detector word.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorWord.ofWord_underlying {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) (C : Word P.relations) : (ofWord S C).underlying = C

def MagnitudeConjecture.BoundQuiver.StringWord.DetectorWord.InverseEquivalent {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} (C D : DetectorWord S) : Prop

Equivalence of detector words under formal inversion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorWord.inverseEquivalent_refl {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} (C : DetectorWord S) : C.InverseEquivalent C

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorWord.inverseEquivalent_symm {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} {C D : DetectorWord S} (h : C.InverseEquivalent D) : D.InverseEquivalent C

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorWord.inverseEquivalent_trans {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} {C D E : DetectorWord S} (hCD : C.InverseEquivalent D) (hDE : D.InverseEquivalent E) : C.InverseEquivalent E

def MagnitudeConjecture.BoundQuiver.StringWord.DetectorWord.inverseSetoid {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) : Setoid (DetectorWord S)

Setoid of finite strings modulo formal inversion.

def MagnitudeConjecture.BoundQuiver.StringWord.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) : Type u

The index type for finite-string detecting functors.

def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.ofWord {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) (C : Word P.relations) : DetectorIndex S

The detector index of a literal word.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.ofWord_reverse {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) (C : Word P.relations) : ofWord S (Word.reverse P.relations C) = ofWord S C

A word and its formal inverse determine the same detector index.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.ofWord_eq_iff {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) (C D : Word P.relations) : ofWord S C = ofWord S D ↔ C = D ∨ C = Word.reverse P.relations D

Equality of word indices is exactly equality up to formal inversion.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.ofWord_surjective {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) : Function.Surjective (ofWord S)

Every finite-string detector index is represented by a literal word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.representative {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} (i : DetectorIndex S) : DetectorWord S

A noncanonical representative of a detector index, matching the source's choice of a representative set.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.mk_representative {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} (i : DetectorIndex S) : Quotient.mk'' i.representative = i

The chosen representative belongs to the requested quotient class.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.endpointWord {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} (i : DetectorIndex S) : EndpointWord S i.representative.fst i.representative.snd.fst

The endpoint-polarized word selected by an index.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.ofWord_endpointWord {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} (i : DetectorIndex S) : ofWord S i.endpointWord.word = i

Reindexing the underlying word of the chosen representative recovers the original detector index.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.detectorFunctor {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} (i : DetectorIndex S) : CategoryTheory.Functor (CoveringHom.LinearModuleCategory k) (ModuleCat k)

The finite-string detector attached to the chosen representative of an inversion class.