evalHorizontalCompAux'_whisker

Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Monoidal.evalHorizontalCompAux'_whisker

Lean4

theorem evalHorizontalCompAux'_whisker {f f' g g' h : C} {η : g ⟶ h} {θ : f' ⟶ g'} {ηθ : g ⊗ f' ⟶ h ⊗ g'}
    {η₁ : f ⊗ (g ⊗ f') ⟶ f ⊗ (h ⊗ g')} {η₂ : f ⊗ (g ⊗ f') ⟶ (f ⊗ h) ⊗ g'} {η₃ : (f ⊗ g) ⊗ f' ⟶ (f ⊗ h) ⊗ g'}
    (e_ηθ : η ⊗ₘ θ = ηθ) (e_η₁ : f ◁ ηθ = η₁) (e_η₂ : η₁ ≫ (α_ _ _ _).inv = η₂) (e_η₃ : (α_ _ _ _).hom ≫ η₂ = η₃) :
    (f ◁ η) ⊗ₘ θ = η₃ := by
  simp only [← e_ηθ, ← e_η₁, ← e_η₂, ← e_η₃]
  simp [MonoidalCategory.tensorHom_def]

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

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

Разделы

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

Аффилиация

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