English
In a vector space over a division ring, the span of a nonzero element is an atom in the lattice of submodules.
Русский
В векторном пространстве над кольцом делений порождающее подпространство ненулевого элемента является атомом в решётке подпространий.
LaTeX
$$$\text{IsAtom}(\mathrm{span}_K\{v\})$ whenever $v \neq 0$$$
Lean4
/-- For a module over a division ring, the span of a nonzero element is an atom of the
lattice of submodules. -/
theorem nonzero_span_atom (v : V) (hv : v ≠ 0) : IsAtom (span K { v } : Submodule K V) :=
by
constructor
· rw [Submodule.ne_bot_iff]
exact ⟨v, ⟨mem_span_singleton_self v, hv⟩⟩
· intro T hT
by_contra h
apply hT.2
change span K { v } ≤ T
simp_rw [span_singleton_le_iff_mem, ← Ne.eq_def, Submodule.ne_bot_iff] at *
rcases h with ⟨s, ⟨hs, hz⟩⟩
rcases mem_span_singleton.1 (hT.1 hs) with ⟨a, rfl⟩
rcases eq_or_ne a 0 with rfl | h
· simp only [zero_smul, ne_eq, not_true] at hz
· rwa [T.smul_mem_iff h] at hs
