bijective_toDualRight_symm_toDualLeft

English

For a perfect pairing p between M and N over R, the map m ↦ p(toDualLeft(m)) composed with the right inverse yields a bijection M → M^*. In particular, the map m ↦ p(-, m) defines a linear isomorphism between M and its dual M^*.

Русский

Для идеальной пары p между M и N над R отображение m ↦ p(-, m) задаёт линейное изоморфизм между M и ее дуалом M^*.

LaTeX

$$$f: M \to M^*,\quad f(m)(m') = p(m', m),\quad f \text{ is bijective}.$$

Lean4

@[deprecated "No replacement" (since := "2025-05-27")]
theorem bijective_toDualRight_symm_toDualLeft : Bijective (fun x => p.toDualRight.symm.dualMap (p.toDualLeft x)) :=
  Bijective.comp (LinearEquiv.bijective p.toDualRight.symm.dualMap) (LinearEquiv.bijective p.toDualLeft)

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