feat(algebra/lie/basic): define ideal operations for Lie modules (#5337)

Co-authored-by: Johan Commelin <johan@commelin.net>

src/algebra/lie/basic.lean

@@ -718,6 +718,13 @@ instance has_mem : has_mem M (lie_submodule R L M) := ⟨λ x N, x ∈ (N : set
 @[simp] lemma mem_carrier (N : lie_submodule R L M) {x : M} : x ∈ N.carrier ↔ x ∈ (N : set M) :=
 iff.rfl
 
+@[simp] lemma coe_to_set_mk (S : set M) (h₁ h₂ h₃ h₄) :
+  ((⟨S, h₁, h₂, h₃, h₄⟩ : lie_submodule R L M) : set M) = S := rfl
+
+@[simp] lemma coe_to_submodule_mk (p : submodule R M) (h) :
+  (({lie_mem := h, ..p} : lie_submodule R L M) : submodule R M) = p :=
+by { cases p, refl, }
+
 @[ext] lemma ext (N N' : lie_submodule R L M) (h : ∀ m, m ∈ N ↔ m ∈ N') : N = N' :=
 by { cases N, cases N', simp only [], ext m, exact h m, }
 
@@ -761,7 +768,7 @@ namespace lie_submodule
 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 (N : lie_submodule R L M) (I : lie_ideal R L)
+variables (N N' : lie_submodule R L M) (I J : lie_ideal R L)
 
 section lattice_structure
 
@@ -774,7 +781,10 @@ instance : partial_order (lie_submodule R L M) :=
 { le := λ N N', ∀ ⦃x⦄, x ∈ N → x ∈ N', -- Overriding `le` like this gives a better defeq.
   ..partial_order.lift (coe : lie_submodule R L M → set M) coe_injective }
 
-lemma le_def (N N' : lie_submodule R L M) : N ≤ N' ↔ (N : set M) ⊆ N' := iff.rfl
+lemma le_def : N ≤ N' ↔ (N : set M) ⊆ N' := iff.rfl
+
+@[simp, norm_cast] lemma coe_submodule_le_coe_submodule : (N : submodule R M) ≤ N' ↔ N ≤ N' :=
+iff.rfl
 
 instance : has_bot (lie_submodule R L M) := ⟨0⟩
 
@@ -840,7 +850,26 @@ instance : add_comm_monoid (lie_submodule R L M) :=
   add_zero  := λ _, sup_bot_eq,
   add_comm  := λ _ _, sup_comm, }
 
-@[simp] lemma add_eq_sup (N N' : lie_submodule R L M) : N + N' = N ⊔ N' := rfl
+@[simp] lemma add_eq_sup : N + N' = N ⊔ N' := rfl
+
+@[norm_cast] lemma coe_sup :
+  (↑(N ⊔ N') : submodule R M) = (N : submodule R M) ⊔ (N' : submodule R M) :=
+begin
+  have aux : ∀ (x : L) m, m ∈ (N ⊔ N' : submodule R M) → ⁅x,m⁆ ∈ (N ⊔ N' : submodule R M),
+  { simp only [submodule.mem_sup],
+    rintro x m ⟨y, hy, z, hz, rfl⟩,
+    refine ⟨⁅x, y⁆, N.lie_mem hy, ⁅x, z⁆, N'.lie_mem hz, (lie_add _ _ _).symm⟩ },
+  refine le_antisymm (Inf_le ⟨{ lie_mem := aux, ..(N ⊔ N' : submodule R M) }, _⟩) _,
+  { simp only [exists_prop, and_true, mem_set_of_eq, eq_self_iff_true, coe_to_submodule_mk,
+      ← coe_submodule_le_coe_submodule, and_self, le_sup_left, le_sup_right] },
+  { simp, },
+end
+
+lemma mem_sup (x : M) : x ∈ N ⊔ N' ↔ ∃ (y ∈ N) (z ∈ N'), y + z = x :=
+by { erw [← submodule.mem_sup, ← coe_sup], refl, }
+
+lemma eq_bot_iff : N = ⊥ ↔ ∀ (m : M), m ∈ N → m = 0 :=
+by { rw eq_bot_iff, exact iff.rfl, }
 
 section inclusion_maps
 
@@ -853,7 +882,7 @@ def incl : N →ₗ⁅R,L⁆ M :=
 
 lemma incl_eq_val : (N.incl : N → M) = subtype.val := rfl
 
-variables {N} {N' : lie_submodule R L M} (h : N ≤ N')
+variables {N N'} (h : N ≤ N')
 
 /-- Given two nested Lie submodules `N ⊆ N'`, the inclusion `N ↪ N'` is a morphism of Lie modules.-/
 def hom_of_le : N →ₗ⁅R,L⁆ N' :=
@@ -891,6 +920,88 @@ end lie_span
 
 end lattice_structure
 
+section lie_ideal_operations
+
+/-- Given a Lie module `M` over a Lie algebra `L`, the set of Lie ideals of `L` acts on the set
+of submodules of `M`. -/
+instance : has_bracket (lie_ideal R L) (lie_submodule R L M) :=
+⟨λ I N, lie_span R L { m | ∃ (x : I) (n : N), ⁅(x : L), (n : M)⁆ = m }⟩
+
+lemma lie_ideal_oper_eq_span :
+  ⁅I, N⁆ = lie_span R L { m | ∃ (x : I) (n : N), ⁅(x : L), (n : M)⁆ = m } := rfl
+
+lemma lie_mem_lie (x : I) (m : N) : ⁅(x : L), (m : M)⁆ ∈ ⁅I, N⁆ :=
+by { rw lie_ideal_oper_eq_span, apply subset_lie_span, use [x, m], }
+
+lemma lie_comm : ⁅I, J⁆ = ⁅J, I⁆ :=
+begin
+  suffices : ∀ (I J : lie_ideal R L), ⁅I, J⁆ ≤ ⁅J, I⁆, { exact le_antisymm (this I J) (this J I), },
+  clear I J, intros I J,
+  rw [lie_ideal_oper_eq_span, lie_span_le], rintros x ⟨y, z, h⟩, rw ← h,
+  rw [← lie_skew, ← lie_neg, ← submodule.coe_neg],
+  apply lie_mem_lie,
+end
+
+lemma lie_le_right : ⁅I, N⁆ ≤ N :=
+begin
+  rw [lie_ideal_oper_eq_span, lie_span_le], rintros m ⟨x, n, hn⟩, rw ← hn,
+  exact N.lie_mem n.property,
+end
+
+lemma lie_le_left : ⁅I, J⁆ ≤ I :=
+by { rw lie_comm, exact lie_le_right I J, }
+
+lemma lie_le_inf : ⁅I, J⁆ ≤ I ⊓ J :=
+by { rw le_inf_iff, exact ⟨lie_le_left I J, lie_le_right J I⟩, }
+
+@[simp] lemma lie_bot : ⁅I, (⊥ : lie_submodule R L M)⁆ = ⊥ :=
+by { rw eq_bot_iff, apply lie_le_right, }
+
+@[simp] lemma bot_lie : ⁅(⊥ : lie_ideal R L), N⁆ = ⊥ :=
+begin
+  suffices : ⁅(⊥ : lie_ideal R L), N⁆ ≤ ⊥, { exact le_bot_iff.mp this, },
+  rw [lie_ideal_oper_eq_span, lie_span_le], rintros m ⟨⟨x, hx⟩, n, hn⟩, rw ← hn,
+  change x ∈ (⊥ : lie_ideal R L) at hx, rw mem_bot at hx, simp [hx],
+end
+
+lemma mono_lie (h₁ : I ≤ J) (h₂ : N ≤ N') : ⁅I, N⁆ ≤ ⁅J, N'⁆ :=
+begin
+  intros m h,
+  rw [lie_ideal_oper_eq_span, mem_lie_span] at h, rw [lie_ideal_oper_eq_span, mem_lie_span],
+  intros N hN, apply h, rintros m' ⟨⟨x, hx⟩, ⟨n, hn⟩, hm⟩, rw ← hm, apply hN,
+  use [⟨x, h₁ hx⟩, ⟨n, h₂ hn⟩], refl,
+end
+
+lemma mono_lie_left (h : I ≤ J) : ⁅I, N⁆ ≤ ⁅J, N⁆ := mono_lie _ _ _ _ h (le_refl N)
+
+lemma mono_lie_right (h : N ≤ N') : ⁅I, N⁆ ≤ ⁅I, N'⁆ := mono_lie _ _ _ _ (le_refl I) h
+
+@[simp] lemma lie_sup : ⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, N'⁆ :=
+begin
+  have h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆,
+  { rw sup_le_iff, split; apply mono_lie_right; [exact le_sup_left, exact le_sup_right], },
+  suffices : ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆, { exact le_antisymm this h, }, clear h,
+  rw [lie_ideal_oper_eq_span, lie_span_le], rintros m ⟨x, ⟨n, hn⟩, h⟩, erw lie_submodule.mem_sup,
+  erw lie_submodule.mem_sup at hn, rcases hn with ⟨n₁, hn₁, n₂, hn₂, hn'⟩,
+  use ⁅(x : L), (⟨n₁, hn₁⟩ : N)⁆, split, { apply lie_mem_lie, },
+  use ⁅(x : L), (⟨n₂, hn₂⟩ : N')⁆, split, { apply lie_mem_lie, },
+  simp [← h, ← hn'],
+end
+
+@[simp] lemma sup_lie : ⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆ :=
+begin
+  have h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆,
+  { rw sup_le_iff, split; apply mono_lie_left; [exact le_sup_left, exact le_sup_right], },
+  suffices : ⁅I ⊔ J, N⁆ ≤ ⁅I, N⁆ ⊔ ⁅J, N⁆, { exact le_antisymm this h, }, clear h,
+  rw [lie_ideal_oper_eq_span, lie_span_le], rintros m ⟨⟨x, hx⟩, n, h⟩, erw lie_submodule.mem_sup,
+  erw lie_submodule.mem_sup at hx, rcases hx with ⟨x₁, hx₁, x₂, hx₂, hx'⟩,
+  use ⁅((⟨x₁, hx₁⟩ : I) : L), (n : N)⁆, split, { apply lie_mem_lie, },
+  use ⁅((⟨x₂, hx₂⟩ : J) : L), (n : N)⁆, split, { apply lie_mem_lie, },
+  simp [← h, ← hx'],
+end
+
+end lie_ideal_operations
+
 /-- The quotient of a Lie module by a Lie submodule. It is a Lie module. -/
 abbreviation quotient := N.to_submodule.quotient
 
@@ -986,6 +1097,32 @@ end quotient
 
 end lie_submodule
 
+section lie_module
+
+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]
+
+section lie_module
+
+/-- The derived Lie submodule of a Lie module. -/
+def derived_lie_submodule : lie_submodule R L M := ⁅(⊤ : lie_ideal R L), ⊤⁆
+
+lemma trivial_iff_derived_eq_bot : lie_module.is_trivial L M ↔ derived_lie_submodule R L M = ⊥ :=
+begin
+  split; intros h,
+  { erw [eq_bot_iff, lie_submodule.lie_span_le], rintros m ⟨x, n, hn⟩, rw [← hn, h.trivial], simp,},
+  { rw lie_submodule.eq_bot_iff at h, apply is_trivial.mk, intros x m, apply h,
+    apply lie_submodule.subset_lie_span, use [x, m], refl, },
+end
+
+end lie_module
+
+/-- The derived Lie ideal of a Lie algebra. -/
+abbreviation derived_lie_ideal : lie_ideal R L := derived_lie_submodule R L L
+
+end lie_module
+
 section lie_submodule_map_and_comap
 
 variables {R : Type u} {L : Type v} {L' : Type w₂} {M : Type w} {M' : Type w₁}

src/algebra/module/submodule.lean

@@ -64,6 +64,9 @@ theorem coe_injective : injective (coe : submodule R M → set M) :=
 
 @[simp, norm_cast] theorem coe_set_eq : (p : set M) = q ↔ p = q := coe_injective.eq_iff
 
+@[simp] lemma mk_coe (S : set M) (h₁ h₂ h₃) :
+  ((⟨S, h₁, h₂, h₃⟩ : submodule R M) : set M) = S := rfl
+
 theorem ext'_iff : p = q ↔ (p : set M) = q := coe_set_eq.symm
 
 @[ext] theorem ext (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := coe_injective $ set.ext h

src/linear_algebra/finite_dimensional.lean

@@ -341,7 +341,7 @@ begin
     { intros _ _ _ _ _ _, exact subtype.mk.inj, },
     { intros b hbs hb,
       use b,
-      simpa only [hbs, exists_prop, dif_pos, mk_coe, and_true, if_true, finset.coe_mem,
+      simpa only [hbs, exists_prop, dif_pos, finset.mk_coe, and_true, if_true, finset.coe_mem,
         eq_self_iff_true, exists_prop_of_true, ne.def] using hb, },
     { intros a h₁, dsimp, rw [dif_pos h₁],
       intro h₂, rw [if_pos], contrapose! h₂,