English
Let p be a perfect pairing between M and N over a commutative ring R. Denote by Φ_L: M → N^* and Φ_R: N → M^* the left and right dual maps induced by p, i.e. Φ_L(m)(n) = p(m,n) and Φ_R(n)(m) = p(m,n). Then the composition Φ_R^{-1} ∘ Φ_L equals the canonical evaluation map ev_M: M → M^*, i.e. for all m ∈ M, (Φ_R^{-1} ∘ Φ_L)(m) = ev_M(m).
Русский
Пусть p — идеальная связка между модулями M и N над кольцом R. Пусть Φ_L: M → N^*, Φ_R: N → M^* — соответствующие двойственные отображения, задаваемые p. Тогда композиция Φ_R^{-1} ∘ Φ_L равна каноническому отображению оценки ev_M: M → M^*, то есть для каждого m ∈ M имеем (Φ_R^{-1} ∘ Φ_L)(m) = ev_M(m).
LaTeX
$$$\text{Let } \Phi_L: M \to N^*,\ \Phi_R: N \to M^*,\ \text{with } \Phi_L(m)(n)=p(m,n),\ \Phi_R(n)(m)=p(m,n). \quad (\Phi_R)^{-1}\circ \Phi_L = \mathrm{ev}_M: M\to M^*, \text{ i.e. } (\Phi_R)^{-1}(\Phi_L(m))(m')=p(m',m).$$$
Lean4
@[deprecated "No replacement" (since := "2025-05-27")]
theorem toDualRight_symm_comp_toDualLeft :
p.toDualRight.symm.dualMap ∘ₗ (p.toDualLeft : M →ₗ[R] Dual R N) = Dual.eval R M :=
by
ext1 x
exact p.toDualRight_symm_toDualLeft x
