feat(algebra/lie/direct_sum): direct sums of Lie modules (#5063)

There are three things happening here:
  1. introduction of definitions of direct sums for Lie modules,
  2. introduction of definitions of morphisms, equivs for Lie modules,
  3. splitting out extant definition of direct sums for Lie algebras
     into a new file.

src/algebra/lie/basic.lean

@@ -5,7 +5,7 @@ Authors: Oliver Nash
 -/
 import algebra.algebra.basic
 import linear_algebra.bilinear_form
-import linear_algebra.direct_sum.finsupp
+import linear_algebra.matrix
 import tactic.noncomm_ring
 
 /-!
@@ -23,8 +23,11 @@ submodules, and the quotient of a Lie algebra by an ideal.
 We introduce the notation ⁅x, y⁆ for the Lie bracket. Note that these are the Unicode "square with
 quill" brackets rather than the usual square brackets.
 
-We also introduce the notations L →ₗ⁅R⁆ L' for a morphism of Lie algebras over a commutative ring R,
-and L →ₗ⁅⁆ L' for the same, when the ring is implicit.
+Working over a fixed commutative ring `R`, we introduce the notations:
+ * `L →ₗ⁅R⁆ L'` for a morphism of Lie algebras,
+ * `L ≃ₗ⁅R⁆ L'` for an equivalence of Lie algebras,
+ * `M →ₗ⁅R,L⁆ N` for a morphism of Lie algebra modules `M`, `N` over a Lie algebra `L`,
+ * `M ≃ₗ⁅R,L⁆ N` for an equivalence of Lie algebra modules `M`, `N` over a Lie algebra `L`.
 
 ## Implementation notes
 
@@ -39,7 +42,7 @@ are partially unbundled.
 lie bracket, ring commutator, jacobi identity, lie ring, lie algebra
 -/
 
-universes u v w w₁
+universes u v w w₁ w₂
 
 /-- The has_bracket class has two intended uses:
 
@@ -65,8 +68,9 @@ identity. Forgetting the scalar multiplication, every Lie algebra is a Lie ring.
 @[protect_proj] class lie_algebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] extends semimodule R L :=
 (lie_smul : ∀ (t : R) (x y : L), ⁅x, t • y⁆ = t • ⁅x, y⁆)
 
-/-- A Lie ring module is a module over a commutative ring, together with an additive action of a
-Lie ring on this module, such that the Lie bracket acts as the commutator of endomorphisms. -/
+/-- A Lie ring module is an additive group, together with an additive action of a
+Lie ring on this group, such that the Lie bracket acts as the commutator of endomorphisms.
+(For representations of Lie *algebras* see `lie_module`.) -/
 @[protect_proj] class lie_ring_module (L : Type v) (M : Type w)
   [lie_ring L] [add_comm_group M] extends has_bracket L M :=
 (add_lie : ∀ (x y : L) (m : M), ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆)
@@ -146,7 +150,6 @@ structure morphism (R : Type u) (L : Type v) (L' : Type w)
 
 attribute [nolint doc_blame] lie_algebra.morphism.to_linear_map
 
-infixr ` →ₗ⁅⁆ `:25 := morphism _
 notation L ` →ₗ⁅`:25 R:25 `⁆ `:0 L':0 := morphism R L L'
 
 section morphism_properties
@@ -281,36 +284,149 @@ def trans (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) : L
 
 end equiv
 
-namespace direct_sum
-open dfinsupp
-open_locale direct_sum
+end lie_algebra
 
-variables {R : Type u} [comm_ring R]
-variables {ι : Type v} {L : ι → Type w}
-variables [Π i, lie_ring (L i)] [Π i, lie_algebra R (L i)]
-
-/-- The direct sum of Lie rings carries a natural Lie ring structure. -/
-instance : 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], },
-  lie_self    := λ x, by { ext, simp only [zip_with_apply, add_apply, lie_self, zero_apply], },
-  leibniz_lie := λ x y z, by { ext, simp only [direct_sum.sub_apply,
-    zip_with_apply, add_apply, zero_apply], apply leibniz_lie, },
-  ..(infer_instance : add_comm_group _) }
-
-@[simp] lemma bracket_apply {x y : (⨁ i, L i)} {i : ι} :
-  ⁅x, y⁆ i = ⁅x i, y i⁆ := zip_with_apply _ _ x y i
-
-/-- The direct sum of Lie algebras carries a natural Lie algebra structure. -/
-instance : lie_algebra R (⨁ i, L i) :=
-{ lie_smul := λ c x y, by { ext, simp only [
-    zip_with_apply, direct_sum.smul_apply, bracket_apply, lie_smul] },
-  ..(infer_instance : module R _) }
-
-end direct_sum
+section lie_module_morphisms
 
