feat(group_theory/solvable): S_5 is not solvable (#7453)

This is a rather hacky proof that S_5 is not solvable. The proper proof via the simplicity of A_5 will eventually replace this. But until then, this result is needed for abel-ruffini.

Most of the work done by Jordan Brown



Co-authored-by: Thomas Browning <tb65536@uw.edu>
Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/data/equiv/fintype.lean

@@ -17,7 +17,7 @@ sides of the equivalence are `fintype`s.
 
  - `function.embedding.to_equiv_range`: computably turn an embedding of a
    fintype into an `equiv` of the domain to its range
- - `equiv.perm.via_embedding : perm α → (α ↪ β) → perm β` extends the domain of
+ - `equiv.perm.via_fintype_embedding : perm α → (α ↪ β) → perm β` extends the domain of
    a permutation, fixing everything outside the range of the embedding
 
 # Implementation details
@@ -53,28 +53,30 @@ Extend the domain of `e : equiv.perm α`, mapping it through `f : α ↪ β`.
 Everything outside of `set.range f` is kept fixed. Has poor computational performance,
 due to exhaustive searching in constructed inverse due to using `function.embedding.to_equiv_range`.
 When a better `α ≃ set.range f` is known, use `equiv.perm.via_set_range`.
+When `[fintype α]` is not available, a noncomputable version is available as
+`equiv.perm.via_embedding`.
 -/
-def equiv.perm.via_embedding : equiv.perm β :=
+def equiv.perm.via_fintype_embedding : equiv.perm β :=
 e.extend_domain f.to_equiv_range
 
-@[simp] lemma equiv.perm.via_embedding_apply_image (a : α) :
-  e.via_embedding f (f a) = f (e a) :=
+@[simp] lemma equiv.perm.via_fintype_embedding_apply_image (a : α) :
+  e.via_fintype_embedding f (f a) = f (e a) :=
 begin
-  rw equiv.perm.via_embedding,
+  rw equiv.perm.via_fintype_embedding,
   convert equiv.perm.extend_domain_apply_image e _ _
 end
 
-lemma equiv.perm.via_embedding_apply_mem_range {b : β} (h : b ∈ set.range f) :
-  e.via_embedding f b = f (e (f.inv_of_mem_range ⟨b, h⟩)) :=
-by simpa [equiv.perm.via_embedding, equiv.perm.extend_domain_apply_subtype, h]
+lemma equiv.perm.via_fintype_embedding_apply_mem_range {b : β} (h : b ∈ set.range f) :
+  e.via_fintype_embedding f b = f (e (f.inv_of_mem_range ⟨b, h⟩)) :=
+by simpa [equiv.perm.via_fintype_embedding, equiv.perm.extend_domain_apply_subtype, h]
 
-lemma equiv.perm.via_embedding_apply_not_mem_range {b : β} (h : b ∉ set.range f) :
-  e.via_embedding f b = b :=
-by rwa [equiv.perm.via_embedding, equiv.perm.extend_domain_apply_not_subtype]
+lemma equiv.perm.via_fintype_embedding_apply_not_mem_range {b : β} (h : b ∉ set.range f) :
+  e.via_fintype_embedding f b = b :=
+by rwa [equiv.perm.via_fintype_embedding, equiv.perm.extend_domain_apply_not_subtype]
 
-@[simp] lemma equiv.perm.via_embedding_sign [decidable_eq α] [fintype β] :
-  equiv.perm.sign (e.via_embedding f) = equiv.perm.sign e :=
-by simp [equiv.perm.via_embedding]
+@[simp] lemma equiv.perm.via_fintype_embedding_sign [decidable_eq α] [fintype β] :
+  equiv.perm.sign (e.via_fintype_embedding f) = equiv.perm.sign e :=
+by simp [equiv.perm.via_fintype_embedding]
 
 namespace equiv
 variables {p q : α → Prop} [decidable_pred p] [decidable_pred q]

src/group_theory/perm/basic.lean

@@ -15,7 +15,7 @@ universes u v
 
 namespace equiv
 
-variables {α : Type u}
+variables {α : Type u} {β : Type v}
 
 namespace perm
 
@@ -185,7 +185,7 @@ section extend_domain
 
 /-! Lemmas about `equiv.perm.extend_domain` re-expressed via the group structure. -/
 
-variables {β : Type*} (e : perm α) {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p)
+variables (e : perm α) {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p)
 
 @[simp] lemma extend_domain_one : extend_domain 1 f = 1 :=
 extend_domain_refl f
@@ -196,6 +196,16 @@ extend_domain_refl f
   (e.extend_domain f) * (e'.extend_domain f) = (e * e').extend_domain f :=
 extend_domain_trans _ _ _
 
+/-- `extend_domain` as a group homomorphism -/
+@[simps] def extend_domain_hom : perm α →* perm β :=
+{ to_fun := λ e, extend_domain e f,
+  map_one' := extend_domain_one f,
+  map_mul' := λ e e', (extend_domain_mul f e e').symm }
+
+lemma extend_domain_hom_injective : function.injective (extend_domain_hom f) :=
+((extend_domain_hom f).injective_iff).mpr (λ e he, ext (λ x, f.injective (subtype.ext
+  ((extend_domain_apply_image e f x).symm.trans (ext_iff.mp he (f x))))))
+
 end extend_domain
 
 /-- If the permutation `f` fixes the subtype `{x // p x}`, then this returns the permutation
@@ -249,6 +259,15 @@ lemma of_subtype_apply_of_not_mem {p : α → Prop} [decidable_pred p]
   of_subtype f x = x :=
 dif_neg hx
 
+lemma of_subtype_apply_coe {p : α → Prop} [decidable_pred p]
+  (f : perm (subtype p)) (x : subtype p) :
+  of_subtype f ↑x = ↑(f x) :=
+begin
+  change dite _ _ _ = _,
+  rw [dif_pos, subtype.coe_eta],
+  exact x.2,
+end
+
 lemma mem_iff_of_subtype_apply_mem {p : α → Prop} [decidable_pred p]
   (f : perm (subtype p)) (x : α) :
   p x ↔ p ((of_subtype f : α → α) x) :=
@@ -267,6 +286,30 @@ instance perm_unique {n : Type*} [unique n] : unique (equiv.perm n) :=
 
 @[simp] lemma default_perm {n : Type*} : default (equiv.perm n) = 1 := rfl
 
+variables (e : perm α) (ι : α ↪ β)
+
+open_locale classical
+
+/-- Noncomputable version of `equiv.perm.via_fintype_embedding` that does not assume `fintype` -/
+noncomputable def via_embedding : perm β :=
+extend_domain e (of_injective ι.1 ι.2)
+
+lemma via_embedding_apply (x : α) : e.via_embedding ι (ι x) = ι (e x) :=
+extend_domain_apply_image e (of_injective ι.1 ι.2) x
+
+lemma via_embedding_apply_of_not_mem (x : β) (hx : x ∉ _root_.set.range ι) :
+  e.via_embedding ι x = x :=
+extend_domain_apply_not_subtype e (of_injective ι.1 ι.2) hx
+
+/-- `via_embedding` as a group homomorphism -/
+noncomputable def via_embedding_hom : perm α →* perm β:=
+extend_domain_hom (of_injective ι.1 ι.2)
+
+lemma via_embedding_hom_apply : via_embedding_hom ι e = via_embedding e ι := rfl
+
+lemma via_embedding_hom_injective : function.injective (via_embedding_hom ι) :=
+extend_domain_hom_injective (of_injective ι.1 ι.2)
+
 end perm
 
 section swap

src/group_theory/perm/fin.lean

@@ -108,7 +108,7 @@ lemma cycle_range_of_gt {n : ℕ} {i j : fin n.succ} (h : i < j) :
 begin
   rw [cycle_range, of_left_inverse'_eq_of_injective,
       ←function.embedding.to_equiv_range_eq_of_injective,
-      ←via_embedding, via_embedding_apply_not_mem_range],
+      ←via_fintype_embedding, via_fintype_embedding_apply_not_mem_range],
   simpa
 end
 
@@ -125,7 +125,7 @@ begin
   ext,
   rw [this, cycle_range, of_left_inverse'_eq_of_injective,
       ←function.embedding.to_equiv_range_eq_of_injective,
-      ←via_embedding, via_embedding_apply_image, rel_embedding.coe_fn_to_embedding,
+      ←via_fintype_embedding, via_fintype_embedding_apply_image, rel_embedding.coe_fn_to_embedding,
       coe_cast_le, coe_fin_rotate],
   simp only [fin.ext_iff, coe_last, coe_mk, coe_zero, fin.eta, apply_ite coe, cast_le_mk],
   split_ifs with heq,

src/group_theory/solvable.lean

@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jordan Brown, Thomas Browning, Patrick Lutz
 -/
 
-import group_theory.abelianization
 import data.bracket
+import data.matrix.notation
+import group_theory.abelianization
+import set_theory.cardinal
 
 /-!
 # Solvable Groups
@@ -24,7 +26,7 @@ the derived series of a group.
 
 open subgroup
 
-variables {G : Type*} [group G]
+variables {G G' : Type*} [group G] [group G'] {f : G →* G'}
 
 section general_commutator
 
@@ -74,6 +76,10 @@ begin
     exact h p hp q hq, }
 end
 
+lemma general_commutator_containment (H₁ H₂ : subgroup G) {p q : G} (hp : p ∈ H₁) (hq : q ∈ H₂) :
+  p * q * p⁻¹ * q⁻¹ ∈ ⁅H₁, H₂⁆ :=
+(general_commutator_le H₁ H₂ ⁅H₁, H₂⁆).mp (le_refl ⁅H₁, H₂⁆) p hp q hq
+
 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 _ _) },
