English
There is a canonical equivalence between the quotient of H acting on β and a sigma-type parameterizing orbits of H on β by Ω.
Русский
Существует каноническое эквивеликование между фактор-областью H на β и сигма-типом, параметризующим орбиты H на β через Ω.
LaTeX
$$orbitRel.Quotient H β ≃ Σ ω : Ω, orbitRel.Quotient H (orbitRel.Quotient.orbit ω).Elem$$
Lean4
/-- A bijection between the orbits under the action of a subgroup `H` on `β`, and the orbits
under the action of `H` on each orbit under the action of `G`. -/
@[to_additive /-- A bijection between the orbits under the action of an additive subgroup `H` on
`β`, and the orbits under the action of `H` on each orbit under the action of `G`. -/
]
noncomputable def equivSubgroupOrbits (H : Subgroup α) :
orbitRel.Quotient H β ≃ Σ ω : Ω, orbitRel.Quotient H (orbitRel.Quotient.orbit ω) :=
(Setoid.sigmaQuotientEquivOfLe (orbitRel_subgroup_le H)).symm.trans
(Equiv.sigmaCongrRight fun ω ↦ (equivSubgroupOrbitsSetoidComap H ω).symm)
