Pointwise thin category modules and primitive algebra coordinates #
The projective-generator equivalence for a finite linear category identifies the value of a category module at an object with the coordinate of the corresponding right module at the canonical summand projector. Consequently, pointwise thinness of all indecomposable category modules is exactly the coordinate-thin premise needed on the finite category algebra.
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.thinAlgebraFiniteDimensional
{k : Type u}
[Field k]
{C : Type}
[CategoryTheory.Category.{u, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
:
FiniteDimensional k (algebra hP)
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.thinAlgebraOppositeIsNoetherian
{k : Type u}
[Field k]
{C : Type}
[CategoryTheory.Category.{u, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
:
IsNoetherianRing (algebra hP)ᵐᵒᵖ
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebra_coordinateThin_of_pointwiseThin
{k : Type u}
[Field k]
{C : Type}
[CategoryTheory.Category.{u, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hthin : ∀ (M : FiniteDimensionalModuleCategory k), CategoryTheory.Indecomposable M → IsPointwiseThin M.obj.obj)
(N : RightModule.FinitelyGeneratedCategory (algebra hP))
(hN : CategoryTheory.Indecomposable N)
:
If every indecomposable finite-dimensional category module is pointwise thin, then every indecomposable finitely generated right module over the finite category algebra is thin in all canonical primitive coordinates.