English
Let f,g: M →_R M' be linear maps. If the evaluation map on M' is injective, then f and g are equal whenever their double dual maps are equal: f^{**} = g^{**} implies f = g.
Русский
Пусть f,g: M →_R M' — линейные отображения. Если отображение оценки на M' инъективно, то равенство их двойственных отображений f^{**} = g^{**} влечет равенство f = g.
LaTeX
$$$\\forall f,g: M \\to_{R} M',\\ (\\operatorname{Injective}(\\mathrm{Dual.eval}(R,M'))) \\Rightarrow \\big( f^{**} = g^{**} \\iff f = g \\big).$$$
Lean4
theorem dualMap_dualMap_eq_iff_of_injective {M' : Type*} [AddCommMonoid M'] [Module R M'] {f g : M →ₗ[R] M'}
(h : Injective (Dual.eval R M')) : f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g :=
by
simp only [← Dual.eval_comp_comp_evalEquiv_eq]
refine
⟨fun hfg => ?_, fun a ↦
congrArg (Dual.eval R M').comp (congrFun (congrArg LinearMap.comp a) (evalEquiv R M).symm.toLinearMap)⟩
rw [propext (cancel_left h), LinearEquiv.eq_comp_toLinearMap_iff] at hfg
exact hfg
