Commit 2022-01-13 20:16 6fa2e46e

View on Github →

feat(algebra/lie/nilpotent): central extensions of nilpotent Lie modules / algebras are nilpotent (#11422) The main result is lie_algebra.nilpotent_of_nilpotent_quotient.

Estimated changes

Modified src/algebra/lie/abelian.lean

added theorem lie_module.ideal_oper_max_triv_submodule_eq_bot

Modified src/algebra/lie/basic.lean

added theorem lie_module_hom.coe_id

added def lie_module_hom.id

added theorem lie_module_hom.id_apply

Modified src/algebra/lie/ideal_operations.lean

added theorem lie_submodule.map_bracket_eq

Modified src/algebra/lie/nilpotent.lean

added theorem coe_lower_central_series_ideal_quot_eq

added theorem lie_algebra.nilpotent_of_nilpotent_quotient

deleted theorem lie_ideal.lower_central_series_map_le

added theorem lie_ideal.map_lower_central_series_le

added theorem lie_module.map_lower_central_series_le

added theorem lie_module.nilpotent_of_nilpotent_quotient

Modified src/algebra/lie/quotient.lean

added theorem lie_submodule.quotient.map_mk'_eq_bot_le

added theorem lie_submodule.quotient.mk'_ker

added theorem lie_submodule.quotient.mk_eq_zero

Modified src/algebra/lie/submodule.lean

added theorem lie_module_hom.comp_ker_incl

added def lie_module_hom.ker

added theorem lie_module_hom.ker_id

added theorem lie_module_hom.le_ker_iff_map

added theorem lie_module_hom.mem_ker

modified theorem lie_subalgebra.coe_to_lie_submodule

modified theorem lie_subalgebra.exists_lie_ideal_coe_eq_iff

modified theorem lie_subalgebra.exists_nested_lie_ideal_coe_eq_iff

modified theorem lie_subalgebra.mem_to_lie_submodule

modified def lie_subalgebra.to_lie_submodule

added theorem lie_submodule.coe_submodule_map