feat: sum and product of commuting semisimple endomorphisms (#10808)

+ Prove `isSemisimple_of_mem_adjoin`: if two commuting endomorphisms of a finite-dimensional vector space over a perfect field are both semisimple, then every endomorphism in the algebra generated by them (in particular their product and sum) is semisimple.

+ In the same file LinearAlgebra/Semisimple.lean, `eq_zero_of_isNilpotent_isSemisimple` and `isSemisimple_of_squarefree_aeval_eq_zero` are golfed, and `IsSemisimple.minpoly_squarefree` is proved

RingTheory/SimpleModule.lean:

+ Define `IsSemisimpleRing R` to mean that R is a semisimple R-module.
add properties of simple modules and a characterization (they are exactly the quotients of the ring by maximal left ideals).

+ The annihilator of a semisimple module is a radical ideal.

+ Any module over a semisimple ring is semisimple.

+ A finite product of semisimple rings is semisimple.

+ Any quotient of a semisimple ring is semisimple.

+ Add Artin--Wedderburn as a TODO (proof_wanted).

+ Order/Atoms.lean: add the instance from `IsSimpleOrder` to `ComplementedLattice`, so that `IsSimpleModule → IsSemisimpleModule` is automatically inferred.

Prerequisites for showing a product of semisimple rings is semisimple:

+ Algebra/Module/Submodule/Map.lean: generalize `orderIsoMapComap` so that it only requires `RingHomSurjective` rather than `RingHomInvPair`

+ Algebra/Ring/CompTypeclasses.lean, Mathlib/Algebra/Ring/Pi.lean, Algebra/Ring/Prod.lean: add RingHomSurjective instances


RingTheory/Artinian.lean:

+ `quotNilradicalEquivPi`: the quotient of a commutative Artinian ring R by its nilradical is isomorphic to the (finite) product of its quotients by maximal ideals (therefore a product of fields).
`equivPi`: if the ring is moreover reduced, then the ring itself is a product of fields. Deduce that R is a semisimple ring and both R and R[X] are decomposition monoids. Requires `RingEquiv.quotientBot` in RingTheory/Ideal/QuotientOperations.lean.

+ Data/Polynomial/Eval.lean: the polynomial ring over a finite product of rings is isomorphic to the product of polynomial rings over individual rings. (Used to show R[X] is a decomposition monoid.)

Other necessary results:

+ FieldTheory/Minpoly/Field.lean: the minimal polynomial of an element in a reduced algebra over a field is radical.

+ RingTheory/PowerBasis.lean: generalize `PowerBasis.finiteDimensional` and rename it to `.finite`.

Annihilator stuff, some of which do not end up being used:

+ RingTheory/Ideal/Operations.lean: define `Module.annihilator` and redefine `Submodule.annihilator` in terms of it; add lemmas, including one that says an arbitrary intersection of radical ideals is radical. The new lemma `Ideal.isRadical_iff_pow_one_lt` depends on `pow_imp_self_of_one_lt` in Mathlib/Data/Nat/Interval.lean, which is also used to golf the proof of `isRadical_iff_pow_one_lt`.

+ Algebra/Module/Torsion.lean: add a lemma and an instance (unused)

+ Data/Polynomial/Module/Basic.lean: add a def (unused) and a lemma

+ LinearAlgebra/AnnihilatingPolynomial.lean: add lemma `span_minpoly_eq_annihilator`

Some results about idempotent linear maps (projections) and idempotent elements, used to show that any (left) ideal in a semisimple ring is spanned by an idempotent element (unused):

+ LinearAlgebra/Projection.lean: add def `isIdempotentElemEquiv`

+ LinearAlgebra/Span.lean: add two lemmas




Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/Algebra/Algebra/Tower.lean

@@ -84,14 +84,24 @@ section Module
 
 variable [CommSemiring R] [Semiring A] [Algebra R A]
 
-variable [SMul R M] [MulAction A M] [IsScalarTower R A M]
+variable [MulAction A M]
 
 variable {R} {M}
 
-theorem algebraMap_smul (r : R) (x : M) : algebraMap R A r • x = r • x := by
+theorem algebraMap_smul [SMul R M] [IsScalarTower R A M] (r : R) (x : M) :
+    algebraMap R A r • x = r • x := by
   rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
 #align is_scalar_tower.algebra_map_smul IsScalarTower.algebraMap_smul
 
+variable {A} in
+theorem of_algebraMap_smul [SMul R M] (h : ∀ (r : R) (x : M), algebraMap R A r • x = r • x) :
+    IsScalarTower R A M where
+  smul_assoc r a x := by rw [Algebra.smul_def, mul_smul, h]
+
+variable (R M) in
+theorem of_compHom : letI := MulAction.compHom M (algebraMap R A : R →* A); IsScalarTower R A M :=
+  letI := MulAction.compHom M (algebraMap R A : R →* A); of_algebraMap_smul fun _ _ ↦ rfl
+
 end Module
 
 section Semiring

Mathlib/Algebra/Module/Submodule/Map.lean

@@ -36,8 +36,6 @@ variable [Semiring R] [Semiring R₂] [Semiring R₃]
 variable [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃]
 variable [Module R M] [Module R₂ M₂] [Module R₃ M₃]
 variable {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃}
-variable {σ₂₁ : R₂ →+* R}
-variable [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]
 variable [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
 variable (p p' : Submodule R M) (q q' : Submodule R₂ M₂)
 variable {x : M}
@@ -142,6 +140,7 @@ end
 
 section SemilinearMap
 
+variable {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]
 variable {F : Type*} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂]
 
 /-- The pushforward of a submodule by an injective linear map is
@@ -392,16 +391,22 @@ end SemilinearMap
 
 section OrderIso
 
-variable {F : Type*} [EquivLike F M M₂] [SemilinearEquivClass F σ₁₂ M M₂]
+variable [RingHomSurjective σ₁₂] {F : Type*}
 
 /-- A linear isomorphism induces an order isomorphism of submodules. -/
 @[simps symm_apply apply]
-def orderIsoMapComap (f : F) : Submodule R M ≃o Submodule R₂ M₂ where
+def orderIsoMapComapOfBijective [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂]
+    (f : F) (hf : Bijective f) : Submodule R M ≃o Submodule R₂ M₂ where
   toFun := map f
   invFun := comap f
-  left_inv := comap_map_eq_of_injective (EquivLike.injective f)
-  right_inv := map_comap_eq_of_surjective (EquivLike.surjective f)
-  map_rel_iff' := map_le_map_iff_of_injective (EquivLike.injective f) _ _
+  left_inv := comap_map_eq_of_injective hf.injective
+  right_inv := map_comap_eq_of_surjective hf.surjective
+  map_rel_iff' := map_le_map_iff_of_injective hf.injective _ _
+
+/-- A linear isomorphism induces an order isomorphism of submodules. -/
+@[simps! symm_apply apply]
+def orderIsoMapComap [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) :
+    Submodule R M ≃o Submodule R₂ M₂ := orderIsoMapComapOfBijective f (EquivLike.bijective f)
 #align submodule.order_iso_map_comap Submodule.orderIsoMapComap
 
 end OrderIso

Mathlib/Algebra/Module/Torsion.lean

@@ -232,6 +232,9 @@ def IsTorsion :=
   ∀ ⦃x : M⦄, ∃ a : R⁰, a • x = 0
 #align module.is_torsion Module.IsTorsion
 
+theorem isTorsionBySet_annihilator : IsTorsionBySet R M (Module.annihilator R M) :=
+  fun _ r ↦ Module.mem_annihilator.mp r.2 _
+
 end Module
 
 end Defs
@@ -542,6 +545,11 @@ instance IsTorsionBySet.isScalarTower
     (fun b d x => Quotient.inductionOn' d fun c => (smul_assoc b c x : _))
 #align module.is_torsion_by_set.is_scalar_tower Module.IsTorsionBySet.isScalarTower
 
+/-- Any module is also a modle over the quotient of the ring by the annihilator.
+Not an instance because it causes synthesis failures / timeouts. -/
+def quotientAnnihilator : Module (R ⧸ Module.annihilator R M) M :=
+  (isTorsionBySet_annihilator R M).module
+
 instance : Module (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M)) :=
   IsTorsionBySet.module (R := R) (I := I) fun x r => by
     induction x using Quotient.inductionOn

Mathlib/Algebra/Ring/CompTypeclasses.lean

@@ -198,4 +198,6 @@ theorem comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomSurjective 
       rwa [← RingHom.coe_comp, RingHomCompTriple.comp_eq] at this }
 #align ring_hom_surjective.comp RingHomSurjective.comp
 
