Fully faithful linear extension to finite direct sums #
instance
MagnitudeConjecture.CategoryTheory.finiteMatrixLiftLinear
{k : Type w}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
(F : CategoryTheory.Functor C D)
[F.Additive]
[CategoryTheory.Functor.Linear k F]
:
CategoryTheory.Functor.Linear k (CoveringHom.finiteMatrixLift F)
noncomputable def
MagnitudeConjecture.CategoryTheory.finiteMatrixLiftEndAlgEquiv
{k : Type w}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
(F : CategoryTheory.Functor C D)
[F.Additive]
[F.Full]
[F.Faithful]
[CategoryTheory.Functor.Linear k F]
(X : CategoryTheory.Mat_ C)
:
CategoryTheory.End X ≃ₐ[k] CategoryTheory.End ((CoveringHom.finiteMatrixLift F).obj X)
The endomorphism algebra is preserved under fully faithful realization of the finite additive envelope.