Morphism spaces along a fully faithful linear functor

A fully faithful R-linear functor identifies the morphism space X ⟶ Y with F X ⟶ F Y as R-modules. Mathlib supplies the R-linear map CategoryTheory.Functor.mapLinearMap and, separately, the bijectivity of F.map; this file records the resulting R-linear isomorphism, which is what transports a dimension or a finiteness statement about a morphism space along the functor.

noncomputable def CategoryTheory.Functor.homLinearEquiv {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Preadditive C] [Preadditive D] (R : Type t) [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : Functor C D) [F.Additive] [Linear R F] [F.Full] [F.Faithful] (X Y : C) : (X ⟶ Y) ≃ₗ[R] F.obj X ⟶ F.obj Y

A fully faithful R-linear functor is an isomorphism on morphism spaces.

Equations

• CategoryTheory.Functor.homLinearEquiv R F X Y = LinearEquiv.ofBijective (CategoryTheory.Functor.mapLinearMap R F) ⋯

@[simp]

theorem CategoryTheory.Functor.homLinearEquiv_apply {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Preadditive C] [Preadditive D] (R : Type t) [Semiring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : Functor C D) [F.Additive] [Linear R F] [F.Full] [F.Faithful] {X Y : C} (f : X ⟶ Y) : (homLinearEquiv R F X Y) f = F.map f