feat(Algebra/Lie): Define Lie algebra extensions (#20206)

This PR defines extensions of Lie algebras. We follow the pattern used in defining extensions of groups.

Author: ScottCarnahan

Mathlib.lean

@@ -509,6 +509,7 @@ import Mathlib.Algebra.Lie.Derivation.Killing
 import Mathlib.Algebra.Lie.DirectSum
 import Mathlib.Algebra.Lie.Engel
 import Mathlib.Algebra.Lie.EngelSubalgebra
+import Mathlib.Algebra.Lie.Extension
 import Mathlib.Algebra.Lie.Free
 import Mathlib.Algebra.Lie.IdealOperations
 import Mathlib.Algebra.Lie.InvariantForm

Mathlib/Algebra/Lie/Extension.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2024 Scott Carnahan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Carnahan
+-/
+import Mathlib.Algebra.Lie.Submodule
+
+/-!
+# Extensions of Lie algebras
+This file defines extensions of Lie algebras, given by short exact sequences of Lie algebra
+homomorphisms. They are implemented in two ways: `IsExtension` is a `Prop`-valued class taking two
+homomorphisms as parameters, and `Extension` is a structure that includes the middle Lie algebra.
+
+## Main definitions
+ * `LieAlgebra.IsExtension`: A `Prop`-valued class characterizing an extension of Lie algebras.
+ * `LieAlgebra.Extension`: A bundled structure giving an extension of Lie algebras.
+ * `LieAlgebra.IsExtension.extension`: A function that builds the bundled structure from the class.
+
+## TODO
+ * `IsCentral` - central extensions
+ * `Equiv` - equivalence of extensions
+ * `ofTwoCocycle` - construction of extensions from 2-cocycles
+
+## References
+* [N. Bourbaki, *Lie Groups and Lie Algebras, Chapters 1--3*](bourbaki1975)
+
+-/
+
+namespace LieAlgebra
+
+variable {R N L M : Type*}
+
+variable [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M]
+  [LieAlgebra R M]
+
+/-- A sequence of two Lie algebra homomorphisms is an extension if it is short exact. -/
+class IsExtension (i : N →ₗ⁅R⁆ L) (p : L →ₗ⁅R⁆ M) : Prop where
+  ker_eq_bot : i.ker = ⊥
+  range_eq_top : p.range = ⊤
+  exact : i.range = p.ker
+
+variable (R N M) in
+/-- The type of all Lie extensions of `M` by `N`.  That is, short exact sequences of `R`-Lie algebra
+homomorphisms `0 → N → L → M → 0` where `R`, `M`, and `N` are fixed. -/
+structure Extension where
+  /-- The middle object in the sequence. -/
+  L : Type*
+  /-- `L` is a Lie ring. -/
+  instLieRing : LieRing L
+  /-- `L` is a Lie algebra over `R`. -/
+  instLieAlgebra : LieAlgebra R L
+  /-- The inclusion homomorphism `N →ₗ⁅R⁆ L` -/
+  incl : N →ₗ⁅R⁆ L
+  /-- The projection homomorphism `L →ₗ⁅R⁆ M` -/
+  proj : L →ₗ⁅R⁆ M
+  IsExtension : IsExtension incl proj
+
+/-- The bundled `LieAlgebra.Extension` corresponding to `LieAlgebra.IsExtension` -/
+@[simps] def IsExtension.extension {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) :
+    Extension R N M :=
+  ⟨L, _, _, i, p, h⟩
+
+/-- A surjective Lie algebra homomorphism yields an extension. -/
+theorem isExtension_of_surjective (f : L →ₗ⁅R⁆ M) (hf : Function.Surjective f) :
+    IsExtension f.ker.incl f where
+  ker_eq_bot := LieIdeal.ker_incl f.ker
+  range_eq_top := (LieHom.range_eq_top f).mpr hf
+  exact := LieIdeal.incl_range f.ker
+
+end LieAlgebra