feat: define semisimple linear endomorphisms (#9825)

Mathlib.lean

@@ -2528,6 +2528,7 @@ import Mathlib.LinearAlgebra.Ray
 import Mathlib.LinearAlgebra.Reflection
 import Mathlib.LinearAlgebra.RootSystem.Basic
 import Mathlib.LinearAlgebra.SModEq
+import Mathlib.LinearAlgebra.Semisimple
 import Mathlib.LinearAlgebra.SesquilinearForm
 import Mathlib.LinearAlgebra.Span
 import Mathlib.LinearAlgebra.StdBasis

Mathlib/Algebra/Module/Submodule/Map.lean

@@ -449,6 +449,11 @@ protected theorem map_neg (f : M →ₗ[R] M₂) : map (-f) p = map f p :=
       hy ▸ ⟨-x, show -x ∈ p from neg_mem hx, (map_neg (-f) _).trans (neg_neg (f x))⟩⟩
 #align submodule.map_neg Submodule.map_neg
 
+@[simp]
+lemma comap_neg {f : M →ₗ[R] M₂} {p : Submodule R M₂} :
+    p.comap (-f) = p.comap f := by
+  ext; simp
+
 end AddCommGroup
 
 end Submodule

Mathlib/Data/Polynomial/Module.lean

@@ -24,7 +24,7 @@ In the special case that `A = M →ₗ[R] M` and `φ : M →ₗ[R] M`, the modul
 abbreviated `Module.AEval' φ`. In this module we have `X • m = ↑φ m`.
 -/
 universe u v
-open Polynomial BigOperators
+open Set Function Polynomial BigOperators
 
 namespace Module
 /--
@@ -132,6 +132,18 @@ def mapSubmodule : Submodule R[X] <| AEval R M a :=
     comapSubmodule R M a (mapSubmodule a hp) = p := by
   ext; simp
 
+variable (R M)
+
+lemma injective_comapSubmodule : Injective (comapSubmodule R M a) := by
+  intro q₁ q₂ hq
+  rw [← mapSubmodule_comapSubmodule (q := q₁), ← mapSubmodule_comapSubmodule (q := q₂)]
+  simp_rw [hq]
+
+lemma range_comapSubmodule :
+    range (comapSubmodule R M a) = {p | p ≤ p.comap (Algebra.lsmul R R M a)} :=
+  le_antisymm (fun _ ⟨_, hq⟩ ↦ hq ▸ comapSubmodule_le_comap a)
+    (fun _ hp ↦ ⟨mapSubmodule a hp, comapSubmodule_mapSubmodule a hp⟩)
+
 end Submodule
 
 end AEval

Mathlib/GroupTheory/Nilpotent.lean

@@ -477,7 +477,7 @@ theorem Subgroup.nilpotencyClass_le (H : Subgroup G) [hG : IsNilpotent G] :
   exact eq_bot_iff.mpr fun x hx => Subtype.ext (this x ⟨hx, rfl⟩)
 #align subgroup.nilpotency_class_le Subgroup.nilpotencyClass_le
 
-instance (priority := 100) isNilpotent_of_subsingleton [Subsingleton G] : IsNilpotent G :=
+instance (priority := 100) Group.isNilpotent_of_subsingleton [Subsingleton G] : IsNilpotent G :=
   nilpotent_iff_lowerCentralSeries.2 ⟨0, Subsingleton.elim ⊤ ⊥⟩
 #align is_nilpotent_of_subsingleton isNilpotent_of_subsingleton
 

Mathlib/LinearAlgebra/Semisimple.lean

@@ -0,0 +1,118 @@
+/-
+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.Data.Polynomial.Module
+import Mathlib.LinearAlgebra.Basis.VectorSpace
+import Mathlib.Order.CompleteSublattice
+import Mathlib.RingTheory.Nilpotent
+import Mathlib.RingTheory.SimpleModule
+
+/-!
+# Semisimple linear endomorphisms
+
+Given an `R`-module `M` together with an `R`-linear endomorphism `f : M → M`, the following two
+conditions are equivalent:
+ 1. Every `f`-invariant submodule of `M` has an `f`-invariant complement.
+ 2. `M` is a semisimple `R[X]`-module, where the action of the polynomial ring is induced by `f`.
+
+A linear endomorphism `f` satisfying these equivalent conditions is known as a *semisimple*
+endomorphism. We provide basic definitions and results about such endomorphisms in this file.
+
+## Main definitions / results:
+ * `Module.End.IsSemisimple`: the definition that a linear endomorphism is semisimple
+ * `Module.End.isSemisimple_iff`: the characterisation of semisimplicity in terms of invariant
+   submodules.
+ * `Module.End.eq_zero_of_isNilpotent_isSemisimple`: the zero endomorphism is the only endomorphism
+   that is both nilpotent and semisimple.
+
+## TODO
+
+In finite dimensions over a field:
+ * Sum / difference / product of commuting semisimple endomorphisms is semisimple
+ * If semisimple then generalized eigenspace is eigenspace
+ * Semisimple iff minpoly is squarefree
+ * Restriction of semisimple endomorphism is semisimple
+ * Triangularizable iff diagonalisable for semisimple endomorphisms
+
+-/
+
+open Set Function Polynomial
+
+variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
+
+namespace Module.End
+
+variable (f g : End R M)
+
+/-- A linear endomorphism of an `R`-module `M` is called *semisimple* if the induced `R[X]`-module
+structure on `M` is semisimple. This is equivalent to saying that every `f`-invariant `R`-submodule
+of `M` has an `f`-invariant complement: see `Module.End.isSemisimple_iff`. -/
+abbrev IsSemisimple := IsSemisimpleModule R[X] (AEval' f)
+
+variable {f g}
+
+lemma isSemisimple_iff :
+    f.IsSemisimple ↔ ∀ p : Submodule R M, p ≤ p.comap f → ∃ q, q ≤ q.comap f ∧ IsCompl p q := by
+  set s := (AEval.comapSubmodule R M f).range
+  have h : s = {p : Submodule R M | p ≤ p.comap f} := AEval.range_comapSubmodule R M f
+  let e := CompleteLatticeHom.toOrderIsoRangeOfInjective _ (AEval.injective_comapSubmodule R M f)
+  simp_rw [Module.End.IsSemisimple, IsSemisimpleModule, e.complementedLattice_iff,
+    s.isComplemented_iff, ← SetLike.mem_coe, h, mem_setOf_eq]
+
+@[simp]
+lemma isSemisimple_zero [IsSemisimpleModule R M] : IsSemisimple (0 : Module.End R M) := by
+  simpa [isSemisimple_iff] using exists_isCompl
+
+@[simp]
+lemma isSemisimple_id [IsSemisimpleModule R M] : IsSemisimple (LinearMap.id : Module.End R M) := by
+  simpa [isSemisimple_iff] using exists_isCompl
+
+@[simp] lemma isSemisimple_neg : (-f).IsSemisimple ↔ f.IsSemisimple := by simp [isSemisimple_iff]
+
+lemma eq_zero_of_isNilpotent_isSemisimple (hn : IsNilpotent f) (hs : f.IsSemisimple) : f = 0 := by
+  nontriviality M
+  set k := nilpotencyClass f
+  wlog hk : 2 ≤ k
+  · replace hk : k = 0 ∨ k = 1 := by omega
+    rcases hk with (hk₀ : nilpotencyClass f = 0) | (hk₁ : nilpotencyClass f = 1)
+    · rw [← pos_nilpotencyClass_iff, hk₀] at hn; contradiction
+    · exact eq_zero_of_nilpotencyClass_eq_one hk₁
+  let p := LinearMap.ker (f ^ (k - 1))
+  have hp : p ≤ p.comap f := fun x hx ↦ by
+    rw [Submodule.mem_comap, LinearMap.mem_ker, ← LinearMap.mul_apply, ← pow_succ', add_comm,
+      pow_add, pow_one, LinearMap.mul_apply, hx, map_zero]
+  obtain ⟨q, hq₀, hq₁, hq₂⟩ := isSemisimple_iff.mp hs p hp
+  replace hq₂ : q ≠ ⊥ := hq₂.ne_bot_of_ne_top <|
+    fun contra ↦ pow_pred_nilpotencyClass hn <| LinearMap.ker_eq_top.mp contra
+  obtain ⟨m, hm₁ : m ∈ q, hm₀ : m ≠ 0⟩ := q.ne_bot_iff.mp hq₂
+  suffices m ∈ p by
+    exfalso
+    apply hm₀
+    rw [← Submodule.mem_bot (R := R), ← hq₁.eq_bot]
+    exact ⟨this, hm₁⟩
+  replace hm₁ : f m = 0 := by
+    rw [← Submodule.mem_bot (R := R), ← hq₁.eq_bot]
+    refine ⟨(?_ : f m ∈ p), hq₀ hm₁⟩
+    rw [LinearMap.mem_ker, ← LinearMap.mul_apply, ← pow_succ', (by omega : k - 1 + 1 = k),
+      pow_nilpotencyClass hn, LinearMap.zero_apply]
+  rw [LinearMap.mem_ker]
+  exact LinearMap.pow_map_zero_of_le (by omega : 1 ≤ k - 1) hm₁
+
+section field
+
+variable {K : Type*} [Field K] [Module K M] {f' : End K M}
+
+lemma IsSemisimple_smul_iff {t : K} (ht : t ≠ 0) :
+    (t • f').IsSemisimple ↔ f'.IsSemisimple := by
+  simp [isSemisimple_iff, Submodule.comap_smul f' (h := ht)]
+
+lemma IsSemisimple_smul (t : K) (h : f'.IsSemisimple) :
+    (t • f').IsSemisimple := by
+  wlog ht : t ≠ 0; · simp [not_not.mp ht]
+  rwa [IsSemisimple_smul_iff ht]
+
+end field
+
+end Module.End

Mathlib/Order/CompleteSublattice.lean

@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Oliver Nash. All rights reserved.
+Copyright (c) 2024 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
@@ -122,4 +122,54 @@ sublattice. -/
 
 @[simp] theorem mem_comap {L : CompleteSublattice β} {a : α} : a ∈ L.comap f ↔ f a ∈ L := Iff.rfl
 
+protected lemma disjoint_iff {a b : L} :
+    Disjoint a b ↔ Disjoint (a : α) (b : α) := by
+  rw [disjoint_iff, disjoint_iff, ← Sublattice.coe_inf, ← coe_bot (L := L),
+    Subtype.coe_injective.eq_iff]
+
+protected lemma codisjoint_iff {a b : L} :
+    Codisjoint a b ↔ Codisjoint (a : α) (b : α) := by
+  rw [codisjoint_iff, codisjoint_iff, ← Sublattice.coe_sup, ← coe_top (L := L),
+    Subtype.coe_injective.eq_iff]
+
+protected lemma isCompl_iff {a b : L} :
+    IsCompl a b ↔ IsCompl (a : α) (b : α) := by
+  rw [isCompl_iff, isCompl_iff, CompleteSublattice.disjoint_iff, CompleteSublattice.codisjoint_iff]
+
+lemma isComplemented_iff : ComplementedLattice L ↔ ∀ a ∈ L, ∃ b ∈ L, IsCompl a b := by
+  refine ⟨fun ⟨h⟩ a ha ↦ ?_, fun h ↦ ⟨fun ⟨a, ha⟩ ↦ ?_⟩⟩
+  · obtain ⟨b, hb⟩ := h ⟨a, ha⟩
+    exact ⟨b, b.property, CompleteSublattice.isCompl_iff.mp hb⟩
+  · obtain ⟨b, hb, hb'⟩ := h a ha
+    exact ⟨⟨b, hb⟩, CompleteSublattice.isCompl_iff.mpr hb'⟩
+
+instance : Top (CompleteSublattice α) := ⟨mk' univ (fun _ _ ↦ mem_univ _) (fun _ _ ↦ mem_univ _)⟩
+
+variable (L)
+
+/-- Copy of a complete sublattice with a new `carrier` equal to the old one. Useful to fix
+definitional equalities. -/
+protected def copy (s : Set α) (hs : s = L) : CompleteSublattice α :=
+  mk' s (hs ▸ L.sSupClosed') (hs ▸ L.sInfClosed')
+
+@[simp, norm_cast] lemma coe_copy (s : Set α) (hs) : L.copy s hs = s := rfl
+
+lemma copy_eq (s : Set α) (hs) : L.copy s hs = L := SetLike.coe_injective hs
+
 end CompleteSublattice
+
+namespace CompleteLatticeHom
+
+/-- The range of a `CompleteLatticeHom` is a `CompleteSublattice`.
+
+See Note [range copy pattern]. -/
+protected def range : CompleteSublattice β :=
+  (CompleteSublattice.map f ⊤).copy (range f) image_univ.symm
+
+theorem range_coe : (f.range : Set β) = range f := rfl
+
+/-- We can regard a complete lattice homomorphism as an order equivalence to its range. -/
+@[simps! apply] noncomputable def toOrderIsoRangeOfInjective (hf : Injective f) : α ≃o f.range :=
+  (orderEmbeddingOfInjective f hf).orderIso
+
+end CompleteLatticeHom

Mathlib/Order/Disjoint.lean

@@ -298,7 +298,7 @@ end PartialOrderTop
 
 section PartialBoundedOrder
 
-variable [PartialOrder α] [BoundedOrder α] {a : α}
+variable [PartialOrder α] [BoundedOrder α] {a b : α}
 
 @[simp]
 theorem codisjoint_bot : Codisjoint a ⊥ ↔ a = ⊤ :=
@@ -310,6 +310,12 @@ theorem bot_codisjoint : Codisjoint ⊥ a ↔ a = ⊤ :=
   ⟨fun h ↦ top_unique <| h bot_le le_rfl, fun h _ _ ha ↦ h.symm.trans_le ha⟩
 #align bot_codisjoint bot_codisjoint
 
+lemma Codisjoint.ne_bot_of_ne_top (h : Codisjoint a b) (ha : a ≠ ⊤) : b ≠ ⊥ := by
+  rintro rfl; exact ha <| by simpa using h
+
+lemma Codisjoint.ne_bot_of_ne_top' (h : Codisjoint a b) (hb : b ≠ ⊤) : a ≠ ⊥ := by
+  rintro rfl; exact hb <| by simpa using h
+
 end PartialBoundedOrder
 
 section SemilatticeSupTop

Mathlib/Order/Hom/Lattice.lean

@@ -258,6 +258,14 @@ instance (priority := 100) OrderIsoClass.toBoundedLatticeHomClass [Lattice α] [
   { OrderIsoClass.toLatticeHomClass, OrderIsoClass.toBoundedOrderHomClass with }
 #align order_iso_class.to_bounded_lattice_hom_class OrderIsoClass.toBoundedLatticeHomClass
 
+/-- We can regard an injective map preserving binary infima as an order embedding. -/
+@[simps! apply]
+def orderEmbeddingOfInjective [SemilatticeInf α] [SemilatticeInf β] (f : F) [InfHomClass F α β]
+    (hf : Injective f) : α ↪o β :=
+  OrderEmbedding.ofMapLEIff f (fun x y ↦ by
+    refine ⟨fun h ↦ ?_, fun h ↦ OrderHomClass.mono f h⟩
+    rwa [← inf_eq_left, ← hf.eq_iff, map_inf, inf_eq_left])
+
 section BoundedLattice
 
 variable [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [BoundedLatticeHomClass F α β]

Mathlib/Order/Hom/Set.lean

@@ -83,6 +83,13 @@ def Set.univ : (Set.univ : Set α) ≃o α where
 
 end OrderIso
 
+/-- We can regard an order embedding as an order isomorphism to its range. -/
+@[simps! apply]
+noncomputable def OrderEmbedding.orderIso [LE α] [LE β] {f : α ↪o β} :
+    α ≃o Set.range f :=
+  { Equiv.ofInjective _ f.injective with
+    map_rel_iff' := f.map_rel_iff }
+
 /-- If a function `f` is strictly monotone on a set `s`, then it defines an order isomorphism
 between `s` and its image. -/
 protected noncomputable def StrictMonoOn.orderIso {α β} [LinearOrder α] [Preorder β] (f : α → β)

Mathlib/RingTheory/Nilpotent.lean

@@ -28,7 +28,7 @@ import Mathlib.LinearAlgebra.Matrix.ToLin
 
 universe u v
 
-open BigOperators
+open BigOperators Function Set
 
 variable {R S : Type*} {x y : R}
 
@@ -45,6 +45,9 @@ theorem IsNilpotent.mk [Zero R] [Pow R ℕ] (x : R) (n : ℕ) (e : x ^ n = 0) :
   ⟨n, e⟩
 #align is_nilpotent.mk IsNilpotent.mk
 
+@[simp] lemma isNilpotent_of_subsingleton [Zero R] [Pow R ℕ] [Subsingleton R] : IsNilpotent x :=
+  ⟨0, Subsingleton.elim _ _⟩
+
 @[simp] theorem IsNilpotent.zero [MonoidWithZero R] : IsNilpotent (0 : R) :=
   ⟨1, pow_one 0⟩
 #align is_nilpotent.zero IsNilpotent.zero
@@ -121,6 +124,74 @@ theorem Commute.IsNilpotent.add_isUnit [Ring R] {r : R} {u : Rˣ} (hnil : IsNilp
   rw [neg_pow, hru.mul_pow, hn]
   simp
 
+section NilpotencyClass
+
+section ZeroPow
+
+variable [Zero R] [Pow R ℕ]
+
+variable (x) in
+/-- If `x` is nilpotent, the nilpotency class is the smallest natural number `k` such that
+`x ^ k = 0`. If `x` is not nilpotent, the nilpotency class takes the junk value `0`. -/
+noncomputable def nilpotencyClass : ℕ := sInf {k | x ^ k = 0}
+
+@[simp] lemma nilpotencyClass_eq_zero_of_subsingleton [Subsingleton R] :
+    nilpotencyClass x = 0 := by
+  let s : Set ℕ := {k | x ^ k = 0}
+  suffices s = univ by change sInf _ = 0; simp [this]
+  exact eq_univ_iff_forall.mpr fun k ↦ Subsingleton.elim _ _
+
+lemma isNilpotent_of_pos_nilpotencyClass (hx : 0 < nilpotencyClass x) :
+    IsNilpotent x := by
+  let s : Set ℕ := {k | x ^ k = 0}
+  change s.Nonempty
+  change 0 < sInf s at hx
+  by_contra contra
+  simp [not_nonempty_iff_eq_empty.mp contra] at hx
+
+lemma pow_nilpotencyClass (hx : IsNilpotent x) : x ^ (nilpotencyClass x) = 0 :=
+  Nat.sInf_mem hx
+
+end ZeroPow
+
+section MonoidWithZero
+
+variable [MonoidWithZero R]
+
+lemma nilpotencyClass_eq_succ_iff {k : ℕ} :
+    nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0 := by
+  let s : Set ℕ := {k | x ^ k = 0}
+  have : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s := fun k₁ k₂ h_le hk₁ ↦ pow_eq_zero_of_le h_le hk₁
+  simp [nilpotencyClass, Nat.sInf_upward_closed_eq_succ_iff this]
+
+@[simp] lemma nilpotencyClass_zero [Nontrivial R] :
+    nilpotencyClass (0 : R) = 1 :=
+  nilpotencyClass_eq_succ_iff.mpr <| by constructor <;> simp
+
+@[simp] lemma pos_nilpotencyClass_iff [Nontrivial R] :
+    0 < nilpotencyClass x ↔ IsNilpotent x := by
+  refine ⟨isNilpotent_of_pos_nilpotencyClass, fun hx ↦ Nat.pos_of_ne_zero fun hx' ↦ ?_⟩
+  replace hx := pow_nilpotencyClass hx
+  rw [hx', pow_zero] at hx
+  exact one_ne_zero hx
+
+lemma pow_pred_nilpotencyClass [Nontrivial R] (hx : IsNilpotent x) :
+    x ^ (nilpotencyClass x - 1) ≠ 0 :=
+  (nilpotencyClass_eq_succ_iff.mp <| Nat.eq_add_of_sub_eq (pos_nilpotencyClass_iff.mpr hx) rfl).2
+
+lemma eq_zero_of_nilpotencyClass_eq_one (hx : nilpotencyClass x = 1) :
+    x = 0 := by
+  have : IsNilpotent x := isNilpotent_of_pos_nilpotencyClass (hx ▸ one_pos)
+  rw [← pow_nilpotencyClass this, hx, pow_one]
+
+@[simp] lemma nilpotencyClass_eq_one [Nontrivial R] :
+    nilpotencyClass x = 1 ↔ x = 0 :=
+  ⟨eq_zero_of_nilpotencyClass_eq_one, fun hx ↦ hx ▸ nilpotencyClass_zero⟩
+
+end MonoidWithZero
+
+end NilpotencyClass
+
 /-- A structure that has zero and pow is reduced if it has no nonzero nilpotent elements. -/
 @[mk_iff]
 class IsReduced (R : Type*) [Zero R] [Pow R ℕ] : Prop where