instMonoidalOppositeMop

Mathlib.CategoryTheory.Monoidal.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsIso.instMonoidalOppositeMop

English

If f : X ≅ Y is an iso in C, then f.mop : mop X ≅ mop Y is an isomorphism in the monoidal opposite setting.

Русский

Если f : X ≅ Y изоморфизм в C, то f.mop : mop X ≅ mop Y является изоморфизмом в моноидальном противоположном контексте.

LaTeX

$$IsIso(f.mop)$$

Lean4

instance {X Y : C} (f : X ⟶ Y) [IsIso f] : IsIso f.mop :=
  (mopFunctor C).map_isIso f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru