evalHorizontalComp_cons_cons

Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

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

Lean4

theorem evalHorizontalComp_cons_cons {f f' g g' h h' i i' : C} {α : f ≅ g} {η : g ⟶ h} {ηs : h ⟶ i} {β : f' ≅ g'}
    {θ : g' ⟶ h'} {θs : h' ⟶ i'} {ηθ : g ⊗ g' ⟶ h ⊗ h'} {ηθs : h ⊗ h' ⟶ i ⊗ i'} {ηθ₁ : g ⊗ g' ⟶ i ⊗ i'}
    {ηθ₂ : f ⊗ f' ⟶ i ⊗ i'} (e_ηθ : η ⊗ₘ θ = ηθ) (e_ηθs : ηs ⊗ₘ θs = ηθs) (e_ηθ₁ : ηθ ≫ ηθs = ηθ₁)
    (e_ηθ₂ : (α ⊗ᵢ β).hom ≫ ηθ₁ = ηθ₂) : (α.hom ≫ η ≫ ηs) ⊗ₘ (β.hom ≫ θ ≫ θs) = ηθ₂ := by
  simp [← e_ηθ, ← e_ηθs, ← e_ηθ₁, ← e_ηθ₂]

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

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

Разделы

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

Аффилиация

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