hom_hom_rightUnitor — Mathlib

English

The hom component of the right unitor is the canonical rid map: (ρ_M).hom = (TensorProduct.rid _ _).toLinearMap.

Русский

Гом-компонента правого унитора есть каноническая карта rid: (ρ_M).hom = (TensorProduct.rid _ _).toLinearMap.

LaTeX

$$$ (\\rho_M).hom = (\\text{TensorProduct}.rid \\, R \\, M)^{\\toLinearMap} $$$

Lean4

theorem hom_hom_rightUnitor {M : ModuleCat.{u} R} : (ρ_ M).hom.hom = (TensorProduct.rid _ _).toLinearMap :=
  rfl

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