feat(algebra/lie/basic): define the module and lie_module structures on morphisms of Lie modules (#7225)

Also sundry `simp` lemmas

Author: ocfnash

src/algebra/lie/basic.lean

@@ -80,9 +80,10 @@ algebra on this module, such that the Lie bracket acts as the commutator of endo
 
 section basic_properties
 
-variables {R : Type u} {L : Type v} {M : Type w}
-variables [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M]
-variables [lie_ring_module L M] [lie_module R L M]
+variables {R : Type u} {L : Type v} {M : Type w} {N : Type w₁}
+variables [comm_ring R] [lie_ring L] [lie_algebra R L]
+variables [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M]
+variables [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N]
 variables (t : R) (x y z : L) (m n : M)
 
 @[simp] lemma add_lie : ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆ := lie_ring_module.add_lie x y m
@@ -119,6 +120,18 @@ by { rw [←sub_eq_zero, sub_neg_eq_add, ←add_lie], simp, }
 @[simp] lemma lie_neg : ⁅x, -m⁆ = -⁅x, m⁆ :=
 by { rw [←sub_eq_zero, sub_neg_eq_add, ←lie_add], simp, }
 
+@[simp] lemma sub_lie : ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆ :=
+by simp [sub_eq_add_neg]
+
+@[simp] lemma lie_sub : ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆ :=
+by simp [sub_eq_add_neg]
+
+@[simp] lemma nsmul_lie (n : ℕ) : ⁅n • x, m⁆ = n • ⁅x, m⁆ :=
+add_monoid_hom.map_nsmul ⟨λ (x : L), ⁅x, m⁆, zero_lie m, λ _ _, add_lie _ _ _⟩ _ _
+
+@[simp] lemma lie_nsmul (n : ℕ) : ⁅x, n • m⁆ = n • ⁅x, m⁆ :=
+add_monoid_hom.map_nsmul ⟨λ (m : M), ⁅x, m⁆, lie_zero x, λ _ _, lie_add _ _ _⟩ _ _
+
 @[simp] lemma gsmul_lie (a : ℤ) : ⁅a • x, m⁆ = a • ⁅x, m⁆ :=
 add_monoid_hom.map_gsmul ⟨λ (x : L), ⁅x, m⁆, zero_lie m, λ _ _, add_lie _ _ _⟩ _ _
 
@@ -131,6 +144,30 @@ by rw [leibniz_lie, add_sub_cancel]
 lemma lie_jacobi : ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0 :=
 by { rw [← neg_neg ⁅x, y⁆, lie_neg z, lie_skew y x, ← lie_skew, lie_lie], abel, }
 
+instance : lie_ring_module L (M →ₗ[R] N) :=
+{ bracket     := λ x f,
+  { to_fun    := λ m, ⁅x, f m⁆ - f ⁅x, m⁆,
+    map_add'  := λ m n, by { simp only [lie_add, linear_map.map_add], abel, },
+    map_smul' := λ t m, by simp only [smul_sub, linear_map.map_smul, lie_smul], },
+  add_lie     := λ x y f, by
+    { ext n, simp only [add_lie, linear_map.coe_mk, linear_map.add_apply, linear_map.map_add],
+      abel, },
+  lie_add     := λ x f g, by
+    { ext n, simp only [linear_map.coe_mk, lie_add, linear_map.add_apply], abel, },
+  leibniz_lie := λ x y f, by
+    { ext n,
+      simp only [lie_lie, linear_map.coe_mk, linear_map.map_sub, linear_map.add_apply, lie_sub],
+      abel, }, }
+
+@[simp] lemma bracket_apply (f : M →ₗ[R] N) (x : L) (m : M) : ⁅x, f⁆ m = ⁅x, f m⁆ - f ⁅x, m⁆ := rfl
+
+instance : lie_module R L (M →ₗ[R] N) :=
+{ smul_lie := λ t x f, by
+    { ext n,
+      simp only [smul_sub, smul_lie, linear_map.smul_apply, bracket_apply, linear_map.map_smul], },
+  lie_smul := λ t x f, by
+    { ext n, simp only [smul_sub, linear_map.smul_apply, bracket_apply, lie_smul], }, }
+
 end basic_properties
 
 set_option old_structure_cmd true
@@ -157,9 +194,6 @@ instance : has_coe_to_fun (L₁ →ₗ⁅R⁆ L₂) := ⟨_, lie_hom.to_fun⟩
 
 initialize_simps_projections lie_hom (to_fun → apply)
 
-@[simp] lemma coe_mk (f : L₁ → L₂) (h₁ h₂ h₃) :
-  ((⟨f, h₁, h₂, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = f := rfl
-
 @[simp, norm_cast] lemma coe_to_linear_map (f : L₁ →ₗ⁅R⁆ L₂) : ((f : L₁ →ₗ[R] L₂) : L₁ → L₂) = f :=
 rfl
 
@@ -169,13 +203,23 @@ linear_map.map_smul (f : L₁ →ₗ[R] L₂) c x
 @[simp] lemma map_add (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f (x + y) = (f x) + (f y) :=
 linear_map.map_add (f : L₁ →ₗ[R] L₂) x y
 
+@[simp] lemma map_sub (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f (x - y) = (f x) - (f y) :=
+linear_map.map_sub (f : L₁ →ₗ[R] L₂) x y
+
+@[simp] lemma map_neg (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) : f (-x) = -(f x) :=
+linear_map.map_neg (f : L₁ →ₗ[R] L₂) x
+
 @[simp] lemma map_lie (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f ⁅x, y⁆ = ⁅f x, f y⁆ := lie_hom.map_lie' f
 
 @[simp] lemma map_zero (f : L₁ →ₗ⁅R⁆ L₂) : f 0 = 0 := (f : L₁ →ₗ[R] L₂).map_zero
 
 /-- The constant 0 map is a Lie algebra morphism. -/
 instance : has_zero (L₁ →ₗ⁅R⁆ L₂) := ⟨{ map_lie' := by simp, ..(0 : L₁ →ₗ[R] L₂)}⟩
 
+@[norm_cast, simp] lemma coe_zero : ((0 : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = 0 := rfl
+
+lemma zero_apply (x : L₁) : (0 : L₁ →ₗ⁅R⁆ L₂) x = 0 := rfl
+
 /-- The identity map is a Lie algebra morphism. -/
 instance : has_one (L₁ →ₗ⁅R⁆ L₁) := ⟨{ map_lie' := by simp, ..(1 : L₁ →ₗ[R] L₁)}⟩
 
@@ -190,6 +234,17 @@ coe_injective $ funext h
 lemma ext_iff {f g : L₁ →ₗ⁅R⁆ L₂} : f = g ↔ ∀ x, f x = g x :=
 ⟨by { rintro rfl x, refl }, ext⟩
 
+@[simp] lemma mk_coe (f : L₁ →ₗ⁅R⁆ L₂) (h₁ h₂ h₃) :
+  (⟨f, h₁, h₂, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) = f :=
+by { ext, refl, }
+
+@[simp] lemma coe_mk (f : L₁ → L₂) (h₁ h₂ h₃) :
+  ((⟨f, h₁, h₂, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = f := rfl
+
+@[norm_cast, simp] lemma coe_linear_mk (f : L₁ →ₗ[R] L₂) (h₁ h₂ h₃) :
+  ((⟨f, h₁, h₂, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) : L₁ →ₗ[R] L₂) = ⟨f, h₁, h₂⟩ :=
+by { ext, refl, }
+
 /-- The composition of morphisms is a morphism. -/
 def 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], },
@@ -325,18 +380,34 @@ instance : has_coe (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N) := ⟨lie_module_hom.to
 /-- 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_smul (f : M →ₗ⁅R,L⁆ N) (c : R) (x : M) : f (c • x) = c • f x :=
+linear_map.map_smul (f : M →ₗ[R] N) c x
+
+@[simp] lemma map_add (f : M →ₗ⁅R,L⁆ N) (x y : M) : f (x + y) = (f x) + (f y) :=
+linear_map.map_add (f : M →ₗ[R] N) x y
+
+@[simp] lemma map_sub (f : M →ₗ⁅R,L⁆ N) (x y : M) : f (x - y) = (f x) - (f y) :=
+linear_map.map_sub (f : M →ₗ[R] N) x y
+
+@[simp] lemma map_neg (f : M →ₗ⁅R,L⁆ N) (x : M) : f (-x) = -(f x) :=
+linear_map.map_neg (f : M →ₗ[R] N) x
+
 @[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
 
+@[simp] lemma map_zero (f : M →ₗ⁅R,L⁆ N) : f 0 = 0 :=
+linear_map.map_zero (f : M →ₗ[R] N)
+
 /-- The constant 0 map is a Lie module morphism. -/
 instance : has_zero (M →ₗ⁅R,L⁆ N) := ⟨{ map_lie' := by simp, ..(0 : M →ₗ[R] N) }⟩
 
+@[norm_cast, simp] lemma coe_zero : ((0 : M →ₗ⁅R,L⁆ N) : M → N) = 0 := rfl
+
+lemma zero_apply (m : M) : (0 : M →ₗ⁅R,L⁆ N) m = 0 := rfl
+
 /-- The identity map is a Lie module morphism. -/
 instance : has_one (M →ₗ⁅R,L⁆ M) := ⟨{ map_lie' := by simp, ..(1 : M →ₗ[R] M) }⟩
 
@@ -351,6 +422,17 @@ 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⟩
 
+@[simp] lemma mk_coe (f : M →ₗ⁅R,L⁆ N) (h₁ h₂ h₃) :
+  (⟨f, h₁, h₂, h₃⟩ : M →ₗ⁅R,L⁆ N) = f :=
+by { ext, refl, }
+
+@[simp] lemma coe_mk (f : M → N) (h₁ h₂ h₃) :
+  ((⟨f, h₁, h₂, h₃⟩ : M →ₗ⁅R,L⁆ N) : M → N) = f := rfl
+
+@[norm_cast, simp] lemma coe_linear_mk (f : M →ₗ[R] N) (h₁ h₂ h₃) :
+  ((⟨f, h₁, h₂, h₃⟩ : M →ₗ⁅R,L⁆ N) : M →ₗ[R] N) = ⟨f, h₁, h₂⟩ :=
+by { ext, refl, }
+
 /-- 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], },
@@ -371,6 +453,48 @@ def inverse (f : M →ₗ⁅R,L⁆ N) (g : N → M)
               ... = ⁅x, g n⁆ : (h₁ _),
   ..linear_map.inverse f.to_linear_map g h₁ h₂ }
 
+instance : has_add (M →ₗ⁅R,L⁆ N) :=
+{ add := λ f g, { map_lie' := by simp, ..((f : M →ₗ[R] N) + (g : M →ₗ[R] N)) }, }
+
+instance : has_sub (M →ₗ⁅R,L⁆ N) :=
+{ sub := λ f g, { map_lie' := by simp, ..((f : M →ₗ[R] N) - (g : M →ₗ[R] N)) }, }
+
+instance : has_neg (M →ₗ⁅R,L⁆ N) :=
+{ neg := λ f, { map_lie' := by simp, ..(-(f : (M →ₗ[R] N))) }, }
+
+@[norm_cast, simp] lemma coe_add (f g : M →ₗ⁅R,L⁆ N) : ⇑(f + g) = f + g := rfl
+
+lemma add_apply (f g : M →ₗ⁅R,L⁆ N) (m : M) : (f + g) m = f m + g m := rfl
+
+@[norm_cast, simp] lemma coe_sub (f g : M →ₗ⁅R,L⁆ N) : ⇑(f - g) = f - g := rfl
+
+lemma sub_apply (f g : M →ₗ⁅R,L⁆ N) (m : M) : (f - g) m = f m - g m := rfl
+
+@[norm_cast, simp] lemma coe_neg (f : M →ₗ⁅R,L⁆ N) : ⇑(-f) = -f := rfl
+
+lemma neg_apply (f : M →ₗ⁅R,L⁆ N) (m : M) : (-f) m = -(f m) := rfl
+
+instance : add_comm_group (M →ₗ⁅R,L⁆ N) :=
+{ zero           := 0,
+  add            := (+),
+  neg            := has_neg.neg,
+  sub            := has_sub.sub,
+  nsmul          := λ n f, { map_lie' := λ x m, by simp, ..(n • (f : M →ₗ[R] N)) },
+  nsmul_zero'    := λ f, by { ext, simp, },
+  nsmul_succ'    := λ n f, by { ext, simp [nat.succ_eq_one_add, add_nsmul], },
+  ..(coe_injective.add_comm_group _ coe_zero coe_add coe_neg coe_sub :
+    add_comm_group (M →ₗ⁅R,L⁆ N)) }
+
+instance : has_scalar R (M →ₗ⁅R,L⁆ N) :=
+{ smul := λ t f, { map_lie' := by simp, ..(t • (f : M →ₗ[R] N)) }, }
+
+@[norm_cast, simp] lemma coe_smul (t : R) (f : M →ₗ⁅R,L⁆ N) : ⇑(t • f) = t • f := rfl
+
+lemma smul_apply (t : R) (f : M →ₗ⁅R,L⁆ N) (m : M) : (t • f) m = t • (f m) := rfl
+
+instance : module R (M →ₗ⁅R,L⁆ N) :=
+function.injective.semimodule R ⟨to_fun, rfl, coe_add⟩ coe_injective coe_smul
+
 end lie_module_hom
 
 /-- An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of