A matrix additive model of the finite category algebra #
def
MagnitudeConjecture.CoveringHom.categoryAlgebraTuple
{C : Type}
[Fintype C]
:
CategoryTheory.Mat_ Cᵒᵖ
The tuple representing the sum of all covariant representables.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.categoryAlgebraTupleEquiv
{k : Type v}
[Field k]
{C : Type}
[CategoryTheory.Category.{v, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
:
CategoryTheory.End categoryAlgebraTuple ≃ₐ[k] finiteCategoryProjectiveGenerator.algebra hP
The existing category algebra equals the realized tuple's endomorphism algebra.