Universal cover: quotient model and sheets

This file introduces the based-path quotient model for the universal cover based at a point x₀, and builds the sheet decomposition of proj ⁻¹' U over a good neighborhood U.

It is adapted from mathlib4#38292 by Kim Morrison.

The underlying point of the universal cover is still represented by an endpoint together with a homotopy class of paths from x₀, but the topology is not the naive sigma topology. Instead it is the quotient topology coming from the compact-open based-path space.

Main definitions

• UniversalCover x₀: a structure with fields proj : X (the endpoint) and path : Path.Homotopic.Quotient x₀ proj (the homotopy class of paths from x₀), topologized as the quotient of BasedPath x₀ under endpoint-preserving homotopy.
• UniversalCover.proj : UniversalCover x₀ → X: the endpoint projection (auto-generated).
• UniversalCover.basepointLift: the constant-path point over x₀.
• UniversalCover.sheet: the sheet indexed by q : Path.Homotopic.Quotient x₀ x over a good neighborhood U, viewed as a subset of UniversalCover x₀.

Main results

• UniversalCover.range_proj: the endpoint projection has range the path component of x₀.
• UniversalCover.isOpenMap_proj: the endpoint projection is an open map.
• UniversalCover.toPath_homotopic_of_ofBasedPath_eq and UniversalCover.ofBasedPath_eq_of_homotopic_toPath: equality in the universal cover is equivalent to endpoint-preserving path homotopy of representatives.
• UniversalCover.proj_surjOn_sheet, UniversalCover.pairwise_disjoint_sheet, UniversalCover.sheet_exhaustive, UniversalCover.proj_injOn_sheet: structure of the sheet decomposition over a good neighborhood U.

Implementation note

Hatcher (and many textbook treatments) topologize the universal cover directly, declaring a basic open set for each pair (q, U) of a homotopy class q and a good neighborhood U.

Here we take a different route: the based-path space BasedPath x₀ already naturally has the compact-open topology, and we put the quotient topology on the endpoint/homotopy-class model via the surjection ofBasedPath. This introduces slightly more complexity, that is hidden in book presentations that omit proving their introduced topology is actually the standard one.

structure TauCeti.UniversalCover {X : Type u_1} [TopologicalSpace X] (x₀ : X) : Type u_1

The endpoint-plus-homotopy-class model for the universal cover. The topology is supplied below as the quotient topology from BasedPath x₀.

• proj : X

  The endpoint of a representative path.

• path : Path.Homotopic.Quotient x₀ self.proj

  The homotopy class of paths from the basepoint to proj.

theorem TauCeti.UniversalCover.ext {X : Type u_1} {inst✝ : TopologicalSpace X} {x₀ : X} {x y : UniversalCover x₀} (proj : x.proj = y.proj) (path : x.path ≍ y.path) : x = y

theorem TauCeti.UniversalCover.ext_iff {X : Type u_1} {inst✝ : TopologicalSpace X} {x₀ : X} {x y : UniversalCover x₀} : x = y ↔ x.proj = y.proj ∧ x.path ≍ y.path

def TauCeti.UniversalCover.ofBasedPath {X : Type u_1} [TopologicalSpace X] (x₀ : X) (α : BasedPath x₀) : UniversalCover x₀

The quotient map from based paths to endpoint/path-homotopy classes.

Equations

• TauCeti.UniversalCover.ofBasedPath x₀ α = { proj := α.endpoint, path := Path.Homotopic.Quotient.mk α.toPath }

theorem TauCeti.UniversalCover.ofBasedPath_def {X : Type u_1} [TopologicalSpace X] {x₀ : X} (α : BasedPath x₀) : ofBasedPath x₀ α = { proj := α.endpoint, path := Path.Homotopic.Quotient.mk α.toPath }

ofBasedPath records the endpoint and homotopy class of its based path.

@[instance_reducible]

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

