[Merged by Bors] - feat: add proof of Jordan-Chevalley-Dunford decomposition

Mathlib.lean

@@ -2471,6 +2471,7 @@ import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 import Mathlib.LinearAlgebra.GeneralLinearGroup
 import Mathlib.LinearAlgebra.InvariantBasisNumber
 import Mathlib.LinearAlgebra.Isomorphisms
+import Mathlib.LinearAlgebra.JordanChevalley
 import Mathlib.LinearAlgebra.Lagrange
 import Mathlib.LinearAlgebra.LinearIndependent
 import Mathlib.LinearAlgebra.LinearPMap

Mathlib/Algebra/Group/Units.lean

@@ -674,6 +674,11 @@ theorem isUnit_of_mul_eq_one [CommMonoid M] (a b : M) (h : a * b = 1) : IsUnit a
 #align is_unit_of_mul_eq_one isUnit_of_mul_eq_one
 #align is_add_unit_of_add_eq_zero isAddUnit_of_add_eq_zero
 
+@[to_additive]
+theorem isUnit_of_mul_eq_one_right [CommMonoid M] (a b : M) (h : a * b = 1) : IsUnit b := by
+  rw [mul_comm] at h
+  exact isUnit_of_mul_eq_one b a h
+
 section Monoid
 variable [Monoid M] {a b : M}
 

Mathlib/Data/Polynomial/AlgebraMap.lean

@@ -304,6 +304,11 @@ theorem aeval_algHom_apply {F : Type*} [FunLike F A B] [AlgHomClass F R A B]
   rw [map_add, hp, hq, ← map_add, ← map_add]
 #align polynomial.aeval_alg_hom_apply Polynomial.aeval_algHom_apply
 
+@[simp]
+lemma coe_aeval_mk_apply {S : Subalgebra R A} (h : x ∈ S) :
+    (aeval (⟨x, h⟩ : S) p : A) = aeval x p :=
+  (aeval_algHom_apply S.val (⟨x, h⟩ : S) p).symm
+
 theorem aeval_algEquiv (f : A ≃ₐ[R] B) (x : A) : aeval (f x) = (f : A →ₐ[R] B).comp (aeval x) :=
   aeval_algHom (f : A →ₐ[R] B) x
 #align polynomial.aeval_alg_equiv Polynomial.aeval_algEquiv
@@ -365,6 +370,23 @@ theorem _root_.Algebra.adjoin_singleton_eq_range_aeval (x : A) :
   rw [← Algebra.map_top, ← adjoin_X, AlgHom.map_adjoin, Set.image_singleton, aeval_X]
 #align algebra.adjoin_singleton_eq_range_aeval Algebra.adjoin_singleton_eq_range_aeval
 
