English
Let N be a normal subgroup of G and H a subgroup of the normalizer of N. Then there is a natural isomorphism H/(H ∩ N) ≅ (HN)/N.
Русский
Пусть N — нормальная подгруппа группы G, H — подгруппа нормализатора N. Тогда существует естественный изоморфизм H/(H ∩ N) ≅ (HN)/N.
LaTeX
$$$H \\backslash N \\cong (HN)/N$, with H ≤ N^{{\\rm normalizer}}$$
Lean4
/-- **Noether's second isomorphism theorem**: given a subgroup `N` of `G` and a
subgroup `H` of the normalizer of `N` in `G`,
defines an isomorphism between `H/(H ∩ N)` and `(HN)/N`. -/
@[to_additive /-- Noether's second isomorphism theorem: given a subgroup `N` of `G` and a
subgroup `H` of the normalizer of `N` in `G`,
defines an isomorphism between `H/(H ∩ N)` and `(H + N)/N` -/
]
noncomputable def quotientInfEquivProdNormalizerQuotient (H N : Subgroup G) (hLE : H ≤ N.normalizer) :
letI := Subgroup.normal_subgroupOf_of_le_normalizer hLE
letI := Subgroup.normal_subgroupOf_sup_of_le_normalizer hLE
H ⧸ N.subgroupOf H ≃* (H ⊔ N : Subgroup G) ⧸ N.subgroupOf (H ⊔ N) :=
letI := Subgroup.normal_subgroupOf_of_le_normalizer hLE
letI := Subgroup.normal_subgroupOf_sup_of_le_normalizer hLE
let φ : -- φ is the natural homomorphism H →* (HN)/N.
H →* _ ⧸ N.subgroupOf (H ⊔ N) := (mk' <| N.subgroupOf (H ⊔ N)).comp (inclusion le_sup_left)
have φ_surjective : Surjective φ := fun x =>
x.inductionOn' <| by
rintro ⟨y, hy : y ∈ (H ⊔ N)⟩
rw [← SetLike.mem_coe] at hy
rw [coe_mul_of_left_le_normalizer_right H N hLE] at hy
rcases hy with ⟨h, hh, n, hn, rfl⟩
use ⟨h, hh⟩
refine Quotient.eq.mpr ?_
change leftRel _ _ _
rw [leftRel_apply]
change h⁻¹ * (h * n) ∈ N
rwa [← mul_assoc, inv_mul_cancel, one_mul]
(quotientMulEquivOfEq (by simp [φ, ← comap_ker])).trans (quotientKerEquivOfSurjective φ φ_surjective)
