Documentation

TauCeti.Topology.Algebra.GroupAction.FreeLocus

The free locus of a properly discontinuous group action #

For a group acting on a space, the free locus consists of the points with trivial stabilizer. It is naturally an invariant subspace. If the action is properly discontinuous on a locally compact Hausdorff space, this subspace is open: a sufficiently small neighbourhood of a free point meets none of its nontrivial translates.

On the free locus, the orbit projection is a quotient covering map. In particular it is both a covering map and a local homeomorphism. This separates the unramified part of a quotient from points with nontrivial stabilizer, where the full orbit projection need not be a covering map. The free locus is locally compact and the action on it is free and properly discontinuous, so the generic constructions for free properly discontinuous quotients apply to it by instance search.

source
def TauCeti.freeLocus (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] :
SubMulAction G X

The invariant subspace of points whose stabilizer is trivial.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.mem_freeLocus (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] {x : X} :
    x ∈ freeLocus G X ↔ MulAction.stabilizer G x = ⊥
    source
    instance TauCeti.freeLocus.instIsCancelSMul (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] :
    IsCancelSMul G ↥(freeLocus G X)

    The action restricted to the free locus is free.

    source
    instance TauCeti.freeLocus.instContinuousConstSMul (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] :
    ContinuousConstSMul G ↥(freeLocus G X)

    The action on the free locus is continuous in the point when the ambient action is.

    source
    instance TauCeti.freeLocus.instProperlyDiscontinuousSMul (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [TopologicalSpace X] [ProperlyDiscontinuousSMul G X] :
    ProperlyDiscontinuousSMul G ↥(freeLocus G X)

    A properly discontinuous action remains properly discontinuous on its free locus.

    source
    instance TauCeti.freeLocus.instSecondCountableTopologyQuotient (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [TopologicalSpace X] [SecondCountableTopology X] [ContinuousConstSMul G X] :
    SecondCountableTopology (MulAction.orbitRel.Quotient G ↥(freeLocus G X))

    The orbit space of the free locus of a continuous action on a second countable space is second countable.

    source
    theorem TauCeti.isOpen_freeLocus (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [ContinuousConstSMul G X] [ProperlyDiscontinuousSMul G X] :
    IsOpen ↑(freeLocus G X)

    The free locus of a properly discontinuous action on a locally compact Hausdorff space is open.

    source
    instance TauCeti.freeLocus.instLocallyCompactSpace (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [ContinuousConstSMul G X] [ProperlyDiscontinuousSMul G X] :
    LocallyCompactSpace ↥(freeLocus G X)

    The free locus of a properly discontinuous action on a locally compact Hausdorff space is locally compact, being open.

    source
    theorem TauCeti.isQuotientCoveringMap_quotientMk_freeLocus (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [ContinuousConstSMul G X] [ProperlyDiscontinuousSMul G X] :
    IsQuotientCoveringMap (Quotient.mk (MulAction.orbitRel G ↥(freeLocus G X))) G

    On the free locus of a properly discontinuous action, the ordinary orbit projection is a quotient covering map.

    source
    theorem TauCeti.isCoveringMap_quotientMk_freeLocus (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [ContinuousConstSMul G X] [ProperlyDiscontinuousSMul G X] :
    IsCoveringMap (Quotient.mk (MulAction.orbitRel G ↥(freeLocus G X)))

    The orbit projection from the free locus of a properly discontinuous action is a covering map.

    source
    theorem TauCeti.isLocalHomeomorph_quotientMk_freeLocus (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [ContinuousConstSMul G X] [ProperlyDiscontinuousSMul G X] :
    IsLocalHomeomorph (Quotient.mk (MulAction.orbitRel G ↥(freeLocus G X)))

    The orbit projection from the free locus of a properly discontinuous action is a local homeomorphism.