String representations as finite-dimensional linear modules

The canonical position-basis representation of a string word was initially constructed as a raw functor. This file records that it is additive and linear, bundles it in the finite-dimensional module category, and exhibits a canonical nonzero coordinate. These are the ambient categorical interfaces needed by finite string reconstruction and the almost-split sequences.

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

The right-module realization preserves addition of morphisms.

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

The right-module realization preserves coefficient-field scalars.

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

The canonical string representation, bundled as a linear module.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightLinearModule_obj {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) (X : (Category R)ᵒᵖ) : (C.rightLinearModule hmono).obj.obj X = (C.rightModule hmono).obj X

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightModule_source_nontrivial {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (C : Word R) (hmono : IsMonomial R) : Nontrivial ↑((C.rightModule hmono).obj (Opposite.op (obj R C.source)))

The string representation is nonzero at its source endpoint.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.rightLinearModule_isFiniteDimensional {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (C : Word R) (hmono : IsMonomial R) : CoveringHom.IsFiniteDimensionalModule k (C.rightLinearModule hmono)

A string representation over a finite displayed quiver is pointwise finite-dimensional and has finite support.

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

The canonical string representation, bundled as a finite-dimensional linear module.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.finiteRightModule_obj {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} [Fintype Q] (C : Word R) (hmono : IsMonomial R) (X : (Category R)ᵒᵖ) : (C.finiteRightModule hmono).obj.obj.obj X = (C.rightModule hmono).obj X