@@ -159,8 +165,6 @@ end derived_series
 
 section commutator_map
 
-variables {G} {G' : Type*} [group G'] {f : G →* G'}
-
 lemma map_commutator_eq_commutator_map (H₁ H₂ : subgroup G) :
   ⁅H₁, H₂⁆.map f = ⁅H₁.map f, H₂.map f⁆ :=
 begin
@@ -243,7 +247,7 @@ lemma is_solvable_of_top_eq_bot (h : (⊤ : subgroup G) = ⊥) : is_solvable G :
 instance is_solvable_of_subsingleton [subsingleton G] : is_solvable G :=
 is_solvable_of_top_eq_bot G (by ext; simp at *)
 
-variables {G} {G' : Type*} [group G'] {f : G →* G'}
+variables {G}
 
 lemma solvable_of_solvable_injective (hf : function.injective f) [h : is_solvable G'] :
   is_solvable G :=
@@ -331,3 +335,39 @@ lemma is_simple_group.comm_iff_is_solvable :
 end⟩
 
 end is_simple_group
+
+section perm_not_solvable
+
+lemma not_solvable_of_mem_derived_series {g : G} (h1 : g ≠ 1)
+  (h2 : ∀ n : ℕ, g ∈ derived_series G n) : ¬ is_solvable G :=
+mt (is_solvable_def _).mp (not_exists_of_forall_not
+  (λ n h, h1 (subgroup.mem_bot.mp ((congr_arg (has_mem.mem g) h).mp (h2 n)))))
+
+lemma equiv.perm.fin_5_not_solvable : ¬ is_solvable (equiv.perm (fin 5)) :=
+begin
+  let x : equiv.perm (fin 5) := ⟨![1, 2, 0, 3, 4], ![2, 0, 1, 3, 4], dec_trivial, dec_trivial⟩,
+  let y : equiv.perm (fin 5) := ⟨![3, 4, 2, 0, 1], ![3, 4, 2, 0, 1], dec_trivial, dec_trivial⟩,
+  let z : equiv.perm (fin 5) := ⟨![0, 3, 2, 1, 4], ![0, 3, 2, 1, 4], dec_trivial, dec_trivial⟩,
+  have x_ne_one : x ≠ 1, { rw [ne.def, equiv.ext_iff], dec_trivial },
+  have key : x = z * (x * (y * x * y⁻¹) * x⁻¹ * (y * x * y⁻¹)⁻¹) * z⁻¹,
+  { ext a, dec_trivial! },
+  refine not_solvable_of_mem_derived_series x_ne_one (λ n, _),
+  induction n with n ih,
+  { exact mem_top x },
+  { rw key,
+    exact (derived_series_normal _ _).conj_mem _
+      (general_commutator_containment _ _ ih ((derived_series_normal _ _).conj_mem _ ih _)) _ },
+end
+
+lemma equiv.perm.not_solvable (X : Type*) (hX : 5 ≤ cardinal.mk X) :
+  ¬ is_solvable (equiv.perm X) :=
+begin
+  introI h,
+  have key : nonempty (fin 5 ↪ X),
+  { rwa [←cardinal.lift_mk_le, cardinal.mk_fin, cardinal.lift_nat_cast,
+    nat.cast_bit1, nat.cast_bit0, nat.cast_one, cardinal.lift_id] },
+  exact equiv.perm.fin_5_not_solvable (solvable_of_solvable_injective
+    (equiv.perm.via_embedding_hom_injective (nonempty.some key))),
+end
+
+end perm_not_solvable