leftUnitor_inv_apply — Mathlib

English

The inverse of the left unitor has a natural action given by lid_symm: ((λ_M).inv).hom m = 1 ⊗ m.

Русский

Обратная к левому унитору действует как lid_symm: ((λ_M).inv).hom m = 1 ⊗ m.

LaTeX

$$$ (\\lambda_M).inv.hom = (TensorProduct.lid \\; R \\; M)^{\\mathrm{symm}}^{\\;toLinearMap} $$$

Lean4

@[simp]
theorem leftUnitor_inv_apply {M : ModuleCat.{u} R} (m : M) :
    ((λ_ M).inv : M ⟶ 𝟙_ (ModuleCat.{u} R) ⊗ M) m = 1 ⊗ₜ[R] m :=
  TensorProduct.lid_symm_apply m

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