surjective_of_nonzero_of_finrank_eq_one

English

Given a finite-dimensional K-space W (dimension 1) and a nonzero map f, f is surjective onto W whenever the target is 1-dimensional.

Русский

Если W конечномерно по K размерности 1 и линейное отображение не нуль, то отображение сюръективно на W, если размерность цели равна 1.

LaTeX

$$$\text{finrank}_K W = 1 \Rightarrow \Surjective f$ for appropriate f$$

Lean4

theorem surjective_of_nonzero_of_finrank_eq_one {W A : Type*} [Semiring A] [Module A V] [AddCommGroup W] [Module K W]
    [Module A W] [LinearMap.CompatibleSMul V W K A] (h : finrank K W = 1) {f : V →ₗ[A] W} (w : f ≠ 0) : Surjective f :=
  by
  change Surjective (f.restrictScalars K)
  obtain ⟨v, n⟩ := DFunLike.ne_iff.mp w
  intro z
  obtain ⟨c, rfl⟩ := (finrank_eq_one_iff_of_nonzero' (f v) n).mp h z
  exact ⟨c • v, by simp⟩

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