Commit 2024-05-15 09:43 c93482b4

View on Github →

feat: Cartan subalgebras contain only semisimple elements if the Killing form is non-singular and the coefficients are a perfect field. (#12712) This PR contains the following changes:

The headline result: LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra
Necessary supporting lemmas in linear algebra / order theory

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/DirectSum/Module.lean

Modified Mathlib/Algebra/Lie/Derivation/Killing.lean

added theorem LieDerivation.IsKilling.ad_apply_eq_zero_iff

added theorem LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal

added theorem LieDerivation.IsKilling.ad_mem_orthogonal_of_mem_orthogonal

added theorem LieDerivation.IsKilling.exists_eq_ad

added theorem LieDerivation.IsKilling.killingForm_restrict_range_ad

added theorem LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate

added theorem LieDerivation.IsKilling.range_ad_eq_top

deleted theorem LieDerivation.Killing.ad_apply_eq_zero_iff

deleted theorem LieDerivation.Killing.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal

deleted theorem LieDerivation.Killing.ad_mem_orthogonal_of_mem_orthogonal

deleted theorem LieDerivation.Killing.exists_eq_ad

deleted theorem LieDerivation.Killing.killingForm_restrict_range_ad

deleted theorem LieDerivation.Killing.killingForm_restrict_range_ad_nondegenerate

deleted theorem LieDerivation.Killing.range_ad_eq_top

Modified Mathlib/Algebra/Lie/Submodule.lean

added theorem LieSubmodule.mk_eq_bot_iff

added theorem LieSubmodule.mk_eq_top_iff

Modified Mathlib/Algebra/Lie/Weights/Basic.lean

added theorem LieModule.Weight.apply_eq_zero_of_isNilpotent

added theorem LieModule.Weight.hasEigenvalueAt

added theorem LieModule.Weight.weightSpaceOf_ne_bot

added theorem LieModule.Weight.weightSpace_ne_bot

Modified Mathlib/Algebra/Lie/Weights/Killing.lean

added theorem LieAlgebra.IsKilling.eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebra

added theorem LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra

Modified Mathlib/Algebra/Module/Submodule/LinearMap.lean

added theorem LinearMap.restrict_sub

Modified Mathlib/Algebra/Module/Submodule/Map.lean

Modified Mathlib/Algebra/Module/Submodule/Range.lean

added theorem Submodule.coe_mapIic_apply

added def Submodule.mapIic

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added theorem Module.End.HasEigenvalue.isNilpotent_of_isNilpotent

added theorem Module.End.HasEigenvalue.pow

Created Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean

added theorem Module.End.IsSemisimple.generalizedEigenspace_eq_eigenspace

added theorem Module.End.apply_eq_of_mem_genEigenspace_of_comm_of_isSemisimple_of_isNilpotent_sub

Modified Mathlib/LinearAlgebra/Semisimple.lean

added theorem Module.End.IsSemisimple.restrict

added theorem Module.End.isSemisimple_sub_algebraMap_iff

Modified Mathlib/LinearAlgebra/Span.lean

added theorem Submodule.isCompl_comap_subtype_of_isCompl_of_le

Modified Mathlib/Order/LatticeIntervals.lean

modified theorem Set.Iic.coe_bot

modified theorem Set.Iic.coe_top

Modified Mathlib/Order/ModularLattice.lean

added theorem Set.Iic.isCompl_inf_inf_of_isCompl_of_le

Modified Mathlib/RingTheory/Adjoin/Basic.lean

added theorem Algebra.commute_of_mem_adjoin_of_forall_mem_commute

added theorem Algebra.commute_of_mem_adjoin_self

added theorem Algebra.commute_of_mem_adjoin_singleton_of_commute

Modified Mathlib/RingTheory/Nilpotent/Lemmas.lean

added theorem Module.End.isNilpotent.restrict

Modified Mathlib/RingTheory/SimpleModule.lean