rightUnitor_hom_apply — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem rightUnitor_hom_apply {M : ModuleCat.{u} R} (m : M) (r : R) :
    ((ρ_ M).hom : M ⊗ 𝟙_ (ModuleCat R) ⟶ M) (m ⊗ₜ r) = r • m :=
  TensorProduct.rid_tmul m r

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