Commit 2025-11-21 12:49 4e3dee5c

View on Github →

feat(Algebra/Lie/Extension): 2-cocycle from a Lie algebra extension with abelian kernel and a linear splitting (#31462) This PR defines the Lie algebra 2-cocycle of a Lie algebra extension with abelian kernel equipped with a linear splitting.

Estimated changes

Modified Mathlib/Algebra/Lie/Abelian.lean

added theorem LieIdeal.isLieAbelian_iff

Modified Mathlib/Algebra/Lie/Cochain.lean

added theorem LieModule.Cohomology.mem_twoCochain_iff

Modified Mathlib/Algebra/Lie/Extension.lean

added theorem LieAlgebra.Extension.incl_apply_mem_ker

added theorem LieAlgebra.Extension.incl_injective

added theorem LieAlgebra.Extension.lieModuleOf

added theorem LieAlgebra.Extension.lie_apply_proj_of_leftInverse_eq

added theorem LieAlgebra.Extension.lie_incl_mem_ker

added theorem LieAlgebra.Extension.lie_toKer_apply

added theorem LieAlgebra.Extension.ofTwoCocycle_incl_apply

added theorem LieAlgebra.Extension.ofTwoCocycle_proj_apply

added theorem LieAlgebra.Extension.proj_incl

added theorem LieAlgebra.Extension.proj_surjective

added theorem LieAlgebra.Extension.toKer_bracket

added def LieAlgebra.IsExtension.kerEquivRange

modified theorem LieAlgebra.isExtension_of_surjective

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.LeftInverse.eq

added theorem Function.RightInverse.eq