English
If a division ring D is algebraic over its center and the center equals D's center, there exists a noncentral separable element.
Русский
Если D алгебраичен над своим центром и центр D не совпадает с D, существует сепарабельный элемент за пределами центра.
LaTeX
$$$\\exists x:\\; D \\setminus (\\text{center } D) \\text{ with } IsSeparable(\\text{center } D, x)$$$
Lean4
/-- Jacobson-Noether theorem: For a non-commutative division algebra `D`
that is algebraic over a field `L`, if the center of
`D` coincides with `L`, then there exist an element `x` of `D \ L`
that is separable over `L`. -/
theorem exists_separable_and_not_isCentral' {L D : Type*} [Field L] [DivisionRing D] [Algebra L D]
[Algebra.IsAlgebraic L D] [Algebra.IsCentral L D] (hneq : (⊥ : Subalgebra L D) ≠ ⊤) :
∃ x : D, x ∉ (⊥ : Subalgebra L D) ∧ IsSeparable L x :=
by
have hcenter : Subalgebra.center L D = ⊥ := le_bot_iff.mp IsCentral.out
have ntrivial : Subring.center D ≠ ⊤ :=
congr(Subalgebra.toSubring $hcenter).trans_ne (Subalgebra.toSubring_injective.ne hneq)
set φ := Subalgebra.equivOfEq (⊥ : Subalgebra L D) (.center L D) hcenter.symm
set equiv : L ≃+* (center D) := ((botEquiv L D).symm.trans φ).toRingEquiv
let _ : Algebra L (center D) := equiv.toRingHom.toAlgebra
let _ : Algebra (center D) L := equiv.symm.toRingHom.toAlgebra
have _ : IsScalarTower L (center D) D := .of_algebraMap_eq fun _ ↦ rfl
have _ : IsScalarTower (center D) L D :=
.of_algebraMap_eq fun x ↦ by
rw [IsScalarTower.algebraMap_apply L (center D)]
congr
exact (equiv.apply_symm_apply x).symm
have _ : Algebra.IsAlgebraic (center D) D := .tower_top (K := L) _
obtain ⟨x, hxd, hx⟩ := exists_separable_and_not_isCentral D ntrivial
exact ⟨x, ⟨by rwa [← Subalgebra.center_toSubring L, hcenter] at hxd, IsSeparable.tower_top _ hx⟩⟩
