stabilizerEquivStabilizerOfOrbitRel

English

If a and b are related by orbitRel G α, there is a canonical isomorphism between stabilizers of a and b, obtained from transporting along the chosen orbit relation.

Русский

Если элементы a и b связаны отношением орбиты, существует естественное изоморождение стабилизаторов stabilizer_G(a) и stabilizer_G(b).

LaTeX

$$$\\forall a,b,\\; (\\text{orbitRel } G \\; \\alpha\\; a\\; b) \\Rightarrow \\mathrm{stabilizer}_G(a) \\cong_* \\mathrm{stabilizer}_G(b)$.$$

Lean4

/-- A bijection between the stabilizers of two elements in the same orbit. -/
noncomputable def stabilizerEquivStabilizerOfOrbitRel (h : orbitRel G α a b) : stabilizer G a ≃* stabilizer G b :=
  (stabilizerEquivStabilizer (Classical.choose_spec h).symm).symm

Похожие утверждения