English
The fixed points of the action of H on its left cosets correspond to a quotient of the normalizer by H.
Русский
Фиксированные точки действия H на левых смежных классах соответствуют нормализатору/H.
LaTeX
$$fixedPoints H (G/H) ≅ normalizer H / (comap ((normalizer H).subtype) H)$$
Lean4
theorem mem_fixedPoints_mul_left_cosets_iff_mem_normalizer {H : Subgroup G} [Finite (H : Set G)] {x : G} :
(x : G ⧸ H) ∈ MulAction.fixedPoints H (G ⧸ H) ↔ x ∈ normalizer H :=
⟨fun hx =>
have ha : ∀ {y : G ⧸ H}, y ∈ orbit H (x : G ⧸ H) → y = x := mem_fixedPoints'.1 hx _
(inv_mem_iff (G := G)).1
(mem_normalizer_fintype fun n (hn : n ∈ H) =>
have : (n⁻¹ * x)⁻¹ * x ∈ H := QuotientGroup.eq.1 (ha ⟨⟨n⁻¹, inv_mem hn⟩, rfl⟩)
show _ ∈ H by
rw [mul_inv_rev, inv_inv] at this
convert this
rw [inv_inv]),
fun hx : ∀ n : G, n ∈ H ↔ x * n * x⁻¹ ∈ H =>
mem_fixedPoints'.2 fun y =>
Quotient.inductionOn' y fun y hy =>
QuotientGroup.eq.2
(let ⟨⟨b, hb₁⟩, hb₂⟩ := hy
have hb₂ : (b * x)⁻¹ * y ∈ H := QuotientGroup.eq.1 hb₂
(inv_mem_iff (G := G)).1 <|
(hx _).2 <|
(mul_mem_cancel_left (inv_mem hb₁)).1 <| by rw [hx] at hb₂; simpa [mul_inv_rev, mul_assoc] using hb₂)⟩
