Linear algebra comparison for finite representable sums #
instance
MagnitudeConjecture.CoveringHom.finiteRepresentableLinear
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
:
CategoryTheory.Functor.Linear k (finiteDimensionalLinearCoyonedaFunctor hP)
noncomputable def
MagnitudeConjecture.CoveringHom.finiteRepresentableSumEndAlgEquiv
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(X : CategoryTheory.Mat_ Cᵒᵖ)
:
CategoryTheory.End X ≃ₐ[k] CategoryTheory.End ((finiteMatrixLift (finiteDimensionalLinearCoyonedaFunctor hP)).obj X)
Endomorphism algebras of finite sums agree with their actual representable realization.