pentagon — Mathlib

English

The left unitor is natural: for any morphism f: M → N, tensorHom (id ⊗ f) ∘ leftUnitor(N) = leftUnitor(M) ∘ f.

Русский

Левый унитор естественен: для любого отображения f между модулями выполняется тождество натуральности левого унитора.

LaTeX

$$$\\mathrm{tensorHom}(\\mathrm{id}_{R}, f) \\; \\circ \\lambda_N = \\lambda_M \\; \\circ f$$$

Lean4

theorem pentagon (W X Y Z : ModuleCat R) :
    whiskerRight (associator W X Y).hom Z ≫
        (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom =
      (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom :=
  by
  ext : 1
  apply TensorProduct.ext_fourfold
  intro w x y z
  rfl

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