toUnit_ε

Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Monoidal.toUnit_ε

← MathLib Explorer

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

@[reassoc (attr := simp)]
theorem toUnit_ε (X : C) : toUnit (F.obj X) ≫ ε F = F.map (toUnit X) := by rw [← cancel_mono (εIso F).inv];
  exact toUnit_unique ..

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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