feat(algebra/lie_algebra): define Lie subalgebras, morphisms, modules…

…, submodules, quotients (#1835)

* feat(algebra/lie_algebra): define Lie subalgebras, morphisms, modules, submodules, quotients

* Code review: colons at end of line

* Update src/algebra/lie_algebra.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/algebra/lie_algebra.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/algebra/lie_algebra.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Catch up after GH commits from code review

* Remove accidentally-included '#lint'

* Rename: lie_subalgebra.bracket --> lie_subalgebra.lie_mem

* Lie ideals are subalgebras

* Add missing doc string

* Update src/algebra/lie_algebra.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Allow quotients of lie_modules by lie_submodules (part 1)

The missing piece is the construction of a lie_module structure on
the quotient by a lie_submodule, i.e.,:
`instance lie_quotient_lie_module : lie_module R L N.quotient := ...`

I will add this in due course.

* Code review: minor fixes

* New lie_module approach based on add_action, linear_action

* Remove add_action by merging into linear_action.

I would prefer to keep add_action, and especially like to keep the feature
that linear_action extends has_scalar, but unfortunately this is not
possible with the current typeclass resolution algorithm since we should
never extend a class with fewer carrier types.

* Add missing doc string

* Simplify Lie algebra adjoing action definitions

* whitespace tweaks

* Remove redundant explicit type

* Update src/algebra/lie_algebra.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/algebra/lie_algebra.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/algebra/lie_algebra.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/algebra/lie_algebra.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Catch up after rename bracket --> map_lie in morphism

* Update src/linear_algebra/linear_action.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/linear_algebra/linear_action.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/linear_algebra/linear_action.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/linear_algebra/linear_action.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/linear_algebra/linear_action.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/linear_algebra/linear_action.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/linear_algebra/linear_action.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/linear_algebra/linear_action.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/linear_algebra/linear_action.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/algebra/lie_algebra.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import ring_theory.algebra data.matrix.basic
+import ring_theory.algebra data.matrix.basic linear_algebra.linear_action
 
 /-!
 # Lie algebras
@@ -12,11 +12,17 @@ This file defines Lie rings, and Lie algebras over a commutative ring. It shows
 associative rings and algebras via the ring commutator. In particular it defines the Lie algebra
 of endomorphisms of a module as well as of the algebra of square matrices over a commutative ring.
 
+It also includes definitions of morphisms of Lie algebras, Lie subalgebras, Lie modules, Lie
+submodules, and the quotient of a Lie algebra by an ideal.
+
 ## Notations
 
 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.
+
 ## Implementation notes
 
 Lie algebras are defined as modules with a compatible Lie ring structure, and thus are partially
@@ -174,23 +180,26 @@ end prio
 
 namespace lie_algebra
 
-variables (R : Type u) (L : Type v) [comm_ring R] [add_comm_group L] [lie_algebra R L]
-
 /--
-The adjoint action of a Lie algebra on itself.
+A morphism of Lie algebras is a linear map respecting the bracket operations.
 -/
-def Ad (x : L) : L →ₗ[R] L :=
-{ to_fun := has_bracket.bracket x,
-  add    := by { intros, apply lie_add },
-  smul   := by { intros, apply lie_smul } }
+structure morphism (R : Type u) (L : Type v) (L' : Type v)
+  [comm_ring R] [add_comm_group L] [lie_algebra R L] [add_comm_group L'] [lie_algebra R L']
+  extends linear_map R L L' :=
+(map_lie : ∀ {x y : L}, to_fun ⁅x, y⁆ = ⁅to_fun x, to_fun y⁆)
 
-/--
-The bracket of a Lie algebra as a bilinear map.
--/
-def bil_lie : L →ₗ[R] L →ₗ[R] L :=
-{ to_fun := lie_algebra.Ad R L,
-  add    := by { unfold lie_algebra.Ad, intros, ext, simp [add_lie], },
-  smul   := by { unfold lie_algebra.Ad, intros, ext, simp, } }
+infixr ` →ₗ⁅⁆ `:25 := morphism _
+notation L ` →ₗ⁅`:25 R:25 `⁆ `:0 L':0 := morphism R L L'
+
+instance (R : Type u) (L : Type v) (L' : Type v)
+  [comm_ring R] [add_comm_group L] [lie_algebra R L] [add_comm_group L'] [lie_algebra R L'] :
+  has_coe (L →ₗ⁅R⁆ L') (L →ₗ[R] L') := ⟨morphism.to_linear_map⟩
+
+@[simp] lemma map_lie {R : Type u} {L : Type v} {L' : Type v}
+  [comm_ring R] [add_comm_group L] [lie_algebra R L] [add_comm_group L'] [lie_algebra R L']
+  (f : L →ₗ⁅R⁆ L') (x y : L) : f ⁅x, y⁆ = ⁅f x, f y⁆ := morphism.map_lie f
+
+variables {R : Type u} {L : Type v} [comm_ring R] [add_comm_group L] [lie_algebra R L]
 
 /--
 An associative algebra gives rise to a Lie algebra by taking the bracket to be the ring commutator.
@@ -205,16 +214,208 @@ def of_associative_algebra (A : Type v) [ring A] [algebra R A] : lie_algebra R A
 An important class of Lie algebras are those arising from the associative algebra structure on
 module endomorphisms.
 -/
-def of_endomorphism_algebra (M : Type v)
+instance of_endomorphism_algebra (M : Type v)
   [add_comm_group M] [module R M] : lie_algebra R (module.End R M) :=
-of_associative_algebra R (module.End R M)
+of_associative_algebra (module.End R M)
+
+lemma endo_algebra_bracket (M : Type v)
+  [add_comm_group M] [module R M] (f g : module.End R M) :
+  ⁅f, g⁆ = f.comp g - g.comp f := rfl
+
+/--
+The adjoint action of a Lie algebra on itself.
+-/
+def Ad : L →ₗ⁅R⁆ module.End R L := {
+  to_fun  := λ x, {
+    to_fun := has_bracket.bracket x,
+    add    := by { intros, apply lie_add, },
+    smul   := by { intros, apply lie_smul, } },
+  add     := by { intros, ext, simp, },
+  smul    := by { intros, ext, simp, },
+  map_lie := by {
+    intros x y, ext z,
+    rw endo_algebra_bracket,
+    suffices : ⁅⁅x, y⁆, z⁆ = ⁅x, ⁅y, z⁆⁆ + ⁅⁅x, z⁆, y⁆, by simpa,
+    rw [eq_comm, ←lie_skew ⁅x, y⁆ z, ←lie_skew ⁅x, z⁆ y, ←lie_skew x z, lie_neg, neg_neg,
+        ←sub_eq_zero_iff_eq, sub_neg_eq_add, lie_ring.jacobi], } }
 
 end lie_algebra
 
+section lie_subalgebra
+
+variables (R : Type u) (L : Type v) [comm_ring R] [add_comm_group L] [lie_algebra R L]
+
+/--
+A Lie subalgebra of a Lie algebra is submodule that is closed under the Lie bracket.
+This is a sufficient condition for the subset itself to form a Lie algebra.
+-/
+structure lie_subalgebra extends submodule R L :=
+(lie_mem : ∀ {x y}, x ∈ carrier → y ∈ carrier → ⁅x, y⁆ ∈ carrier)
+
+instance lie_subalgebra_coe_submodule : has_coe (lie_subalgebra R L) (submodule R L) :=
+⟨lie_subalgebra.to_submodule⟩
+
+instance lie_subalgebra_lie_algebra [L' : lie_subalgebra R L] : lie_algebra R L' := {
+  bracket  := λ x y, ⟨⁅x.val, y.val⁆, L'.lie_mem x.property y.property⟩,
+  lie_add  := by { intros, apply set_coe.ext, apply lie_add, },
+  add_lie  := by { intros, apply set_coe.ext, apply add_lie, },
+  lie_self := by { intros, apply set_coe.ext, apply lie_self, },
+  jacobi   := by { intros, apply set_coe.ext, apply lie_ring.jacobi, },
+  lie_smul := by { intros, apply set_coe.ext, apply lie_smul, } }
+
+end lie_subalgebra
+
+section lie_module
+
+variables (R : Type u) (L : Type v) [comm_ring R] [add_comm_group L] [lie_algebra R L]
+variables (M  : Type v) [add_comm_group M] [module R M]
+
+section prio
+set_option default_priority 100 -- see Note [default priority]
+/--
+A Lie module is a module over a commutative ring, together with a linear action of a Lie algebra
+on this module, such that the Lie bracket acts as the commutator of endomorphisms.
+-/
+class lie_module extends linear_action R L M :=
+(lie_act : ∀ (l l' : L) (m : M), act ⁅l, l'⁆ m = act l (act l' m) - act l' (act l m))
+end prio
+
+@[simp] lemma lie_act [lie_module R L M]
+  (l l' : L) (m : M) : linear_action.act R ⁅l, l'⁆ m =
+                       linear_action.act R l (linear_action.act R l' m) -
+                       linear_action.act R l' (linear_action.act R l m) :=
+  lie_module.lie_act R l l' m
+
+protected lemma of_endo_map_action (α : L →ₗ⁅R⁆ module.End R M) (x : L) (m : M) :
+  @linear_action.act R _ _ _ _ _ _ _ (linear_action.of_endo_map R L M α) x m = α x m := rfl
+
+/--
+A Lie morphism from a Lie algebra to the endomorphism algebra of a module yields
+a Lie module structure.
+-/
+def lie_module.of_endo_morphism (α : L →ₗ⁅R⁆ module.End R M) : lie_module R L M := {
+  lie_act := by { intros x y m, rw [of_endo_map_action, lie_algebra.map_lie,
+                                    lie_algebra.endo_algebra_bracket], refl, },
+  ..(linear_action.of_endo_map R L M α) }
+
+/--
+Every Lie algebra is a module over itself.
+-/
+instance lie_algebra_self_module : lie_module R L L :=
+  lie_module.of_endo_morphism R L L lie_algebra.Ad
+
+/--
+A Lie submodule of a Lie module is a submodule that is closed under the Lie bracket.
+This is a sufficient condition for the subset itself to form a Lie module.
+-/
+structure lie_submodule [lie_module R L M] extends submodule R M :=
+(lie_mem : ∀ {x : L} {m : M}, m ∈ carrier → linear_action.act R x m ∈ carrier)
+
+instance lie_submodule_coe_submodule [lie_module R L M] :
+  has_coe (lie_submodule R L M) (submodule R M) := ⟨lie_submodule.to_submodule⟩
+
+instance lie_submodule_has_mem [lie_module R L M] :
+  has_mem M (lie_submodule R L M) := ⟨λ x N, x ∈ (N : set M)⟩
+
+instance lie_submodule_lie_module [lie_module R L M] (N : lie_submodule R L M) :
+  lie_module R L N := {
+  act      := λ x m, ⟨linear_action.act R x m.val, N.lie_mem m.property⟩,
+  add_act  := by { intros x y m, apply set_coe.ext, apply linear_action.add_act, },
+  act_add  := by { intros x m n, apply set_coe.ext, apply linear_action.act_add, },
+  act_smul := by { intros r x y, apply set_coe.ext, apply linear_action.act_smul, },
+  smul_act := by { intros r x y, apply set_coe.ext, apply linear_action.smul_act, },
+  lie_act  := by { intros x y m, apply set_coe.ext, apply lie_module.lie_act, } }
+
+/--
+An ideal of a Lie algebra is a Lie submodule of the Lie algebra as a Lie module over itself.
+-/
+abbreviation lie_ideal := lie_submodule R L L
+
+lemma lie_mem_right (I : lie_ideal R L) (x y : L) (h : y ∈ I) : ⁅x, y⁆ ∈ I := I.lie_mem h
+
+lemma lie_mem_left (I : lie_ideal R L) (x y : L) (h : x ∈ I) : ⁅x, y⁆ ∈ I := by {
+  rw [←lie_skew, ←neg_lie], apply lie_mem_right, assumption, }
+
+/--
+An ideal of a Lie algebra is a Lie subalgebra.
+-/
+def lie_ideal_subalgebra (I : lie_ideal R L) : lie_subalgebra R L := {
+  lie_mem := by { intros x y hx hy, apply lie_mem_right, exact hy, },
+  ..I.to_submodule, }
+
+end lie_module
+
+namespace lie_submodule
+
+variables {R : Type u} {L : Type v} [comm_ring R] [add_comm_group L] [lie_algebra R L]
+variables {M : Type v} [add_comm_group M] [module R M] [lie_module R L M]
+variables (N : lie_submodule R L M) (I : lie_ideal R L)
+
+/--
+The quotient of a Lie module by a Lie submodule. It is a Lie module.
+-/
+abbreviation quotient := N.to_submodule.quotient
+
+namespace quotient
+
+variables {N I}
+
+/--
+Map sending an element of `M` to the corresponding element of `M/N`, when `N` is a lie_submodule of
+the lie_module `N`.
+-/
+abbreviation mk : M → N.quotient := submodule.quotient.mk
+
+lemma is_quotient_mk (m : M) :
+  quotient.mk' m = (mk m : N.quotient) := rfl
+
+instance lie_quotient_has_bracket : has_bracket (quotient I) := ⟨by {
+  intros x y,
+  apply quotient.lift_on₂' x y (λ x' y', mk ⁅x', y'⁆),
+  intros x₁ x₂ y₁ y₂ h₁ h₂,
+  apply (submodule.quotient.eq I.to_submodule).2,
+  have h : ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ = ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆ := by { simp [-lie_skew], },
+  rw h,
+  apply submodule.add_mem,
+  { apply lie_mem_right R L I x₁ (x₂ - y₂) h₂, },
+  { apply lie_mem_left R L I (x₁ - y₁) y₂ h₁, }, }⟩
+
+@[simp] lemma mk_bracket (x y : L) :
+  (mk ⁅x, y⁆ : quotient I) = ⁅mk x, mk y⁆ := rfl
+
+instance lie_quotient_lie_algebra : lie_algebra R (quotient I) := {
+  add_lie  := by { intros x' y' z', apply quotient.induction_on₃' x' y' z', intros x y z,
+                   repeat { rw is_quotient_mk <|>
+                            rw ←mk_bracket <|>
+                            rw ←submodule.quotient.mk_add, },
+                   apply congr_arg, apply add_lie, },
+  lie_add  := by { intros x' y' z', apply quotient.induction_on₃' x' y' z', intros x y z,
+                   repeat { rw is_quotient_mk <|>
+                            rw ←mk_bracket <|>
+                            rw ←submodule.quotient.mk_add, },
+                   apply congr_arg, apply lie_add, },
+  lie_self := by { intros x', apply quotient.induction_on' x', intros x,
+                   rw [is_quotient_mk, ←mk_bracket],
+                   apply congr_arg, apply lie_self, },
+  jacobi   := by { intros x' y' z', apply quotient.induction_on₃' x' y' z', intros x y z,
+                   repeat { rw is_quotient_mk <|>
+                            rw ←mk_bracket <|>
+                            rw ←submodule.quotient.mk_add, },
+                   apply congr_arg, apply lie_ring.jacobi, },
+  lie_smul := by { intros t x' y', apply quotient.induction_on₂' x' y', intros x y,
+                   repeat { rw is_quotient_mk <|>
+                            rw ←mk_bracket <|>
+                            rw ←submodule.quotient.mk_smul, },
+                   apply congr_arg, apply lie_smul, } }
+
+end quotient
+
+end lie_submodule
+
 /--
 An important class of Lie algebras are those arising from the associative algebra structure on
 square matrices over a commutative ring.
 -/
 def matrix.lie_algebra (n : Type u) (R : Type v)
   [fintype n] [decidable_eq n] [comm_ring R] : lie_algebra R (matrix n n R) :=
-lie_algebra.of_associative_algebra R (matrix n n R)
+lie_algebra.of_associative_algebra (matrix n n R)

src/linear_algebra/linear_action.lean

@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2020 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import linear_algebra.basic
+
+/-!
+# Linear actions
+
+For modules M and N, we can regard a linear map M →ₗ End N as a "linear action" of M on N.
+In this file we introduce the class `linear_action` to make it easier to work with such actions.
+
+## Tags
+
+linear action
+-/
+
+universes u v
+
+section linear_action
+
+variables (R : Type u) (M N : Type v)
+variables [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N]
+
+section prio
+set_option default_priority 100 -- see Note [default priority]
+/--
+A binary operation representing one module acting linearly on another.
+-/
+class linear_action :=
+(act      : M → N → N)
+(add_act  : ∀ (m m' : M) (n : N), act (m + m') n = act m n + act m' n)
+(act_add  : ∀ (m : M) (n n' : N), act m (n + n') = act m n + act m n')
+(act_smul : ∀ (r : R) (m : M) (n : N), act (r • m) n = r • (act m n))
+(smul_act : ∀ (r : R) (m : M) (n : N), act m (r • n) = act (r • m) n)
+end prio
+
+@[simp] lemma zero_linear_action [linear_action R M N] (n : N) :
+  linear_action.act R (0 : M) n = 0 :=
+begin
+  let z := linear_action.act R (0 : M) n,
+  have H : z + z = z + 0 := by { rw ←linear_action.add_act, simp, },
+  exact add_left_cancel H,
+end
+
+@[simp] lemma linear_action_zero [linear_action R M N] (m : M) :
+  linear_action.act R m (0 : N) = 0 :=
+begin
+  let z := linear_action.act R m (0 : N),
+  have H : z + z = z + 0 := by { rw ←linear_action.act_add, simp, },
+  exact add_left_cancel H,
+end
+
+@[simp] lemma linear_action_add_act [linear_action R M N] (m m' : M) (n : N) :
+  linear_action.act R (m + m') n = linear_action.act R m n +
+                                   linear_action.act R m' n :=
+linear_action.add_act R m m' n
+
+@[simp] lemma linear_action_act_add [linear_action R M N] (m : M) (n n' : N) :
+  linear_action.act R m (n + n') = linear_action.act R m n +
+                                   linear_action.act R m n' :=
+linear_action.act_add R m n n'
+
+@[simp] lemma linear_action_act_smul [linear_action R M N] (r : R) (m : M) (n : N) :
+  linear_action.act R (r • m) n = r • (linear_action.act R m n) :=
+linear_action.act_smul r m n
+
+@[simp] lemma linear_action_smul_act [linear_action R M N] (r : R) (m : M) (n : N) :
+  linear_action.act R m (r • n) = linear_action.act R (r • m) n :=
+linear_action.smul_act r m n
+
+end linear_action
+
+namespace linear_action
+
+variables (R : Type u) (M N : Type v)
+variables [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N]
+
+/--
+A linear map to the endomorphism algebra yields a linear action.
+-/
+def of_endo_map (α : M →ₗ[R] module.End R N) : linear_action R M N :=
+{ act      := λ m n, α m n,
+  add_act  := by { intros, rw linear_map.map_add, simp, },
+  act_add  := by { intros, simp, },
+  act_smul := by { intros, rw linear_map.map_smul, simp, },
+  smul_act := by { intros, repeat { rw linear_map.map_smul }, simp, } }
+
+/--
+A linear action yields a linear map to the endomorphism algebra.
+-/
+def to_endo_map (α : linear_action R M N) : M →ₗ[R] module.End R N :=
+{ to_fun  := λ m,
+  { to_fun := λ n, linear_action.act R m n,
+    add    := by { intros, simp, },
+    smul   := by { intros, simp, }, },
+  add     := by { intros, ext, simp, },
+  smul    := by { intros, ext, simp, } }
+
+end linear_action