rightUnitor_naturality — Mathlib

English

The triangle identity holds: the interaction of associator and unitors satisfies the standard unit axioms in a monoidal category.

Русский

Треугольная тождественность выполняется: взаимодействие ассоциатора и униторов удовлетворяет стандартным аксиомам тензорного произведения.

LaTeX

$$$\\alpha_{M,I,N} \\; \\circ \\; (id_M \\otimes \\lambda_N) = \\rho_M \\otimes id_N$$$

Lean4

theorem rightUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
    tensorHom f (𝟙 (ModuleCat.of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f :=
  by
  ext : 1
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): broken ext

  apply TensorProduct.ext
  ext x
  dsimp
  erw [TensorProduct.rid_tmul, TensorProduct.rid_tmul]
  rw [LinearMap.map_smul]
  rfl

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