Commit 2023-10-11 20:05 2c0ab8d7

View on Github →

feat: Fitting decomposition of a representation of a nilpotent Lie algebra (#7556)

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Algebra/Lie/Weights.lean to Mathlib/Algebra/Lie/Weights/Basic.lean

deleted theorem LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul

deleted theorem LieAlgebra.coe_zeroRootSubalgebra

deleted theorem LieAlgebra.is_cartan_of_zeroRootSubalgebra_eq

deleted theorem LieAlgebra.le_zeroRootSubalgebra

deleted theorem LieAlgebra.lie_mem_weightSpace_of_mem_weightSpace

deleted theorem LieAlgebra.mem_zeroRootSubalgebra

deleted def LieAlgebra.rootSpaceProduct

deleted theorem LieAlgebra.rootSpaceProduct_def

deleted theorem LieAlgebra.rootSpaceProduct_tmul

deleted def LieAlgebra.rootSpaceWeightSpaceProduct

deleted def LieAlgebra.rootSpaceWeightSpaceProductAux

deleted theorem LieAlgebra.rootSpace_comap_eq_weightSpace

deleted theorem LieAlgebra.toLieSubmodule_le_rootSpace_zero

deleted def LieAlgebra.zeroRootSubalgebra

deleted theorem LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan

deleted theorem LieAlgebra.zeroRootSubalgebra_eq_of_is_cartan

deleted theorem LieAlgebra.zeroRootSubalgebra_normalizer_eq_self

deleted theorem LieAlgebra.zero_rootSpace_eq_top_of_nilpotent

deleted def LieModule.IsWeight

added theorem LieModule.coe_weightSpaceOf_zero

modified theorem LieModule.coe_weightSpace_of_top

added theorem LieModule.comap_weightSpace_eq_of_injective

modified theorem LieModule.iSup_ucs_eq_weightSpace_zero

modified theorem LieModule.iSup_ucs_le_weightSpace_zero

added theorem LieModule.isCompl_weightSpaceOf_zero_posFittingCompOf

added theorem LieModule.isCompl_weightSpace_zero_posFittingComp

modified theorem LieModule.isNilpotent_toEndomorphism_weightSpace_zero

deleted theorem LieModule.isWeight_zero_of_nilpotent

added theorem LieModule.map_posFittingComp_eq

added theorem LieModule.map_posFittingComp_le

added theorem LieModule.map_weightSpace_eq

added theorem LieModule.map_weightSpace_eq_of_injective

added theorem LieModule.map_weightSpace_le

modified theorem LieModule.mem_posFittingComp

modified theorem LieModule.mem_posFittingCompOf

modified theorem LieModule.mem_weightSpace

modified theorem LieModule.mem_weightSpaceOf

modified def LieModule.posFittingComp

modified def LieModule.posFittingCompOf

modified theorem LieModule.posFittingCompOf_le_lowerCentralSeries

modified theorem LieModule.posFittingCompOf_le_posFittingComp

modified theorem LieModule.posFittingComp_le_iInf_lowerCentralSeries

added theorem LieModule.posFittingComp_map_incl_sup_of_codisjoint

modified def LieModule.weightSpace

modified def LieModule.weightSpaceOf

modified theorem LieModule.weightSpace_zero_normalizer_eq_self

modified theorem LieModule.zero_weightSpace_eq_top_of_nilpotent'

modified theorem LieModule.zero_weightSpace_eq_top_of_nilpotent

Created Mathlib/Algebra/Lie/Weights/Cartan.lean

added theorem LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul

added theorem LieAlgebra.coe_zeroRootSubalgebra

added theorem LieAlgebra.is_cartan_of_zeroRootSubalgebra_eq

added theorem LieAlgebra.le_zeroRootSubalgebra

added theorem LieAlgebra.lie_mem_weightSpace_of_mem_weightSpace

added theorem LieAlgebra.mem_zeroRootSubalgebra

added def LieAlgebra.rootSpaceProduct

added theorem LieAlgebra.rootSpaceProduct_def

added theorem LieAlgebra.rootSpaceProduct_tmul

added def LieAlgebra.rootSpaceWeightSpaceProduct

added def LieAlgebra.rootSpaceWeightSpaceProductAux

added theorem LieAlgebra.rootSpace_comap_eq_weightSpace

added theorem LieAlgebra.toLieSubmodule_le_rootSpace_zero

added def LieAlgebra.zeroRootSubalgebra

added theorem LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan

added theorem LieAlgebra.zeroRootSubalgebra_eq_of_is_cartan

added theorem LieAlgebra.zeroRootSubalgebra_normalizer_eq_self

added theorem LieAlgebra.zero_rootSpace_eq_top_of_nilpotent

added def LieModule.IsWeight

added theorem LieModule.isWeight_zero_of_nilpotent