selfEquivOrbitsQuotientProd — Mathlib

English

A refinement: under LeftInverse φ and freeness, there is an equivalence β ≃ Σ ω, α / Stab(ω.out) ≃ β

Русский

При наличии левой обратной φ и свободы действия существует эквивалентность β с разбивкой по орбитам.

LaTeX

$$selfEquivOrbitsQuotientProd' hφ h ≃ β ≃ Σ ω : Ω, α$$

Lean4

/-- If `α` acts freely on `β`, `β` is equivalent to the product of the quotient of `β` by `α` and
`α`. -/
@[to_additive selfEquivOrbitsQuotientProd /--
    If `α` acts freely on `β`, `β` is equivalent to the product of the quotient of `β` by
    `α` and `α`. -/
    ]
noncomputable def selfEquivOrbitsQuotientProd (h : ∀ b : β, MulAction.stabilizer α b = ⊥) :
    β ≃ Quotient (MulAction.orbitRel α β) × α :=
  MulAction.selfEquivOrbitsQuotientProd' Quotient.out_eq' h

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