How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Covering Spaces and Lifting
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Homotopy and Homotopy Equivalence
- Limits of Real Functions
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Metric Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Order, Zorn's Lemma, and the Axiom of Choice
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Fundamental Group
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
Covering spaces combine the local topology of homeomorphic sheets with the global path and homotopy invariants supplied by Based loops and the fundamental group. Compactness controls finite subdivisions and finite-sheeted coverings, while Left group actions, transitive actions, and faithful actions and A free group action has no nonidentity element fixing a point provide the algebraic language for monodromy, deck transformations, and quotient actions. Local path-connectedness and semilocal simple connectedness are kept distinct because they enter different lifting and existence arguments.
Covering maps, maps of covers, lifts, pullbacks, monodromy, deck groups, and covering-space actions are defined before their structural results. Path and homotopy lifting lead to fundamental-group injectivity, lift uniqueness, and the subgroup lifting criterion. The path-class construction then proves existence and uniqueness of universal covers, after which fibre cardinality is identified with subgroup index, compactness is compared across finite-sheeted coverings, and the deck group of a universal cover is identified with the fundamental group using the inverse-path convention.
3 · Logical flowchart
4 · Definitions, theorems and proofs
Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings
Definition
A covering map is a continuous surjection such that every has an open neighbourhood for which is a disjoint union of open sets , called sheets, and each restriction is a homeomorphism (Continuity of a map of topological spaces at a point and globally, Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological, The disjoint union (coproduct) with the final topology of the canonical injections: a set is open exactly when each of its traces is). Such a is evenly covered, and is the fibre over . A covering is trivial when it is isomorphic over to a product projection with discrete.
Maps and isomorphisms of covering spaces over a fixed base
Definition
For coverings and , a map of covering spaces over is a continuous map with . It is an isomorphism of covering spaces when is a homeomorphism; its inverse is then also over (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological, Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).
Lifts of maps, paths, and homotopies through a covering map
Definition
Let be a covering and continuous. A lift of through is a continuous map with . This includes lifts of paths and of homotopies ; an initial lift prescribes the restriction at time (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints, Paths, path-connected spaces and path components).
Covering maps are surjective local homeomorphisms with discrete fibres
Statement
Every covering map is a surjective local homeomorphism, and each of its fibres is discrete in the subspace topology.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
A covering map is a continuous surjection such that every has an open neighbourhood for which is a disjoint union of open sets , called sheets, and each restriction is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a is evenly covered, and is the fibre over . A covering is trivial when it is isomorphic over to a product projection with discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).
Let and be topological spaces and let be a function. Continuity is as in def-continuous-map-top, injections, surjections and bijections as in def-injection-surjection-bijection. is an open map if is open in for every open , a closed map if is closed in for every closed , and a homeomorphism if is a continuous bijection whose inverse is also continuous; the spaces are homeomorphic when such an exists. (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).
Throughout, a topology is as in def-topological-space, and finite, at most countable and uncountable are as in def-countable, so that "countable" always means "at most countable" and every finite set is countable. Let be a set. The six families below are topologies on ; that each really satisfies (T1), (T2) and (T3) is discharged in full after the list. Among those six is the discrete topology , in which every subset is open and hence every subset is also closed. (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies).
Proof
An evenly covered neighbourhood restricts the projection to a homeomorphism on each sheet, which gives the local-homeomorphism property.
Intersect a sheet with a fibre to isolate its unique point.
Keep surjectivity as part of the covering-map definition rather than infer it from local data.
The preceding construction and implications establish the assertion.
The cardinality of a covering fibre is locally constant and is constant on a connected base
Statement
For a covering , the cardinality of is locally constant as a function of . If is connected, all fibres are equinumerous.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
A covering map is a continuous surjection such that every has an open neighbourhood for which is a disjoint union of open sets , called sheets, and each restriction is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a is evenly covered, and is the fibre over . A covering is trivial when it is isomorphic over to a product projection with discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).
Let be a topological space (def-topological-space). A separation of is an ordered pair of open, nonempty, disjoint subsets of with ; is disconnected when a separation of exists and connected when none does. Since and are complementary each is clopen, so a separation is the same thing as a partition of into two nonempty clopen pieces. A subset is a connected subset when the subspace is connected. (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).
Let and be sets (def-injection-surjection-bijection for the terminology). and are equinumerous, written , if there exists a bijection ; is dominated by , written , if there exists an injection . (Equinumerous sets, and ).
Proof
Over an evenly covered neighbourhood every fibre meets each sheet in exactly one point, so all fibres there are in bijection with the sheet index set.
The subsets on which a fixed fibre cardinal occurs are open; connectedness permits only one nonempty such subset.
The preceding construction and implications establish the assertion.
Existence and uniqueness of path lifts through a covering map
Statement
Let be a covering, let be a path, and let satisfy . There is a unique path with and .
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
Let be a covering and continuous. A lift of through is a continuous map with . This includes lifts of paths and of homotopies ; an initial lift prescribes the restriction at time (def-homotopy-relative-and-path-homotopy, def-path-connected). (Lifts of maps, paths, and homotopies through a covering map).
Let be a compact metric space (def-metric-compactness, def-metric-space) and let be an open cover of . Then there is a real , a Lebesgue number for , such that every nonempty with (def-metric-bounded-diameter) satisfies for some . Diameters of nonempty subsets of are defined because a compact space is bounded (thm-compact-subset-is-closed-and-bounded) and a subset of a bounded set is bounded. No choice principle is used. (Every open cover of a compact metric space has a Lebesgue number: a such that every nonempty subset of diameter less than lies inside a single member of the cover).
Let , and be topological spaces, with subspaces carrying the subspace topology (def-subspace-topology-top). Then: 1. Composites. If and are continuous (def-continuous-map-top) then is continuous. 2. Open cover. Let be a function and let be a family of open subsets of with . If is continuous for every , then is continuous. 3. Finite closed cover. Let be a function, let and let be closed subsets of with . If is continuous for every , then is continuous. The converses of claims 2 and 3 hold with no hypothesis on the cover at all: every restriction of a continuous map to a subspace is continuous (def-subspace-topology-top). The finiteness in claim 3 is not removable; see the remarks. (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).
Let be a topological space (def-topological-space). An open cover of is a family of open sets with ; a subcover of is a subfamily that is itself an open cover; and is compact when every open cover of it has a finite subcover. (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).
Proof
Pull back evenly covered neighbourhoods along the path to obtain an open cover of the compact interval, choose a Lebesgue subdivision, and lift successively sheet by sheet from the prescribed initial point.
Agreement at subdivision endpoints gives a continuous pasted path; sheet uniqueness proves uniqueness, including constant paths.
The preceding construction and implications establish the assertion.
Existence and uniqueness of homotopy lifts through a covering map
Statement
Let be a covering, a homotopy, and a lift of . There is a unique lift of extending .
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
Let be a covering and continuous. A lift of through is a continuous map with . This includes lifts of paths and of homotopies ; an initial lift prescribes the restriction at time (def-homotopy-relative-and-path-homotopy, def-path-connected). (Lifts of maps, paths, and homotopies through a covering map).
Let be a covering, let be a path, and let satisfy . There is a unique path with and . (Existence and uniqueness of path lifts through a covering map).
The product set. Let be a set and let be a set for each . The product is and we write , the -th coordinate of . Two elements of the product are equal exactly when they agree at every index, functions being equal when they have the same domain and the same values. For the -th projection is . The product topology on is the initial topology of the projections: the topology generated by the subbasis . Finite intersections of subbasic sets form a basis for it, and they are exactly the boxes with every open in and for all but finitely many . (The product set of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).
Let , and be topological spaces, with subspaces carrying the subspace topology (def-subspace-topology-top). Then: 1. Composites. If and are continuous (def-continuous-map-top) then is continuous. 2. Open cover. Let be a function and let be a family of open subsets of with . If is continuous for every , then is continuous. 3. Finite closed cover. Let be a function, let and let be closed subsets of with . If is continuous for every , then is continuous. The converses of claims 2 and 3 hold with no hypothesis on the cover at all: every restriction of a continuous map to a subspace is continuous (def-subspace-topology-top). The finiteness in claim 3 is not removable; see the remarks. (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).
Let be a topological space (def-topological-space). An open cover of is a family of open sets with ; a subcover of is a subfamily that is itself an open cover; and is compact when every open cover of it has a finite subcover. (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).
Proof
For a homotopy and a lift at time zero, use evenly covered neighbourhoods and compactness of the interval to extend the lift over successive time strips locally in .
Pasting gives a global lift, and the set of points where two lifts agree is open and closed on each vertical interval, yielding uniqueness.
The preceding construction and implications establish the assertion.
The endpoint of a lifted path depends only on its endpoint-fixed homotopy class
Statement
Endpoint-fixed homotopic paths in the base have lifts with the same endpoint whenever their lifts begin at the same point.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
Let be a covering, a homotopy, and a lift of . There is a unique lift of extending . (Existence and uniqueness of homotopy lifts through a covering map).
Every covering map is a surjective local homeomorphism, and each of its fibres is discrete in the subspace topology. (Covering maps are surjective local homeomorphisms with discrete fibres).
Let be a topological space (def-topological-space). A separation of is an ordered pair of open, nonempty, disjoint subsets of with ; is disconnected when a separation of exists and connected when none does. Since and are complementary each is clopen, so a separation is the same thing as a partition of into two nonempty clopen pieces. A subset is a connected subset when the subspace is connected. (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).
Proof
Lift an endpoint-fixed homotopy starting from the chosen lift of one path.
Along each endpoint edge the lifted map takes values in a discrete fibre; connectedness of the interval makes it constant, so the terminal endpoints agree.
The preceding construction and implications establish the assertion.
A covering map induces an injective homomorphism on fundamental groups
Statement
For a covering , the induced homomorphism is injective.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
Let be a covering, a homotopy, and a lift of . There is a unique lift of extending . (Existence and uniqueness of homotopy lifts through a covering map).
Let be continuous and let . Composition sends a loop at to the loop at . Using the loop classes and fundamental group of def-based-loops-and-fundamental-group, the proposed induced homomorphism is The next theorem proves that this value is independent of the representative, that it is a group homomorphism in the sense of def-group-homomorphism, and that induced maps respect identities, composition and homotopies that fix the basepoint. (The homomorphism on fundamental groups induced by a pointed continuous map).
A topological space is simply connected when it is nonempty and path-connected (def-path-connected) and, for every , the group has exactly one element. (Simply connected topological spaces).
Proof
If a loop upstairs maps to a nullhomotopic loop downstairs, lift a nullhomotopy with the given loop as its initial edge.
Uniqueness forces the opposite edge to be constant, yielding a nullhomotopy upstairs.
Preserve the chosen basepoints and the exact published definition of the induced map.
The preceding construction and implications establish the assertion.
Two lifts from a connected space that agree at one point agree everywhere
Statement
Let be connected and let be lifts through the same covering of the same map . If for some , then .
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
Let be a covering and continuous. A lift of through is a continuous map with . This includes lifts of paths and of homotopies ; an initial lift prescribes the restriction at time (def-homotopy-relative-and-path-homotopy, def-path-connected). (Lifts of maps, paths, and homotopies through a covering map).
Let be a topological space (def-topological-space). A separation of is an ordered pair of open, nonempty, disjoint subsets of with ; is disconnected when a separation of exists and connected when none does. Since and are complementary each is clopen, so a separation is the same thing as a partition of into two nonempty clopen pieces. A subset is a connected subset when the subspace is connected. (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).
A covering map is a continuous surjection such that every has an open neighbourhood for which is a disjoint union of open sets , called sheets, and each restriction is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a is evenly covered, and is the fibre over . A covering is trivial when it is isomorphic over to a product projection with discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).
Proof
The equaliser of two lifts is open because a common image point has an evenly covered neighbourhood and both lifts must lie in the same sheet near an agreement point.
Its complement is open by choosing disjoint sheets near a disagreement point.
Connectedness and the named agreement point force the equaliser to be the whole domain.
The preceding construction and implications establish the assertion.
Lifting criterion for maps from path-connected locally path-connected spaces
Statement
Let be path-connected and locally path-connected, let be based, and let be a covering. A based lift exists if and only if ; when it exists it is unique.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
Let be a covering, let be a path, and let satisfy . There is a unique path with and . (Existence and uniqueness of path lifts through a covering map).
Endpoint-fixed homotopic paths in the base have lifts with the same endpoint whenever their lifts begin at the same point. (The endpoint of a lifted path depends only on its endpoint-fixed homotopy class).
Let be connected and let be lifts through the same covering of the same map . If for some , then . (Two lifts from a connected space that agree at one point agree everywhere).
Let be continuous and let . Composition sends a loop at to the loop at . Using the loop classes and fundamental group of def-based-loops-and-fundamental-group, the proposed induced homomorphism is The next theorem proves that this value is independent of the representative, that it is a group homomorphism in the sense of def-group-homomorphism, and that induced maps respect identities, composition and homotopies that fix the basepoint. (The homomorphism on fundamental groups induced by a pointed continuous map).
Let be a topological space (def-topological-space) and let . Subsets carry the subspace topology (def-subspace-topology-top); connectedness is def-connected-space and path-connectedness is def-path-connected. is locally connected at when for every open with there is an open connected with , and locally connected when this holds at every point; is locally path-connected at when for every open with there is an open path-connected with , and locally path-connected when this holds at every point. (Locally connected and locally path-connected spaces: a neighbourhood base of open connected, respectively open path-connected, sets at every point).
Let be continuous with . Then is a well-defined group homomorphism, and for pointed continuous maps and (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).
Proof
For a based map with path-connected and locally path-connected, necessity follows by functoriality: if a based lift exists then , so by the composition law of [F6], whence . [F4] is the definition of the induced map and expressly leaves functoriality to [F6].
For sufficiency, define the candidate lift at by lifting along any path from ; the subgroup inclusion makes the endpoint independent of the chosen path.
Local path-connectedness and an evenly covered neighbourhood make the candidate continuous.
Uniqueness follows from connectedness.
The preceding construction and implications establish the assertion.
The pullback of a covering space along a continuous map
Definition
For a covering and a continuous map , define with the subspace topology, and let be (The product set of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace). This is the pullback covering space; its covering property is proved in Covering spaces are stable under restriction, finite products, and pullback.
Covering spaces are stable under restriction, finite products, and pullback
Statement
Restrictions of coverings to open subspaces, finite products of coverings, and pullbacks of coverings are covering maps. The empty product is the identity covering of a one-point space.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
For a covering and a continuous map , define with the subspace topology, and let be (def-product-topology, def-subspace-topology-top). This is the pullback covering space; its covering property is proved in prop-covering-spaces-are-stable-under-restriction-finite-products-and-pullback. (The pullback of a covering space along a continuous map).
A covering map is a continuous surjection such that every has an open neighbourhood for which is a disjoint union of open sets , called sheets, and each restriction is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a is evenly covered, and is the fibre over . A covering is trivial when it is isomorphic over to a product projection with discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).
The product set. Let be a set and let be a set for each . The product is and we write , the -th coordinate of . Two elements of the product are equal exactly when they agree at every index, functions being equal when they have the same domain and the same values. For the -th projection is . The product topology on is the initial topology of the projections: the topology generated by the subbasis . Finite intersections of subbasic sets form a basis for it, and they are exactly the boxes with every open in and for all but finitely many . (The product set of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).
Let be a topological space (def-topological-space) and let . The subspace topology (also relative topology) on is the family of traces on of the open sets of . The pair is a subspace of . A subset of that lies in is said to be open in , and relatively open where the ambient space needs emphasis. (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).
Proof
Restrict an evenly covered neighbourhood for restriction, take products of evenly covered neighbourhoods for finite products, and identify each pullback sheet with the corresponding open subset of the new base.
The preceding construction and implications establish the assertion.
A composite of covering maps is a covering when the outer covering is finite-sheeted
Statement
If and are covering maps and is finite-sheeted, then is a covering map.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
A covering map is a continuous surjection such that every has an open neighbourhood for which is a disjoint union of open sets , called sheets, and each restriction is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a is evenly covered, and is the fibre over . A covering is trivial when it is isomorphic over to a product projection with discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).
Proof
For coverings and , evenly cover a neighbourhood of for .
There are only finitely many resulting -sheets.
Around the unique point of each such sheet over , choose a smaller neighbourhood evenly covered by ; intersect their finitely many images downstairs and restrict all sheets to that common neighbourhood.
The resulting two-level sheets evenly cover the composite.
Separate the empty base case, and record that the finite-sheet hypothesis is what permits the common intersection.
The preceding construction and implications establish the assertion.
The monodromy right action on a covering fibre and its equivalent left-action convention
Definition
Fix a covering , a basepoint , and . For , define as the endpoint of the unique lift of beginning at (Existence and uniqueness of path lifts through a covering map). Endpoint homotopy invariance makes this well defined (The endpoint of a lifted path depends only on its endpoint-fixed homotopy class). With the library's traversal-order product this is a right action; the corresponding left action is (Left group actions, transitive actions, and faithful actions).
Monodromy acts by fibre bijections, and its orbits are the intersections of path components with the fibre
Statement
Monodromy acts on each covering fibre by bijections. Its orbit through is exactly the intersection of the path component of with that fibre.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
Fix a covering , a basepoint , and . For , define as the endpoint of the unique lift of beginning at (thm-path-lifting-for-covering-maps). Endpoint homotopy invariance makes this well defined (cor-lifted-path-endpoints-depend-only-on-path-homotopy). With the library's traversal-order product this is a right action; the corresponding left action is (def-group-action). (The monodromy right action on a covering fibre and its equivalent left-action convention).
For every pointed topological space , the product is well defined and makes a group. Its identity is the class of the constant loop , and . (Loop classes form the group under concatenation).
Throughout, (def-interval) carries the subspace topology inherited from with its usual topology (def-subspace-topology-top, lem-real-line-is-a-metric-space, def-metric-topology, def-metrizable-space). It is called the unit interval. A path in from to is a continuous map with and , where carries the subspace topology inherited from ; is path-connected when any two of its points are joined by such a path. (Paths, path-connected spaces and path components).
Proof
Path reversal gives the inverse endpoint permutation and concatenation gives the right-action law under the library's convention that traverses first.
A lifted loop is a path upstairs joining its starting and endpoint fibre points.
Conversely, project any path upstairs between fibre points to a loop downstairs.
Thus transitivity is equivalent to path-connectedness of the relevant covering component.
The preceding construction and implications establish the assertion.
Deck transformations and the deck-transformation group of a covering
Definition
For a covering , a deck transformation is an isomorphism over , so (Maps and isomorphisms of covering spaces over a fixed base). Deck transformations form the deck group under composition, and this group acts on by evaluation (Group and abelian group, Left group actions, transitive actions, and faithful actions).
On a connected covering space, a deck transformation is determined by one point and the deck action is free
Statement
For a covering with connected total space, two deck transformations agreeing at one point are equal. Consequently the deck group acts freely on the total space.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
For a covering , a deck transformation is an isomorphism over , so (def-map-and-isomorphism-of-covering-spaces). Deck transformations form the deck group under composition, and this group acts on by evaluation (def-group, def-group-action). (Deck transformations and the deck-transformation group of a covering).
Let be connected and let be lifts through the same covering of the same map . If for some , then . (Two lifts from a connected space that agree at one point agree everywhere).
A left action of a group on a set (def-group-action) is free when for every and . Equivalently, no nonidentity element of fixes any point of . (A free group action has no nonidentity element fixing a point).
Proof
Two deck transformations are lifts of the same projection.
If they agree at one point, uniqueness of lifts from the connected total space makes them equal.
Applying this to a deck transformation and the identity shows that a fixed point forces the transformation to be the identity.
The preceding construction and implications establish the assertion.
Covering-space actions by disjoint translates of neighbourhoods
Definition
A left action of a group on a space by homeomorphisms is a covering-space action when every has an open neighbourhood such that for every nonidentity (Left group actions, transitive actions, and faithful actions, Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological). Acting by homeomorphisms means that each map is a homeomorphism of ; the underlying set action alone would not make the translates open. This condition implies freeness (A free group action has no nonidentity element fixing a point) and makes the translates of pairwise disjoint.
The orbit map of a covering-space action is a covering, with the acting group equal to the deck group when the total space is path-connected
Statement
For a covering-space action of on , the orbit map is a covering. If is path-connected, the deck group of this covering consists exactly of the transformations supplied by .
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
A left action of a group on a space by homeomorphisms is a covering-space action when every has an open neighbourhood such that for every nonidentity (def-group-action, def-homeomorphism-and-open-maps). Acting by homeomorphisms means that each map is a homeomorphism of ; the underlying set action alone would not make the translates open. This condition implies freeness (def-free-group-action) and makes the translates of pairwise disjoint. (Covering-space actions by disjoint translates of neighbourhoods).
A covering map is a continuous surjection such that every has an open neighbourhood for which is a disjoint union of open sets , called sheets, and each restriction is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a is evenly covered, and is the fibre over . A covering is trivial when it is isomorphic over to a product projection with discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).
The quotient topology. Let be a topological space (def-topological-space), let be a set and let be a surjection (def-injection-surjection-bijection). The quotient topology on induced by is the final topology of the one-element family (def-initial-and-final-topology): That this is a topology is discharged in def-initial-and-final-topology, where every final topology is verified to satisfy (T1), (T2) and (T3). Dually, is closed in exactly when is closed in , because . (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection).
For a covering , a deck transformation is an isomorphism over , so (def-map-and-isomorphism-of-covering-spaces). Deck transformations form the deck group under composition, and this group acts on by evaluation (def-group, def-group-action). (Deck transformations and the deck-transformation group of a covering).
For a covering with connected total space, two deck transformations agreeing at one point are equal. Consequently the deck group acts freely on the total space. (On a connected covering space, a deck transformation is determined by one point and the deck action is free).
Let and be topological spaces and let be continuous (def-continuous-map-top). Each of the following three conditions makes a quotient map (def-quotient-topology). 1. is a surjection and an open map (def-homeomorphism-and-open-maps). 2. is a surjection and a closed map. 3. admits a continuous section: a continuous with . (Surjectivity of is then automatic and need not be assumed.) Neither clause 1 nor clause 2 is necessary: a quotient map need be neither open nor closed. A witness that is a quotient map by clause 3 while failing clauses 1 and 2 is worked on the companion page, and is named in the remarks below. (A continuous open surjection, a continuous closed surjection, and a continuous surjection admitting a continuous section are all quotient maps).
Proof
Let be a neighbourhood whose nonidentity translates are disjoint. Each acts by a homeomorphism of by [F1], so every translate is open, and the full preimage of the orbit image of is , a disjoint union of open sets. That preimage being open makes the orbit image open in the quotient topology of [F3], and the orbit map is then an open continuous surjection, so [F6] applies to it.
Each translate maps homeomorphically onto that quotient neighbourhood.
The action is free automatically, and when is nonempty this embeds the acting group in the deck group: freeness makes force , so distinct group elements give distinct translates. The nonemptiness is needed — on every translate is the identity, so a nontrivial does not embed.
If the total space is path-connected, compare any deck transformation at one point with the unique group translate taking that point to its image; one-point determination then proves equality with that translate.
The preceding construction and implications establish the assertion.
Local path-connectedness lifts and descends along covering maps
Statement
For a covering , the total space is locally path-connected if and only if the base is locally path-connected.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
A covering map is a continuous surjection such that every has an open neighbourhood for which is a disjoint union of open sets , called sheets, and each restriction is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a is evenly covered, and is the fibre over . A covering is trivial when it is isomorphic over to a product projection with discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).
Let be a topological space (def-topological-space) and let . Subsets carry the subspace topology (def-subspace-topology-top); connectedness is def-connected-space and path-connectedness is def-path-connected. is locally connected at when for every open with there is an open connected with , and locally connected when this holds at every point; is locally path-connected at when for every open with there is an open path-connected with , and locally path-connected when this holds at every point. (Locally connected and locally path-connected spaces: a neighbourhood base of open connected, respectively open path-connected, sets at every point).
Let and be topological spaces and let be a function. Continuity is as in def-continuous-map-top, injections, surjections and bijections as in def-injection-surjection-bijection. is an open map if is open in for every open , a closed map if is closed in for every closed , and a homeomorphism if is a continuous bijection whose inverse is also continuous; the spaces are homeomorphic when such an exists. (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).
Proof
Every point has a sheet homeomorphic to an open neighbourhood of its image.
Local path-connectedness passes to open subspaces and across homeomorphisms, which proves both directions using surjectivity to choose a point over each basepoint.
The preceding construction and implications establish the assertion.
Semilocally simply connected spaces with explicit basepoint convention
Definition
A space is semilocally simply connected at when there is a neighbourhood of and a basepoint-preserving inclusion whose induced map on fundamental groups is trivial (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open, The homomorphism on fundamental groups induced by a pointed continuous map, Based loops and the fundamental group). It is semilocally simply connected when this holds at every point. The neighbourhood need not itself be simply connected.
Universal covering spaces
Definition
A universal covering space of is a covering map whose total space is simply connected (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings, Simply connected topological spaces).
A space admitting a universal covering is semilocally simply connected
Statement
If a space admits a universal covering, then it is semilocally simply connected. No local path-connectedness hypothesis is required.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
A universal covering space of is a covering map whose total space is simply connected (def-covering-map-and-evenly-covered-neighbourhoods, def-simply-connected). (Universal covering spaces).
A space is semilocally simply connected at when there is a neighbourhood of and a basepoint-preserving inclusion whose induced map on fundamental groups is trivial (def-neighbourhood-top, def-induced-homomorphism-on-fundamental-groups, def-based-loops-and-fundamental-group). It is semilocally simply connected when this holds at every point. The neighbourhood need not itself be simply connected. (Semilocally simply connected spaces with explicit basepoint convention).
For a covering , the induced homomorphism is injective. (A covering map induces an injective homomorphism on fundamental groups).
A topological space is simply connected when it is nonempty and path-connected (def-path-connected) and, for every , the group has exactly one element. (Simply connected topological spaces).
Proof
At a basepoint choose an evenly covered neighbourhood and a lift of that point.
Any loop in the neighbourhood lifts to a loop in its sheet.
The induced fundamental-group map of the universal cover is injective and its domain group is trivial, so the inclusion-induced class downstairs is trivial.
No local path-connectedness is needed for this necessity direction.
The preceding construction and implications establish the assertion.
The based path-class model and basic sets for a universal cover
Definition
Fix a path-connected space and . Let be the set of endpoint-fixed homotopy classes of paths beginning at , and put . If is an open path-connected neighbourhood of on which the inclusion-induced fundamental-group map is trivial, define to consist of the classes with a path in beginning at . These sets are the proposed basic neighbourhoods for the path-class model (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints, Semilocally simply connected spaces with explicit basepoint convention, Paths, path-connected spaces and path components).
For a nonempty path-connected locally path-connected semilocally simply connected space, the path-class projection is a covering map
Statement
If is nonempty, path-connected, locally path-connected, and semilocally simply connected, then after a basepoint is fixed the path-class basic sets define a topology on for which the endpoint projection is a covering map.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
Fix a path-connected space and . Let be the set of endpoint-fixed homotopy classes of paths beginning at , and put . If is an open path-connected neighbourhood of on which the inclusion-induced fundamental-group map is trivial, define to consist of the classes with a path in beginning at . These sets are the proposed basic neighbourhoods for the path-class model (def-homotopy-relative-and-path-homotopy, def-semilocally-simply-connected-space, def-path-connected). (The based path-class model and basic sets for a universal cover).
A covering map is a continuous surjection such that every has an open neighbourhood for which is a disjoint union of open sets , called sheets, and each restriction is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a is evenly covered, and is the fibre over . A covering is trivial when it is isomorphic over to a product projection with discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).
A space is semilocally simply connected at when there is a neighbourhood of and a basepoint-preserving inclusion whose induced map on fundamental groups is trivial (def-neighbourhood-top, def-induced-homomorphism-on-fundamental-groups, def-based-loops-and-fundamental-group). It is semilocally simply connected when this holds at every point. The neighbourhood need not itself be simply connected. (Semilocally simply connected spaces with explicit basepoint convention).
Let be a topological space (def-topological-space) and let . Subsets carry the subspace topology (def-subspace-topology-top); connectedness is def-connected-space and path-connectedness is def-path-connected. is locally connected at when for every open with there is an open connected with , and locally connected when this holds at every point; is locally path-connected at when for every open with there is an open path-connected with , and locally path-connected when this holds at every point. (Locally connected and locally path-connected spaces: a neighbourhood base of open connected, respectively open path-connected, sets at every point).
Proof
Refine each semilocally simply connected neighbourhood to an open path-connected one.
For a path class ending at its centre, append paths in that neighbourhood to obtain a basic sheet.
Triviality of the inclusion-induced fundamental group makes the endpoint description independent of the appended path, and distinct initial classes give disjoint sheets.
Verify that these basic sets form a topology and map homeomorphically onto the chosen neighbourhood.
The preceding construction and implications establish the assertion.
Every nonempty path-connected locally path-connected semilocally simply connected space has a universal cover
Statement
Every nonempty path-connected, locally path-connected, semilocally simply connected space has a universal covering space.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
If is nonempty, path-connected, locally path-connected, and semilocally simply connected, then after a basepoint is fixed the path-class basic sets define a topology on for which the endpoint projection is a covering map. (For a nonempty path-connected locally path-connected semilocally simply connected space, the path-class projection is a covering map).
A universal covering space of is a covering map whose total space is simply connected (def-covering-map-and-evenly-covered-neighbourhoods, def-simply-connected). (Universal covering spaces).
A topological space is simply connected when it is nonempty and path-connected (def-path-connected) and, for every , the group has exactly one element. (Simply connected topological spaces).
For a covering , the induced homomorphism is injective. (A covering map induces an injective homomorphism on fundamental groups).
Proof
Use the path-class projection, already proved to be a covering.
The path-class space is nonempty and path-connected by truncating representatives.
A loop upstairs projects to a loop whose path-class endpoint is the starting class, hence to the trivial element downstairs; injectivity of the fundamental-group map then makes every upstairs loop nullhomotopic.
Thus the total space is simply connected.
The preceding construction and implications establish the assertion.
For a path-connected locally path-connected base, a universal cover maps uniquely over the base to every connected covering, and any two universal covers are uniquely isomorphic
Statement
Let be path-connected and locally path-connected. After basepoints over the same point are fixed, a universal cover of admits a unique based continuous map over to every connected covering of ; in particular any two universal covers of are uniquely isomorphic over .
The map to a connected covering is asserted here only as a continuous map over the base. The classical stronger form, that this map is itself a covering map, needs a surjectivity argument and evenly covered neighbourhoods for it, and is not established on this page.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
A universal covering space of is a covering map whose total space is simply connected (def-covering-map-and-evenly-covered-neighbourhoods, def-simply-connected). (Universal covering spaces).
Let be path-connected and locally path-connected, let be based, and let be a covering. A based lift exists if and only if ; when it exists it is unique. (Lifting criterion for maps from path-connected locally path-connected spaces).
Let be connected and let be lifts through the same covering of the same map . If for some , then . (Two lifts from a connected space that agree at one point agree everywhere).
For a covering , the total space is locally path-connected if and only if the base is locally path-connected. (Local path-connectedness lifts and descends along covering maps).
Proof
Let the base be path-connected and locally path-connected and fix points over a common basepoint.
By [F1] the total space of a universal cover is simply connected, so its fundamental group is trivial and the subgroup condition of [F2] holds for any target covering. [F2] therefore supplies a based lift to any connected covering, and asserts that lift to be unique. What [F2] delivers is a continuous map over the base; it carries no covering-map conclusion, and no later step supplies one.
Applying this in both directions between two universal covers and using uniqueness of lifts makes the composites identities.
The preceding construction and implications establish the assertion.
A connected covering of a locally path-connected simply connected space is one-sheeted and trivial
Statement
Every connected covering of a locally path-connected simply connected space is one-sheeted and isomorphic to the identity covering.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
For a covering , the total space is locally path-connected if and only if the base is locally path-connected. (Local path-connectedness lifts and descends along covering maps).
Endpoint-fixed homotopic paths in the base have lifts with the same endpoint whenever their lifts begin at the same point. (The endpoint of a lifted path depends only on its endpoint-fixed homotopy class).
A topological space is simply connected when it is nonempty and path-connected (def-path-connected) and, for every , the group has exactly one element. (Simply connected topological spaces).
A covering map is a continuous surjection such that every has an open neighbourhood for which is a disjoint union of open sets , called sheets, and each restriction is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a is evenly covered, and is the fibre over . A covering is trivial when it is isomorphic over to a product projection with discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).
Proof
Local path-connectedness lifts to the connected total space, making it path-connected.
If two points lie in one fibre, join them upstairs; the projected loop is null-homotopic because the base is simply connected, while endpoint homotopy invariance forces its lift to have the same initial and final point.
Thus every fibre is a singleton, and a one-sheeted covering is a homeomorphism by its local sheet descriptions.
The preceding construction and implications establish the assertion.
For a nonempty path-connected total space, a covering fibre is in bijection with the right cosets of the induced fundamental-group subgroup
Statement
For a covering with nonempty path-connected total space, put . With traversal-order multiplication, the fibre is in bijection with the set of right cosets . Thus its finite number of sheets equals the subgroup index, and one is infinite exactly when the other is recorded as .
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
Fix a covering , a basepoint , and . For , define as the endpoint of the unique lift of beginning at (thm-path-lifting-for-covering-maps). Endpoint homotopy invariance makes this well defined (cor-lifted-path-endpoints-depend-only-on-path-homotopy). With the library's traversal-order product this is a right action; the corresponding left action is (def-group-action). (The monodromy right action on a covering fibre and its equivalent left-action convention).
For a covering , the induced homomorphism is injective. (A covering map induces an injective homomorphism on fundamental groups).
Monodromy acts on each covering fibre by bijections. Its orbit through is exactly the intersection of the path component of with that fibre. (Monodromy acts by fibre bijections, and its orbits are the intersections of path components with the fibre).
Let be a group and let be a subgroup (def-group, def-subgroup). For , the left coset and right coset of represented by are The element is a representative of these cosets. The notation denotes subsets of ; it does not assert that either subset is a subgroup. (Left and right cosets and of a subgroup).
Let . The left coset set is By lem-coset-partition, its elements are exactly the blocks of the coset partition of . The index of in is when is finite, with finite cardinality as in def-finite-cardinality. If is not finite, write . Here is a symbol, not a natural number, and no arithmetic with it is defined. The right coset set has the same finite or infinite size, because lem-left-and-right-cosets-equinumerous gives an explicit bijection between the two coset sets; thus the index does not depend on choosing left rather than right cosets. (The coset set and the index of a subgroup).
Proof
Fix a point in the fibre.
Send a loop class to the endpoint of its lifted path.
Endpoint homotopy invariance makes this well defined; with traversal-order multiplication, two classes have the same endpoint exactly when their quotient lies in the image of the upstairs fundamental group, and holds exactly when . By the convention of [F4] the sets are right cosets, so the fibres of the endpoint map are precisely the members of .
Path-connectedness of the total space gives surjectivity onto the fibre.
Translate the bijection into the published index convention. That convention defines from the left coset set , so use the clause of [F5] giving an explicit bijection between the left and right coset sets: and have the same finite or infinite size. Composing with step 4.1, the finite cardinalities agree with the number of sheets, and one side is infinite exactly when the other is recorded as .
The preceding construction and implications establish the assertion.
For a finite-sheeted covering, the total space is compact exactly when the base is compact
Statement
If is a finite-sheeted covering, then is compact if and only if is compact.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
A covering map is a continuous surjection such that every has an open neighbourhood for which is a disjoint union of open sets , called sheets, and each restriction is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a is evenly covered, and is the fibre over . A covering is trivial when it is isomorphic over to a product projection with discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).
Let be a topological space (def-topological-space). An open cover of is a family of open sets with ; a subcover of is a subfamily that is itself an open cover; and is compact when every open cover of it has a finite subcover. (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).
Let and be topological spaces (def-topological-space), and let carry its usual topology, the metric topology of (lem-real-line-is-a-metric-space, def-metric-topology, def-metrizable-space). Then: 1. Continuous images. If is continuous (def-continuous-map-top) and is compact (def-compact-space), then is a compact subset of . More generally, if is a compact subset of then is a compact subset of . 2. Extreme values. If is compact and nonempty and is continuous, then has a maximum and a minimum (def-max-min): there are with 3. Compact to Hausdorff. If is compact, is Hausdorff (def-hausdorff-space) and is a continuous bijection, then is a homeomorphism (def-homeomorphism-and-open-maps). Nonemptiness in claim 2 is a hypothesis and not an oversight: for the image is empty and has neither a maximum nor a minimum. No choice principle is used: the one selection made below is over a finite index set, where lem-finite-choice is a theorem of ZF. (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).
Proof
The forward direction is the continuous image theorem and uses surjectivity.
For the reverse direction, call an open adapted to a given open cover upstairs when is evenly covered and every sheet above lies in a single member of that cover. Because each fibre is finite, every point of lies in some adapted : take an evenly covered neighbourhood, and shrink it finitely many times, once per sheet. Let be the set of all adapted open sets, formed outright rather than by selecting one per basepoint, so no choice principle is used.
covers , so the finite-subcover clause of [F2] supplies finitely many members of covering ; each contributes finitely many sheets, each inside one cover member, so finitely many cover members exhaust the total space.
The preceding construction and implications establish the assertion.
For a path-connected locally path-connected semilocally simply connected base, the deck group of a universal cover is isomorphic to the fundamental group
Statement
For a path-connected, locally path-connected, semilocally simply connected base , the deck group of a universal cover is isomorphic to . With the library's traversal-order path product the monodromy action is a right action, and the assignment carrying a loop class to the deck transformation that moves the chosen point of the fibre to the corresponding lifted endpoint is itself an isomorphism; no path reversal is inserted.
Facts & Assumptions
Given: The objects, hypotheses, and choice principles stated above.
For a covering , a deck transformation is an isomorphism over , so (def-map-and-isomorphism-of-covering-spaces). Deck transformations form the deck group under composition, and this group acts on by evaluation (def-group, def-group-action). (Deck transformations and the deck-transformation group of a covering).
Fix a covering , a basepoint , and . For , define as the endpoint of the unique lift of beginning at (thm-path-lifting-for-covering-maps). Endpoint homotopy invariance makes this well defined (cor-lifted-path-endpoints-depend-only-on-path-homotopy). With the library's traversal-order product this is a right action; the corresponding left action is (def-group-action). (The monodromy right action on a covering fibre and its equivalent left-action convention).
Let be path-connected and locally path-connected. After basepoints over the same point are fixed, a universal cover of admits a unique based continuous map over to every connected covering of ; in particular any two universal covers of are uniquely isomorphic over . (For a path-connected locally path-connected base, a universal cover maps uniquely over the base to every connected covering, and any two universal covers are uniquely isomorphic).
For a covering with connected total space, two deck transformations agreeing at one point are equal. Consequently the deck group acts freely on the total space. (On a connected covering space, a deck transformation is determined by one point and the deck action is free).
For every pointed topological space , the product is well defined and makes a group. Its identity is the class of the constant loop , and . (Loop classes form the group under concatenation).
Proof
For a path-connected locally path-connected semilocally simply connected base and a chosen point upstairs, each loop class determines the endpoint of its lift.
The universal-cover lifting criterion gives the unique deck transformation taking the chosen point to that endpoint.
Because the library multiplies loops in traversal order, [F2] makes the monodromy a right action, and no path reversal is needed. A deck transformation satisfies : since , composing with the lift of a loop starting at gives a lift of that loop starting at , and lifts from a given point are unique, so the endpoints correspond. Writing for the deck transformation of step 2.1 with , this gives , so and agree at and [F4] makes them equal. Hence is a homomorphism as it stands; assigning inverse classes instead would reverse products and give an antihomomorphism.
For injectivity, suppose two loop classes give the same lifted endpoint. Their quotient then fixes the chosen point of the fibre, so it lies in the stabiliser of that point under the monodromy action [F2]. That stabiliser is the image of the upstairs fundamental group, which is trivial because the total space of a universal cover is simply connected; so the two classes are equal. Freeness of the deck action then makes the induced assignment injective as a map of groups, and path-connectedness of the total space gives surjectivity.
The preceding construction and implications establish the assertion.
5 · Examples, counterexamples and false statements
None yet.
Sources
Standard references
Recommended treatments; not extraction sources.