dualMap_injective_iff — Mathlib

English

The finite dimension of the range of f.dualMap equals that of range f.

Русский

Размерность образа дуального отображения f.dualMap равна размерности образа f.

LaTeX

$$$\\dim_K(\\operatorname{range}(f^{\\*})) = \\dim_K(\\operatorname{range}(f))$$$

Lean4

/-- `f.dualMap` is injective if and only if `f` is surjective -/
@[simp]
theorem dualMap_injective_iff {f : V₁ →ₗ[K] V₂} : Function.Injective f.dualMap ↔ Function.Surjective f :=
  by
  refine ⟨Function.mtr fun not_surj inj ↦ ?_, dualMap_injective_of_surjective⟩
  rw [← range_eq_top, ← Ne, ← lt_top_iff_ne_top] at not_surj
  obtain ⟨φ, φ0, range_le_ker⟩ := (range f).exists_le_ker_of_lt_top not_surj
  exact φ0 (inj <| ext fun x ↦ range_le_ker ⟨x, rfl⟩)

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