feat(FieldTheory.JacobsonNoether) : add proof of the Jacobson-Noether…

… theorem (#16525)

In this PR we provide a proof of the Jacobson-Noether theorem following [this blog](https://ysharifi.wordpress.com/2011/09/30/the-jacobson-noether-theorem/)

Co-authored by: Filippo A. E. Nuccio @faenuccio
Co-authored by: Wanyi He @Blackfeather007
Co-authored by: Huanyu Zheng @Yu-Misaka
Co-authored by: Yi Yuan @yuanyi-350
Co-authored by: Weichen Jiao @AlbertJ-314
Co-authored by: Sihan Wu @Old-Turtledove
Co-authored by: @FR-vdash-bot



Co-authored-by: faenuccio <[email protected]>

Mathlib.lean

@@ -164,6 +164,7 @@ import Mathlib.Algebra.CharP.ExpChar
 import Mathlib.Algebra.CharP.IntermediateField
 import Mathlib.Algebra.CharP.Invertible
 import Mathlib.Algebra.CharP.Lemmas
+import Mathlib.Algebra.CharP.LinearMaps
 import Mathlib.Algebra.CharP.LocalRing
 import Mathlib.Algebra.CharP.MixedCharZero
 import Mathlib.Algebra.CharP.Pi
@@ -2946,6 +2947,7 @@ import Mathlib.FieldTheory.IsAlgClosed.Classification
 import Mathlib.FieldTheory.IsAlgClosed.Spectrum
 import Mathlib.FieldTheory.IsPerfectClosure
 import Mathlib.FieldTheory.IsSepClosed
+import Mathlib.FieldTheory.JacobsonNoether
 import Mathlib.FieldTheory.KrullTopology
 import Mathlib.FieldTheory.KummerExtension
 import Mathlib.FieldTheory.Laurent

Mathlib/Algebra/Algebra/Basic.lean

@@ -133,18 +133,24 @@ end CommSemiring
 
 section Ring
 
-variable [CommRing R]
-variable (R)
-
 /-- A `Semiring` that is an `Algebra` over a commutative ring carries a natural `Ring` structure.
 See note [reducible non-instances]. -/
-abbrev semiringToRing [Semiring A] [Algebra R A] : Ring A :=
+abbrev semiringToRing (R : Type*) [CommRing R] [Semiring A] [Algebra R A] : Ring A :=
   { __ := (inferInstance : Semiring A)
     __ := Module.addCommMonoidToAddCommGroup R
     intCast := fun z => algebraMap R A z
     intCast_ofNat := fun z => by simp only [Int.cast_natCast, map_natCast]
     intCast_negSucc := fun z => by simp }
 
+instance {R : Type*} [Ring R] : Algebra (Subring.center R) R where
+  toFun := Subtype.val
+  map_one' := rfl
+  map_mul' _ _ := rfl
+  map_zero' := rfl
+  map_add' _ _ := rfl
+  commutes' r x := (Subring.mem_center_iff.1 r.2 x).symm
+  smul_def' _ _ := rfl
+
 end Ring
 
 end Algebra

Mathlib/Algebra/CharP/LinearMaps.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2024 Wanyi He. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wanyi He, Huanyu Zheng
+-/
+import Mathlib.Algebra.CharP.Algebra
+/-!
+# Characteristic of the ring of linear Maps
+
+This file contains properties of the characteristic of the ring of linear maps.
+The characteristic of the ring of linear maps is determined by its base ring.
+
+## Main Results
+
+- `CharP_if` : For a commutative semiring `R` and a `R`-module `M`,
+  the characteristic of `R` is equal to the characteristic of the `R`-linear
+  endomorphisms of `M` when `M` contains an element `x` such that
+  `r • x = 0` implies `r = 0`.
+
+## Notations
+
+- `R` is a commutative semiring
+- `M` is a `R`-module
+
+## Implementation Notes
+
+One can also deduce similar result via `charP_of_injective_ringHom` and
+  `R → (M →ₗ[R] M) : r ↦ (fun (x : M) ↦ r • x)`. But this will require stronger condition
+  compared to `CharP_if`.
+
+-/
+
+namespace Module
+
+variable {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
+
+/-- For a commutative semiring `R` and a `R`-module `M`, if `M` contains an
+  element `x` such that `r • x = 0` implies `r = 0` (finding such element usually
+  depends on specific `•`), then the characteristic of `R` is equal to the
+  characteristic of the `R`-linear endomorphisms of `M`.-/
+theorem charP_end {p : ℕ} [hchar : CharP R p]
+    (hreduction : ∃ x : M, ∀ r : R, r • x = 0 → r = 0) : CharP (M →ₗ[R] M) p where
+  cast_eq_zero_iff' n := by
+    have exact : (n : M →ₗ[R] M) = (n : R) • 1 := by
+      simp only [Nat.cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]
+    rw [exact, LinearMap.ext_iff, ← hchar.1]
+    exact ⟨fun h ↦ Exists.casesOn hreduction fun x hx ↦ hx n (h x),
+      fun h ↦ (congrArg (fun t ↦ ∀ x, t • x = 0) h).mpr fun x ↦ zero_smul R x⟩
+
+end Module
+
+/-- For a division ring `D` with center `k`, the ring of `k`-linear endomorphisms
+  of `D` has the same characteristic as `D`-/
+instance {D : Type*} [DivisionRing D] {p : ℕ} [CharP D p] :
+    CharP (D →ₗ[(Subring.center D)] D) p :=
+  charP_of_injective_ringHom (Algebra.lmul (Subring.center D) D).toRingHom.injective p
+
+instance {D : Type*} [DivisionRing D] {p : ℕ} [ExpChar D p] :
+    ExpChar (D →ₗ[Subring.center D] D) p :=
+  expChar_of_injective_ringHom (Algebra.lmul (Subring.center D) D).toRingHom.injective p

Mathlib/Algebra/CharP/Subring.lean

@@ -3,8 +3,7 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import Mathlib.Algebra.CharP.Defs
-import Mathlib.Algebra.Ring.Subring.Defs
+import Mathlib.Algebra.CharP.Algebra
 
 /-!
 # Characteristic of subrings
@@ -33,4 +32,18 @@ instance subring (R : Type u) [Ring R] (p : ℕ) [CharP R p] (S : Subring R) : C
 instance subring' (R : Type u) [CommRing R] (p : ℕ) [CharP R p] (S : Subring R) : CharP S p :=
   CharP.subring R p S
 
+/-- The characteristic of a division ring is equal to the characteristic
+  of its center-/
+theorem charP_center_iff {R : Type u} [Ring R] {p : ℕ} :
+    CharP (Subring.center R) p ↔ CharP R p :=
+  (algebraMap (Subring.center R) R).charP_iff Subtype.val_injective p
+
 end CharP
+
+namespace ExpChar
+
+theorem expChar_center_iff {R : Type u} [Ring R] {p : ℕ} :
+    ExpChar (Subring.center R) p ↔ ExpChar R p :=
+  (algebraMap (Subring.center R) R).expChar_iff Subtype.val_injective p
+
+end ExpChar

Mathlib/Algebra/GroupWithZero/Conj.lean

@@ -14,9 +14,17 @@ assert_not_exists Multiset
 -- TODO
 -- assert_not_exists DenselyOrdered
 
+namespace GroupWithZero
+
 variable {α : Type*} [GroupWithZero α] {a b : α}
 
 @[simp] lemma isConj_iff₀ : IsConj a b ↔ ∃ c : α, c ≠ 0 ∧ c * a * c⁻¹ = b := by
   rw [IsConj, Units.exists_iff_ne_zero (p := (SemiconjBy · a b))]
   congr! 2 with c
   exact and_congr_right (mul_inv_eq_iff_eq_mul₀ · |>.symm)
+
+lemma conj_pow₀ {s : ℕ} {a d : α} (ha : a ≠ 0) : (a⁻¹ * d * a) ^ s = a⁻¹ * d ^ s * a :=
+  let u : αˣ := ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩
+  Units.conj_pow' u d s
+
+end GroupWithZero

Mathlib/FieldTheory/JacobsonNoether.lean

@@ -0,0 +1,195 @@
+/-
+Copyright (c) 2024 F. Nuccio, H. Zheng, W. He, S. Wu, Y. Yuan, W. Jiao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Filippo A. E. Nuccio, Huanyu Zheng, Sihan Wu, Wanyi He, Weichen Jiao, Yi Yuan
+-/
+import Mathlib.Algebra.Central.Defs
+import Mathlib.Algebra.CharP.LinearMaps
+import Mathlib.Algebra.CharP.Subring
+import Mathlib.Algebra.GroupWithZero.Conj
+import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.FieldTheory.PurelyInseparable
+
+/-!
+# 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/>
+-/
+
+namespace JacobsonNoether
+
+variable {D : Type*} [DivisionRing D] [Algebra.IsAlgebraic (Subring.center D) D]
+
+local notation3 "k" => Subring.center D
+
+open Polynomial LinearMap LieAlgebra
+
+/-- 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`. -/
+lemma exists_pow_mem_center_of_inseparable (p : ℕ) [hchar : ExpChar D p] (a : D)
+    (hinsep : ∀ x : D, IsSeparable k x → x ∈ k) : ∃ n, a ^ (p ^ n) ∈ k := by
+  have := (@isPurelyInseparable_iff_pow_mem k D _ _ _ _ p (ExpChar.expChar_center_iff.2 hchar)).1
+  have pure : IsPurelyInseparable k D := ⟨Algebra.IsAlgebraic.isIntegral, fun x hx ↦ by
+    rw [RingHom.mem_range, Subtype.exists]
+    exact ⟨x, ⟨hinsep x hx, rfl⟩⟩⟩
+  obtain ⟨n, ⟨m, hm⟩⟩ := this pure a
+  have := Subalgebra.range_subset (R := k) ⟨(k).toSubsemiring, fun r ↦ r.2⟩
+  exact ⟨n, Set.mem_of_subset_of_mem this <| Set.mem_range.2 ⟨m, hm⟩⟩
+
+/-- 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`. -/
+lemma exists_pow_mem_center_of_inseparable' (p : ℕ) [ExpChar D p] {a : D}
+    (ha : a ∉ k) (hinsep : ∀ x : D, IsSeparable k x → x ∈ k) : ∃ n, 1 ≤ n ∧ a ^ (p ^ n) ∈ k := by
+  obtain ⟨n, hn⟩ := exists_pow_mem_center_of_inseparable p a hinsep
+  by_cases nzero : n = 0
+  · rw [nzero, pow_zero, pow_one] at hn
+    exact (ha hn).elim
+  · exact ⟨n, ⟨Nat.one_le_iff_ne_zero.mpr nzero, hn⟩⟩
+
+/-- 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)`. -/
+lemma exist_pow_eq_zero_of_le (p : ℕ) [hchar : ExpChar D p]
+    {a : D} (ha : a ∉ k) (hinsep : ∀ x : D, IsSeparable k x → x ∈ k):
+  ∃ m, 1 ≤ m ∧ ∀ n, p ^ m ≤ n → (ad k D a)^[n] = 0 := by
+  obtain ⟨m, hm⟩ := exists_pow_mem_center_of_inseparable' p ha hinsep
+  refine ⟨m, ⟨hm.1, fun n hn ↦ ?_⟩⟩
+  have inter : (ad k D a)^[p ^ m] = 0 := by
+    ext x
+    rw [ad_eq_lmul_left_sub_lmul_right, ← pow_apply, Pi.sub_apply,
+      sub_pow_expChar_pow_of_commute p m (commute_mulLeft_right a a), sub_apply,
+      pow_mulLeft, mulLeft_apply, pow_mulRight, mulRight_apply, Pi.zero_apply,
+      Subring.mem_center_iff.1 hm.2 x]
+    exact sub_eq_zero_of_eq rfl
+  rw [(Nat.sub_eq_iff_eq_add hn).1 rfl, Function.iterate_add, inter, Pi.comp_zero,
+    iterate_map_zero, Function.const_zero]
+
+variable (D) in
+/-- 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
+  -- The element `a` below is in `D` but not in `k`.
+  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
+    show a * ha.choose - ha.choose * a ≠ 0
+    simpa only [ne_eq, sub_eq_zero] using Ne.symm ha.choose_spec
+  -- We find a maximum natural number `n` such that `(a * x - x * a) ^ n b ≠ 0`.
+  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 _ _)]; rfl⟩⟩
+    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 omega)) h_pos
+      omega
+    · 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]; rfl
+    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,
+    self_eq_add_left] at deq
+  exact one_ne_zero deq
+
+open Subring Algebra in
+/-- 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⟩⟩
+
+end JacobsonNoether