English
There is a natural structure EquivLike for PerfectPairing R M N giving an equivalence between M and the dual of N, i.e., a canonical duality in the pairing.
Русский
Существуют естественные структуры EquivLike для идеальной пары, устанавливающей эквивалентность между M и двойственным пространством N.
LaTeX
$$$\text{EquivLike}( \text{PerfectPairing } R M N, M, \mathrm{Dual}(R,N))$ is defined by the left dual map and its inverse.$$
Lean4
@[deprecated "No replacement" (since := "2025-05-27")]
instance : EquivLike (PerfectPairing R M N) M (Dual R N)
where
coe p := p.toDualLeft
inv p := p.toDualLeft.symm
left_inv p x := LinearEquiv.symm_apply_apply _ _
right_inv p x := LinearEquiv.apply_symm_apply _ _
coe_injective' p q h
h' := by
cases p
cases q
simp only [mk.injEq]
ext m n
simp only [DFunLike.coe_fn_eq] at h
exact LinearMap.congr_fun (LinearEquiv.congr_fun h m) n
