English
If a group acts freely on β, there is a canonical equivalence between β and the product of the orbit set with α, i.e., β ≃ Ω × α.
Русский
При свободном действии β имеется каноническое эквивалентство β ≃ Ω × α.
LaTeX
$$β ≃ Ω × α$$
Lean4
/-- If `α` acts on `β` with trivial stabilizers, `β` is equivalent
to the product of the quotient of `β` by `α` and `α`.
See `MulAction.selfEquivOrbitsQuotientProd` with `φ = Quotient.out`. -/
@[to_additive selfEquivOrbitsQuotientProd' /-- If `α` acts freely on `β`, `β` is equivalent
to the product of the quotient of `β` by `α` and `α`.
See `AddAction.selfEquivOrbitsQuotientProd` with `φ = Quotient.out`. -/
]
noncomputable def selfEquivOrbitsQuotientProd' {φ : Quotient (MulAction.orbitRel α β) → β}
(hφ : Function.LeftInverse Quotient.mk'' φ) (h : ∀ b : β, MulAction.stabilizer α b = ⊥) :
β ≃ Quotient (MulAction.orbitRel α β) × α :=
(MulAction.selfEquivSigmaOrbitsQuotientStabilizer' α β hφ).trans <|
(Equiv.sigmaCongrRight <| fun _ ↦
(Subgroup.quotientEquivOfEq (h _)).trans (QuotientGroup.quotientEquivSelf α)).trans <|
Equiv.sigmaEquivProd _ _
