Commit 2024-04-23 19:39 2ae61622

View on Github →

feat(Algebra/Lie): prove derivations are inner in finite-dimensional Killing Lie algebra (#12250) This finishes the proof that all derivations in a finite-dimensional Lie algebra with non-degenerate Killing form are inner derivations, a project discussed in this thread with @ocfnash.

Estimated changes

Modified Mathlib.lean

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

added theorem LieDerivation.injective_ad_of_center_eq_bot

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

added theorem LieDerivation.Killing.ad_apply_eq_zero_iff

added theorem LieDerivation.Killing.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal

added theorem LieDerivation.Killing.ad_mem_orthogonal_of_mem_orthogonal

added theorem LieDerivation.Killing.exists_eq_ad

added theorem LieDerivation.Killing.killingForm_restrict_range_ad

added theorem LieDerivation.Killing.killingForm_restrict_range_ad_nondegenerate

added theorem LieDerivation.Killing.range_ad_eq_top

Modified Mathlib/Algebra/Lie/Killing.lean

added theorem LieIdeal.toSubmodule_killingCompl

added theorem LieModule.traceForm_isSymm

Modified Mathlib/Algebra/Lie/Submodule.lean

added theorem LieHom.IsIdealMorphism.eq

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

added theorem LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot

modified theorem LinearMap.BilinForm.finrank_add_finrank_orthogonal

added theorem LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict

added theorem LinearMap.BilinForm.orthogonal_bot

added theorem LinearMap.BilinForm.orthogonal_eq_bot_iff

added theorem LinearMap.BilinForm.orthogonal_eq_top_iff

modified theorem LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal

modified theorem LinearMap.BilinForm.restrict_nondegenerate_of_isCompl_orthogonal