Simple-module counts for finite skeletal category algebras #
theorem
MagnitudeConjecture.CoveringHom.simpleCountCategoryAlgebraFinite
{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 (finiteCategoryProjectiveGenerator.algebra hP)
theorem
MagnitudeConjecture.CoveringHom.simpleCountCategoryAlgebraNoetherian
{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 (finiteCategoryProjectiveGenerator.algebra hP)ᵐᵒᵖ
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryAlgebra_simpleCount
{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))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(hskel : CategoryTheory.Skeletal C)
(S : RightModule.FiniteIndecomposableSkeleton k (finiteCategoryProjectiveGenerator.algebra hP))
:
S.simpleCount = Fintype.card C
Local endomorphism rings and skeletal objects identify the simple classes of the category algebra with the objects of the category.
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryAlgebra_simpleCount_of_algEquiv
{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))
{A : Type u}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(f : A ≃ₐ[k] finiteCategoryProjectiveGenerator.algebra hP)
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(hskel : CategoryTheory.Skeletal C)
(S : RightModule.FiniteIndecomposableSkeleton k A)
:
S.simpleCount = Fintype.card C
The count applies to any algebra identified with the representable model, including the finite matrix model.