+instance (σ : R₁ ≃+* R₂) : RingHomSurjective (σ : R₁ →+* R₂) := ⟨σ.surjective⟩
+
 end RingHomSurjective

Mathlib/Algebra/Ring/Pi.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
 import Mathlib.Algebra.Group.Pi.Lemmas
+import Mathlib.Algebra.Ring.CompTypeclasses
 import Mathlib.Algebra.Ring.Hom.Defs
 
 #align_import algebra.ring.pi from "leanprover-community/mathlib"@"ba2245edf0c8bb155f1569fd9b9492a9b384cde6"
@@ -170,6 +171,10 @@ def Pi.evalRingHom (f : I → Type v) [∀ i, NonAssocSemiring (f i)] (i : I) :
 #align pi.eval_ring_hom Pi.evalRingHom
 #align pi.eval_ring_hom_apply Pi.evalRingHom_apply
 
+instance (f : I → Type*) [∀ i, Semiring (f i)] (i) :
+    RingHomSurjective (Pi.evalRingHom f i) where
+  is_surjective x := ⟨by classical exact (if h : · = i then h ▸ x else 0), by simp⟩
+
 /-- `Function.const` as a `RingHom`. -/
 @[simps]
 def Pi.constRingHom (α β : Type*) [NonAssocSemiring β] : β →+* α → β :=

