of_isIso — Mathlib

English

If e: F1 ≅ F2 is an isomorphism and F1, F2 have a shift structure, and e.hom is a CommShift, then the inverse morphism e.inv also carries a CommShift structure, giving a NatTrans.CommShift e.inv A.

Русский

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

LaTeX

$$$[NatTrans.CommShift e.inv A]$$$

Lean4

theorem of_isIso [IsIso τ] [NatTrans.CommShift τ A] : NatTrans.CommShift (inv τ) A :=
  by
  haveI : NatTrans.CommShift (asIso τ).hom A := by assumption
  change NatTrans.CommShift (asIso τ).inv A
  infer_instance

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