feat(algebra/lie/direct_sum): define direct_sum.lie_of, `direct_sum…

….to_lie_algebra`, `direct_sum.lie_algebra_is_internal` (#8369)

Various other minor improvements.

src/algebra/lie/direct_sum.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import algebra.lie.basic
+import algebra.lie.submodule
+import algebra.lie.of_associative
 import linear_algebra.direct_sum.finsupp
 
 /-!
@@ -72,10 +74,10 @@ section algebras
 
 /-! The direct sum of Lie algebras carries a natural Lie algebra structure. -/
 
-variables {L : ι → Type w}
+variables (L : ι → Type w)
 variables [Π i, lie_ring (L i)] [Π i, lie_algebra R (L i)]
 
-instance : lie_ring (⨁ i, L i) :=
+instance lie_ring : lie_ring (⨁ i, L i) :=
 { bracket     := zip_with (λ i, λ x y, ⁅x, y⁆) (λ i, lie_zero 0),
   add_lie     := λ x y z, by { ext, simp only [zip_with_apply, add_apply, add_lie], },
   lie_add     := λ x y z, by { ext, simp only [zip_with_apply, add_apply, lie_add], },
@@ -87,27 +89,125 @@ instance : lie_ring (⨁ i, L i) :=
 @[simp] lemma bracket_apply (x y : ⨁ i, L i) (i : ι) :
   ⁅x, y⁆ i = ⁅x i, y i⁆ := zip_with_apply _ _ x y i
 
-instance : lie_algebra R (⨁ i, L i) :=
+instance lie_algebra : lie_algebra R (⨁ i, L i) :=
 { lie_smul := λ c x y, by { ext, simp only [
     zip_with_apply, smul_apply, bracket_apply, lie_smul] },
   ..(infer_instance : module R _) }
 
 variables (R ι L)
 
 /-- The inclusion of each component into the direct sum as morphism of Lie algebras. -/
-def lie_algebra_of [decidable_eq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i :=
-{ map_lie' := λ x y, by
+@[simps] def lie_algebra_of [decidable_eq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i :=
+{ to_fun   := of L j,
+  map_lie' := λ x y, by
   { ext i, by_cases h : j = i,
-    { rw ← h, simp, },
-    { simp [lof, single_eq_of_ne h], }, },
+    { rw ← h, simp [of], },
+    { simp [of, single_eq_of_ne h], }, },
   ..lof R ι L j, }
 
 /-- The projection map onto one component, as a morphism of Lie algebras. -/
-def lie_algebra_component (j : ι) : (⨁ i, L i) →ₗ⁅R⁆ L j :=
-{ map_lie' := λ x y,
+@[simps] def lie_algebra_component (j : ι) : (⨁ i, L i) →ₗ⁅R⁆ L j :=
+{ to_fun   := component R ι L j,
+  map_lie' := λ x y,
     by simp only [component, bracket_apply, lapply_apply, linear_map.to_fun_eq_coe],
   ..component R ι L j }
 
+@[ext] lemma lie_algebra_ext {x y : ⨁ i, L i}
+  (h : ∀ i, lie_algebra_component R ι L i x = lie_algebra_component R ι L i y) : x = y :=
+dfinsupp.ext h
+
+include R
+
+lemma lie_of_of_ne [decidable_eq ι] {i j : ι} (hij : j ≠ i) (x : L i) (y : L j) :
+  ⁅of L i x, of L j y⁆ = 0 :=
+begin
+  apply lie_algebra_ext R ι L, intros k,
+  rw lie_hom.map_lie,
+  simp only [component, of, lapply_apply, single_add_hom_apply, lie_algebra_component_apply,
+    single_apply, zero_apply],
+  by_cases hik : i = k,
+  { simp only [dif_neg, not_false_iff, lie_zero, hik.symm, hij], },
+  { simp only [dif_neg, not_false_iff, zero_lie, hik], },
+end
+
+lemma lie_of_of_eq [decidable_eq ι] {i j : ι} (hij : j = i) (x : L i) (y : L j) :
+  ⁅of L i x, of L j y⁆ = of L i ⁅x, hij.rec_on y⁆ :=
+begin
+  have : of L j y = of L i (hij.rec_on y), { exact eq.drec (eq.refl _) hij, },
+  rw [this, ← lie_algebra_of_apply R ι L i ⁅x, hij.rec_on y⁆, lie_hom.map_lie,
+    lie_algebra_of_apply, lie_algebra_of_apply],
+end
+
+@[simp] lemma lie_of [decidable_eq ι] {i j : ι} (x : L i) (y : L j) :
+  ⁅of L i x, of L j y⁆ =
+  if hij : j = i then lie_algebra_of R ι L i ⁅x, hij.rec_on y⁆ else 0 :=
+begin
+  by_cases hij : j = i,
+  { simp only [lie_of_of_eq R ι L hij x y, hij, dif_pos, not_false_iff, lie_algebra_of_apply], },
+  { simp only [lie_of_of_ne R ι L hij x y, hij, dif_neg, not_false_iff], },
+end
+
+variables {R L ι}
+
+/-- Given a family of Lie algebras `L i`, together with a family of morphisms of Lie algebras
+`f i : L i →ₗ⁅R⁆ L'` into a fixed Lie algebra `L'`, we have a natural linear map:
+`(⨁ i, L i) →ₗ[R] L'`. If in addition `⁅f i x, f j y⁆ = 0` for any `x ∈ L i` and `y ∈ L j` (`i ≠ j`)
+then this map is a morphism of Lie algebras. -/
+@[simps] def to_lie_algebra [decidable_eq ι] (L' : Type w₁) [lie_ring L'] [lie_algebra R L']
+  (f : Π i, L i →ₗ⁅R⁆ L') (hf : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅f i x, f j y⁆ = 0) :
+  (⨁ i, L i) →ₗ⁅R⁆ L' :=
+{ to_fun   := to_module R ι L' (λ i, (f i : L i →ₗ[R] L')),
+  map_lie' := λ x y,
+    begin
+      let f' := λ i, (f i : L i →ₗ[R] L'),
+      /- The goal is linear in `y`. We can use this to reduce to the case that `y` has only one
+        non-zero component. -/
+      suffices : ∀ (i : ι) (y : L i), to_module R ι L' f' ⁅x, of L i y⁆ =
+        ⁅to_module R ι L' f' x, to_module R ι L' f' (of L i y)⁆,
+      { simp only [← lie_algebra.ad_apply R, ← linear_map.comp_apply],
+        congr, clear y, ext i y, exact this i y, },
+      /- Similarly, we can reduce to the case that `x` has only one non-zero component. -/
+      suffices : ∀ i j (y : L i) (x : L j), to_module R ι L' f' ⁅of L j x, of L i y⁆ =
+        ⁅to_module R ι L' f' (of L j x), to_module R ι L' f' (of L i y)⁆,
+      { intros i y,
+        rw [← lie_skew x, ← lie_skew (to_module R ι L' f' x)],
+        simp only [linear_map.map_neg, neg_inj, ← lie_algebra.ad_apply R, ← linear_map.comp_apply],
+        congr, clear x, ext j x, exact this j i x y, },
+      /- Tidy up and use `lie_of`. -/
+      intros i j y x,
+      simp only [lie_of R, lie_algebra_of_apply, lie_hom.coe_to_linear_map, to_add_monoid_of,
+        coe_to_module_eq_coe_to_add_monoid, linear_map.to_add_monoid_hom_coe],
+      /- And finish with trivial case analysis. -/
+      rcases eq_or_ne i j with h | h,
+      { have h' : f j (h.rec_on y) = f i y, { exact eq.drec (eq.refl _) h, },
+        simp only [h, h', lie_hom.coe_to_linear_map, dif_pos, lie_hom.map_lie, to_add_monoid_of,
+          linear_map.to_add_monoid_hom_coe], },
+      { simp only [h, hf j i h.symm x y, dif_neg, not_false_iff, add_monoid_hom.map_zero], },
+    end,
+.. to_module R ι L' (λ i, (f i : L i →ₗ[R] L')) }
+
 end algebras
 
+section ideals
+
+variables {L : Type w} [lie_ring L] [lie_algebra R L] (I : ι → lie_ideal R L)
+
+/-- Given a Lie algebra `L` and a family of ideals `I i ⊆ L`, informally this definition is the
+statement that `L = ⨁ i, I i`.
+
+More formally, the inclusions give a natural map from the (external) direct sum to the enclosing Lie
+algebra: `(⨁ i, I i) → L`, and this definition is the proposition that this map is bijective. -/
+def lie_algebra_is_internal [decidable_eq ι] : Prop :=
+function.bijective $ to_module R ι L $ λ i, ((I i).incl : I i →ₗ[R] L)
+
+/-- The fact that this instance is necessary seems to be a bug in typeclass inference. See
+[this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/
+Typeclass.20resolution.20under.20binders/near/245151099). -/
+instance lie_ring_of_ideals : lie_ring (⨁ i, I i) := direct_sum.lie_ring (λ i, ↥(I i))
+
+/-- See `direct_sum.lie_ring_of_ideals` comment. -/
+instance lie_algebra_of_ideals : lie_algebra R (⨁ i, I i) := direct_sum.lie_algebra (λ i, ↥(I i))
+
+end ideals
+
 end direct_sum

src/linear_algebra/direct_sum_module.lean

@@ -81,6 +81,12 @@ variables (R ι N φ)
 def to_module : (⨁ i, M i) →ₗ[R] N :=
 dfinsupp.lsum ℕ φ
 
+/-- Coproducts in the categories of modules and additive monoids commute with the forgetful functor
+from modules to additive monoids. -/
+lemma coe_to_module_eq_coe_to_add_monoid :
+  (to_module R ι N φ : (⨁ i, M i) → N) = to_add_monoid (λ i, (φ i).to_add_monoid_hom) :=
+rfl
+
 variables {ι N φ}
 
 /-- The map constructed using the universal property gives back the original maps when