associator_naturality₃ — Mathlib

English

Coherence of associator in the presence of whiskers and localization.

Русский

Когерентность ассоциатора в присутствии whisker и локализации.

LaTeX

$$$\\text{as before}$$$

Lean4

@[reassoc]
theorem associator_naturality₃ {X₁ X₂ X₃ Y₃ : LocalizedMonoidal L W ε} (f₃ : X₃ ⟶ Y₃) :
    ((X₁ ⊗ X₂) ◁ f₃) ≫ (α_ X₁ X₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (X₁ ◁ (X₂ ◁ f₃)) := by
  simp only [← id_tensorHom, ← id_tensorHom_id, associator_naturality]

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