Commit 2024-10-22 08:37 1ece609f

View on Github →

feat: define finitely-semisimple linear maps (#17689) The motivation is to be able to apply IsFinitelySemisimple.maxGenEigenspace_eq_eigenspace to symmetric maps in infinite dimensions. Such maps are not in general semisimple but are semisimple on each invariant finite-dimensional subspace.

Estimated changes

Modified Mathlib.lean

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

Created Mathlib/Algebra/Module/Submodule/Invariant.lean

added theorem Module.End.invtSubmodule.map_subtype_mem_of_mem_invtSubmodule

added def Module.End.invtSubmodule

added theorem Module.End.mem_invtSubmodule

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

added theorem Submodule.orderIsoMapComap_symm_apply

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

added theorem Submodule.comap_subtype_le_iff

Modified Mathlib/Algebra/Polynomial/Module/AEval.lean

added def LinearEquiv.ofAEval

deleted def Module.AEval.comapSubmodule

deleted theorem Module.AEval.comapSubmodule_le_comap

deleted theorem Module.AEval.comapSubmodule_mapSubmodule

added def Module.AEval.equiv_mapSubmodule

deleted theorem Module.AEval.injective_comapSubmodule

modified def Module.AEval.mapSubmodule

deleted theorem Module.AEval.mapSubmodule_comapSubmodule

deleted theorem Module.AEval.mem_comapSubmodule

deleted theorem Module.AEval.mem_mapSubmodule

added theorem Module.AEval.mem_mapSubmodule_apply

added theorem Module.AEval.mem_mapSubmodule_symm_apply

deleted theorem Module.AEval.range_comapSubmodule

Modified Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean

added theorem Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace

added theorem Module.End.IsFinitelySemisimple.maxGenEigenspace_eq_eigenspace

deleted theorem Module.End.IsSemisimple.genEigenspace_eq_eigenspace

deleted theorem Module.End.IsSemisimple.maxGenEigenspace_eq_eigenspace

deleted theorem Module.End.apply_eq_of_mem_genEigenspace_of_comm_of_isSemisimple_of_isNilpotent_sub

added theorem Module.End.apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil

Modified Mathlib/LinearAlgebra/Semisimple.lean

added theorem Module.End.IsFinitelySemisimple.restrict

added def Module.End.IsFinitelySemisimple

added theorem Module.End.IsSemisimple.isFinitelySemisimple

modified theorem Module.End.IsSemisimple.restrict

added def Module.End.IsSemisimple

added theorem Module.End.eq_zero_of_isNilpotent_of_isFinitelySemisimple

added theorem Module.End.isFinitelySemisimple_iff'

added theorem Module.End.isFinitelySemisimple_iff

added theorem Module.End.isFinitelySemisimple_iff_isSemisimple

added theorem Module.End.isFinitelySemisimple_sub_algebraMap_iff

added theorem Module.End.isSemisimple_iff'

modified theorem Module.End.isSemisimple_neg

added theorem Module.End.isSemisimple_restrict_iff

Modified Mathlib/Order/Disjoint.lean

added theorem complementedLattice_iff

Modified Mathlib/Order/Hom/Set.lean

Modified Mathlib/Order/LatticeIntervals.lean