English
If a K-algebra A acts on a K-vector space V such that V is 1-dimensional over K, then the lattice of A-submodules of V is simple; equivalently, V has no nontrivial A-submodules.
Русский
Если алгебра A над полем K действует на пространстве V так, что dim_K V = 1, то решетка подмодулей A-симметрична проста; то есть не существует ненулевых подмодулей A.
LaTeX
$$$\\text{IsSimpleOrder}(\\operatorname{Submodule}_A V)$ при $\\operatorname{finrank}_K V = 1$.$$
Lean4
/-- Any `K`-algebra module that is 1-dimensional over `K` is simple. -/
theorem is_simple_module_of_finrank_eq_one {A} [Semiring A] [Module A V] [SMul K A] [IsScalarTower K A V]
(h : finrank K V = 1) : IsSimpleOrder (Submodule A V) :=
by
haveI := nontrivial_of_finrank_eq_succ h
refine ⟨fun S => or_iff_not_imp_left.2 fun hn => ?_⟩
rw [← restrictScalars_inj K] at hn ⊢
haveI : FiniteDimensional _ _ := .of_finrank_eq_succ h
refine eq_top_of_finrank_eq ((Submodule.finrank_le _).antisymm ?_)
simpa only [h, finrank_bot] using Submodule.finrank_strictMono (Ne.bot_lt hn)
