English
There is a canonical equivalence between α and a sigma-type coding of its orbit decomposition.
Русский
Существует каноническое эквивалентное отображение между α и сигма-типом, кодирующим разбиение на орбиты.
LaTeX
$$def selfEquivSigmaOrbits' : α ≃ Σ ω : Ω, ω.orbit$$
Lean4
/-- Decomposition of a type `X` as a disjoint union of its orbits under a group action.
This version is expressed in terms of `MulAction.orbitRel.Quotient.orbit` instead of
`MulAction.orbit`, to avoid mentioning `Quotient.out`. -/
@[to_additive /-- Decomposition of a type `X` as a disjoint union of its orbits under an additive group action.
This version is expressed in terms of `AddAction.orbitRel.Quotient.orbit` instead of
`AddAction.orbit`, to avoid mentioning `Quotient.out`. -/
]
def selfEquivSigmaOrbits' : α ≃ Σ ω : Ω, ω.orbit :=
letI := orbitRel G α
calc
α ≃ Σ ω : Ω, { a // Quotient.mk' a = ω } := (Equiv.sigmaFiberEquiv Quotient.mk').symm
_ ≃ Σ ω : Ω, ω.orbit :=
Equiv.sigmaCongrRight fun _ => Equiv.subtypeEquivRight fun _ => orbitRel.Quotient.mem_orbit.symm
