English
Let f be a linear map with det f = 0. Then f is not onto; equivalently, its image is a proper subspace of the target space.
Русский
Пусть f — линейное отображение с det f = 0. Тогда отображение не сюръектно; образ f является допустимым подпространством, не равным всему пространству.
LaTeX
$$$\det f = 0 \quad\Rightarrow\quad \operatorname{Im}(f) \neq \top$$$
Lean4
/-- If the determinant of a map vanishes, then the map is not onto.
TODO: This should only require `[IsDomain R] [Free R M]`, which we get if we generalize
LinearAlgebra.LinearAlgebra.FiniteDimensional.Basic, which includes ker_eq_bot_iff_range_eq_top.
-/
theorem range_lt_top_of_det_eq_zero {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] {f : M →ₗ[𝕜] M} (hf : f.det = 0) : range f < ⊤ :=
by
have : Module.Finite 𝕜 M := by simp [finite_of_det_ne_one (f := f), hf]
rw [lt_top_iff_ne_top, ne_eq, ← ker_eq_bot_iff_range_eq_top, ← ne_eq, ← bot_lt_iff_ne_bot]
exact bot_lt_ker_of_det_eq_zero hf
