The homotopy lifting property for covering maps #
IsCoveringMap.exists_path_lifts,IsCoveringMap.liftPath: any path in the base of a covering map lifts uniquely to the covering space (given a lift of the starting point).IsCoveringMap.liftHomotopy: any homotopyI × A → Xin the base of a covering mapE → Xcan be lifted to a homotopyI × A → E, starting from a given lift of the restriction{0} × A → X.IsCoveringMap.existsUnique_continuousMap_lifts: any continuous map from a simply-connected, locally path-connected space lifts uniquely through a covering map (given a lift of an arbitrary point).
If p : E → X is a local homeomorphism, and if g : I × A → E is a lift of f : C(I × A, X)
continuous on {0} × A ∪ I × {a} for some a : A, then there exists a neighborhood N ∈ 𝓝 a
and g' : I × A → E continuous on I × N that agrees with g on {0} × A ∪ I × {a}.
The proof follows [hatcher02], Proof of Theorem 1.7, p.30.
Possible TODO: replace I by an arbitrary space assuming A is locally connected
and p is a separated map, which guarantees uniqueness and therefore well-definedness
on the intersections.
The abstract monodromy theorem: if γ₀ and γ₁ are two paths in a topological space X,
γ is a homotopy between them relative to the endpoints, and the path at each time step of
the homotopy, γ (t, ·), lifts to a continuous path Γ t through a separated local
homeomorphism p : E → X, starting from some point in E independent of t. Then the
endpoints of these lifts are also independent of t.
This can be applied to continuation of analytic functions as follows: for a sheaf of analytic
functions on an analytic manifold X, we may consider its étale space E (whose points are
analytic germs) with the natural projection p : E → X, which is a local homeomorphism and a
separated map (because two analytic functions agreeing on a nonempty open set agree on the
whole connected component). An analytic continuation of a germ along a path γ (t, ·) : C(I, X)
corresponds to a continuous lift of γ (t, ·) to E starting from that germ. If γ is a
homotopy and the germ admits continuation along every path γ (t, ·), then the result of the
continuations are independent of t. In particular, if X is simply connected and an analytic
germ at p : X admits a continuation along every path in X from p to q : X, then the
continuation to q is independent of the path chosen.
A map f from a path-connected, locally path-connected space A to another space X lifts
uniquely through a local homeomorphism p : E → X if for every path γ in A, the composed
path f ∘ γ in X lifts to E with endpoint only dependent on the endpoint of γ and
independent of the path chosen. In this theorem, we require that a specific point a₀ : A is
lifted to a specific point e₀ : E over a₀.
The path lifting property (existence) for covering maps.
The lift of a path to a covering space given a lift of the left endpoint.
Instances For
Unique characterization of the lifted path.
The existence of liftHomotopy satisfying liftHomotopy_lifts and liftHomotopy_zero is
the homotopy lifting property for covering maps.
In other words, a covering map is a Hurewicz fibration.
Proposition 1.30 of [hatcher02].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The lift to a covering space of a homotopy between two continuous maps relative to a set given compatible lifts of the continuous maps.
Equations
- cov.liftHomotopyRel F he h₀ h₁ = { toContinuousMap := cov.liftHomotopy (↑F) f₀' ⋯, map_zero_left := ⋯, map_one_left := ⋯, prop' := ⋯ }
Instances For
Two continuous maps from a preconnected space to the total space of a covering map
are homotopic relative to a set S if and only if their compositions with the covering map
are homotopic relative to S, assuming that they agree at a point in S.
Lifting two paths that are homotopic relative to {0,1}
starting from the same point also ends up in the same point.
The monodromy of a covering map p : E → X, which sends a lift of the starting point of a
path in X to the endpoint of the lifted path in E. It only depends on the homotopy class
of the path.
Equations
Instances For
Lift a homotopy class of paths to a covering space.
Equations
- cov.liftPathQuotient γ e = Quotient.hrecOn γ (fun (γ : Path x y) => Path.Homotopic.Quotient.mk { toContinuousMap := cov.liftPath ↑γ ↑e ⋯, source' := ⋯, target' := ⋯ }) ⋯
Instances For
The monodromy action of the fundamental group at x on the fiber over x.
Equations
- cov.fundamentalGroupMulAction x = { smul := cov.monodromy, mul_smul := ⋯, one_smul := ⋯ }
Instances For
The monodromy action of the fundamental group at x on the fiber over x.
Equations
- cov.monodromyPerm x = MulAction.toPermHom (FundamentalGroup X x) ↑(p ⁻¹' {x})
Instances For
Monodromy of a covering map as a functor. Definition 2.1 in https://ncatlab.org/nlab/show/monodromy.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A covering map induces an injection on all Hom-sets of the fundamental groupoid, in particular on the fundamental group. The first part of Proposition 1.31 of [hatcher02].
A continuous map f from a simply-connected, locally path-connected space A to another
space X lifts uniquely through a covering map p : E → X, after specifying any lift
e₀ : E of any point a₀ : A.
A continuous map f from a path connected, locally path-connected space A to another
space X lifts uniquely through a covering map p : E → X (such that f a₀ is lifted to e₀)
if f⁎ π₁(A, a₀) ⊆ p⁎ π₁(E, e₀). Proposition 1.33 of [hatcher02], known as
the lifting criterion.
A version of IsCoveringMap.existsUnique_continuousMap_lifts for maps
that are covering on a subset of the codomain.
Let p be a covering map on s.
Let f be a continuous map with a simply connected locally path connected domain
such that all values of f belong to s.
Given a point a₀ in the domain of f and a lift e₀ of f a₀ along p,
there exists a unique lift F of f along p such that F a₀ = e₀.
The monodromy action of a quotient covering map commutes with the group action.
Alias of the forward direction of IsQuotientCoveringMap.monodromy_ext_iff.
Choosing an arbitrary basepoint e ∈ f ⁻¹' {x} induces a bijection f ⁻¹' {x} ≃ G, and the
G-action on f ⁻¹' {x} corresponds to left multiplication. The monodromy action commutes
with the G-action, so each monodromy must corresponds must correspond to a right multiplication.
Equations
- hp.fundamentalGroupToMulOpposite e = { toFun := fun (γ : FundamentalGroup X x) => MulOpposite.op ((hp.fiberEquivGroup e) (⋯.monodromy γ e)), map_one' := ⋯, map_mul' := ⋯ }
Instances For
The fundamental group of the base of simply-connected covering map is contravariantly equivalent to the group of the covering map.
Equations
Instances For
Alias of the forward direction of IsAddQuotientCoveringMap.monodromy_ext_iff.
Choosing an arbitrary basepoint e ∈ f ⁻¹' {x} induces a bijection f ⁻¹' {x} ≃ G, and the
G-action on f ⁻¹' {x} corresponds to left multiplication. The monodromy action commutes
with the G-action, so each monodromy must corresponds must correspond to a right multiplication.
Equations
Instances For
The fundamental group of the base of simply-connected covering map is contravariantly equivalent to the group of the covering map.
Equations
- hp.fundamentalGroupEquiv e = ⋯.fundamentalGroupEquiv e