instIsIsoδ

Mathlib.CategoryTheory.Monoidal.Functor

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

English

General δ coherence in oplax setting with left/right whiskering and associator.

Русский

Обобщенная когерентность δ в условиях oplax с левым/правым отводом и ассоциатором.

LaTeX

$$$δ F X (Y ⊗ Z) ≫ δ F X Y ⊗ Z = F.map (associator) ≫ δ F X (Y ⊗ Z) ≫ δ F Y Z ≫ (associator)^{-1}$$$

Lean4

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

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

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

Разделы

Аффилиация

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