The Jacobson-Noether theorem

This file contains a proof of the Jacobson-Noether theorem and some auxiliary lemmas. Here we discuss different cases of characteristics of the noncommutative division algebra D with center k.

Main Results

• exists_separable_and_not_isCentral : (Jacobson-Noether theorem) For a non-commutative algebraic division algebra D (with base ring being its center k), then there exist an element x of D \ k that is separable over its center.
• exists_separable_and_not_isCentral' : (Jacobson-Noether theorem) For a non-commutative algebraic division algebra D (with base ring being a field L), if the center of D over L is L, then there exist an element x of D \ L that is separable over L.

Notations

• D is a noncommutative division algebra
• k is the center of D

Implementation Notes

Mathematically, exists_separable_and_not_isCentral and exists_separable_and_not_isCentral' are equivalent.

The difference however, is that the former takes D as the only variable and fixing D would forces k. Whereas the later takes D and L as separate variables constrained by certain relations.

Reference

• https://ysharifi.wordpress.com/2011/09/30/the-jacobson-noether-theorem/

theorem JacobsonNoether.exists_pow_mem_center_of_inseparable {D : Type u_1} [DivisionRing D] [Algebra.IsAlgebraic (↥(Subring.center D)) D] (p : ℕ) [hchar : ExpChar D p] (a : D) (hinsep : ∀ (x : D), IsSeparable (↥(Subring.center D)) x → x ∈ Subring.center D) : ∃ (n : ℕ), a ^ p ^ n ∈ Subring.center D

If D is a purely inseparable extension of k with characteristic p, then for every element a of D, there exists a natural number n such that a ^ (p ^ n) is contained in k.

theorem JacobsonNoether.exists_pow_mem_center_of_inseparable' {D : Type u_1} [DivisionRing D] [Algebra.IsAlgebraic (↥(Subring.center D)) D] (p : ℕ) [ExpChar D p] {a : D} (ha : a ∉ Subring.center D) (hinsep : ∀ (x : D), IsSeparable (↥(Subring.center D)) x → x ∈ Subring.center D) : ∃ (n : ℕ), 1 ≤ n ∧ a ^ p ^ n ∈ Subring.center D

If D is a purely inseparable extension of k with characteristic p, then for every element a of D \ k, there exists a natural number n greater than 0 such that a ^ (p ^ n) is contained in k.

theorem JacobsonNoether.exist_pow_eq_zero_of_le {D : Type u_1} [DivisionRing D] [Algebra.IsAlgebraic (↥(Subring.center D)) D] (p : ℕ) [hchar : ExpChar D p] {a : D} (ha : a ∉ Subring.center D) (hinsep : ∀ (x : D), IsSeparable (↥(Subring.center D)) x → x ∈ Subring.center D) : ∃ (m : ℕ), 1 ≤ m ∧ ∀ (n : ℕ), p ^ m ≤ n → (⇑((LieAlgebra.ad (↥(Subring.center D)) D) a))^[n] = 0

If D is a purely inseparable extension of k of characteristic p, then for every element a of D \ k, there exists a natural number m greater than 0 such that (a * x - x * a) ^ n = 0 (as linear maps) for every n greater than (p ^ m).

theorem JacobsonNoether.exists_separable_and_not_isCentral (D : Type u_1) [DivisionRing D] [Algebra.IsAlgebraic (↥(Subring.center D)) D] (H : Subring.center D ≠ ⊤) : ∃ x ∉ Subring.center D, IsSeparable (↥(Subring.center D)) x

Jacobson-Noether theorem: For a non-commutative division algebra D that is algebraic over its center k, there exists an element x of D \ k that is separable over k.

theorem JacobsonNoether.exists_separable_and_not_isCentral' {L : Type u_2} {D : Type u_3} [Field L] [DivisionRing D] [Algebra L D] [Algebra.IsAlgebraic L D] [Algebra.IsCentral L D] (hneq : ⊥ ≠ ⊤) : ∃ x ∉ ⊥, IsSeparable L x

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.