English
Let e: C ≅ D be a monoidal equivalence between monoidal categories. Then the inverse equivalence e^{-1}: D ≅ C is also a monoidal equivalence.
Русский
Пусть e: C ≅ D — моноидальное эквивалентность между моноидальными категориями. Тогда обратная эквивалентность e^{-1}: D ≅ C также является моноидальной эквивалентностью.
LaTeX
$$$IsMonoidal(e^{-1})$$$
Lean4
/-- The inverse of a monoidal category equivalence is also a monoidal category equivalence. -/
instance isMonoidal_symm [e.inverse.Monoidal] [e.IsMonoidal] : e.symm.IsMonoidal
where
leftAdjoint_ε := by
simp only [toAdjunction, Adjunction.homEquiv_unit]
dsimp [symm]
rw [counitIso_inv_app_comp_functor_map_η_inverse]
leftAdjoint_μ X
Y := by
simp only [toAdjunction, Adjunction.homEquiv_unit]
dsimp [symm]
rw [map_comp, counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc]
simp [← map_comp]
