eval_apply_injective — Mathlib

English

For a finite projective R-module V, the evaluation map ev: V* → V** is injective.

Русский

Для проективного конечного модуля V над R отображение оценки ev: V* → V** инъективно.

LaTeX

$$$\\operatorname{ev}_V: V^{\\ast} \\to V^{**}$ is injective.$$

Lean4

theorem eval_apply_injective : Function.Injective (eval K V) :=
  have ⟨s, hs⟩ := Module.projective_def'.mp ‹Projective K V›
  .of_comp (f := s.dualMap.dualMap) (Finsupp.basisSingleOne.eval_injective.comp <| injective_of_comp_eq_id s _ hs)

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