English
Let F be a field and A an F-algebra that is an integral domain, finite-dimensional over F with prime dimension. Then the lattice of Subalgebras of A over F is simple; equivalently, every Subalgebra S with ⊥ ≤ S ≤ ⊤ satisfies S = ⊥ or S = ⊤.
Русский
Пусть F — поле, A — F-алгебра, которая является интегральным доменом и имеет простую размерность над F. Тогда решётка подалгебр A над F проста: для любой подалгебры S верно S = ⊥ или S = ⊤ (отношение ⊥ ≤ S ≤ ⊤).
LaTeX
$$IsSimpleOrder( Subalgebra F A )$$
Lean4
theorem isSimpleOrder_of_finrank_prime (F A) [Field F] [Ring A] [IsDomain A] [Algebra F A] (hp : (finrank F A).Prime) :
IsSimpleOrder (Subalgebra F A) :=
{ toNontrivial := ⟨⟨⊥, ⊤, fun he => Nat.not_prime_one ((Subalgebra.bot_eq_top_iff_finrank_eq_one.1 he).subst hp)⟩⟩
eq_bot_or_eq_top := fun K => by
haveI : FiniteDimensional _ _ := .of_finrank_pos hp.pos
letI := divisionRingOfFiniteDimensional F K
refine (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp ?_ fun h => ?_
· exact fun h' => Subalgebra.eq_bot_of_finrank_one h'
· exact Algebra.toSubmodule_eq_top.1 (eq_top_of_finrank_eq <| K.finrank_toSubmodule.trans h) }
-- TODO: `IntermediateField` version