+@[simp]
+theorem aeval_mem_adjoin_singleton :
+    aeval x p ∈ Algebra.adjoin R {x} := by
+  simpa only [Algebra.adjoin_singleton_eq_range_aeval] using Set.mem_range_self p
+
+instance instCommSemiringAdjoinSingleton :
+    CommSemiring <| Algebra.adjoin R {x} :=
+  { mul_comm := fun ⟨p, hp⟩ ⟨q, hq⟩ ↦ by
+      obtain ⟨p', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hp
+      obtain ⟨q', rfl⟩ := Algebra.adjoin_singleton_eq_range_aeval R x ▸ hq
+      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Submonoid.mk_mul_mk, ← AlgHom.map_mul,
+        mul_comm p' q'] }
+
+instance instCommRingAdjoinSingleton {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (x : A) :
+    CommRing <| Algebra.adjoin R {x} :=
+  { mul_comm := mul_comm }
+
 variable {R}
 
 section Semiring

Mathlib/LinearAlgebra/JordanChevalley.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2024 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import Mathlib.Algebra.Squarefree.UniqueFactorizationDomain
+import Mathlib.Dynamics.Newton
+import Mathlib.FieldTheory.Perfect
+import Mathlib.LinearAlgebra.Semisimple
+
+/-!
+# Jordan-Chevalley-Dunford decomposition
+
+Given a finite-dimensional linear endomorphism `f`, the Jordan-Chevalley-Dunford theorem provides a
+sufficient condition for there to exist a nilpotent endomorphism `n` and a semisimple endomorphism
+`s`, such that `f = n + s` and both `n` and `s` are polynomial expressions in `f`.
+
+The condition is that there exists a separable polynomial `P` such that the endomorphism `P(f)` is
+nilpotent. This condition is always satisfied when the coefficients are a perfect field.
+
+The proof given here uses Newton's method and is taken from Chambert-Loir's notes:
+[Algebre](http://webusers.imj-prg.fr/~antoine.chambert-loir/enseignement/2022-23/agreg/algebre.pdf)
+
+## Main definitions / results:
+
+ * `Module.End.exists_isNilpotent_isSemisimple`: an endomorphism of a finite-dimensional vector
+   space over a perfect field may be written as a sum of nilpotent and semisimple endomorphisms.
+   Moreover these nilpotent and semisimple components are polynomial expressions in the original
+   endomorphism.
+
+## TODO
+
+ * Uniqueness of decomposition (once we prove that the sum of commuting semisimple endomorphims is
+   semisimple, this will follow from `Module.End.eq_zero_of_isNilpotent_isSemisimple`).
+
+-/
+
+open Algebra Polynomial
+
+namespace Module.End
+
+variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : End K V}
+
+theorem exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow {P : K[X]} {k : ℕ}
+    (sep : P.Separable) (nil : minpoly K f ∣ P ^ k) :
+    ∃ᵉ (n ∈ adjoin K {f}) (s ∈ adjoin K {f}), IsNilpotent n ∧ IsSemisimple s ∧ f = n + s := by
+  set ff : adjoin K {f} := ⟨f, self_mem_adjoin_singleton K f⟩
+  set P' := derivative P
+  have nil' : IsNilpotent (aeval ff P) := by
+    use k
+    obtain ⟨q, hq⟩ := nil
+    rw [← AlgHom.map_pow, Subtype.ext_iff]
+    simp [hq]
+  have sep' : IsUnit (aeval ff P') := by
+    obtain ⟨a, b, h⟩ : IsCoprime (P ^ k) P' := sep.pow_left
+    replace h : (aeval f b) * (aeval f P') = 1 := by
+      simpa only [map_add, map_mul, map_one, minpoly.dvd_iff.mp nil, mul_zero, zero_add]
+        using (aeval f).congr_arg h
+    refine isUnit_of_mul_eq_one_right (aeval ff b) _ (Subtype.ext_iff.mpr ?_)
+    simpa [coe_aeval_mk_apply] using h
+  obtain ⟨⟨s, mem⟩, ⟨⟨k, hk⟩, hss⟩, -⟩ := exists_unique_nilpotent_sub_and_aeval_eq_zero nil' sep'
+  refine ⟨f - s, ?_, s, mem, ⟨k, ?_⟩, ?_, (sub_add_cancel f s).symm⟩
+  · exact sub_mem (self_mem_adjoin_singleton K f) mem
+  · rw [Subtype.ext_iff] at hk
+    simpa using hk
+  · replace hss : aeval s P = 0 := by rwa [Subtype.ext_iff, coe_aeval_mk_apply] at hss
+    exact isSemisimple_of_squarefree_aeval_eq_zero sep.squarefree hss
+
+/-- **Jordan-Chevalley-Dunford decomposition**: an endomorphism of a finite-dimensional vector space
+over a perfect field may be written as a sum of nilpotent and semisimple endomorphisms. Moreover
+these nilpotent and semisimple components are polynomial expressions in the original endomorphism.
+-/
+theorem exists_isNilpotent_isSemisimple [PerfectField K] :
+    ∃ᵉ (n ∈ adjoin K {f}) (s ∈ adjoin K {f}), IsNilpotent n ∧ IsSemisimple s ∧ f = n + s := by
+  obtain ⟨g, k, sep, -, nil⟩ := exists_squarefree_dvd_pow_of_ne_zero (minpoly.ne_zero_of_finite K f)
+  rw [← PerfectField.separable_iff_squarefree] at sep
+  exact exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow sep nil
+
+end Module.End

docs/undergrad.yaml

@@ -63,7 +63,7 @@ Linear algebra:
     invariant subspaces of an endomorphism: 'https://en.wikipedia.org/wiki/Invariant_subspace'
     generalized eigenspaces: 'Module.End.generalizedEigenspace'
     kernels lemma: 'https://fr.wikipedia.org/wiki/Lemme_des_noyaux'
-    Jordan-Chevalley-Dunford decomposition: 'https://en.wikipedia.org/wiki/Jordan%E2%80%93Chevalley_decomposition'
+    Jordan-Chevalley-Dunford decomposition: 'Module.End.exists_isNilpotent_isSemisimple'
     Jordan normal form: 'https://en.wikipedia.org/wiki/Jordan_normal_form'
   Linear representations:
     irreducible representation: 'https://en.wikipedia.org/wiki/Irreducible_representation'