Fully faithful linear functors on finite matrix objects #
instance
MagnitudeConjecture.CategoryTheory.matrixFunctor_additive
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v, u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[F.Additive]
:
F.mapMat_.Additive
instance
MagnitudeConjecture.CategoryTheory.matrixFunctor_linear
{k : Type v}
[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]
(F : CategoryTheory.Functor C D)
[F.Additive]
[CategoryTheory.Functor.Linear k F]
:
CategoryTheory.Functor.Linear k F.mapMat_
instance
MagnitudeConjecture.CategoryTheory.matrixFunctor_faithful
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v, u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[F.Additive]
[F.Faithful]
:
F.mapMat_.Faithful
instance
MagnitudeConjecture.CategoryTheory.matrixFunctor_full
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{D : Type u'}
[CategoryTheory.Category.{v, u'} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[F.Additive]
[F.Full]
:
F.mapMat_.Full
noncomputable def
MagnitudeConjecture.CategoryTheory.matrixFunctorEndAlgEquiv
{k : Type v}
[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]
(F : CategoryTheory.Functor C D)
[F.Additive]
[CategoryTheory.Functor.Linear k F]
[F.Full]
[F.Faithful]
(X : CategoryTheory.Mat_ C)
:
CategoryTheory.End X ≃ₐ[k] CategoryTheory.End (F.mapMat_.obj X)
Entrywise transport along a fully faithful linear functor preserves the finite matrix object's endomorphism algebra.