English
The whole module has rank at most 1 iff the top submodule is principal.
Русский
Вся надмодуль имеет ранг не больше 1 тогда и только тогда, когда верхний подмодуль является главной.
LaTeX
$$$$ Module.rank\\,K\\,V \\le 1 \\leftrightarrow (\\top : Submodule K V).IsPrincipal $$$$
Lean4
/-- A vector space has dimension `1` if and only if there is a
single non-zero vector of which all vectors are multiples. -/
theorem rank_eq_one_iff [Module.Free K V] : Module.rank K V = 1 ↔ ∃ v₀ : V, v₀ ≠ 0 ∧ ∀ v, ∃ r : K, r • v₀ = v :=
by
haveI := nontrivial_of_invariantBasisNumber K
refine ⟨fun h ↦ ?_, fun ⟨v₀, h, hv⟩ ↦ (rank_le_one_iff.2 ⟨v₀, hv⟩).antisymm ?_⟩
· obtain ⟨v₀, hv⟩ := rank_le_one_iff.1 h.le
refine ⟨v₀, fun hzero ↦ ?_, hv⟩
simp_rw [hzero, smul_zero, exists_const] at hv
haveI : Subsingleton V := .intro fun _ _ ↦ by simp_rw [← hv]
exact one_ne_zero (h ▸ rank_subsingleton' K V)
· by_contra H
rw [not_le, lt_one_iff_zero] at H
obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := K) (M := V)
haveI := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'')
haveI := b.repr.toEquiv.subsingleton
exact h (Subsingleton.elim _ _)
