associator_inv_conjugation — Mathlib

English

Naturality of the associator: conjugating a morphism by tensoring yields a corresponding transformed morphism.

Русский

Натуральность ассоциатора: конъюгация морфизма под тензоризацией приводит к соответствующему преобразованию морфизма.

LaTeX

$$$$ f \otimes g \otimes h = (α_{X,Y,Z})^{-1} \circ ((f \otimes g) \otimes h) \circ (α_{X',Y',Z'}).hom $$$$

Lean4

@[reassoc]
theorem associator_inv_conjugation {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
    f ⊗ₘ g ⊗ₘ h = (α_ X Y Z).inv ≫ ((f ⊗ₘ g) ⊗ₘ h) ≫ (α_ X' Y' Z').hom := by
  rw [associator_naturality, inv_hom_id_assoc]
    -- TODO these next two lemmas aren't so fundamental, and perhaps could be removed
    -- (replacing their usages by their proofs).

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