Changing the basepoint of a universal cover

A path γ : Path x y singles out a point of UniversalCover x over y. Prepending γ gives a homeomorphism over X from UniversalCover y to UniversalCover x, carrying the constant-path point to this point. This is the basepoint change of the universal cover. The direction agrees with concatenation: a path beginning at y is regarded, after changing basepoint, as beginning with γ at x.

The universal-cover construction itself adapts Kim Morrison's work in mathlib4#38292. The uniqueness proof uses Thomas Browning's IsCoveringMap.eq_of_comp_eq in Mathlib.Topology.Covering.Basic, recorded there as Proposition 1.34 of [hatcher02].

noncomputable def TauCeti.UniversalCover.basepointChangeHomeomorph {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : UniversalCover y ≃ₜ UniversalCover x

Changing the basepoint along γ gives a homeomorphism over X that sends the constant path at y to the class of γ at x.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.UniversalCover.basepointChangeHomeomorph_apply_basepointLift {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : (basepointChangeHomeomorph γ) ↑(basepointLift y) = { proj := y, path := Path.Homotopic.Quotient.mk γ }

Basepoint change sends the distinguished point to the path class defining the change.

@[simp]

theorem TauCeti.UniversalCover.proj_basepointChangeHomeomorph {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) (e : UniversalCover y) : ((basepointChangeHomeomorph γ) e).proj = e.proj

Basepoint change commutes with the projections to X.

@[simp]

theorem TauCeti.UniversalCover.basepointChangeHomeomorph_apply_mk {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) {z : X} (q : Path.Homotopic.Quotient y z) : (basepointChangeHomeomorph γ) { proj := z, path := q } = { proj := z, path := (Path.Homotopic.Quotient.mk γ).trans q }

Basepoint change prepends γ to a represented path class.

@[simp]

theorem TauCeti.UniversalCover.basepointChangeHomeomorph_trans {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) {z : X} (δ : Path y z) : basepointChangeHomeomorph (γ.trans δ) = (basepointChangeHomeomorph δ).trans (basepointChangeHomeomorph γ)

Changing basepoint along concatenated paths composes the corresponding homeomorphisms.

theorem TauCeti.UniversalCover.basepointChangeHomeomorph_eq_of_homotopic {X : Type u_1} [TopologicalSpace X] {x y : X} {γ δ : Path x y} (h : γ.Homotopic δ) : basepointChangeHomeomorph γ = basepointChangeHomeomorph δ

Homotopic paths induce the same basepoint change.

@[simp]

theorem TauCeti.UniversalCover.basepointChangeHomeomorph_symm {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : (basepointChangeHomeomorph γ).symm = basepointChangeHomeomorph γ.symm

Reversing the path reverses the basepoint-change homeomorphism.

theorem TauCeti.UniversalCover.eq_basepointChangeHomeomorph {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : C(UniversalCover y, UniversalCover x)) [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (hf₀ : f ↑(basepointLift y) = { proj := y, path := Path.Homotopic.Quotient.mk γ }) (hf : ∀ (e : UniversalCover y), (f e).proj = e.proj) : f = ↑(basepointChangeHomeomorph γ)

Projection and the image of the constant path determine the basepoint-change map uniquely among continuous maps when the projection is a covering map.

@[simp]

theorem TauCeti.UniversalCover.basepointChangeHomeomorph_refl {X : Type u_1} [TopologicalSpace X] (x : X) : basepointChangeHomeomorph (Path.refl x) = Homeomorph.refl (UniversalCover x)

Changing the basepoint along a constant path is the identity.