Linear Hom equivalences from adjunctions #
An adjunction between preadditive linear categories gives an additive equivalence between its Hom groups when the left adjoint is additive. If the left adjoint is also linear, naturality in the source upgrades that equivalence to a linear equivalence.
Only the left adjoint needs a linearity hypothesis: scalar multiplication on a morphism out of
F.obj X is rewritten as precomposition by F.map (r • 𝟙 X).
noncomputable def
CategoryTheory.Adjunction.homLinearEquiv
{R : Type w}
[Semiring R]
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₂, u₂} D]
[Preadditive C]
[Preadditive D]
[Linear R C]
[Linear R D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.Additive]
[Functor.Linear R F]
(X : C)
(Y : D)
:
The Hom equivalence of an additive adjunction is linear when its left adjoint is linear.
Equations
- adj.homLinearEquiv X Y = { toFun := (adj.homAddEquiv X Y).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (adj.homAddEquiv X Y).invFun, left_inv := ⋯, right_inv := ⋯ }