orbitProdStabilizerEquivGroup — Mathlib

English

There is an equivalence between the product of the orbit with the stabilizer and the group, linking orbit and stabilizer data.

Русский

Существует эквивалентность между произведением орбиты и стабилизатора и группой, связывающая данные об орбите и стабилизаторе.

LaTeX

$$$\\operatorname{orbitProdStabilizerEquivGroup}(b) : \\operatorname{orbit}(\\alpha,b) \\times \\operatorname{stabilizer}(\\alpha,b) \\simeq \\alpha$$$

Lean4

/-- Orbit-stabilizer theorem. -/
@[to_additive AddAction.orbitProdStabilizerEquivAddGroup /-- Orbit-stabilizer theorem. -/
    ]
noncomputable def orbitProdStabilizerEquivGroup (b : β) : orbit α b × stabilizer α b ≃ α :=
  (Equiv.prodCongr (orbitEquivQuotientStabilizer α _) (Equiv.refl _)).trans Subgroup.groupEquivQuotientProdSubgroup.symm

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