The topology on UniversalCover x₀ as the quotient topology coinduced from the compact-open topology on BasedPath x₀ via ofBasedPath. See the module-level ## Implementation note for why we do not use the Hatcher-style bespoke basis.

Equations

• TauCeti.UniversalCover.instTopologicalSpaceUniversalCover x₀ = TopologicalSpace.coinduced (TauCeti.UniversalCover.ofBasedPath x₀) inferInstance

theorem TauCeti.UniversalCover.continuous_ofBasedPath {X : Type u_1} [TopologicalSpace X] (x₀ : X) : Continuous (ofBasedPath x₀)

The canonical map from based paths to the universal cover is continuous.

@[simp]

theorem TauCeti.UniversalCover.ofBasedPath_ofPath {X : Type u_1} [TopologicalSpace X] {x₀ y : X} (p : Path x₀ y) : ofBasedPath x₀ (BasedPath.ofPath p) = { proj := y, path := Path.Homotopic.Quotient.mk p }

ofBasedPath applied to the canonical based path from p : Path x₀ y gives the endpoint-and-homotopy-class pair.

theorem TauCeti.UniversalCover.surjective_ofBasedPath {X : Type u_1} [TopologicalSpace X] (x₀ : X) : Function.Surjective (ofBasedPath x₀)

Every point of UniversalCover x₀ is represented by some based path.

theorem TauCeti.UniversalCover.isQuotientMap_ofBasedPath {X : Type u_1} [TopologicalSpace X] (x₀ : X) : Topology.IsQuotientMap (ofBasedPath x₀)

ofBasedPath is a quotient map: UniversalCover x₀ carries the quotient topology from BasedPath x₀ under endpoint-preserving path homotopy.

theorem TauCeti.UniversalCover.continuous_prepend {X : Type u_1} [TopologicalSpace X] {x₀ y : X} (γ : Path x₀ y) : Continuous fun (e : UniversalCover y) => { proj := e.proj, path := (Path.Homotopic.Quotient.mk γ).trans e.path }

Prepending a fixed path is continuous on the based-path quotient.

@[simp]

theorem TauCeti.UniversalCover.proj_ofBasedPath {X : Type u_1} [TopologicalSpace X] (x₀ : X) (γ : BasedPath x₀) : (ofBasedPath x₀ γ).proj = γ.endpoint

proj composed with ofBasedPath reads off the endpoint of the representative.

