feat(group_theory): add definition of solvable group (leanprover-comm…

…unity#5565)

Defines solvable groups using the definition that a group is solvable if its nth commutator is eventually trivial. Defines the nth commutator of a group and provides some lemmas for working with it. More facts about solvable groups will come in future PRs.

src/algebra/lie/basic.lean

@@ -3,6 +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 data.bracket
 import algebra.algebra.basic
 import linear_algebra.bilinear_form
 import linear_algebra.matrix
@@ -44,17 +45,6 @@ lie bracket, ring commutator, jacobi identity, lie ring, lie algebra
 
 universes u v w w₁ w₂
 
-/-- The has_bracket class has two intended uses:
-
-  1. for the product `⁅x, y⁆` of two elements `x`, `y` in a Lie algebra
-     (analogous to `has_mul` in the associative setting),
-
-  2. for the action `⁅x, m⁆` of an element `x` of a Lie algebra on an element `m` in one of its
-     modules (analogous to `has_scalar` in the associative setting). -/
-class has_bracket (L : Type v) (M : Type w) := (bracket : L → M → M)
-
-notation `⁅`x`,` y`⁆` := has_bracket.bracket x y
-
 /-- A Lie ring is an additive group with compatible product, known as the bracket, satisfying the
 Jacobi identity. The bracket is not associative unless it is identically zero. -/
 @[protect_proj] class lie_ring (L : Type v) extends add_comm_group L, has_bracket L L :=

src/data/bracket.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2021 Patrick Lutz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Lutz and Oliver Nash.
+-/
+
+/-!
+# Bracket Notation
+
+This file provides notation which can be used for the Lie bracket, for the commutator of two
+subgroups, and for other similar operations.
+
+## Main Definitions
+
+* `has_bracket L M` for a binary operation that takes something in `L` and something in `M` and
+produces something in `M`. Defining an instance of this structure gives access to the notation `⁅ ⁆`
+
+## Notation
+
+We introduce the notation `⁅x, y⁆` for the `bracket` of any `has_bracket` structure. Note that
+these are the Unicode "square with quill" brackets rather than the usual square brackets.
+-/
+
+/-- The has_bracket class has three intended uses:
+
+  1. for certain binary operations on structures, like the product `⁅x, y⁆` of two elements
+    `x`, `y` in a Lie algebra or the commutator of two elements `x` and `y` in a group.
+
+  2. for certain actions of one structure on another, like the action `⁅x, m⁆` of an element `x`
+    of a Lie algebra on an element `m` in one of its modules (analogous to `has_scalar` in the
+    associative setting).
+
+  3. for binary operations on substructures, like the commutator `⁅H, K⁆` of two subgroups `H` and
+     `K` of a group. -/
+class has_bracket (L M : Type*) := (bracket : L → M → M)
+
+notation `⁅`x`,` y`⁆` := has_bracket.bracket x y

src/group_theory/solvable.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2021 Jordan Brown, Thomas Browning and Patrick Lutz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jordan Brown, Thomas Browning and Patrick Lutz
+-/
+
+import group_theory.abelianization
+import data.bracket
+
+/-!
+# Solvable Groups
+
+In this file we introduce the notion of a solvable group. We define a solvable group as one whose
+derived series is eventually trivial. This requires defining the commutator of two subgroups and
+the derived series of a group.
+
+## Main definitions
+
+* `general_commutator H₁ H₂` : the commutator of the subgroups `H₁` and `H₂`
+* `derived_series G n` : the `n`th term in the derived series of `G`, defined by iterating
+  `general_commutator` starting with the top subgroup
+* `is_solvable G` : the group `G` is solvable
+-/
+
+open subgroup
+
+variables {G : Type*} [group G]
+
+section general_commutator
+
+/-- The commutator of two subgroups `H₁` and `H₂`. -/
+instance general_commutator : has_bracket (subgroup G) (subgroup G) :=
+⟨λ H₁ H₂, closure {x | ∃ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ = x}⟩
+
+lemma general_commutator_def (H₁ H₂ : subgroup G) :
+  ⁅H₁, H₂⁆ = closure {x | ∃ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ = x} := rfl
+
+instance general_commutator_normal (H₁ H₂ : subgroup G) [h₁ : H₁.normal]
+  [h₂ : H₂.normal] : normal ⁅H₁, H₂⁆ :=
+begin
+  let base : set G := {x | ∃ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ = x},
+  suffices h_base : base = group.conjugates_of_set base,
+  { dsimp only [general_commutator_def, ←base],
+    rw h_base,
+    exact subgroup.normal_closure_normal },
+  apply set.subset.antisymm group.subset_conjugates_of_set,
+  intros a h,
+  rw group.mem_conjugates_of_set_iff at h,
+  rcases h with ⟨b, ⟨c, hc, e, he, rfl⟩, d, rfl⟩,
+  exact ⟨d * c * d⁻¹, h₁.conj_mem c hc d, d * e * d⁻¹, h₂.conj_mem e he d, by group⟩,
+end
+
+lemma general_commutator_mono {H₁ H₂ K₁ K₂ : subgroup G} (h₁ : H₁ ≤ K₁) (h₂ : H₂ ≤ K₂) :
+  ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆ :=
+begin
+  apply closure_mono,
+  rintros x ⟨p, hp, q, hq, rfl⟩,
+  exact ⟨p, h₁ hp, q, h₂ hq, rfl⟩,
+end
+
+lemma general_commutator_def' (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :
+  ⁅H₁, H₂⁆ = normal_closure {x | ∃ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ = x} :=
+by rw [← normal_closure_eq_self ⁅H₁, H₂⁆, general_commutator_def,
+  normal_closure_closure_eq_normal_closure]
+
+lemma general_commutator_le (H₁ H₂ : subgroup G) (K : subgroup G) :
+  ⁅H₁, H₂⁆ ≤ K ↔ ∀ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ ∈ K :=
+begin
+  rw [general_commutator, closure_le],
+  split,
+  { intros h p hp q hq,
+    exact h ⟨p, hp, q, hq, rfl⟩, },
+  { rintros h x ⟨p, hp, q, hq, rfl⟩,
+    exact h p hp q hq, }
+end
+
+lemma general_commutator_comm (H₁ H₂ : subgroup G) : ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆ :=
+begin
+  suffices : ∀ H₁ H₂ : subgroup G, ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆, { exact le_antisymm (this _ _) (this _ _) },
+  intros H₁ H₂,
+  rw general_commutator_le,
+  intros p hp q hq,
+  have h : (p * q * p⁻¹ * q⁻¹)⁻¹ ∈ ⁅H₂, H₁⁆ := subset_closure ⟨q, hq, p, hp, by group⟩,
+  convert inv_mem ⁅H₂, H₁⁆ h,
+  group,
+end
+
+lemma general_commutator_le_right (H₁ H₂ : subgroup G) [h : normal H₂] :
+  ⁅H₁, H₂⁆ ≤ H₂ :=
+begin
+  rw general_commutator_le,
+  intros p hp q hq,
+  exact mul_mem H₂ (h.conj_mem q hq p) (inv_mem H₂ hq),
+end
+
+lemma general_commutator_le_left (H₁ H₂ : subgroup G) [h : normal H₁] :
+  ⁅H₁, H₂⁆ ≤ H₁ :=
+begin
+  rw general_commutator_comm,
+  exact general_commutator_le_right H₂ H₁,
+end
+
+@[simp] lemma general_commutator_bot (H : subgroup G) : ⁅H, ⊥⁆ = (⊥ : subgroup G) :=
+by { rw eq_bot_iff, exact general_commutator_le_right H ⊥ }
+
+@[simp] lemma bot_general_commutator (H : subgroup G) : ⁅(⊥ : subgroup G), H⁆ = (⊥ : subgroup G) :=
+by { rw eq_bot_iff, exact general_commutator_le_left ⊥ H }
+
+lemma general_commutator_le_inf (H₁ H₂ : subgroup G) [normal H₁] [normal H₂] :
+  ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂ :=
+by simp only [general_commutator_le_left, general_commutator_le_right, le_inf_iff, and_self]
+
+end general_commutator
+
+section derived_series
+
+variables (G)
+
+/-- The derived series of the group `G`, obtained by starting from the subgroup `⊤` and repeatedly
+  taking the commutator of the previous subgroup with itself for `n` times. -/
+def derived_series : ℕ → subgroup G
+| 0       := ⊤
+| (n + 1) := ⁅(derived_series n), (derived_series n)⁆
+
+@[simp] lemma derived_series_zero : derived_series G 0 = ⊤ := rfl
+
+@[simp] lemma derived_series_succ (n : ℕ) :
+  derived_series G (n + 1) = ⁅(derived_series G n), (derived_series G n)⁆ := rfl
+
+lemma derived_series_normal (n : ℕ) : (derived_series G n).normal :=
+begin
+  induction n with n ih,
+  { exact subgroup.top_normal, },
+  { rw derived_series_succ,
+    exactI general_commutator_normal (derived_series G n) (derived_series G n), }
+end
+
+@[simp] lemma general_commutator_eq_commutator :
+  ⁅(⊤ : subgroup G), (⊤ : subgroup G)⁆ = commutator G :=
+begin
+  rw [commutator, general_commutator_def'],
+  apply le_antisymm; apply normal_closure_mono,
+  { exact λ x ⟨p, _, q, _, h⟩, ⟨p, q, h⟩, },
+  { exact λ x ⟨p, q, h⟩, ⟨p, mem_top p, q, mem_top q, h⟩, }
+end
+
+lemma commutator_def' : commutator G = subgroup.closure {x : G | ∃ p q, p * q * p⁻¹ * q⁻¹ = x} :=
+begin
+  rw [← general_commutator_eq_commutator, general_commutator],
+  apply le_antisymm; apply closure_mono,
+  { exact λ x ⟨p, _, q, _, h⟩, ⟨p, q, h⟩ },
+  { exact λ x ⟨p, q, h⟩, ⟨p, mem_top p, q, mem_top q, h⟩ }
+end
+
+@[simp] lemma derived_series_one : derived_series G 1 = commutator G :=
+general_commutator_eq_commutator G
+
+end derived_series
+
+section solvable
+
+variables (G)
+
+/-- A group `G` is solvable if its derived series is eventually trivial. We use this definition
+  because it's the most convenient one to work with. -/
+class is_solvable : Prop :=
+(solvable : ∃ n : ℕ, derived_series G n = ⊥)
+
+@[priority 100]
+instance is_solvable_of_comm {G : Type*} [comm_group G] : is_solvable G :=
+begin
+  use 1,
+  rw [eq_bot_iff, derived_series_one],
+  calc commutator G ≤ (monoid_hom.id G).ker : abelianization.commutator_subset_ker (monoid_hom.id G)
+  ... = ⊥ : rfl,
+end
+
+end solvable

src/group_theory/subgroup.lean

@@ -932,6 +932,9 @@ subset_closure
 theorem subset_normal_closure : s ⊆ normal_closure s :=
 set.subset.trans subset_conjugates_of_set conjugates_of_set_subset_normal_closure
 
+theorem le_normal_closure {H : subgroup G} : H ≤ normal_closure ↑H :=
+λ _ h, subset_normal_closure h
+
 /-- The normal closure of `s` is a normal subgroup. -/
 instance normal_closure_normal : (normal_closure s).normal :=
 ⟨λ n h g,
@@ -970,6 +973,20 @@ le_antisymm
   (infi_le_of_le (normal_closure s) (infi_le_of_le (by apply_instance)
     (infi_le_of_le subset_normal_closure (le_refl _))))
 
+@[simp] theorem normal_closure_eq_self (H : subgroup G) [H.normal] : normal_closure ↑H = H :=
+le_antisymm (normal_closure_le_normal rfl.subset) (le_normal_closure)
+
+@[simp] theorem normal_closure_idempotent : normal_closure ↑(normal_closure s) = normal_closure s :=
+normal_closure_eq_self _
+
+theorem closure_le_normal_closure {s : set G} : closure s ≤ normal_closure s :=
+by simp only [subset_normal_closure, closure_le]
+
+@[simp] theorem normal_closure_closure_eq_normal_closure {s : set G} :
+  normal_closure ↑(closure s) = normal_closure s :=
+le_antisymm (normal_closure_le_normal closure_le_normal_closure)
+  (normal_closure_mono subset_closure)
+
 end subgroup
 namespace add_subgroup