Algebra equivalences from finite linear category equivalences

noncomputable def MagnitudeConjecture.CoveringHom.categoryAlgebraMatrixEquiv {k : Type v} [Field k] {C D : Type} [CategoryTheory.Category.{v, 0} C] [CategoryTheory.Category.{v, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [Fintype C] [Fintype D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] (hobj : Function.Bijective F.obj) : CategoryTheory.End categoryAlgebraTuple ≃ₐ[k] CategoryTheory.End categoryAlgebraTuple

A fully faithful linear functor bijective on objects identifies the finite matrix category algebras.