The finite-string embedding functor

For a literal string word C, Butler--Ringel's functor S_C replaces every one-dimensional position of the literal string module by a copy of a supplied vector space. Concretely, its value at a quiver vertex x is

C.Space x ⊗ V,

and an arrow acts by the literal string arrow map tensored with the identity of V. Defining this after the string representation has descended through the relation quotient makes the relation check automatic.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.scalarRightModule {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (V : ModuleCat k) : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)

The right module obtained by replacing each position basis line of a literal string module by a copy of V.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.scalarRightModule_additive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (V : ModuleCat k) : (C.scalarRightModule hmono V).Additive

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.scalarRightModule_linear {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (V : ModuleCat k) : CategoryTheory.Functor.Linear k (C.scalarRightModule hmono V)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.scalarRightModule_map_pathMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (V : ModuleCat k) {x y : Q} (p : Quiver.Path x y) : (C.scalarRightModule hmono V).map (pathMap R p).op = CategoryTheory.MonoidalCategoryStruct.whiskerRight (C.quiverMap p) V

The coefficient-copy string module evaluates a quotient path by the literal string path map tensored with the identity of the coefficient space.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.scalarRightLinearModule {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (V : ModuleCat k) : CoveringHom.LinearModuleCategory k

The scalar-copy string representation as a bundled linear module.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.scalarRightLinearModule_obj {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (V : ModuleCat k) (X : (Category R)ᵒᵖ) : (C.scalarRightLinearModule hmono V).obj.obj X = CategoryTheory.MonoidalCategoryStruct.tensorObj ((C.rightModule hmono).obj X) V

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.scalarRightLinearModuleUnitIso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : C.scalarRightLinearModule hmono (ModuleCat.of k k) ≅ C.rightLinearModule hmono

Replacing each position line by the one-dimensional vector space recovers the literal string module.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.stringEmbeddingFunctor {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : CategoryTheory.Functor (ModuleCat k) (CoveringHom.LinearModuleCategory k)

Butler--Ringel's finite-string embedding functor S_C.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.stringEmbeddingFunctor_additive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : (C.stringEmbeddingFunctor hmono).Additive

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.stringEmbeddingFunctor_linear {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : CategoryTheory.Functor.Linear k (C.stringEmbeddingFunctor hmono)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.stringEmbeddingFunctor_obj_obj {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (V : ModuleCat k) (X : (Category R)ᵒᵖ) : ((C.stringEmbeddingFunctor hmono).obj V).obj.obj X = CategoryTheory.MonoidalCategoryStruct.tensorObj ((C.rightModule hmono).obj X) V

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.stringEmbeddingFunctor_map_app {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) {V W : ModuleCat k} (f : V ⟶ W) (X : (Category R)ᵒᵖ) : ((C.stringEmbeddingFunctor hmono).map f).hom.app X = CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((C.rightModule hmono).obj X) f

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.scalarRightLinearModule_isFiniteDimensional {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (C : Word R) (hmono : IsMonomial R) (V : FGModuleCat k) : CoveringHom.IsFiniteDimensionalModule k (C.scalarRightLinearModule hmono V.obj)

Scalar-copy string modules are finite-dimensional when the coefficient space is finite-dimensional.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.scalarFiniteRightModule {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (C : Word R) (hmono : IsMonomial R) (V : FGModuleCat k) : CoveringHom.FiniteDimensionalModuleCategory k

The scalar-copy string module bundled in the finite-dimensional module category.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteStringEmbeddingFunctor {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (C : Word R) (hmono : IsMonomial R) : CategoryTheory.Functor (FGModuleCat k) (CoveringHom.FiniteDimensionalModuleCategory k)

The finite-dimensional restriction of Butler--Ringel's embedding functor.

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteStringEmbeddingFunctor_additive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (C : Word R) (hmono : IsMonomial R) : (C.finiteStringEmbeddingFunctor hmono).Additive

instance MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteStringEmbeddingFunctor_linear {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (C : Word R) (hmono : IsMonomial R) : CategoryTheory.Functor.Linear k (C.finiteStringEmbeddingFunctor hmono)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.scalarFiniteRightModuleUnitIso {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (C : Word R) (hmono : IsMonomial R) : C.scalarFiniteRightModule hmono (FGModuleCat.of k k) ≅ C.finiteRightModule hmono

On the one-dimensional coefficient space, the finite embedding functor recovers the literal finite string module.