Finite-dimensional string detector and embedding functors

This file restricts Butler--Ringel's finite-string functors to the categories used by finite reconstruction. A detector of a finite-dimensional module is finite-dimensional, and a finite coefficient space copied along a finite string again gives a finite-dimensional module.

For the chosen representatives of inversion classes, the coordinate calculation gives the natural finite-string orthogonality identities

F_i S_i ≅ id and F_i S_j ≅ 0 for i ≠ j.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorSpace_finiteDimensional {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} (C : EndpointWord S u₀ t) (N : CoveringHom.FiniteDimensionalModuleCategory k) : FiniteDimensional k (DetectorSpace N.obj.obj C)

A detector of a finite-dimensional module is a finite-dimensional vector space.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.finiteDetectorFunctor {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} (C : EndpointWord S u₀ t) : CategoryTheory.Functor (CoveringHom.FiniteDimensionalModuleCategory k) (FGModuleCat k)

The detector restricted to finite-dimensional modules and bundled with a finite-dimensional target.

instance MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.finiteDetectorFunctor_additive {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} (C : EndpointWord S u₀ t) : C.finiteDetectorFunctor.Additive

instance MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.finiteDetectorFunctor_linear {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} (C : EndpointWord S u₀ t) : CategoryTheory.Functor.Linear k C.finiteDetectorFunctor

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.finiteDetectorFunctor_obj_carrier {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} (C : EndpointWord S u₀ t) (N : CoveringHom.FiniteDimensionalModuleCategory k) : ↑(C.finiteDetectorFunctor.obj N) = DetectorSpace N.obj.obj C

@[instance_reducible]

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

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

The finite detector attached to a chosen inversion-class index.

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

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

instance MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteStringEmbeddingFunctor_additive {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} (i : DetectorIndex S) : i.finiteStringEmbeddingFunctor.Additive

instance MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteStringEmbeddingFunctor_linear {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} (i : DetectorIndex S) : CategoryTheory.Functor.Linear k i.finiteStringEmbeddingFunctor

instance MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteDetectorFunctor_additive {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} (i : DetectorIndex S) : i.finiteDetectorFunctor.Additive

instance MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteDetectorFunctor_linear {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} (i : DetectorIndex S) : CategoryTheory.Functor.Linear k i.finiteDetectorFunctor

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteDetectorEmbeddingFunctor {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} (i j : DetectorIndex S) : CategoryTheory.Functor (FGModuleCat k) (FGModuleCat k)

The composite F_i S_j on finite-dimensional coefficient spaces.

instance MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteDetectorEmbeddingFunctor_additive {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} (i j : DetectorIndex S) : (i.finiteDetectorEmbeddingFunctor j).Additive

instance MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteDetectorEmbeddingFunctor_linear {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} (i j : DetectorIndex S) : CategoryTheory.Functor.Linear k (i.finiteDetectorEmbeddingFunctor j)

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finrank_finiteDetectorFunctor_finiteStringEmbeddingFunctor_unit {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} (i j : DetectorIndex S) : Module.finrank k ↑(i.finiteDetectorFunctor.obj (j.finiteStringEmbeddingFunctor.obj (FGModuleCat.of k k))) = if i = j then 1 else 0

The finite detector and embedding functors satisfy the finite-string part of Butler--Ringel's orthogonality formula on the one-dimensional coefficient space.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finrank_finiteDetectorEmbeddingFunctor {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} (i j : DetectorIndex S) (V : FGModuleCat k) : Module.finrank k ↑((i.finiteDetectorEmbeddingFunctor j).obj V) = if i = j then Module.finrank k ↑V else 0

The full finite-string orthogonality formula: on every finite coefficient space V, F_i S_j(V) has dimension dim V on the matching inversion class and dimension zero off that class.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteDetectorEmbeddingFunctorUnitIso {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} (i : DetectorIndex S) : (i.finiteDetectorEmbeddingFunctor i).obj (FGModuleCat.of k k) ≅ FGModuleCat.of k k

The diagonal detector-embedding composite on the ground field is canonically one-dimensional, with coordinate given by the target position of the literal string.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteDetectorEmbeddingFunctorSelfIso {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} (i : DetectorIndex S) : i.finiteDetectorEmbeddingFunctor i ≅ CategoryTheory.Functor.id (FGModuleCat k)

Butler--Ringel's diagonal identity as a natural isomorphism: F_i S_i ≅ id on finite-dimensional coefficient spaces.

theorem MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteDetectorEmbeddingFunctor_subsingleton_of_ne {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} {i j : DetectorIndex S} (hij : i ≠ j) (V : FGModuleCat k) : Subsingleton ↑((i.finiteDetectorEmbeddingFunctor j).obj V)

Off the diagonal, F_i S_j(V) is the zero vector space.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.finiteDetectorEmbeddingFunctorZeroIsoOfNe {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} {i j : DetectorIndex S} (hij : i ≠ j) : i.finiteDetectorEmbeddingFunctor j ≅ (CategoryTheory.Functor.const (FGModuleCat k)).obj (FGModuleCat.of k PUnit.{u + 1})

Off the diagonal, the detector-embedding composite is naturally the zero functor.