instIsMonoidalInvFunctor — Mathlib

English

If e is a monoidal isomorphism between functors F1 ≅ F2, then its inverse e.inv is also monoidal.

Русский

Если e — моноидальное изоморфизм между функторaми F1 ≅ F2, то его обратный e.inv также моноидален.

LaTeX

$$IsMonoidal(e.inv)$$

Lean4

instance : NatTrans.IsMonoidal e.inv
    where
  unit := by rw [← NatTrans.IsMonoidal.unit (τ := e.hom), assoc, hom_inv_id_app, comp_id]
  tensor X
    Y := by
    rw [← cancel_mono (e.hom.app (X ⊗ Y)), assoc, assoc, inv_hom_id_app, comp_id, NatTrans.IsMonoidal.tensor,
      MonoidalCategory.tensorHom_comp_tensorHom_assoc, inv_hom_id_app, inv_hom_id_app, tensorHom_id, id_whiskerRight,
      id_comp]

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