instIsIsoδ

Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

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

English

If F preserves finite products, then δ F X Y is an isomorphism for all X,Y.

Русский

Если F сохраняет конечные произведения, то δ F X Y является изоморфизмом для всех X,Y.

LaTeX

$$$IsIso(\delta F X Y)$$$

Lean4

instance (X Y : C) : IsIso (δ F X Y) :=
  δ_of_cartesianMonoidalCategory F X Y ▸ isIso_prodComparison_of_preservesLimit_pair F X Y

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

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

Разделы

Аффилиация

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