Mathlib/Algebra/Ring/Prod.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Chris Hughes, Mario Carneiro, Yury Kudryashov
 -/
 import Mathlib.Data.Int.Cast.Prod
 import Mathlib.Algebra.Group.Prod
+import Mathlib.Algebra.Ring.CompTypeclasses
 import Mathlib.Algebra.Ring.Equiv
 import Mathlib.Algebra.Order.Group.Prod
 import Mathlib.Algebra.Order.Ring.Defs
@@ -202,6 +203,9 @@ def snd : R × S →+* S :=
   { MonoidHom.snd R S, AddMonoidHom.snd R S with toFun := Prod.snd }
 #align ring_hom.snd RingHom.snd
 
+instance (R S) [Semiring R] [Semiring S] : RingHomSurjective (fst R S) := ⟨(⟨⟨·, 0⟩, rfl⟩)⟩
+instance (R S) [Semiring R] [Semiring S] : RingHomSurjective (snd R S) := ⟨(⟨⟨0, ·⟩, rfl⟩)⟩
+
 variable {R S}
 
 @[simp]

Mathlib/Data/Nat/Interval.lean

@@ -396,4 +396,11 @@ theorem Nat.cauchy_induction_two_mul (seed : ℕ) (hs : P seed.succ)
   Nat.cauchy_induction_mul h 2 seed one_lt_two hs hm n
 #align nat.cauchy_induction_two_mul Nat.cauchy_induction_two_mul
 
