Coordinate thinness after finite-object reindexing #
An arbitrary finite object type is replaced by its small Fin model before
forming the category algebra. This file transports pointwise thinness to the
small model and then applies the canonical-projector coordinate theorem.
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finiteObjectModelThinFGHasFiniteBiproducts
{R : Type v}
[Ring R]
[IsNoetherianRing R]
:
CategoryTheory.Limits.HasFiniteBiproducts (FGModuleCat R)
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finiteObjectModelThinAlgebraFiniteDimensional
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
:
FiniteDimensional k (algebra ⋯)
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finiteObjectModelThinAlgebraOppositeIsNoetherian
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
:
IsNoetherianRing (algebra ⋯)ᵐᵒᵖ
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finiteObjectModelThinRightModuleHasFiniteBiproducts
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
:
CategoryTheory.Limits.HasFiniteBiproducts (RightModule.FinitelyGeneratedCategory (algebra ⋯))
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finiteObjectModelAlgebra_coordinateThin_of_pointwiseThin
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} 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 ⋯))
[CategoryTheory.Limits.HasBinaryBiproducts (RightModule.FinitelyGeneratedCategory (algebra ⋯))]
(hN : CategoryTheory.Indecomposable N)
:
Pointwise thinness of all indecomposable modules on a finite linear category makes every indecomposable right module over the category algebra of its small object model thin in every canonical primitive coordinate.