English
Let α act on α with a ∈ α. If (i) the only h ∈ H fixing a is h = 1, and (ii) for every g ∈ G there exists h ∈ H with h · g · a = a, then H and the stabilizer of a form a complement: IsComplement'(H, Stab_G(a)).
Русский
Пусть группа G действует на множестве α. Если (i) единственный элемент h ∈ H, фиксирующий a, равен 1, и (ii) для каждого g ∈ G существует h ∈ H such that h g действует на a как фиксация, то H и стабилизатор a образуют дополнение: IsComplement'(H, Stab_G(a)).
LaTeX
$$(∀ h ∈ H, h • a = a ⇒ h = 1) ∧ (∀ g ∈ G, ∃ h ∈ H, h • g • a = a) ⇒ IsComplement'(H, MulAction.stabilizer G a)$$
Lean4
theorem isComplement'_stabilizer {α : Type*} [MulAction G α] (a : α) (h1 : ∀ h : H, h • a = a → h = 1)
(h2 : ∀ g : G, ∃ h : H, h • g • a = a) : IsComplement' H (MulAction.stabilizer G a) :=
by
refine isComplement_iff_existsUnique.mpr fun g => ?_
obtain ⟨h, hh⟩ := h2 g
have hh' : (↑h * g) • a = a := by rwa [mul_smul]
refine ⟨⟨h⁻¹, h * g, hh'⟩, inv_mul_cancel_left (↑h) g, ?_⟩
rintro ⟨h', g, hg : g • a = a⟩ rfl
specialize h1 (h * h') (by rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg])
refine Prod.ext (eq_inv_of_mul_eq_one_right h1) (Subtype.ext ?_)
rwa [Subtype.ext_iff, coe_one, coe_mul, ← right_eq_mul, mul_assoc (↑h) (↑h') g] at h1
