linearEquiv — Mathlib

English

If M is an invertible module over a commutative semiring R, then the canonical evaluation pairing M^* ⊗_R M → R is a linear isomorphism.

Русский

Если M — обратимый модуль над коммутативным полупкольем R, то канонический оценочный упругий отображение M^* ⊗_R M → R является линейным изоморфизмом.

LaTeX

$$$M^{*} \\otimes_R M \\cong_R R \\\\ \\text{via } (f \\otimes m) \\mapsto f(m).$$$

Lean4

/-- Promote the canonical map `Mᵛ ⊗[R] M → R` to a linear equivalence for invertible `M`. -/
noncomputable def linearEquiv [Module.Invertible R M] : Module.Dual R M ⊗[R] M ≃ₗ[R] R :=
  .ofBijective _ Invertible.bijective

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