English
The separatingLeft property of dualProd is equivalent to the injectivity of the evaluation map Module.Dual.eval R M.
Русский
Свойство separatingLeft для dualProd эквивалентно инъективности отображения оценки Module.Dual.eval R M.
LaTeX
$$dualProd.SeparatingLeft ⇔ Function.Injective (Module.Dual.eval R M)$$
Lean4
theorem separatingLeft_dualProd : (dualProd R M).SeparatingLeft ↔ Function.Injective (Module.Dual.eval R M) := by
classical
rw [separatingLeft_iff_ker_eq_bot, ker_eq_bot]
let e := LinearEquiv.prodComm R _ _ ≪≫ₗ Module.dualProdDualEquivDual R (Module.Dual R M) M
let h_d := e.symm.toLinearMap.comp (dualProd R M)
refine (Function.Injective.of_comp_iff e.symm.injective (dualProd R M)).symm.trans ?_
rw [← LinearEquiv.coe_toLinearMap, ← coe_comp]
change Function.Injective h_d ↔ _
have : h_d = prodMap id (Module.Dual.eval R M) :=
by
refine ext fun x => Prod.ext ?_ ?_
· ext
dsimp [e, h_d, Module.Dual.eval, LinearEquiv.prodComm]
simp
· ext
dsimp [e, h_d, Module.Dual.eval, LinearEquiv.prodComm]
simp
rw [this, coe_prodMap]
refine Prod.map_injective.trans ?_
exact and_iff_right Function.injective_id
