of_isPerfPair — Mathlib

English

Let R be a commutative ring and M,N be additive groups with R-module structures, together with a perfect pairing p : M →ₗ[R] N →ₗ[R] R. Then M is reflexive as an R-module; equivalently, the natural map M → Hom_R(Hom_R(M,R),R) is an isomorphism.

Русский

Пусть R — коммутативное кольцо, M и N — добавочные группы с структурами R-модуля, и p : M →ₗ[R] N →ₗ[R] R — совершенная парная форма. Тогда M является рефлексивным R-модулем; то есть естественный отображение M → Hom_R(Hom_R(M,R),R) является изоморфизмом.

LaTeX

$$$\operatorname{IsReflexive}(R,M)$$$

Lean4

theorem _root_.Module.IsReflexive.of_isPerfPair : IsReflexive R M where
  bijective_dual_eval' := by
    convert (p.toPerfPair.trans p.flip.toPerfPair.dualMap.symm).bijective
    ext x f
    simp

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