Normality tested on generators

Two criteria for a subgroup to be normal, each read off from a generating set.

A subgroup is normal as soon as its normalizer is everything, and the normalizer contains both the subgroup itself and anything centralising it. So a subgroup C that is centralised elementwise by a subgroup P with C ⊔ P = ⊤ is normal. Mathlib has each ingredient (Subgroup.normalizer_eq_top_iff, Subgroup.le_normalizer, Subgroup.centralizer_le_normalizer) but not this combination.

The subgroup generated by a set that is stable under conjugation is normal: every element of the group normalizes the subgroup as soon as it conjugates the generators into it (Subgroup.le_normalizer_closure_iff).

Main results

• TauCeti.normal_of_commute_of_sup_eq_top: a subgroup centralised elementwise by a subgroup that joins with it to the whole group is normal.
• Subgroup.closure_normal_of_forall_conj_mem: the subgroup generated by a conjugation-stable set is normal.

theorem TauCeti.normal_of_commute_of_sup_eq_top {G : Type u_1} [Group G] {C P : Subgroup G} (hcomm : ∀ c ∈ C, ∀ x ∈ P, Commute c x) (hsup : C ⊔ P = ⊤) : C.Normal

A subgroup centralised elementwise by a subgroup that joins with it to the whole group is normal.

The commutation hypothesis is elementwise rather than P ≤ centralizer C because that is the form a direct-product decomposition supplies; C ⊔ P = ⊤ is weaker than C and P being complements, which is what such a decomposition actually gives.

theorem Subgroup.closure_normal_of_forall_conj_mem {G : Type u_1} [Group G] {S : Set G} (h : ∀ (g s : G), s ∈ S → g * s * g⁻¹ ∈ S) : (closure S).Normal

The subgroup generated by a set that is stable under conjugation is normal.