feat(group_theory/commutator): The commutator subgroup is characteris…

…tic (#13255)

This PR adds instances stating that the commutator subgroup is characteristic.

src/group_theory/abelianization.lean

@@ -43,6 +43,9 @@ lemma commutator_eq_normal_closure :
   commutator G = subgroup.normal_closure {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g} :=
 by simp_rw [commutator, subgroup.commutator_def', subgroup.mem_top, exists_true_left]
 
+instance commutator_characteristic : (commutator G).characteristic :=
+subgroup.commutator_characteristic ⊤ ⊤
+
 lemma commutator_centralizer_commutator_le_center :
   ⁅(commutator G).centralizer, (commutator G).centralizer⁆ ≤ subgroup.center G :=
 begin

src/group_theory/commutator.lean

@@ -145,6 +145,19 @@ begin
     exact mem_map_of_mem _ (commutator_mem_commutator hp hq) }
 end
 
+variables {H₁ H₂}
+
+lemma commutator_le_map_commutator {f : G →* G'} {K₁ K₂ : subgroup G'}
+  (h₁ : K₁ ≤ H₁.map f) (h₂ : K₂ ≤ H₂.map f) : ⁅K₁, K₂⁆ ≤ ⁅H₁, H₂⁆.map f :=
+(commutator_mono h₁ h₂).trans (ge_of_eq (map_commutator H₁ H₂ f))
+
+variables (H₁ H₂)
+
+instance commutator_characteristic [h₁ : characteristic H₁] [h₂ : characteristic H₂] :
+  characteristic ⁅H₁, H₂⁆ :=
+characteristic_iff_le_map.mpr (λ ϕ, commutator_le_map_commutator
+  (characteristic_iff_le_map.mp h₁ ϕ) (characteristic_iff_le_map.mp h₂ ϕ))
+
 lemma commutator_prod_prod (K₁ K₂ : subgroup G') :
   ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ :=
 begin
@@ -159,12 +172,6 @@ begin
         monoid_hom.fst_comp_inr, monoid_hom.snd_comp_inr ], }, }
 end
 
-variables {H₁ H₂}
-
-lemma commutator_le_map_commutator {f : G →* G'} {K₁ K₂ : subgroup G'}
-  (h₁ : K₁ ≤ H₁.map f) (h₂ : K₂ ≤ H₂.map f) : ⁅K₁, K₂⁆ ≤ ⁅H₁, H₂⁆.map f :=
-(commutator_mono h₁ h₂).trans (ge_of_eq (map_commutator H₁ H₂ f))
-
 /-- The commutator of direct product is contained in the direct product of the commutators.
 
 See `commutator_pi_pi_of_fintype` for equality given `fintype η`.