feat(algebra/universal_enveloping_algebra): construction of universal…

… enveloping algebra and its universal property (#4041)

## Main definitions

  * `universal_enveloping_algebra`
  * `universal_enveloping_algebra.algebra`
  * `universal_enveloping_algebra.lift`
  * `universal_enveloping_algebra.ι_comp_lift`
  * `universal_enveloping_algebra.lift_unique`
  * `universal_enveloping_algebra.hom_ext`

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/lie_algebra.lean

@@ -191,6 +191,9 @@ instance : has_coe (L₁ →ₗ⁅R⁆ L₂) (L₁ →ₗ[R] L₂) := ⟨morphis
 /-- see Note [function coercion] -/
 instance : has_coe_to_fun (L₁ →ₗ⁅R⁆ L₂) := ⟨_, morphism.to_fun⟩
 
+@[simp, norm_cast] lemma coe_to_linear_map (f : L₁ →ₗ⁅R⁆ L₂) : ((f : L₁ →ₗ[R] L₂) : L₁ → L₂) = f :=
+rfl
+
 @[simp] lemma map_lie (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f ⁅x, y⁆ = ⁅f x, f y⁆ := morphism.map_lie f
 
 /-- The constant 0 map is a Lie algebra morphism. -/
@@ -201,6 +204,12 @@ instance : has_one (L₁ →ₗ⁅R⁆ L₁) := ⟨{ map_lie := by simp, ..(1 :
 
 instance : inhabited (L₁ →ₗ⁅R⁆ L₂) := ⟨0⟩
 
+@[ext] lemma morphism.ext {f g : L₁ →ₗ⁅R⁆ L₂} (h : ∀ x, f x = g x) : f = g :=
+begin
+  cases f, cases g, simp only,
+  ext, apply h,
+end
+
 /-- The composition of morphisms is a morphism. -/
 def morphism.comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) : L₁ →ₗ⁅R⁆ L₃ :=
 { map_lie := λ x y, by { change f (g ⁅x, y⁆) = ⁅f (g x), f (g y)⁆, rw [map_lie, map_lie], },

src/algebra/universal_enveloping_algebra.lean

@@ -0,0 +1,119 @@
+/-
+Copyright (c) 2020 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import algebra.lie_algebra
+import algebra.ring_quot
+import linear_algebra.tensor_algebra
+
+/-!
+# Universal enveloping algebra
+
+Given a commutative ring `R` and a Lie algebra `L` over `R`, we construct the universal
+enveloping algebra of `L`, together with its universal property.
+
+## Main definitions
+
+  * `universal_enveloping_algebra`: the universal enveloping algebra, endowed with an
+    `R`-algebra structure.
+  * `universal_enveloping_algebra.ι`: the Lie algebra morphism from `L` to its universal
+    enveloping algebra.
+  * `universal_enveloping_algebra.lift`: given an associative algebra `A`, together with a Lie
+    algebra morphism `f : L →ₗ⁅R⁆ A`, `lift R L f : universal_enveloping_algebra R L →ₐ[R] A` is the
+    unique morphism of algebras through which `f` factors.
+  * `universal_enveloping_algebra.ι_comp_lift`: states that the lift of a morphism is indeed part
+    of a factorisation.
+  * `universal_enveloping_algebra.lift_unique`: states that lifts of morphisms are indeed unique.
+  * `universal_enveloping_algebra.hom_ext`: a restatement of `lift_unique` as an extensionality
+    lemma.
+
+## Tags
+
+lie algebra, universal enveloping algebra, tensor algebra
+-/
+
+universes u₁ u₂ u₃
+
+variables (R : Type u₁) (L : Type u₂)
+variables [comm_ring R] [lie_ring L] [lie_algebra R L]
+
+local notation `ιₜ` := tensor_algebra.ι R L
+
+namespace universal_enveloping_algebra
+
+/-- The quotient by the ideal generated by this relation is the universal enveloping algebra.
+
+Note that we have avoided using the more natural expression:
+| lie_compat (x y : L) : rel (ιₜ ⁅x, y⁆) ⁅ιₜ x, ιₜ y⁆
+so that our construction needs only the semiring structure of the tensor algebra. -/
+inductive rel : tensor_algebra R L → tensor_algebra R L → Prop
+| lie_compat (x y : L) : rel (ιₜ ⁅x, y⁆ + (ιₜ y) * (ιₜ x)) ((ιₜ x) * (ιₜ y))
+
+end universal_enveloping_algebra
+
+/-- The universal enveloping algebra of a Lie algebra. -/
+@[derive [inhabited, semiring, algebra R]]
+def universal_enveloping_algebra := ring_quot (universal_enveloping_algebra.rel R L)
+
+namespace universal_enveloping_algebra
+
+instance : ring (universal_enveloping_algebra R L) := algebra.semiring_to_ring R
+
+/-- The quotient map from the tensor algebra to the universal enveloping algebra as a morphism of
+associative algebras. -/
+def mk_alg_hom : tensor_algebra R L →ₐ[R] universal_enveloping_algebra R L :=
+ring_quot.mk_alg_hom R (rel R L)
+
+/-- The natural Lie algebra morphism from a Lie algebra to its universal enveloping algebra. -/
+def ι : L →ₗ⁅R⁆ universal_enveloping_algebra R L :=
+{ map_lie   := λ x y, by
+  { suffices : mk_alg_hom R L (ιₜ ⁅x, y⁆ + (ιₜ y) * (ιₜ x)) = mk_alg_hom R L ((ιₜ x) * (ιₜ y)),
+    { rw alg_hom.map_mul at this, simp [lie_ring.of_associative_ring_bracket, ← this], },
+    exact ring_quot.mk_alg_hom_rel _ (rel.lie_compat x y), },
+  ..(mk_alg_hom R L).to_linear_map.comp ιₜ }
+
+variables {A : Type u₃} [ring A] [algebra R A] (f : L →ₗ⁅R⁆ A)
+
+/-- The universal property of the universal enveloping algebra: Lie algebra morphisms into
+associative algebras lift to associative algebra morphisms from the universal enveloping algebra. -/
+def lift : universal_enveloping_algebra R L →ₐ[R] A :=
+ring_quot.lift_alg_hom R (tensor_algebra.lift R L (f : L →ₗ[R] A))
+begin
+  intros a b h, induction h with x y,
+  simp [lie_ring.of_associative_ring_bracket],
+end
+
+@[simp] lemma lift_ι_apply (x : L) : lift R L f (ι R L x) = f x :=
+begin
+  have : ι R L x = ring_quot.mk_alg_hom R (rel R L) (ιₜ x), by refl,
+  simp [this, lift],
+end
+
+lemma ι_comp_lift : (lift R L f) ∘ (ι R L) = f :=
+by { ext, simp, }
+
+lemma lift_unique (g : universal_enveloping_algebra R L →ₐ[R] A) :
+  g ∘ (ι R L) = f ↔ g = lift R L f :=
+begin
+  split; intros h,
+  { apply ring_quot.lift_alg_hom_unique,
+    rw ← tensor_algebra.lift_unique,
+    ext x,
+    change _ = f x, rw ← congr h rfl,
+    refl, },
+  { subst h, apply ι_comp_lift, },
+end
+
+@[ext] lemma hom_ext {g₁ g₂ : universal_enveloping_algebra R L →ₐ[R] A}
+  (h : g₁ ∘ (ι R L) = g₂ ∘ (ι R L)) : g₁ = g₂ :=
+begin
+  let f₁ := (lie_algebra.of_associative_algebra_hom g₁).comp (ι R L),
+  let f₂ := (lie_algebra.of_associative_algebra_hom g₂).comp (ι R L),
+  have h' : f₁ = f₂, { ext, exact congr h rfl, },
+  have h₁ : g₁ = lift R L f₁, { rw ← lift_unique, refl, },
+  have h₂ : g₂ = lift R L f₂, { rw ← lift_unique, refl, },
+  rw [h₁, h₂, h'],
+end
+
+end universal_enveloping_algebra

src/linear_algebra/tensor_algebra.lean

@@ -35,7 +35,7 @@ modulo the additional relations making the inclusion of `M` into an `R`-linear m
 -/
 
 variables (R : Type*) [comm_semiring R]
-variables (M : Type*) [add_comm_group M] [semimodule R M]
+variables (M : Type*) [add_comm_monoid M] [semimodule R M]
 
 namespace tensor_algebra
 

src/ring_theory/algebra.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
+import tactic.nth_rewrite
 import data.matrix.basic
 import linear_algebra.tensor_product
 import ring_theory.subring