orbitEquivQuotientStabilizer — Mathlib

English

There is a canonical equivalence between the orbit of an element and the quotient by its stabilizer.

Русский

Существует каноническое эквивалентность между орбитой элемента и фактор-множество по его стабилизатору.

LaTeX

$$$\\operatorname{orbit}(\\alpha,b) \\simeq G/\\operatorname{stabilizer}(\\alpha,b)$$$

Lean4

/-- **Orbit-stabilizer theorem**. -/
@[to_additive /-- Orbit-stabilizer theorem. -/
    ]
noncomputable def orbitEquivQuotientStabilizer (b : β) : orbit α b ≃ α ⧸ stabilizer α b :=
  Equiv.symm <|
    Equiv.ofBijective (fun g => ⟨ofQuotientStabilizer α b g, ofQuotientStabilizer_mem_orbit α b g⟩)
      ⟨fun x y hxy => injective_ofQuotientStabilizer α b (by convert congr_arg Subtype.val hxy), fun ⟨_, ⟨g, hgb⟩⟩ =>
        ⟨g, Subtype.eq hgb⟩⟩

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