English
If H ≤ N.normalizer, then the underlying set of H ⊔ N equals H N as a product of subgroups.
Русский
Пусть H ≤ N.normalizer. Тогда множество-носитель H ⊔ N равно произведению H на N.
LaTeX
$$$\\uparrow (H\\lor N) = H N$$$
Lean4
/-- The carrier of `H ⊔ N` is just `↑H * ↑N` (pointwise set product)
when `H` is a subgroup of the normalizer of `N` in `G`. -/
@[to_additive /-- The carrier of `H ⊔ N` is just `↑H + ↑N` (pointwise set addition)
when `H` is a subgroup of the normalizer of `N` in `G`. -/
]
theorem coe_mul_of_left_le_normalizer_right (H N : Subgroup G) (hLE : H ≤ N.normalizer) : (↑(H ⊔ N) : Set G) = H * N :=
by
rw [sup_eq_closure_mul]
refine Set.Subset.antisymm (fun x hx => ?_) subset_closure
induction hx using closure_induction'' with
| one => exact ⟨1, one_mem _, 1, one_mem _, mul_one 1⟩
| mem _ hx => exact hx
| inv_mem x hx =>
obtain ⟨x, hx, y, hy, rfl⟩ := hx
simpa only [mul_inv_rev, mul_assoc, inv_inv, inv_mul_cancel_left] using
mul_mem_mul (inv_mem hx) ((mem_normalizer_iff.mp (hLE hx) y⁻¹).mp (inv_mem hy))
| mul x' x' _ _ hx hx' =>
obtain ⟨x, hx, y, hy, rfl⟩ := hx
obtain ⟨x', hx', y', hy', rfl⟩ := hx'
refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩
· exact (mem_normalizer_iff''.mp (hLE hx') y).mp hy
· simp only [mul_assoc, mul_inv_cancel_left]
