English
A submodule has rank at most 1 iff it is a principal submodule.
Русский
Подмодуль имеет ранг не более 1 тогда и только тогда, когда он является главной подмодулем.
LaTeX
$$$$ Module.rank\\,K\\,W \\le 1 \\iff W.IsPrincipal $$$$
Lean4
/-- A vector space has dimension at most `1` if and only if there is a
single vector of which all vectors are multiples. -/
theorem rank_le_one_iff [Module.Free K V] : Module.rank K V ≤ 1 ↔ ∃ v₀ : V, ∀ v, ∃ r : K, r • v₀ = v :=
by
obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := K) (M := V)
constructor
· intro hd
rw [← b.mk_eq_rank'', le_one_iff_subsingleton] at hd
rcases isEmpty_or_nonempty κ with hb | ⟨⟨i⟩⟩
· use 0
have h' : ∀ v : V, v = 0 := by simpa [range_eq_empty, Submodule.eq_bot_iff] using b.span_eq.symm
intro v
simp [h' v]
· use b i
have h' : (K ∙ b i) = ⊤ := (subsingleton_range b).eq_singleton_of_mem (mem_range_self i) ▸ b.span_eq
intro v
have hv : v ∈ (⊤ : Submodule K V) := mem_top
rwa [← h', mem_span_singleton] at hv
· rintro ⟨v₀, hv₀⟩
have h : (K ∙ v₀) = ⊤ := by
ext
simp [mem_span_singleton, hv₀]
rw [← rank_top, ← h]
refine (rank_span_le _).trans_eq ?_
simp
