English
There is a correspondence between blocks containing a and subgroups containing the stabilizer of a, forming an order isomorphism between these structures.
Русский
Установлено взаимное соответствие между блоками, содержащими a, и подгруппами, содержащими стабилизатор a, образующее порядковое изоморфизм.
LaTeX
$$$\\text{block_stabilizerOrderIso}(a) : {B\\subset X | a\\in B \\wedge IsBlock G B} \\cong_o \\{H \\le G : *\\}$$$
Lean4
/-- A subgroup containing the stabilizer of `a`
is the stabilizer of the orbit of `a` under that subgroup -/
@[to_additive /-- A subgroup containing the stabilizer of `a`
is the stabilizer of the orbit of `a` under that subgroup -/
]
theorem stabilizer_orbit_eq {a : X} {H : Subgroup G} (hH : stabilizer G a ≤ H) : stabilizer G (orbit H a) = H :=
by
ext g
constructor
· intro hg
obtain ⟨-, ⟨b, rfl⟩, h⟩ := hg.symm ▸ mem_orbit_self a
simp_rw [H.toSubmonoid.smul_def, ← mul_smul, ← mem_stabilizer_iff] at h
exact (mul_mem_cancel_right b.2).mp (hH h)
· intro hg
rw [mem_stabilizer_iff, ← Subgroup.coe_mk H g hg, ← Submonoid.smul_def (S := H.toSubmonoid)]
apply smul_orbit (G := H)
