String classification on the quotient-category algebra skeleton

The quotient-category algebra is built from covariant representables, whereas the manuscript's literal right string modules are contravariant functors on the quotient category. The finite-category projective-generator equivalence therefore first pulls an algebra-module skeleton back to covariant quotient- category modules. Pointwise coefficient duality then transports that skeleton to the contravariant variance classified by literal strings.

Consequently each original algebra-skeleton object is represented by the reverse coefficient dual of one canonically selected literal string. This file keeps that duality explicit; it does not identify the two variances.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.algebraSkeletonClassificationFiniteDimensional {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) : FiniteDimensional k P.quotientCategoryAlgebra

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.algebraSkeletonClassificationNoetherian {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) : IsNoetherianRing P.quotientCategoryAlgebraᵐᵒᵖ

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.finiteCategoryModuleIndecomposableSkeleton {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) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton

Pull the chosen quotient-category algebra skeleton back to finite covariant modules on the quotient category.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.finiteCategoryModuleIndecomposableSkeletonObjIso {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) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (i : Fin T.n) : have hP := ⋯; (CoveringHom.finiteCategoryProjectiveGenerator.moduleEquivalence hP).functor.obj ((P.finiteCategoryModuleIndecomposableSkeleton T).obj i) ≅ T.fgObj i

The counit identifies a pulled-back covariant category-module skeleton object with the original quotient-algebra skeleton object.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.finiteCategoryDualModuleIndecomposableSkeleton {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) (T : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : StringWord.DetectorIndex.FiniteIndecomposableSkeleton

The coefficient-dual skeleton lies in the contravariant variance of the literal right string modules.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.algebraSkeletonDetectorIndex {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 : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (i : Fin T.n) : StringWord.DetectorIndex S

The detector index canonically selected for one quotient-algebra skeleton label after pullback and coefficient duality.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedAlgebraSkeletonStringDualIso {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 : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (i : Fin T.n) : have hP := ⋯; have L := (P.algebraSkeletonDetectorIndex S T i).endpointWord.word.finiteRightModule ⋯; (CoveringHom.finiteCategoryProjectiveGenerator.representedFGFunctor hP).obj (CoveringHom.reverseFiniteCoefficientDual L) ≅ T.fgObj i

Every object of the chosen quotient-algebra skeleton is the represented image of the reverse coefficient dual of a canonically selected literal string module.