pentagon_aux₁ — Mathlib

English

Three-factor associator naturality in localization.

Русский

Естественность трёхфакторного ассоциатора в локализации.

LaTeX

$$$\\text{naturality of associator for three factors}$$$

Lean4

theorem pentagon_aux₁ {X₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε} (i : X₁ ≅ Y₁) :
    ((i.hom ▷ X₂) ▷ X₃) ≫ (α_ Y₁ X₂ X₃).hom ≫ (i.inv ▷ (X₂ ⊗ X₃)) = (α_ X₁ X₂ X₃).hom := by
  simp only [associator_naturality₁_assoc, ← whiskerRight_comp, Iso.hom_inv_id, whiskerRight_id, comp_id]

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