-end lie_algebra
+variables (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂)
+variables [comm_ring R] [lie_ring L] [lie_algebra R L]
+variables [add_comm_group M] [add_comm_group N] [add_comm_group P]
+variables [module R M] [module R N] [module R P]
+variables [lie_ring_module L M] [lie_ring_module L N] [lie_ring_module L P]
+variables [lie_module R L M] [lie_module R L N] [lie_module R L P]
+
+set_option old_structure_cmd true
+
+/-- A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie
+algebra. -/
+structure lie_module_hom extends M →ₗ[R] N :=
+(map_lie : ∀ {x : L} {m : M}, to_fun ⁅x, m⁆ = ⁅x, to_fun m⁆)
+
+attribute [nolint doc_blame] lie_module_hom.to_linear_map
+
+notation M ` →ₗ⁅`:25 R,L:25 `⁆ `:0 N:0 := lie_module_hom R L M N
+
+namespace lie_module_hom
+
+variables {R L M N P}
+
+instance : has_coe (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N) := ⟨lie_module_hom.to_linear_map⟩
+
+/-- see Note [function coercion] -/
+instance : has_coe_to_fun (M →ₗ⁅R,L⁆ N) := ⟨_, lie_module_hom.to_fun⟩
+
+@[simp] lemma coe_mk (f : M → N) (h₁ h₂ h₃) :
+  ((⟨f, h₁, h₂, h₃⟩ : M →ₗ⁅R,L⁆ N) : M → N) = f := rfl
+
+@[simp, norm_cast] lemma coe_to_linear_map (f : M →ₗ⁅R,L⁆ N) : ((f : M →ₗ[R] N) : M → N) = f :=
+rfl
+
+@[simp] lemma map_lie' (f : M →ₗ⁅R,L⁆ N) (x : L) (m : M) : f ⁅x, m⁆ = ⁅x, f m⁆ :=
+lie_module_hom.map_lie f
+
+/-- The constant 0 map is a Lie module morphism. -/
+instance : has_zero (M →ₗ⁅R,L⁆ N) := ⟨{ map_lie := by simp, ..(0 : M →ₗ[R] N) }⟩
+
+/-- The identity map is a Lie module morphism. -/
+instance : has_one (M →ₗ⁅R,L⁆ M) := ⟨{ map_lie := by simp, ..(1 : M →ₗ[R] M) }⟩
+
+instance : inhabited (M →ₗ⁅R,L⁆ N) := ⟨0⟩
+
+lemma coe_injective : function.injective (λ f : M →ₗ⁅R,L⁆ N, show M → N, from f) :=
+by { rintros ⟨f, _⟩ ⟨g, _⟩ ⟨h⟩, congr, }
+
+@[ext] lemma ext {f g : M →ₗ⁅R,L⁆ N} (h : ∀ m, f m = g m) : f = g :=
+coe_injective $ funext h
+
+lemma ext_iff {f g : M →ₗ⁅R,L⁆ N} : f = g ↔ ∀ m, f m = g m :=
+⟨by { rintro rfl m, refl, }, ext⟩
+
+/-- The composition of Lie module morphisms is a morphism. -/
+def comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) : M →ₗ⁅R,L⁆ P :=
+{ map_lie := λ x m, by { change f (g ⁅x, m⁆) = ⁅x, f (g m)⁆, rw [map_lie', map_lie'], },
+  ..linear_map.comp f.to_linear_map g.to_linear_map }
+
+@[simp] lemma comp_apply (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) (m : M) :
+  f.comp g m = f (g m) := rfl
+
+@[norm_cast] lemma comp_coe (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) :
+  (f : N → P) ∘ (g : M → N) = f.comp g := rfl
+
+/-- The inverse of a bijective morphism of Lie modules is a morphism of Lie modules. -/
+def inverse (f : M →ₗ⁅R,L⁆ N) (g : N → M)
+  (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : N →ₗ⁅R,L⁆ M :=
+{ map_lie := λ x n,
+    calc g ⁅x, n⁆ = g ⁅x, f (g n)⁆ : by rw h₂
+              ... = g (f ⁅x, g n⁆) : by rw map_lie'
+              ... = ⁅x, g n⁆ : (h₁ _),
+  ..linear_map.inverse f.to_linear_map g h₁ h₂ }
+
+end lie_module_hom
+
+/-- An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of
+Lie algebra modules. -/
+structure lie_module_equiv extends M ≃ₗ[R] N, M →ₗ⁅R,L⁆ N
+
+attribute [nolint doc_blame] lie_module_equiv.to_lie_module_hom
+attribute [nolint doc_blame] lie_module_equiv.to_linear_equiv
+
+notation M ` ≃ₗ⁅`:25 R,L:25 `⁆ `:0 N:0 := lie_module_equiv R L M N
+
+namespace lie_module_equiv
+
+variables {R L M N P}
+
+instance has_coe_to_lie_module_hom : has_coe (M ≃ₗ⁅R,L⁆ N) (M →ₗ⁅R,L⁆ N) := ⟨to_lie_module_hom⟩
+instance has_coe_to_linear_equiv : has_coe (M ≃ₗ⁅R,L⁆ N) (M ≃ₗ[R] N) := ⟨to_linear_equiv⟩
+
+/-- see Note [function coercion] -/
+instance : has_coe_to_fun (M ≃ₗ⁅R,L⁆ N) := ⟨_, to_fun⟩
+
+@[simp, norm_cast] lemma coe_to_lie_module_hom (e : M ≃ₗ⁅R,L⁆ N) : ((e : M →ₗ⁅R,L⁆ N) : M → N) = e :=
+  rfl
+
+@[simp, norm_cast] lemma coe_to_linear_equiv (e : M ≃ₗ⁅R,L⁆ N) : ((e : M ≃ₗ[R] N) : M → N) = e :=
+  rfl
+
+instance : has_one (M ≃ₗ⁅R,L⁆ M) := ⟨{ map_lie := λ x m, rfl, ..(1 : M ≃ₗ[R] M) }⟩
+
+@[simp] lemma one_apply (m : M) : (1 : (M ≃ₗ⁅R,L⁆ M)) m = m := rfl
+
+instance : inhabited (M ≃ₗ⁅R,L⁆ M) := ⟨1⟩
+
+/-- Lie module equivalences are reflexive. -/
+@[refl] def refl : M ≃ₗ⁅R,L⁆ M := 1
+
+@[simp] lemma refl_apply (m : M) : (refl : M ≃ₗ⁅R,L⁆ M) m = m := rfl
+
+/-- Lie module equivalences are syemmtric. -/
+@[symm] def symm (e : M ≃ₗ⁅R,L⁆ N) : N ≃ₗ⁅R,L⁆ M :=
+{ ..lie_module_hom.inverse e.to_lie_module_hom e.inv_fun e.left_inv e.right_inv,
+  ..(e : M ≃ₗ[R] N).symm }
+
+@[simp] lemma symm_symm (e : M ≃ₗ⁅R,L⁆ N) : e.symm.symm = e :=
+by { cases e, refl, }
+
+@[simp] lemma apply_symm_apply (e : M ≃ₗ⁅R,L⁆ N) : ∀ x, e (e.symm x) = x :=
+  e.to_linear_equiv.apply_symm_apply
+
+@[simp] lemma symm_apply_apply (e : M ≃ₗ⁅R,L⁆ N) : ∀ x, e.symm (e x) = x :=
+  e.to_linear_equiv.symm_apply_apply
+
+/-- Lie module equivalences are transitive. -/
+@[trans] def trans (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) : M ≃ₗ⁅R,L⁆ P :=
+{ ..lie_module_hom.comp e₂.to_lie_module_hom e₁.to_lie_module_hom,
+  ..linear_equiv.trans e₁.to_linear_equiv e₂.to_linear_equiv }
+
+@[simp] lemma trans_apply (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) (m : M) :
+  (e₁.trans e₂) m = e₂ (e₁ m) := rfl
+
+@[simp] lemma symm_trans_apply (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) (p : P) :
+  (e₁.trans e₂).symm p = e₁.symm (e₂.symm p) := rfl
+
+end lie_module_equiv
+
+end lie_module_morphisms
 
 section of_associative
 
@@ -895,8 +1011,9 @@ begin
   simp only [mem_skew_adjoint_matrices_submodule] at *,
   change ⁅A, B⁆ᵀ ⬝ J = J ⬝ -⁅A, B⁆, change Aᵀ ⬝ J = J ⬝ -A at hA, change Bᵀ ⬝ J = J ⬝ -B at hB,
   simp only [←matrix.mul_eq_mul] at *,
-  rw [matrix.lie_transpose, lie_ring.of_associative_ring_bracket, lie_ring.of_associative_ring_bracket,
-    sub_mul, mul_assoc, mul_assoc, hA, hB, ←mul_assoc, ←mul_assoc, hA, hB],
+  rw [matrix.lie_transpose, lie_ring.of_associative_ring_bracket,
+    lie_ring.of_associative_ring_bracket, sub_mul, mul_assoc, mul_assoc, hA, hB, ←mul_assoc,
+    ←mul_assoc, hA, hB],
   noncomm_ring,
 end
 
@@ -948,7 +1065,8 @@ end
 rfl
 
 lemma mem_skew_adjoint_matrices_lie_subalgebra_unit_smul (u : units R) (J A : matrix n n R) :
-  A ∈ skew_adjoint_matrices_lie_subalgebra ((u : R) • J) ↔ A ∈ skew_adjoint_matrices_lie_subalgebra J :=
+  A ∈ skew_adjoint_matrices_lie_subalgebra ((u : R) • J) ↔
+  A ∈ skew_adjoint_matrices_lie_subalgebra J :=
 begin
   change A ∈ skew_adjoint_matrices_submodule ((u : R) • J) ↔  A ∈ skew_adjoint_matrices_submodule J,
   simp only [mem_skew_adjoint_matrices_submodule, matrix.is_skew_adjoint, matrix.is_adjoint_pair],

src/algebra/lie/direct_sum.lean

@@ -0,0 +1,112 @@
+/-
+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.basic
+import linear_algebra.direct_sum.finsupp
+
+/-!
+# Direct sums of Lie algebras and Lie modules
+
+Direct sums of Lie algebras and Lie modules carry natural algbebra and module structures.
+
+## Tags
+
+lie algebra, lie module, direct sum
+-/
+
+universes u v w w₁
+
+namespace direct_sum
+open dfinsupp
+open_locale direct_sum
+
+variables {R : Type u} {ι : Type v} [comm_ring R]
+
+section modules
+
+/-! The direct sum of Lie modules over a fixed Lie algebra carries a natural Lie module
+structure. -/
+
+variables {L : Type w₁} {M : ι → Type w}
+variables [lie_ring L] [lie_algebra R L]
+variables [Π i, add_comm_group (M i)] [Π i, module R (M i)]
+variables [Π i, lie_ring_module L (M i)] [Π i, lie_module R L (M i)]
+
+instance : lie_ring_module L (⨁ i, M i) :=
+{ bracket     := λ x m, m.map_range (λ i m', ⁅x, m'⁆) (λ i, lie_zero x),
+  add_lie     := λ x y m, by { ext, simp only [map_range_apply, add_apply, add_lie], },
+  lie_add     := λ x m n, by { ext, simp only [map_range_apply, add_apply, lie_add], },
+  leibniz_lie := λ x y m, by { ext, simp only [map_range_apply, lie_lie, add_apply,
+    sub_add_cancel], }, }
+
+@[simp] lemma lie_module_bracket_apply (x : L) (m : ⨁ i, M i) (i : ι) :
+  ⁅x, m⁆ i = ⁅x, m i⁆ := map_range_apply _ _ m i
+
+instance : lie_module R L (⨁ i, M i) :=
+{ smul_lie := λ t x m, by { ext i, simp only [smul_lie, lie_module_bracket_apply, smul_apply], },
+  lie_smul := λ t x m, by { ext i, simp only [lie_smul, lie_module_bracket_apply, smul_apply], }, }
+
+variables (R ι L M)
+
+/-- The inclusion of each component into a direct sum as a morphism of Lie modules. -/
+def lie_module_of [decidable_eq ι] (j : ι) : M j →ₗ⁅R,L⁆ ⨁ i, M i :=
+{ map_lie := λ x m,
+    begin
+      ext i, by_cases h : j = i,
+      { rw ← h, simp, },
+      { simp [lof, single_eq_of_ne h], },
+    end,
+  ..lof R ι M j }
+
+/-- The projection map onto one component, as a morphism of Lie modules. -/
+def lie_module_component (j : ι) : (⨁ i, M i) →ₗ⁅R,L⁆ M j :=
+{ map_lie := λ x m,
+    by simp only [component, lapply_apply, lie_module_bracket_apply, linear_map.to_fun_eq_coe],
+  ..component R ι M j }
+
+end modules
+
+section algebras
+
+/-! The direct sum of Lie algebras carries a natural Lie algebra structure. -/
+
+variables {L : ι → Type w}
+variables [Π i, lie_ring (L i)] [Π i, lie_algebra R (L i)]
+
+instance : 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], },
+  lie_self    := λ x, by { ext, simp only [zip_with_apply, add_apply, lie_self, zero_apply], },
+  leibniz_lie := λ x y z, by { ext, simp only [sub_apply,
+    zip_with_apply, add_apply, zero_apply], apply leibniz_lie, },
+  ..(infer_instance : add_comm_group _) }
+
+@[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) :=
+{ 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
+  { ext i, by_cases h : j = i,
+    { rw ← h, simp, },
+    { simp [lof, 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, by simp only [component, bracket_apply, lapply_apply, linear_map.to_fun_eq_coe],
+  ..component R ι L j }
+
+end algebras
+
+end direct_sum