def TauCeti.UniversalCover.basepointLift {X : Type u_1} [TopologicalSpace X] (x₀ : X) : ↑(proj ⁻¹' {x₀})

The constant-path point in the fibre of the universal covering projection over x₀.

Equations

• TauCeti.UniversalCover.basepointLift x₀ = ⟨TauCeti.UniversalCover.ofBasedPath x₀ (BasedPath.ofPath (Path.refl x₀)), ⋯⟩

theorem TauCeti.UniversalCover.proj_basepointLift {X : Type u_1} [TopologicalSpace X] (x₀ : X) : (↑(basepointLift x₀)).proj = x₀

The endpoint projection sends the constant-path point to the basepoint.

@[simp]

theorem TauCeti.UniversalCover.basepointLift_coe {X : Type u_1} [TopologicalSpace X] (x₀ : X) : ↑(basepointLift x₀) = { proj := x₀, path := Path.Homotopic.Quotient.refl x₀ }

The underlying point of basepointLift is represented by the constant path.

@[simp]

theorem TauCeti.UniversalCover.range_proj {X : Type u_1} [TopologicalSpace X] (x₀ : X) : Set.range proj = pathComponent x₀

The endpoint projection of the universal cover has range the path component of x₀.

theorem TauCeti.UniversalCover.endpoint_eq_of_ofBasedPath_eq {X : Type u_1} [TopologicalSpace X] {x₀ : X} {α β : BasedPath x₀} (h : ofBasedPath x₀ α = ofBasedPath x₀ β) : α.endpoint = β.endpoint

Equal images under ofBasedPath have equal endpoints.

theorem TauCeti.UniversalCover.toPath_homotopic_of_ofBasedPath_eq {X : Type u_1} [TopologicalSpace X] {x₀ : X} {α β : BasedPath x₀} (h : ofBasedPath x₀ α = ofBasedPath x₀ β) : (α.toPath.cast ⋯ ⋯).Homotopic β.toPath

Equality in the universal cover induces an endpoint-preserving homotopy of representative based paths.

theorem TauCeti.UniversalCover.ofBasedPath_eq_of_homotopic_toPath {X : Type u_1} [TopologicalSpace X] {x₀ : X} {α β : BasedPath x₀} (heq : α.endpoint = β.endpoint) (h : (α.toPath.cast ⋯ ⋯).Homotopic β.toPath) : ofBasedPath x₀ α = ofBasedPath x₀ β

If two based paths have the same endpoint and homotopic toPaths (after casting to a common target), then they represent the same element of the UniversalCover.

theorem TauCeti.UniversalCover.continuous_proj {X : Type u_1} [TopologicalSpace X] (x₀ : X) : Continuous proj

The endpoint projection from the universal cover is continuous.

theorem TauCeti.UniversalCover.isOpenMap_proj {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] (x₀ : X) : IsOpenMap proj

The endpoint projection UniversalCover x₀ → X is an open map when X is locally path-connected.

Sheet construction over a good neighborhood

Below we construct, for each point x and a good neighborhood U of x, the sheets indexed by the homotopy classes q : Path.Homotopic.Quotient x₀ x.

def TauCeti.UniversalCover.basedPathComponent {X : Type u_1} [TopologicalSpace X] {x₀ : X} (U : Set X) {y : X} (p : Path x₀ y) : Set (BasedPath x₀)

The path component (in endpoint ⁻¹' U) of the based path ofPath p.

Equations

• TauCeti.UniversalCover.basedPathComponent U p = pathComponentIn (BasedPath.endpoint ⁻¹' U) (BasedPath.ofPath p)

noncomputable def TauCeti.UniversalCover.basedPathSheet {X : Type u_1} [TopologicalSpace X] {x₀ x : X} (U : Set X) (hxU : x ∈ U) (q : Path.Homotopic.Quotient x₀ x) : Set (BasedPath x₀)

The sheet over U (with x ∈ U) corresponding to a homotopy class q : Path.Homotopic.Quotient x₀ x, expressed as a set of based paths.

Equations

• TauCeti.UniversalCover.basedPathSheet U hxU q = Quotient.liftOn q (fun (p : Path x₀ x) => TauCeti.UniversalCover.basedPathComponent U p) ⋯

@[simp]

theorem TauCeti.UniversalCover.basedPathSheet_mk {X : Type u_1} [TopologicalSpace X] {x₀ x : X} (U : Set X) (hxU : x ∈ U) (p : Path x₀ x) : basedPathSheet U hxU (Path.Homotopic.Quotient.mk p) = basedPathComponent U p

basedPathSheet of a quotient class unfolds to the path component of any representative.

theorem TauCeti.UniversalCover.basedPathSheet_subset_endpoint_preimage {X : Type u_1} [TopologicalSpace X] {x₀ x : X} (U : Set X) (hxU : x ∈ U) (q : Path.Homotopic.Quotient x₀ x) : basedPathSheet U hxU q ⊆ BasedPath.endpoint ⁻¹' U

Every based path in a basedPathSheet over U has its endpoint in U.

noncomputable def TauCeti.UniversalCover.sheet {X : Type u_1} [TopologicalSpace X] {x₀ x : X} (U : Set X) (hxU : x ∈ U) (q : Path.Homotopic.Quotient x₀ x) : Set (UniversalCover x₀)

The sheet over U corresponding to q, viewed as a subset of UniversalCover x₀.

Equations

• TauCeti.UniversalCover.sheet U hxU q = TauCeti.UniversalCover.ofBasedPath x₀ '' TauCeti.UniversalCover.basedPathSheet U hxU q

theorem TauCeti.UniversalCover.sheet_subset_proj_preimage {X : Type u_1} [TopologicalSpace X] {x₀ x : X} (U : Set X) (hxU : x ∈ U) (q : Path.Homotopic.Quotient x₀ x) : sheet U hxU q ⊆ proj ⁻¹' U

Points of the sheet over U project into U.

theorem TauCeti.UniversalCover.ofBasedPath_preimage_sheet {X : Type u_1} [TopologicalSpace X] {x₀ x : X} (U : Set X) (hxU : x ∈ U) (q : Path.Homotopic.Quotient x₀ x) : ofBasedPath x₀ ⁻¹' sheet U hxU q = basedPathSheet U hxU q

The preimage of a sheet under ofBasedPath is the corresponding basedPathSheet. This expresses that the sheet is saturated under the ofBasedPath quotient.

@[simp]

theorem TauCeti.UniversalCover.ofBasedPath_mem_sheet_iff {X : Type u_1} [TopologicalSpace X] {x₀ x : X} {U : Set X} {hxU : x ∈ U} {q : Path.Homotopic.Quotient x₀ x} {α : BasedPath x₀} : ofBasedPath x₀ α ∈ sheet U hxU q ↔ α ∈ basedPathSheet U hxU q

Saturated membership criterion: a based path's image lies in a sheet iff the based path itself lies in the corresponding basedPathSheet.

theorem TauCeti.UniversalCover.isOpen_sheet {X : Type u_1} [TopologicalSpace X] {x₀ x : X} [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (U : Set X) (hU_open : IsOpen U) (hxU : x ∈ U) (q : Path.Homotopic.Quotient x₀ x) : IsOpen (sheet U hxU q)

A sheet over an open set is open under the local hypotheses for universal covers.

theorem TauCeti.UniversalCover.mem_sheet_self {X : Type u_1} [TopologicalSpace X] {x₀ x : X} {U : Set X} (hxU : x ∈ U) (p : Path x₀ x) : ofBasedPath x₀ (BasedPath.ofPath p) ∈ sheet U hxU (Path.Homotopic.Quotient.mk p)

A path representative belongs to the sheet indexed by its own homotopy class.

theorem TauCeti.UniversalCover.proj_surjOn_sheet {X : Type u_1} [TopologicalSpace X] {x₀ x : X} {U : Set X} (hU_pathConn : IsPathConnected U) (hxU : x ∈ U) (q : Path.Homotopic.Quotient x₀ x) : Set.SurjOn proj (sheet U hxU q) U

Sheet surjection onto U: every point of U is the projection of a point of the sheet.

theorem TauCeti.UniversalCover.pairwise_disjoint_sheet {X : Type u_1} [TopologicalSpace X] {x₀ x : X} {U : Set X} (hU_slsc : IsPathHomotopyTrivial U) (hxU : x ∈ U) : Pairwise fun (q₁ q₂ : Path.Homotopic.Quotient x₀ x) => Disjoint (sheet U hxU q₁) (sheet U hxU q₂)

Sheets over the same good neighborhood, indexed by Path.Homotopic.Quotient, are pairwise disjoint.

theorem TauCeti.UniversalCover.sheet_exhaustive {X : Type u_1} [TopologicalSpace X] {x₀ x : X} {U : Set X} (hU_pathConn : IsPathConnected U) (hxU : x ∈ U) : proj ⁻¹' U ⊆ ⋃ (q : Path.Homotopic.Quotient x₀ x), sheet U hxU q

Sheets exhaust proj ⁻¹' U: every element of the preimage lies in some sheet.

theorem TauCeti.UniversalCover.proj_injOn_sheet {X : Type u_1} [TopologicalSpace X] {x₀ x : X} {U : Set X} (hU_slsc : IsPathHomotopyTrivial U) (hxU : x ∈ U) (q : Path.Homotopic.Quotient x₀ x) : Set.InjOn proj (sheet U hxU q)

In a good neighborhood U, the projection proj is injective on each sheet.