The fundamental-group action on the universal cover

The fundamental group FundamentalGroup X x₀ acts on UniversalCover x₀ by deck transformations: an element g acts on a point represented by a homotopy class of paths from x₀ by prepending a loop representing g⁻¹. The action is free, continuous in the universal cover variable, and properly discontinuous in the local form used by IsQuotientCoveringMap. Consequently, the endpoint projection is a quotient covering map for this action.

This file is adapted from Kim Morrison's mathlib4#38292, file Mathlib/AlgebraicTopology/FundamentalGroupoid/UniversalCover/Action.lean.

Convention

FundamentalGroup X x₀ = End (FundamentalGroupoid.mk x₀), and Mathlib's End multiplication reverses composition: (g * h).toPath = h.toPath.trans g.toPath. Geometric concatenation therefore gives a right action. To obtain the left action consumed by Mathlib's quotient-covering API, we define

g • mk x q = mk x (g⁻¹.toPath.trans q).

The inverse-free computation rule is inv_smul_mk.

Main declarations

• The MulAction, FaithfulSMul, ContinuousConstSMul, and IsCancelSMul instances for FundamentalGroup X x₀ acting on UniversalCover x₀.
• TauCeti.UniversalCover.monodromy_basepointLift: monodromy at that point is the fundamental-group action by the inverse loop class.
• TauCeti.UniversalCover.proj_eq_iff_mem_orbit: the fibres of proj are precisely the action orbits.
• TauCeti.UniversalCover.isQuotientCoveringMap: proj is the quotient covering map for the fundamental-group action.

@[instance_reducible]

noncomputable instance TauCeti.UniversalCover.instSMulFundamentalGroup {X : Type u_1} [TopologicalSpace X] {x₀ : X} : SMul (FundamentalGroup X x₀) (UniversalCover x₀)

The fundamental group acts on the universal cover by prepending the inverse loop class.

Equations

• TauCeti.UniversalCover.instSMulFundamentalGroup = { smul := fun (g : FundamentalGroup X x₀) (p : TauCeti.UniversalCover x₀) => { proj := p.proj, path := g⁻¹.toPath.trans p.path } }

@[simp]

theorem TauCeti.UniversalCover.smul_mk {X : Type u_1} [TopologicalSpace X] {x₀ : X} (g : FundamentalGroup X x₀) (x : X) (q : Path.Homotopic.Quotient x₀ x) : g • { proj := x, path := q } = { proj := x, path := g⁻¹.toPath.trans q }

The fundamental-group action prepends the inverse loop class to a representative path.

theorem TauCeti.UniversalCover.inv_smul_mk {X : Type u_1} [TopologicalSpace X] {x₀ : X} (g : FundamentalGroup X x₀) (x : X) (q : Path.Homotopic.Quotient x₀ x) : g⁻¹ • { proj := x, path := q } = { proj := x, path := g.toPath.trans q }

Acting by an inverse prepends the corresponding loop class without an inverse.

@[simp]

theorem TauCeti.UniversalCover.proj_smul {X : Type u_1} [TopologicalSpace X] {x₀ : X} (g : FundamentalGroup X x₀) (p : UniversalCover x₀) : (g • p).proj = p.proj

The fundamental-group action preserves the endpoint projection.

@[instance_reducible]

noncomputable instance TauCeti.UniversalCover.instMulActionFundamentalGroup {X : Type u_1} [TopologicalSpace X] {x₀ : X} : MulAction (FundamentalGroup X x₀) (UniversalCover x₀)

The action of the fundamental group on the universal cover.

Equations

• TauCeti.UniversalCover.instMulActionFundamentalGroup = { toSMul := TauCeti.UniversalCover.instSMulFundamentalGroup, mul_smul := ⋯, one_smul := ⋯ }

instance TauCeti.UniversalCover.instFaithfulSMulFundamentalGroup {X : Type u_1} [TopologicalSpace X] {x₀ : X} : FaithfulSMul (FundamentalGroup X x₀) (UniversalCover x₀)

The action on the universal cover is faithful.

instance TauCeti.UniversalCover.instContinuousConstSMulFundamentalGroup {X : Type u_1} [TopologicalSpace X] {x₀ : X} : ContinuousConstSMul (FundamentalGroup X x₀) (UniversalCover x₀)

Every fundamental-group element acts continuously on the universal cover.

instance TauCeti.UniversalCover.instIsCancelSMulFundamentalGroup {X : Type u_1} [TopologicalSpace X] {x₀ : X} : IsCancelSMul (FundamentalGroup X x₀) (UniversalCover x₀)

The action of the fundamental group on the universal cover is free.

theorem TauCeti.UniversalCover.proj_eq_iff_mem_orbit {X : Type u_1} [TopologicalSpace X] {x₀ : X} {p₁ p₂ : UniversalCover x₀} : p₁.proj = p₂.proj ↔ p₁ ∈ MulAction.orbit (FundamentalGroup X x₀) p₂

Two points of the universal cover have the same projection exactly when they lie in the same fundamental-group orbit.

theorem TauCeti.UniversalCover.exists_nhds_smul_disjoint {X : Type u_1} [TopologicalSpace X] {x₀ : X} [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (e : UniversalCover x₀) : ∃ U ∈ nhds e, ∀ (g : FundamentalGroup X x₀), ((fun (x : UniversalCover x₀) => g • x) '' U ∩ U).Nonempty → g = 1

The fundamental-group action is properly discontinuous: every point of the universal cover has a neighbourhood whose non-identity translates are disjoint from it.

theorem TauCeti.UniversalCover.proj_surjective {X : Type u_1} [TopologicalSpace X] {x₀ : X} [PathConnectedSpace X] : Function.Surjective proj

The endpoint projection is surjective when the base is path-connected.

theorem TauCeti.UniversalCover.isQuotientCoveringMap {X : Type u_1} [TopologicalSpace X] {x₀ : X} [LocallyPathConnectedSpace X] [PathConnectedSpace X] [SemilocallySimplyConnectedSpace X] : IsQuotientCoveringMap proj (FundamentalGroup X x₀)

The endpoint projection is a quotient covering map for the fundamental-group action.

@[simp]

theorem TauCeti.UniversalCover.monodromy_basepointLift {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (g : FundamentalGroup X x₀) : ↑(⋯.monodromy g.toPath (basepointLift x₀)) = g⁻¹ • ↑(basepointLift x₀)

Monodromy of the universal covering projection at its constant-path basepoint is the fundamental-group action by the inverse loop class.