dualMap_injective_of_surjective — Mathlib

English

If f: M1 → M2 is surjective, then the dual map f^*: M2^* → M1^* is injective.

Русский

Если отображение f: M1 → M2 сюръективно, то дуальное отображение f^*: M2^* → M1^* инъективно.

LaTeX

$$$$ \\text{Surjective}(f) \\Rightarrow \\text{Injective}(f^*). $$$$

Lean4

/-- If a linear map is surjective, then its dual is injective. -/
theorem dualMap_injective_of_surjective {f : M₁ →ₗ[R] M₂} (hf : Function.Surjective f) : Function.Injective f.dualMap :=
  by
  intro φ ψ h
  ext x
  obtain ⟨y, rfl⟩ := hf x
  exact congr_arg (fun g : Module.Dual R M₁ => g y) h

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