English
For a subalgebra S of E with Nontrivial E and S free over F, rank_F S = 1 if and only if S = ⊥.
Русский
Для подалгебры S ⊆ E, если E нетривиально и S свободно над F, тогда rank_F S = 1 тогда и только тогда, когда S = ⊥.
LaTeX
$$$\operatorname{rank} F S = 1 \iff S = ⊥$$$
Lean4
@[simp]
theorem rank_eq_one_iff [Nontrivial E] [Module.Free F S] : Module.rank F S = 1 ↔ S = ⊥ :=
by
refine ⟨fun h ↦ Subalgebra.eq_bot_of_rank_le_one h.le, ?_⟩
rintro rfl
obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := F) (M := (⊥ : Subalgebra F E))
refine le_antisymm ?_ ?_
· have := lift_rank_range_le (Algebra.linearMap F E)
rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff, ← Algebra.toSubmodule_bot, rank_toSubmodule] at this
· by_contra H
rw [not_le, lt_one_iff_zero] at H
haveI := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'')
haveI := b.repr.toEquiv.subsingleton
exact one_ne_zero congr((⊥ : Subalgebra F E).val $(Subsingleton.elim 1 0))
