instIsIsoη

Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.OplaxMonoidal.instIsIsoη

English

If F preserves finite products, then η F is an isomorphism (hence η F is invertible).

Русский

Если F сохраняет конечные произведения, то η F является изоморфизмом (обратим).

LaTeX

$$$IsIso(\eta F)$$$

Lean4

instance : IsIso (η F) :=
  η_of_cartesianMonoidalCategory F ▸ terminalComparison_isIso_of_preservesLimits F

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

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

Разделы

Аффилиация

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