Quotients of manifolds

This file contains results about quotients of manifolds by group actions.

Main results

• MulAction.instChartedSpaceQuotient: a choice of charted space structure on the quotient of a charted space by a free, properly-discontinuous group action.

TODO

• if G acts smoothly, the quotient is an IsManifold I n for a suitable ModelWithCorners I.
• if G acts smoothly, the projection map is smooth

tags

smooth manifold, smooth action, quotient manifold

Charted space structure on quotient by a group

@[implicit_reducible]

noncomputable instance MulAction.instChartedSpaceQuotient {M : Type u_1} [TopologicalSpace M] {G : Type u_2} [Group G] [MulAction G M] [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [IsCancelSMul G M] [T2Space M] [LocallyCompactSpace M] {H : Type u_3} [TopologicalSpace H] [ChartedSpace H M] : ChartedSpace H (orbitRel.Quotient G M)

The induced charted space structure on the quotient of a charted space by a free, properly discontinuous group action.

Equations

• MulAction.instChartedSpaceQuotient = ⋯.chartedSpace ⋯

@[implicit_reducible]

noncomputable instance AddAction.instChartedSpaceQuotient {M : Type u_1} [TopologicalSpace M] {G : Type u_2} [AddGroup G] [AddAction G M] [ProperlyDiscontinuousVAdd G M] [ContinuousConstVAdd G M] [IsCancelVAdd G M] [T2Space M] [LocallyCompactSpace M] {H : Type u_3} [TopologicalSpace H] [ChartedSpace H M] : ChartedSpace H (orbitRel.Quotient G M)

Equations

• AddAction.instChartedSpaceQuotient = ⋯.chartedSpace ⋯