English
The lattice of submodules of a module over a division ring is atomistic: every submodule is the sup of spans of nonzero vectors contained in it.
Русский
Решетка подпространств модуля над делителем атомистична: каждый подпространство есть супремум спанов ненулевых векторов, входящих в него.
LaTeX
$$$\text{IsAtomistic}(\mathrm{Submodule}\; K\; V)$$$
Lean4
/-- The atoms of the lattice of submodules of a module over a division ring are the
submodules equal to the span of a nonzero element of the module. -/
theorem atom_iff_nonzero_span (W : Submodule K V) : IsAtom W ↔ ∃ v ≠ 0, W = span K { v } :=
by
refine ⟨fun h => ?_, fun h => ?_⟩
· obtain ⟨hbot, h⟩ := h
rcases (Submodule.ne_bot_iff W).1 hbot with ⟨v, ⟨hW, hv⟩⟩
refine ⟨v, ⟨hv, ?_⟩⟩
by_contra heq
specialize h (span K { v })
rw [span_singleton_eq_bot, lt_iff_le_and_ne] at h
exact hv (h ⟨(span_singleton_le_iff_mem v W).2 hW, Ne.symm heq⟩)
· rcases h with ⟨v, ⟨hv, rfl⟩⟩
exact nonzero_span_atom v hv
