of_iso_inv — Mathlib

English

Let e: F1 ≅ F2 be an isomorphism of functors with a commShift structure; then the corresponding inverse NatTrans.CommShift e.inv A exists, making e.inv a shift-compatible natural transformation as well.

Русский

Пусть e: F1 ≅ F2 — изоморфизм функторов с CommShift; тогда существет NatTrans.CommShift e.inv A, делающий обратный изоморфизм совместимым со сдвигами.

LaTeX

$$$\\text{NatTrans.CommShift } (e.inv)\\ A$$$

Lean4

instance of_iso_inv [NatTrans.CommShift e.hom A] : NatTrans.CommShift e.inv A :=
  ⟨fun a => by
    ext X
    dsimp
    rw [← cancel_epi (e.hom.app (X⟦a⟧)), e.hom_inv_id_app_assoc, ← shift_app_comm_assoc, ← Functor.map_comp,
      e.hom_inv_id_app, Functor.map_id, Category.comp_id]⟩

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