feat(algebra/lie/free): construction of free Lie algebras (#8153)

src/algebra/lie/free.lean

@@ -0,0 +1,235 @@
+/-
+Copyright (c) 2021 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import algebra.lie.of_associative
+import algebra.lie.non_unital_non_assoc_algebra
+import algebra.free_non_unital_non_assoc_algebra
+
+/-!
+# Free Lie algebras
+
+Given a commutative ring `R` and a type `X` we construct the free Lie algebra on `X` with
+coefficients in `R` together with its universal property.
+
+## Main definitions
+
+  * `free_lie_algebra`
+  * `free_lie_algebra.lift`
+  * `free_lie_algebra.of`
+
+## Implementation details
+
+### Quotient of free non-unital, non-associative algebra
+
+We follow [N. Bourbaki, *Lie Groups and Lie Algebras, Chapters 1--3*](bourbaki1975) and construct
+the free Lie algebra as a quotient of the free non-unital, non-associative algebra. Since we do not
+currently have definitions of ideals, lattices of ideals, and quotients for
+`non_unital_non_assoc_semiring`, we construct our quotient using the low-level `quot` function on
+an inductively-defined relation.
+
+### Alternative construction (often used over field of characteristic zero, but not by us)
+
+By universality of the free Lie algebra, there is a natural morphism of Lie algebras:
+`ρ : free_lie_algebra R X →ₗ⁅R⁆ free_algebra R X`, where `free_algebra R X` is the free unital,
+associative algebra, regarded as a Lie algebra via the ring commutator.
+
+By uniqueness, the image of `ρ` is the Lie subalgebra generated by `X` in the free algebra, i.e.:
+`lie_subalgebra.lie_span R (free_algebra R X) (set.range (free_algebra.ι R))`. If `ρ` is injective
+we could thus take the Lie subalgebra generated by `X` in the free associative algebra as the
+definition of the free Lie algebra, and indeed some authors do this. This is valid at least over a
+field of characteristic zero but I do not believe `ρ` is injective for general `R`. Indeed the only
+proof I know that `ρ` is injective relies on using the injectivity of the map from a Lie algebra to
+its universal enveloping algebra, which does not hold in general. Furthermore, even when a Lie
+algebra does inject into its universal enveloping algebra, the only proofs I know of this fact
+use the Poincaré–Birkhoff–Witt theorem. Some related MathOverflow questions are
+[this one](https://mathoverflow.net/questions/61954/) and
+[this one](https://mathoverflow.net/questions/114701/).
+
+## Tags
+
+lie algebra, free algebra, non-unital, non-associative, universal property, forgetful functor,
+adjoint functor
+-/
+
+universes u v w
+
+noncomputable theory
+
+variables (R : Type u) (X : Type v) [comm_ring R]
+
+/-- We save characters by using Bourbaki's name `lib` (as in «libre») for
+`free_non_unital_non_assoc_algebra` in this file. -/
+local notation `lib` := free_non_unital_non_assoc_algebra
+local notation `lib.lift` := free_non_unital_non_assoc_algebra.lift
+local notation `lib.of` := free_non_unital_non_assoc_algebra.of
+local notation `lib.lift_of_apply` := free_non_unital_non_assoc_algebra.lift_of_apply
+local notation `lib.lift_comp_of` := free_non_unital_non_assoc_algebra.lift_comp_of
+
+namespace free_lie_algebra
+
+/-- The quotient of `lib R X` by the equivalence relation generated by this relation will give us
+the free Lie algebra. -/
+inductive rel : lib R X → lib R X → Prop
+| lie_self (a : lib R X) : rel (a * a) 0
+| leibniz_lie (a b c : lib R X) : rel (a * (b * c)) (((a * b) * c) + (b * (a * c)))
+| smul (t : R) (a b : lib R X) : rel a b → rel (t • a) (t • b)
+| add_right (a b c : lib R X) : rel a b → rel (a + c) (b + c)
+| mul_left (a b c : lib R X) : rel b c → rel (a * b) (a * c)
+| mul_right (a b c : lib R X) : rel a b → rel (a * c) (b * c)
+
+variables {R X}
+
+lemma rel.add_left (a b c : lib R X) (h : rel R X b c) : rel R X (a + b) (a + c) :=
+by { rw [add_comm _ b, add_comm _ c], exact rel.add_right _ _ _ h, }
+
+end free_lie_algebra
+
+/-- The free Lie algebra on the type `X` with coefficients in the commutative ring `R`. -/
+@[derive inhabited]
+def free_lie_algebra := quot (free_lie_algebra.rel R X)
+
+namespace free_lie_algebra
+
+instance : has_scalar R (free_lie_algebra R X) :=
+{ smul := λ t a, quot.lift_on a (λ x, quot.mk _ (t • x)) (λ a b h, quot.sound (rel.smul t a b h)), }
+
+instance : has_add (free_lie_algebra R X) :=
+{ add := quot.map₂ (+) rel.add_left rel.add_right, }
+
+instance : add_comm_group (free_lie_algebra R X) :=
+{ add_comm       := by { rintros ⟨a⟩ ⟨b⟩, change quot.mk _ _ = quot.mk _ _, rw add_comm, },
+  add_assoc      := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, change quot.mk _ _ = quot.mk _ _, rw add_assoc, },
+  zero           := quot.mk _ 0,
+  zero_add       := by { rintros ⟨a⟩, change quot.mk _ _ = _, rw zero_add, },
+  add_zero       := by { rintros ⟨a⟩, change quot.mk _ _ = _, rw add_zero, },
+  neg            := λ x, (-1 : R) • x,
+  sub            := λ x y, x + ((-1 : R) • y),
+  sub_eq_add_neg := λ x y, rfl,
+  add_left_neg   :=
+    by { rintros ⟨a⟩, change quot.mk _ _ = _, erw [neg_smul, one_smul, add_left_neg], refl, },
+  ..(infer_instance : has_add _)}
+
+/-- Note that here we turn the `has_mul` coming from the `non_unital_non_assoc_semiring` structure
+on `lib R X` into a `has_bracket` on `free_lie_algebra`. -/
+instance : has_bracket (free_lie_algebra R X) (free_lie_algebra R X) :=
+{ bracket := quot.map₂ (*) (λ a b c, rel.mul_left a b c) (λ a b c, rel.mul_right a b c), }
+
+instance : lie_ring (free_lie_algebra R X) :=
+{ add_lie     := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, change quot.mk _ _ = quot.mk _ _, rw add_mul, },
+  lie_add     := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, change quot.mk _ _ = quot.mk _ _, rw mul_add, },
+  lie_self    := by { rintros ⟨a⟩, exact quot.sound (rel.lie_self a), },
+  leibniz_lie := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, exact quot.sound (rel.leibniz_lie a b c), }, }
+
+instance : module R (free_lie_algebra R X) :=
+{ one_smul  := by { rintros ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw one_smul, },
+  mul_smul  := by { rintros t₁ t₂ ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw mul_smul, },
+  add_smul  := by { rintros t₁ t₂ ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw add_smul, },
+  smul_add  := by { rintros t ⟨a⟩ ⟨b⟩, change quot.mk _ _ = quot.mk _ _, rw smul_add, },
+  zero_smul := by { rintros ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw zero_smul, },
+  smul_zero := λ t, by { change quot.mk _ _ = quot.mk _ _, rw smul_zero, }, }
+
+instance : lie_algebra R (free_lie_algebra R X) :=
+{ lie_smul :=
+  begin
+    rintros t ⟨a⟩ ⟨c⟩,
+    change quot.mk _ (a • (t • c)) = quot.mk _ (t • (a • c)),
+    rw ← smul_comm,
+  end, }
+
+variables {X}
+
+/-- The embedding of `X` into the free Lie algebra of `X` with coefficients in the commutative ring
+`R`. -/
+def of : X → free_lie_algebra R X := λ x, quot.mk _ (lib.of R x)
+
+variables {L : Type w} [lie_ring L] [lie_algebra R L]
+
+local attribute [instance] lie_ring.to_non_unital_non_assoc_semiring
+
+/-- An auxiliary definition used to construct the equivalence `lift` below. -/
+def lift_aux (f : X → L) := lib.lift R f
+
+lemma lift_aux_map_smul (f : X → L) (t : R) (a : lib R X) :
+  lift_aux R f (t • a) = t • lift_aux R f a :=
+non_unital_alg_hom.map_smul _ t a
+
+lemma lift_aux_map_add (f : X → L) (a b : lib R X) :
+  lift_aux R f (a + b) = (lift_aux R f a) + (lift_aux R f b) :=
+non_unital_alg_hom.map_add _ a b
+
+lemma lift_aux_map_mul (f : X → L) (a b : lib R X) :
+  lift_aux R f (a * b) = ⁅lift_aux R f a, lift_aux R f b⁆ :=
+non_unital_alg_hom.map_mul _ a b
+
+lemma lift_aux_spec (f : X → L) (a b : lib R X) (h : free_lie_algebra.rel R X a b) :
+  lift_aux R f a = lift_aux R f b :=
+begin
+  induction h,
+  case rel.lie_self : a'
+  { simp only [lift_aux_map_mul, non_unital_alg_hom.map_zero, lie_self], },
+  case rel.leibniz_lie : a' b' c'
+  { simp only [lift_aux_map_mul, lift_aux_map_add, sub_add_cancel, lie_lie], },
+  case rel.smul : t a' b' h₁ h₂
+  { simp only [lift_aux_map_smul, h₂], },
+  case rel.add_right : a' b' c' h₁ h₂
+  { simp only [lift_aux_map_add, h₂], },
+  case rel.mul_left : a' b' c' h₁ h₂
+  { simp only [lift_aux_map_mul, h₂], },
+  case rel.mul_right : a' b' c' h₁ h₂
+  { simp only [lift_aux_map_mul, h₂], },
+end
+
+/-- The quotient map as a `non_unital_alg_hom`. -/
+def mk : non_unital_alg_hom R (lib R X) (free_lie_algebra R X) :=
+{ to_fun    := quot.mk (rel R X),
+  map_smul' := λ t a, rfl,
+  map_zero' := rfl,
+  map_add'  := λ a b, rfl,
+  map_mul'  := λ a b, rfl, }
+
+/-- The functor `X ↦ free_lie_algebra R X` from the category of types to the category of Lie
+algebras over `R` is adjoint to the forgetful functor in the other direction. -/
+def lift : (X → L) ≃ (free_lie_algebra R X →ₗ⁅R⁆ L) :=
+{ to_fun    := λ f,
+    { to_fun    := λ c, quot.lift_on c (lift_aux R f) (lift_aux_spec R f),
+      map_add'  := by { rintros ⟨a⟩ ⟨b⟩, rw ← lift_aux_map_add, refl, },
+      map_smul' := by { rintros t ⟨a⟩, rw ← lift_aux_map_smul, refl, },
+      map_lie'  := by { rintros ⟨a⟩ ⟨b⟩, rw ← lift_aux_map_mul, refl, }, },
+  inv_fun   := λ F, F ∘ (of R),
+  left_inv  := λ f, by { ext x, simp only [lift_aux, of, quot.lift_on_mk, lie_hom.coe_mk,
+    function.comp_app, lib.lift_of_apply], },
+  right_inv := λ F,
+    begin
+      ext ⟨a⟩,
+      let F' := F.to_non_unital_alg_hom.comp (mk R),
+      exact non_unital_alg_hom.congr_fun (lib.lift_comp_of R F') a,
+    end, }
+
+@[simp] lemma lift_symm_apply (F : free_lie_algebra R X →ₗ⁅R⁆ L) : (lift R).symm F = F ∘ (of R) :=
+rfl
+
+variables {R}
+
+@[simp] lemma of_comp_lift (f : X → L) : (lift R f) ∘ (of R) = f :=
+(lift R).left_inv f
+
+@[simp] lemma lift_unique (f : X → L) (g : free_lie_algebra R X →ₗ⁅R⁆ L) :
+  g ∘ (of R) = f ↔ g = lift R f :=
+(lift R).symm_apply_eq
+
+attribute [irreducible] of lift
+
+@[simp] lemma lift_of_apply (f : X → L) (x) : lift R f (of R x) = f x :=
+by rw [← function.comp_app (lift R f) (of R) x, of_comp_lift]
+
+@[simp] lemma lift_comp_of (F : free_lie_algebra R X →ₗ⁅R⁆ L) : lift R (F ∘ (of R)) = F :=
+by { rw ← lift_symm_apply, exact (lift R).apply_symm_apply F, }
+
+/-- See note [partially-applied ext lemmas]. -/
+@[ext] lemma hom_ext {F₁ F₂ : free_lie_algebra R X →ₗ⁅R⁆ L} (h : F₁ ∘ (of R) = F₂ ∘ (of R)) :
+  F₁ = F₂ :=
+by { rw [← lift_symm_apply, ← lift_symm_apply] at h, exact (lift R).symm.injective h, }
+
+end free_lie_algebra

src/algebra/lie/non_unital_non_assoc_algebra.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2019 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import algebra.lie.basic
+import algebra.non_unital_alg_hom
+
+/-!
+# Lie algebras as non-unital, non-associative algebras
+
+The definition of Lie algebras uses the `has_bracket` typeclass for multiplication whereas we have a
+separate `has_mul` typeclass used for general algebras.
+
+It is useful to have a special typeclass for Lie algebras because:
+ * it enables us to use the traditional notation `⁅x, y⁆` for the Lie multiplication,
+ * associative algebras carry a natural Lie algebra structure via the ring commutator and so we need
+   them to carry both `has_mul` and `has_bracket` simultaneously,
+ * more generally, Poisson algebras (not yet defined) need both typeclasses.
+
+However there are times when it is convenient to be able to regard a Lie algebra as a general
+algebra and we provide some basic definitions for doing so here.
+
+## Main definitions
+
+  * `lie_ring.to_non_unital_non_assoc_semiring`
+  * `lie_hom.to_non_unital_alg_hom`
+
+## Tags
+
+lie algebra, non-unital, non-associative
+-/
+
+universes u v w
+
+variables (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L]
+
+/-- A `lie_ring` can be regarded as a `non_unital_non_assoc_semiring` by turning its
+`has_bracket` (denoted `⁅, ⁆`) into a `has_mul` (denoted `*`). -/
+def lie_ring.to_non_unital_non_assoc_semiring : non_unital_non_assoc_semiring L :=
+{ mul           := has_bracket.bracket,
+  left_distrib  := lie_add,
+  right_distrib := add_lie,
+  zero_mul      := zero_lie,
+  mul_zero      := lie_zero,
+  .. (infer_instance : add_comm_monoid L) }
+
+local attribute [instance] lie_ring.to_non_unital_non_assoc_semiring
+
+/-- Regarding the `lie_ring` of a `lie_algebra` as a `non_unital_non_assoc_semiring`, we can
+reinterpret the `smul_lie` law as an `is_scalar_tower`. -/
+instance lie_algebra.is_scalar_tower : is_scalar_tower R L L := ⟨smul_lie⟩
+
+/-- Regarding the `lie_ring` of a `lie_algebra` as a `non_unital_non_assoc_semiring`, we can
+reinterpret the `lie_smul` law as an `smul_comm_class`. -/
+instance lie_algebra.smul_comm_class : smul_comm_class R L L := ⟨λ t x y, (lie_smul t x y).symm⟩
+
+variables {R L} {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂]
+
+/-- Regarding the `lie_ring` of a `lie_algebra` as a `non_unital_non_assoc_semiring`, we can
+regard a `lie_hom` as a `non_unital_alg_hom`. -/
+@[simps]
+def lie_hom.to_non_unital_alg_hom (f : L →ₗ⁅R⁆ L₂) : non_unital_alg_hom R L L₂ :=
+{ to_fun := f,
+  map_zero' := f.map_zero,
+  map_mul'  := f.map_lie,
+  ..f }

src/algebra/non_unital_alg_hom.lean

@@ -81,6 +81,8 @@ coe_injective $ funext h
 lemma ext_iff {f g : non_unital_alg_hom R A B} : f = g ↔ ∀ x, f x = g x :=
 ⟨by { rintro rfl x, refl }, ext⟩
 
+lemma congr_fun {f g : non_unital_alg_hom R A B} (h : f = g) (x : A) : f x = g x := h ▸ rfl
+
 @[simp] lemma coe_mk (f : A → B) (h₁ h₂ h₃ h₄) :
   ((⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) : A → B) = f :=
 rfl