+theorem Nat.pow_imp_self_of_one_lt {M} [Monoid M] (k : ℕ) (hk : 1 < k)
+    (P : M → Prop) (hmul : ∀ x y, P x → P (x * y) ∨ P (y * x))
+    (hpow : ∀ x, P (x ^ k) → P x) : ∀ n x, P (x ^ n) → P x :=
+  k.cauchy_induction_mul (fun n ih x hx ↦ ih x <| (hmul _ x hx).elim
+    (fun h ↦ by rwa [_root_.pow_succ']) fun h ↦ by rwa [_root_.pow_succ]) 0 hk
+    (fun x hx ↦ pow_one x ▸ hx) fun n _ hn x hx ↦ hpow x <| hn _ <| (pow_mul x k n).subst hx
+
 end Induction

Mathlib/Data/Polynomial/Eval.lean

@@ -837,6 +837,17 @@ theorem map_map [Semiring T] (g : S →+* T) (p : R[X]) : (p.map f).map g = p.ma
 theorem map_id : p.map (RingHom.id _) = p := by simp [Polynomial.ext_iff, coeff_map]
 #align polynomial.map_id Polynomial.map_id
 
+/-- The polynomial ring over a finite product of rings is isomorphic to
+the product of polynomial rings over individual rings. -/
+def piEquiv {ι} [Finite ι] (R : ι → Type*) [∀ i, Semiring (R i)] :
+    (∀ i, R i)[X] ≃+* ∀ i, (R i)[X] :=
+  .ofBijective (Pi.ringHom fun i ↦ mapRingHom (Pi.evalRingHom R i))
+    ⟨fun p q h ↦ by ext n i; simpa using congr_arg (fun p ↦ coeff (p i) n) h,
+      fun p ↦ ⟨.ofFinsupp (.ofSupportFinite (fun n i ↦ coeff (p i) n) <|
+        (Set.finite_iUnion fun i ↦ (p i).support.finite_toSet).subset fun n hn ↦ by
+          simp only [Set.mem_iUnion, Finset.mem_coe, mem_support_iff, Function.mem_support] at hn ⊢
+          contrapose! hn; exact funext hn), by ext i n; exact coeff_map _ _⟩⟩
+
 theorem eval₂_eq_eval_map {x : S} : p.eval₂ f x = (p.map f).eval x := by
   -- Porting note: `apply` → `induction`
   induction p using Polynomial.induction_on' with

Mathlib/Data/Polynomial/Module/Basic.lean

@@ -88,6 +88,24 @@ instance instIsScalarTowerOrigPolynomial : IsScalarTower R R[X] <| AEval R M a w
 instance instFinitePolynomial [Finite R M] : Finite R[X] <| AEval R M a :=
   Finite.of_restrictScalars_finite R _ _
 
+/-- Construct an `R[X]`-linear map out of `AEval R M a` from a `R`-linear map out of `M`. -/
+def _root_.LinearMap.ofAEval {N} [AddCommMonoid N] [Module R N] [Module R[X] N]
+    [IsScalarTower R R[X] N] (f : M →ₗ[R] N) (hf : ∀ m : M, f (a • m) = (X : R[X]) • f m) :
+    AEval R M a →ₗ[R[X]] N where
+  __ := f ∘ₗ (of R M a).symm
+  map_smul' p := p.induction_on (fun k m ↦ by simp [C_eq_algebraMap])
+    (fun p q hp hq m ↦ by simp_all [add_smul]) fun n k h m ↦ by
+      simp_rw [RingHom.id_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
+        LinearMap.comp_apply, LinearEquiv.coe_toLinearMap] at h ⊢
+      simp_rw [pow_succ', ← mul_assoc, mul_smul _ X, ← hf, ← of_symm_X_smul, ← h]
+
+lemma annihilator_eq_ker_aeval [FaithfulSMul A M] :
+    annihilator R[X] (AEval R M a) = RingHom.ker (aeval a) := by
+  ext p
+  simp_rw [mem_annihilator, RingHom.mem_ker]
+  change (∀ m : M, aeval a p • m = 0) ↔ _
+  exact ⟨fun h ↦ eq_of_smul_eq_smul (α := M) <| by simp [h], fun h ↦ by simp [h]⟩
+
 @[simp]
 lemma annihilator_top_eq_ker_aeval [FaithfulSMul A M] :
     (⊤ : Submodule R[X] <| AEval R M a).annihilator = RingHom.ker (aeval a) := by

Mathlib/FieldTheory/Adjoin.lean

@@ -1136,7 +1136,7 @@ noncomputable def adjoin.powerBasis {x : L} (hx : IsIntegral K x) : PowerBasis K
 #align intermediate_field.adjoin.power_basis IntermediateField.adjoin.powerBasis
 
 theorem adjoin.finiteDimensional {x : L} (hx : IsIntegral K x) : FiniteDimensional K K⟮x⟯ :=
-  PowerBasis.finiteDimensional (adjoin.powerBasis hx)
+  (adjoin.powerBasis hx).finite
 #align intermediate_field.adjoin.finite_dimensional IntermediateField.adjoin.finiteDimensional
 
 theorem isAlgebraic_adjoin_simple {x : L} (hx : IsIntegral K x) : Algebra.IsAlgebraic K K⟮x⟯ :=
@@ -1297,7 +1297,7 @@ theorem _root_.Polynomial.irreducible_comp {f g : K[X]} (hfm : f.Monic) (hgm : g
     (this.trans natDegree_comp.symm).ge).irreducible hp₁
   have := Fact.mk hp₁
   let Kx := AdjoinRoot p
-  letI := (AdjoinRoot.powerBasis hp₁.ne_zero).finiteDimensional
+  letI := (AdjoinRoot.powerBasis hp₁.ne_zero).finite
   have key₁ : f = minpoly K (aeval (root p) g) := by
     refine minpoly.eq_of_irreducible_of_monic hf ?_ hfm
     rw [← aeval_comp]

Mathlib/FieldTheory/Minpoly/Field.lean

@@ -82,6 +82,9 @@ variable {A x} in
 lemma dvd_iff {p : A[X]} : minpoly A x ∣ p ↔ Polynomial.aeval x p = 0 :=
   ⟨fun ⟨q, hq⟩ ↦ by rw [hq, map_mul, aeval, zero_mul], minpoly.dvd A x⟩
 
+theorem isRadical [IsReduced B] : IsRadical (minpoly A x) := fun n p dvd ↦ by
+  rw [dvd_iff] at dvd ⊢; rw [map_pow] at dvd; exact IsReduced.eq_zero _ ⟨n, dvd⟩
+
 theorem dvd_map_of_isScalarTower (A K : Type*) {R : Type*} [CommRing A] [Field K] [CommRing R]
     [Algebra A K] [Algebra A R] [Algebra K R] [IsScalarTower A K R] (x : R) :
     minpoly K x ∣ (minpoly A x).map (algebraMap A K) := by

Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean

@@ -177,6 +177,11 @@ theorem monic_generator_eq_minpoly (a : A) (p : 𝕜[X]) (p_monic : p.Monic)
     · apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)
 #align polynomial.monic_generator_eq_minpoly Polynomial.monic_generator_eq_minpoly
 
+theorem span_minpoly_eq_annihilator {M} [AddCommGroup M] [Module 𝕜 M] (f : Module.End 𝕜 M) :
+    Ideal.span {minpoly 𝕜 f} = Module.annihilator 𝕜[X] (Module.AEval' f) := by
+  rw [← annIdealGenerator_eq_minpoly, span_singleton_annIdealGenerator]; ext
+  rw [mem_annIdeal_iff_aeval_eq_zero, DFunLike.ext_iff, Module.mem_annihilator]; rfl
+
 end Field
 
 end Polynomial

Mathlib/LinearAlgebra/FreeModule/Norm.lean

@@ -65,7 +65,7 @@ instance (b : Basis ι F[X] S) {I : Ideal S} (hI : I ≠ ⊥) (i : ι) :
   -- operations to the `Quotient.lift` level and then end up comparing huge
   -- terms.  We should probably make most of the quotient operations
   -- irreducible so that they don't expose `Quotient.lift` accidentally.
-  refine PowerBasis.finiteDimensional ?_
+  refine PowerBasis.finite ?_
   refine AdjoinRoot.powerBasis ?_
   exact I.smithCoeffs_ne_zero b hI i
 

Mathlib/LinearAlgebra/JordanChevalley.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.Dynamics.Newton
-import Mathlib.FieldTheory.Perfect
 import Mathlib.LinearAlgebra.Semisimple
 
 /-!

Mathlib/LinearAlgebra/Projection.lean

@@ -361,6 +361,21 @@ theorem coe_isComplEquivProj_symm_apply (f : { f : E →ₗ[R] p // ∀ x : p, f
     (p.isComplEquivProj.symm f : Submodule R E) = ker (f : E →ₗ[R] p) := rfl
 #align submodule.coe_is_compl_equiv_proj_symm_apply Submodule.coe_isComplEquivProj_symm_apply
 
+/-- The idempotent endomorphisms of a module with range equal to a submodule are in 1-1
+correspondence with linear maps to the submodule that restrict to the identity on the submodule.-/
+@[simps] def isIdempotentElemEquiv :
+    { f : Module.End R E // IsIdempotentElem f ∧ range f = p } ≃
+    { f : E →ₗ[R] p // ∀ x : p, f x = x } where
+  toFun f := ⟨f.1.codRestrict _ fun x ↦ by simp_rw [← f.2.2]; exact mem_range_self f.1 x,
+    fun ⟨x, hx⟩ ↦ Subtype.ext <| by
+      obtain ⟨x, rfl⟩ := f.2.2.symm ▸ hx
+      exact DFunLike.congr_fun f.2.1 x⟩
+  invFun f := ⟨p.subtype ∘ₗ f.1, LinearMap.ext fun x ↦ by simp [f.2], le_antisymm
+    ((range_comp_le_range _ _).trans_eq p.range_subtype)
+    fun x hx ↦ ⟨x, Subtype.ext_iff.1 <| f.2 ⟨x, hx⟩⟩⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
 end Submodule
 
 namespace LinearMap