Endomorphism rings under fully faithful additive functors

A fully faithful functor F gives Mathlib's monoid isomorphism CategoryTheory.Functor.FullyFaithful.mulEquivEnd : End X ≃* End (F.obj X). When F is additive between preadditive categories, it is a ring isomorphism (CategoryTheory.Functor.FullyFaithful.ringEquivEnd). This transports ring-theoretic properties of endomorphism rings, such as being local or Artinian, along the inclusion of a full subcategory or along an equivalence.

noncomputable def CategoryTheory.Functor.FullyFaithful.ringEquivEnd {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] {F : Functor C D} [F.Additive] (hF : F.FullyFaithful) (X : C) : End X ≃+* End (F.obj X)

A fully faithful additive functor F induces a ring isomorphism End X ≃+* End (F.obj X), the additive version of CategoryTheory.Functor.FullyFaithful.mulEquivEnd.

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.ringEquivEnd_apply_asHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] {F : Functor C D} [F.Additive] (hF : F.FullyFaithful) (X : C) (f : End X) : ((hF.ringEquivEnd X) f).asHom = F.map f.asHom

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.ringEquivEnd_symm_apply_asHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] {F : Functor C D} [F.Additive] (hF : F.FullyFaithful) (X : C) (g : End (F.obj X)) : ((hF.ringEquivEnd X).symm g).asHom = hF.preimage g.asHom