compPreadditiveYonedaIso — Mathlib

English

Inverse Yoneda-type isomorphisms relate additive structures through adjunctions.

Русский

Обратные Йонадовы-изоморфизмы связывают аддитивные структуры через сопряжения.

LaTeX

$$$((adj.compPreadditiveYonedaIso.inv.app Y).app X) a = \text{...}$$$

Lean4

/-- If we have an adjunction `adj : F ⊣ G` of functors between preadditive categories,
and if `F` is additive, then the hom set equivalence upgrades to an isomorphism between
`G ⋙ preadditiveYoneda` and `preadditiveYoneda ⋙ F`, once we throw in the necessary
universe lifting functors.
Note that `F` is additive if and only if `G` is, by `Adjunction.right_adjoint_additive` and
`Adjunction.left_adjoint_additive`.
-/
def compPreadditiveYonedaIso :
    G ⋙ preadditiveYoneda ⋙ (whiskeringRight _ _ _).obj AddCommGrpCat.uliftFunctor.{max v₁ v₂} ≅
      preadditiveYoneda ⋙
        (whiskeringLeft _ _ _).obj F.op ⋙ (whiskeringRight _ _ _).obj AddCommGrpCat.uliftFunctor.{max v₁ v₂} :=
  NatIso.ofComponents
    (fun Y ↦
      NatIso.ofComponents
        (fun X ↦ (AddEquiv.ulift.trans ((adj.homAddEquiv (unop X) Y).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso)
        (fun g ↦ by
          ext ⟨y⟩
          exact AddEquiv.ulift.injective (adj.homEquiv_naturality_left_symm g.unop y)))
    (fun f ↦ by
      ext _ ⟨x⟩
      exact AddEquiv.ulift.injective ((adj.homEquiv_naturality_right_symm x f)))

Похожие утверждения