Commit 2024-03-05 01:29 0b52a6a5

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