instIsIsoμ

Mathlib.CategoryTheory.Monoidal.Functor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Monoidal.instIsIsoμ

English

Another left whiskering coherence for δ and δ with associator.

Русский

Еще одно левое отведение δ и δ c ассоциатором.

LaTeX

$$$δ F X (Y ⊗ Z) \\circ F.obj X ◁ δ F Y Z = F.map (α_{X Y Z})^{-1} \\circ δ F (X ⊗ Y) Z \\circ δ F X Y ◁ F.obj Z \\circ α_{F X F Y F Z}^{hom}$$$

Lean4

instance (X Y : C) : IsIso (μ F X Y) :=
  (μIso F X Y).isIso_hom

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

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

Разделы

Аффилиация

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