feat(group_theory/subgroup): Normal Core (#8940)

Defines normal core, and proves lemmas analogous to those for normal closure.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/group_theory/group_action/basic.lean

@@ -5,9 +5,8 @@ Authors: Chris Hughes
 -/
 import group_theory.group_action.defs
 import group_theory.group_action.group
-import group_theory.coset
+import group_theory.quotient_group
 import data.setoid.basic
-import data.set_like.fintype
 import data.fintype.card
 
 /-!
@@ -465,3 +464,29 @@ lemma finset.smul_sum {r : α} {f : γ → β} {s : finset γ} :
 (distrib_mul_action.to_add_monoid_hom β r).map_sum f s
 
 end
+
+namespace subgroup
+
+variables {G : Type*} [group G] (H : subgroup G)
+
+lemma normal_core_eq_ker :
+  H.normal_core = (mul_action.to_perm_hom G (quotient_group.quotient H)).ker :=
+begin
+  refine le_antisymm (λ g hg, equiv.perm.ext (λ q, quotient_group.induction_on q
+    (λ g', (mul_action.quotient.smul_mk H g g').trans (quotient_group.eq.mpr _))))
+    (subgroup.normal_le_normal_core.mpr (λ g hg, _)),
+  { rw [mul_inv_rev, ←inv_inv g', inv_inv],
+    exact H.normal_core.inv_mem hg g'⁻¹ },
+  { rw [←H.inv_mem_iff, ←mul_one g⁻¹, ←quotient_group.eq, ←mul_one g],
+    exact (mul_action.quotient.smul_mk H g 1).symm.trans (equiv.perm.ext_iff.mp hg (1 : G)) },
+end
+
+noncomputable instance fintype_quotient_normal_core [fintype (quotient_group.quotient H)] :
+  fintype (quotient_group.quotient H.normal_core) :=
+begin
+  rw H.normal_core_eq_ker,
+  classical,
+  exact fintype.of_equiv _ (quotient_group.quotient_ker_equiv_range _).symm.to_equiv,
+end
+
+end subgroup

src/group_theory/subgroup.lean

@@ -1248,6 +1248,40 @@ by simp only [subset_normal_closure, closure_le]
 le_antisymm (normal_closure_le_normal closure_le_normal_closure)
   (normal_closure_mono subset_closure)
 
+/-- The normal core of a subgroup `H` is the largest normal subgroup of `G` contained in `H`,
+as shown by `subgroup.normal_core_eq_supr`. -/
+def normal_core (H : subgroup G) : subgroup G :=
+{ carrier := {a : G | ∀ b : G, b * a * b⁻¹ ∈ H},
+  one_mem' := λ a, by rw [mul_one, mul_inv_self]; exact H.one_mem,
+  inv_mem' := λ a h b, (congr_arg (∈ H) conj_inv).mp (H.inv_mem (h b)),
+  mul_mem' := λ a b ha hb c, (congr_arg (∈ H) conj_mul).mp (H.mul_mem (ha c) (hb c)) }
+
+lemma normal_core_le (H : subgroup G) : H.normal_core ≤ H :=
+λ a h, by { rw [←mul_one a, ←one_inv, ←one_mul a], exact h 1 }
+
+instance normal_core_normal (H : subgroup G) : H.normal_core.normal :=
+⟨λ a h b c, by rw [mul_assoc, mul_assoc, ←mul_inv_rev, ←mul_assoc, ←mul_assoc]; exact h (c * b)⟩
+
+lemma normal_le_normal_core {H : subgroup G} {N : subgroup G} [hN : N.normal] :
+  N ≤ H.normal_core ↔ N ≤ H :=
+⟨ge_trans H.normal_core_le, λ h_le n hn g, h_le (hN.conj_mem n hn g)⟩
+
+lemma normal_core_mono {H K : subgroup G} (h : H ≤ K) : H.normal_core ≤ K.normal_core :=
+normal_le_normal_core.mpr (H.normal_core_le.trans h)
+
+lemma normal_core_eq_supr (H : subgroup G) :
+  H.normal_core = ⨆ (N : subgroup G) [normal N] (hs : N ≤ H), N :=
+le_antisymm (le_supr_of_le H.normal_core
+  (le_supr_of_le H.normal_core_normal (le_supr_of_le H.normal_core_le le_rfl)))
+  (supr_le (λ N, supr_le (λ hN, supr_le (by exactI normal_le_normal_core.mpr))))
+
+@[simp] lemma normal_core_eq_self (H : subgroup G) [H.normal] : H.normal_core = H :=
+le_antisymm H.normal_core_le (normal_le_normal_core.mpr le_rfl)
+
+@[simp] theorem normal_core_idempotent (H : subgroup G) :
+  H.normal_core.normal_core = H.normal_core :=
+H.normal_core.normal_core_eq_self
+
 end subgroup
 namespace add_subgroup