diff --git a/Mathlib.lean b/Mathlib.lean index 55552ad2a0f9b..238444e50113b 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean index 3e1c923709bb3..98aab66f635a1 100644 --- a/Mathlib/Algebra/Algebra/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/CharP/LinearMaps.lean b/Mathlib/Algebra/CharP/LinearMaps.lean new file mode 100644 index 0000000000000..36f3baf18a80d --- /dev/null +++ b/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 diff --git a/Mathlib/Algebra/CharP/Subring.lean b/Mathlib/Algebra/CharP/Subring.lean index e6d5faa37044a..23ed075efbeb1 100644 --- a/Mathlib/Algebra/CharP/Subring.lean +++ b/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 diff --git a/Mathlib/Algebra/GroupWithZero/Conj.lean b/Mathlib/Algebra/GroupWithZero/Conj.lean index 17ccffc430192..6aea4c22972a7 100644 --- a/Mathlib/Algebra/GroupWithZero/Conj.lean +++ b/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 diff --git a/Mathlib/FieldTheory/JacobsonNoether.lean b/Mathlib/FieldTheory/JacobsonNoether.lean new file mode 100644 index 0000000000000..e019eaf9f4231 --- /dev/null +++ b/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 +* +-/ + +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