Lean4
/-- 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 exists_separable_and_not_isCentral (H : k ≠ (⊤ : Subring D)) : ∃ x : D, x ∉ k ∧ IsSeparable k x :=
by
obtain ⟨p, hp⟩ := ExpChar.exists D
by_contra! insep
replace insep : ∀ x : D, IsSeparable k x → x ∈ k := fun x h ↦ Classical.byContradiction fun hx ↦ insep x hx h
obtain ⟨a, ha⟩ := not_forall.mp <| mt (Subring.eq_top_iff' k).mpr H
have ha₀ : a ≠ 0 := fun nh ↦
nh ▸ ha <|
Subring.zero_mem
k
-- We construct another element `b` that does not commute with `a`.
obtain ⟨b, hb1⟩ : ∃ b : D, ad k D a b ≠ 0 :=
by
rw [Subring.mem_center_iff, not_forall] at ha
use ha.choose
change a * ha.choose - ha.choose * a ≠ 0
simpa only [ne_eq, sub_eq_zero] using Ne.symm ha.choose_spec
obtain ⟨n, hn, hb⟩ : ∃ n, 0 < n ∧ (ad k D a)^[n] b ≠ 0 ∧ (ad k D a)^[n + 1] b = 0 :=
by
obtain ⟨m, -, hm2⟩ := exist_pow_eq_zero_of_le p ha insep
have h_exist : ∃ n, 0 < n ∧ (ad k D a)^[n + 1] b = 0 :=
⟨p ^ m, ⟨expChar_pow_pos D p m, by rw [hm2 (p ^ m + 1) (Nat.le_add_right _ _), Pi.zero_apply]⟩⟩
classical
refine ⟨Nat.find h_exist, ⟨(Nat.find_spec h_exist).1, ?_, (Nat.find_spec h_exist).2⟩⟩
set t := (Nat.find h_exist - 1 : ℕ) with ht
by_cases h_pos : 0 < t
· convert (ne_eq _ _) ▸ not_and.mp (Nat.find_min h_exist (m := t) (by cutsat)) h_pos
cutsat
· suffices h_find : Nat.find h_exist = 1 by rwa [h_find]
rw [not_lt, Nat.le_zero, ht, Nat.sub_eq_zero_iff_le] at h_pos
linarith [(Nat.find_spec h_exist).1]
-- We define `c` to be the value that we proved above to be non-zero.
set c := (ad k D a)^[n] b with hc_def
let _ : Invertible c :=
⟨c⁻¹, inv_mul_cancel₀ hb.1, mul_inv_cancel₀ hb.1⟩
-- We prove that `c` commutes with `a`.
have hc : a * c = c * a := by
apply eq_of_sub_eq_zero
rw [← mulLeft_apply (R := k), ← mulRight_apply (R := k)]
suffices ad k D a c = 0 from by rw [← this]; simp [LieRing.of_associative_ring_bracket]
rw [← Function.iterate_succ_apply' (ad k D a) n b, hb.2]
-- We now make some computation to obtain the final equation.
set d := c⁻¹ * a * (ad k D a)^[n - 1] b with hd_def
have hc' : c⁻¹ * a = a * c⁻¹ := by
apply_fun (c⁻¹ * · * c⁻¹) at hc
rw [mul_assoc, mul_assoc, mul_inv_cancel₀ hb.1, mul_one, ← mul_assoc, inv_mul_cancel₀ hb.1, one_mul] at hc
exact hc
have c_eq : a * (ad k D a)^[n - 1] b - (ad k D a)^[n - 1] b * a = c := by
rw [hc_def, ← Nat.sub_add_cancel hn, Function.iterate_succ_apply' (ad k D a) _ b]; rfl
have eq1 : c⁻¹ * a * (ad k D a)^[n - 1] b - c⁻¹ * (ad k D a)^[n - 1] b * a = 1 := by
simp_rw [mul_assoc, (mul_sub_left_distrib c⁻¹ _ _).symm, c_eq, inv_mul_cancel_of_invertible]
-- We show that `a` commutes with `d`.
have deq : a * d - d * a = a := by
nth_rw 3 [← mul_one a]
rw [hd_def, ← eq1, mul_sub, mul_assoc _ _ a, sub_right_inj, hc', ← mul_assoc, ← mul_assoc, ← mul_assoc]
-- This then yields a contradiction.
apply_fun (a⁻¹ * ·) at deq
rw [mul_sub, ← mul_assoc, inv_mul_cancel₀ ha₀, one_mul, ← mul_assoc, sub_eq_iff_eq_add] at deq
obtain ⟨r, hr⟩ := exists_pow_mem_center_of_inseparable p d insep
apply_fun (· ^ (p ^ r)) at deq
rw [add_pow_expChar_pow_of_commute p r (Commute.one_left _), one_pow, GroupWithZero.conj_pow₀ ha₀, ← hr.comm,
mul_assoc, inv_mul_cancel₀ ha₀, mul_one, right_eq_add] at deq
exact one_ne_zero deq
