naturality_whiskerLeft

Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Monoidal.naturality_whiskerLeft

Lean4

theorem naturality_whiskerLeft {p f g h pf pfg : C} {η : g ≅ h} (η_f : p ⊗ f ≅ pf) (η_fg : pf ⊗ g ≅ pfg)
    (η_fh : (pf ⊗ h) ≅ pfg) (ih_η : pf ◁ η ≪≫ η_fh = η_fg) :
    p ◁ (f ◁ η) ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f η_fg :=
  by
  rw [← ih_η]
  apply Iso.ext
  simp [← whisker_exchange_assoc]

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

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

Разделы

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

Аффилиация

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