feat(group_theory/{subgroup, order_of_element}): refactors simple groups, classifies finite simple abelian/solvable groups (#6926)

Refactors the deprecated `simple_group` to a new `is_simple_group`
Shows that all cyclic groups of prime order are simple
Shows that all simple `comm_group`s are cyclic
Shows that all simple finite `comm_group`s have prime order
Shows that a simple group is solvable iff it is commutative

Author: awainverse

src/deprecated/subgroup.lean

@@ -659,54 +659,7 @@ theorem normal_closure_mono {s t : set G} : s ⊆ t → normal_closure s ⊆ nor
 
 end group
 
-section simple_group
-
-class simple_group (G : Type*) [group G] : Prop :=
-(simple : ∀ (N : set G) [normal_subgroup N], N = is_subgroup.trivial G ∨ N = set.univ)
-
-class simple_add_group (A : Type*) [add_group A] : Prop :=
-(simple : ∀ (N : set A) [normal_add_subgroup N], N = is_add_subgroup.trivial A ∨ N = set.univ)
-
-attribute [to_additive] simple_group
-
-theorem additive.simple_add_group_iff [group G] :
-  simple_add_group (additive G) ↔ simple_group G :=
-⟨λ hs, ⟨λ N h, @simple_add_group.simple _ _ hs _ (by exactI additive.normal_add_subgroup_iff.2 h)⟩,
-  λ hs, ⟨λ N h, @simple_group.simple _ _ hs _ (by exactI additive.normal_add_subgroup_iff.1 h)⟩⟩
-
-instance additive.simple_add_group [group G] [simple_group G] :
-  simple_add_group (additive G) := additive.simple_add_group_iff.2 (by apply_instance)
-
-theorem multiplicative.simple_group_iff [add_group A] :
-  simple_group (multiplicative A) ↔ simple_add_group A :=
-⟨λ hs, ⟨λ N h, @simple_group.simple _ _ hs _ (by exactI multiplicative.normal_subgroup_iff.2 h)⟩,
-  λ hs, ⟨λ N h,
-          @simple_add_group.simple _ _ hs _ (by exactI multiplicative.normal_subgroup_iff.1 h)⟩⟩
-
-instance multiplicative.simple_group [add_group A] [simple_add_group A] :
-simple_group (multiplicative A) := multiplicative.simple_group_iff.2 (by apply_instance)
-
-@[to_additive]
-lemma simple_group_of_surjective [group G] [group H] [simple_group G] (f : G → H)
-  [is_group_hom f] (hf : function.surjective f) : simple_group H :=
-⟨λ H iH, have normal_subgroup (f ⁻¹' H), by resetI; apply_instance,
-  begin
-    resetI,
-    cases simple_group.simple (f ⁻¹' H) with h h,
-    { refine or.inl (is_subgroup.eq_trivial_iff.2 (λ x hx, _)),
-      cases hf x with y hy,
-      rw ← hy at hx,
-      rw [← hy, is_subgroup.eq_trivial_iff.1 h y hx, is_group_hom.map_one f] },
-    { refine or.inr (set.eq_univ_of_forall (λ x, _)),
-      cases hf x with y hy,
-      rw set.eq_univ_iff_forall at h,
-      rw ← hy,
-      exact h y }
-  end⟩
-
-end simple_group
-
-/-- Create a bundled subgroup from a set `s` and `[is_subroup s]`. -/
+/-- Create a bundled subgroup from a set `s` and `[is_subgroup s]`. -/
 @[to_additive "Create a bundled additive subgroup from a set `s` and `[is_add_subgroup s]`."]
 def subgroup.of [group G] (s : set G) [h : is_subgroup s] : subgroup G :=
 { carrier := s,

src/group_theory/order_of_element.lean

@@ -23,7 +23,9 @@ This file defines the order of an element of a finite group. For a finite group
 
 ## Main statements
 
-`is_cyclic_of_prime_card` proves that a finite group of prime order is cyclic.
+* `is_cyclic_of_prime_card` proves that a finite group of prime order is cyclic.
+* `is_simple_group_of_prime_card`, `is_simple_group.is_cyclic`,
+  and `is_simple_group.prime_card` classify finite simple abelian groups.
 
 ## Implementation details
 
@@ -539,6 +541,10 @@ open subgroup
 class is_cyclic (α : Type u) [group α] : Prop :=
 (exists_generator [] : ∃ g : α, ∀ x, x ∈ gpowers g)
 
+@[priority 100]
+instance is_cyclic_of_subsingleton [group α] [subsingleton α] : is_cyclic α :=
+⟨⟨1, λ x, by { rw subsingleton.elim x 1, exact mem_gpowers 1 }⟩⟩
+
 /-- A cyclic group is always commutative. This is not an `instance` because often we have a better
 proof of `comm_group`. -/
 def is_cyclic.comm_group [hg : group α] [is_cyclic α] : comm_group α :=
@@ -826,4 +832,81 @@ begin
   apply card_order_of_eq_totient_aux₂ (λ n, is_cyclic.card_pow_eq_one_le) hd
 end
 
+/-- A finite group of prime order is simple. -/
+lemma is_simple_group_of_prime_card {α : Type u} [group α] [fintype α] {p : ℕ} [hp : fact p.prime]
+  (h : fintype.card α = p) : is_simple_group α :=
+⟨begin
+  have h' := nat.prime.one_lt (fact.out p.prime),
+  rw ← h at h',
+  haveI := fintype.one_lt_card_iff_nontrivial.1 h',
+  apply exists_pair_ne α,
+end, λ H Hn, begin
+  classical,
+  have hcard := card_subgroup_dvd_card H,
+  rw [h, dvd_prime (fact.out p.prime)] at hcard,
+  refine hcard.imp (λ h1, _) (λ hp, _),
+  { haveI := fintype.card_le_one_iff_subsingleton.1 (le_of_eq h1),
+    apply eq_bot_of_subsingleton },
+  { exact eq_top_of_card_eq _ (hp.trans h.symm) }
+end⟩
+
 end cyclic
+
+namespace is_simple_group
+
+section comm_group
+variables [comm_group α] [is_simple_group α]
+
+@[priority 100]
+instance : is_cyclic α :=
+begin
+  cases subsingleton_or_nontrivial α with hi hi; haveI := hi,
+  { apply is_cyclic_of_subsingleton },
+  { obtain ⟨g, hg⟩ := exists_ne (1 : α),
+    refine ⟨⟨g, λ x, _⟩⟩,
+    cases is_simple_lattice.eq_bot_or_eq_top (subgroup.gpowers g) with hb ht,
+    { exfalso,
+      apply hg,
+      rw [← subgroup.mem_bot, ← hb],
+      apply subgroup.mem_gpowers },
+    { rw ht,
+      apply subgroup.mem_top } }
+end
+
+theorem prime_card [fintype α] : (fintype.card α).prime :=
+begin
+  have h0 : 0 < fintype.card α := fintype.card_pos_iff.2 (by apply_instance),
+  obtain ⟨g, hg⟩ := is_cyclic.exists_generator α,
+  refine ⟨fintype.one_lt_card_iff_nontrivial.2 infer_instance, λ n hn, _⟩,
+  refine (is_simple_lattice.eq_bot_or_eq_top (subgroup.gpowers (g ^ n))).symm.imp _ _,
+  { intro h,
+    have hgo := order_of_pow g,
+    rw [order_of_eq_card_of_forall_mem_gpowers hg, nat.gcd_eq_right_iff_dvd.1 hn,
+      order_of_eq_card_of_forall_mem_gpowers, eq_comm,
+      nat.div_eq_iff_eq_mul_left (nat.pos_of_dvd_of_pos hn h0) hn] at hgo,
+    { exact (mul_left_cancel' (ne_of_gt h0) ((mul_one (fintype.card α)).trans hgo)).symm },
+    { intro x,
+      rw h,
+      exact subgroup.mem_top _ } },
+  { intro h,
+    apply le_antisymm (nat.le_of_dvd h0 hn),
+    rw ← order_of_eq_card_of_forall_mem_gpowers hg,
+    apply order_of_le_of_pow_eq_one (nat.pos_of_dvd_of_pos hn h0),
+    rw [← subgroup.mem_bot, ← h],
+    exact subgroup.mem_gpowers _ }
+end
+
+end comm_group
+
+end is_simple_group
+
+theorem comm_group.is_simple_iff_is_cyclic_and_prime_card [fintype α] [comm_group α] :
+  is_simple_group α ↔ is_cyclic α ∧ (fintype.card α).prime :=
+begin
+  split,
+  { introI h,
+    exact ⟨is_simple_group.is_cyclic, is_simple_group.prime_card⟩ },
+  { rintro ⟨hc, hp⟩,
+    haveI : fact (fintype.card α).prime := ⟨hp⟩,
+    exact is_simple_group_of_prime_card rfl }
+end

src/group_theory/solvable.lean

@@ -302,3 +302,32 @@ solvable_of_ker_le_range (monoid_hom.inl G G') (monoid_hom.snd G G')
   (λ x hx, ⟨x.1, prod.ext rfl hx.symm⟩)
 
 end solvable
+
+section is_simple_group
+
+variable [is_simple_group G]
+
+lemma is_simple_group.derived_series_succ {n : ℕ} : derived_series G n.succ = commutator G :=
+begin
+  induction n with n ih,
+  { exact derived_series_one _ },
+  rw [derived_series_succ, ih],
+  cases (commutator.normal G).eq_bot_or_eq_top with h h; simp [h]
+end
+
+lemma is_simple_group.comm_iff_is_solvable :
+  (∀ a b : G, a * b = b * a) ↔ is_solvable G :=
+⟨is_solvable_of_comm, λ ⟨⟨n, hn⟩⟩, begin
+  cases n,
+  { rw derived_series_zero at hn,
+    intros a b,
+    refine (mem_bot.1 _).trans (mem_bot.1 _).symm;
+    { rw ← hn,
+      exact mem_top _ } },
+  { rw is_simple_group.derived_series_succ at hn,
+    intros a b,
+    rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn],
+    exact subset_normal_closure ⟨a, b, rfl⟩ }
+end⟩
+
+end is_simple_group

src/group_theory/subgroup.lean

@@ -6,7 +6,7 @@ Authors: Kexing Ying
 import group_theory.submonoid
 import algebra.group.conj
 import algebra.pointwise
-import order.modular_lattice
+import order.atoms
 
 /-!
 # Subgroups
@@ -70,6 +70,8 @@ Definitions in the file:
 * `monoid_hom.eq_locus f g` : given group homomorphisms `f`, `g`, the elements of `G` such that
   `f x = g x` form a subgroup of `G`
 
+* `is_simple_group G` : a class indicating that a group has exactly two normal subgroups
+
 ## Implementation notes
 
 Subgroup inclusion is denoted `≤` rather than `⊆`, although `∈` is defined as
@@ -162,8 +164,8 @@ attribute [norm_cast] add_subgroup.mem_coe
 attribute [norm_cast] add_subgroup.coe_coe
 
 @[to_additive]
-instance (K : subgroup G) [d : decidable_pred K.carrier] [fintype G] : fintype K :=
-show fintype {g : G // g ∈ K.carrier}, from infer_instance
+instance (K : subgroup G) [d : decidable_pred (∈ K)] [fintype G] : fintype K :=
+show fintype {g : G // g ∈ K}, from infer_instance
 
 end subgroup
 
@@ -387,6 +389,13 @@ instance : inhabited (subgroup G) := ⟨⊥⟩
 by simp only [subgroup.ext'_iff, coe_bot, set.eq_singleton_iff_unique_mem, mem_coe, H.one_mem,
   true_and]
 
+@[to_additive] lemma eq_bot_of_subsingleton [subsingleton H] : H = ⊥ :=
+begin
+  rw subgroup.eq_bot_iff_forall,
+  intros y hy,
+  rw [← subgroup.coe_mk H y hy, subsingleton.elim (⟨y, hy⟩ : H) 1, subgroup.coe_one],
+end
+
 @[to_additive] lemma eq_top_of_card_eq [fintype H] [fintype G]
   (h : fintype.card H = fintype.card G) : H = ⊤ :=
 begin
@@ -1454,6 +1463,55 @@ end⟩
 
 end subgroup
 
+section
+variables (G) (A)
+
+/-- A `group` is simple when it has exactly two normal `subgroup`s. -/
+class is_simple_group extends nontrivial G : Prop :=
+(eq_bot_or_eq_top_of_normal : ∀ H : subgroup G, H.normal → H = ⊥ ∨ H = ⊤)
+
+/-- An `add_group` is simple when it has exactly two normal `add_subgroup`s. -/
+class is_simple_add_group extends nontrivial A : Prop :=
+(eq_bot_or_eq_top_of_normal : ∀ H : add_subgroup A, H.normal → H = ⊥ ∨ H = ⊤)
+
+attribute [to_additive] is_simple_group
+
+variables {G} {A}
+
+@[to_additive]
+lemma subgroup.normal.eq_bot_or_eq_top [is_simple_group G] {H : subgroup G} (Hn : H.normal) :
+  H = ⊥ ∨ H = ⊤ :=
+is_simple_group.eq_bot_or_eq_top_of_normal H Hn
+
+namespace is_simple_group
+
+@[to_additive]
+instance {C : Type*} [comm_group C] [is_simple_group C] :
+  is_simple_lattice (subgroup C) :=
+⟨λ H, H.normal_of_comm.eq_bot_or_eq_top⟩
+
+@[to_additive]
+lemma is_simple_group_of_surjective {H : Type*} [group H] [is_simple_group G]
+  [nontrivial H] (f : G →* H) (hf : function.surjective f) :
+  is_simple_group H :=
+⟨nontrivial.exists_pair_ne, λ H iH, begin
+  refine ((iH.comap f).eq_bot_or_eq_top).imp (λ h, _) (λ h, _),
+  { rw subgroup.eq_bot_iff_forall at *,
+    simp_rw subgroup.mem_comap at h,
+    intros x hx,
+    obtain ⟨y, hy⟩ := hf x,
+    rw ← hy at hx,
+    rw h y hx at hy,
+    rw [← hy, f.map_one] },
+  { rw [← top_le_iff, ← subgroup.map_le_iff_le_comap, ← monoid_hom.range_eq_map,
+      monoid_hom.range_top_of_surjective f hf, top_le_iff] at h,
+    exact h }
+end⟩
+
+end is_simple_group
+
+end
+
 section pointwise
 
 namespace subgroup