triangle_aux₂

Mathlib.CategoryTheory.Localization.Monoidal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.Monoidal.triangle_aux₂

Lean4

theorem triangle_aux₂ {X Y : LocalizedMonoidal L W ε} {X' Y' : C} (e₁ : (L').obj X' ≅ X) (e₂ : (L').obj Y' ≅ Y) :
    e₁.hom ⊗ₘ (ε.hom ⊗ₘ e₂.hom) ≫ (λ_ Y).hom =
      (L').obj X' ◁ ((ε' L W ε).hom ▷ (L').obj Y' ≫ 𝟙_ _ ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y :=
  by
  simp only [← tensorHom_id, ← id_tensorHom, ← tensor_comp, comp_id, id_comp, ← tensor_comp_assoc, id_comp]
  congr 3
  exact (comp_id _).symm

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

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

Разделы

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

Аффилиация

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