Alphabeta Math
Session-authored (Fable 5 assisted)
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.

22 results · all verified · 4 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 18 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Covering Spaces and Lifting

1 · Prerequisites

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

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-16Open item page →

Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings

Definition

A covering map is a continuous surjection p:EB such that every bB has an open neighbourhood U for which p1(U) is a disjoint union of open sets Vj, called sheets, and each restriction pVj:VjU 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) iXi with the final topology of the canonical injections: a set is open exactly when each of its traces is). Such a U is evenly covered, and p1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×FB with F discrete.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Maps and isomorphisms of covering spaces over a fixed base

Definition

For coverings p:EB and q:FB, a map of covering spaces over B is a continuous map h:EF with qh=p. It is an isomorphism of covering spaces when h is a homeomorphism; its inverse is then also over B (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).

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Lifts of maps, paths, and homotopies through a covering map

Definition

Let p:EB be a covering and f:YB continuous. A lift of f through p is a continuous map f~:YE with pf~=f. This includes lifts of paths IB and of homotopies Y×IB; an initial lift prescribes the restriction at time 0 (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints, Paths, path-connected spaces and path components).

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

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.

[F1]

A covering map is a continuous surjection p:EB such that every bB has an open neighbourhood U for which p1(U) is a disjoint union of open sets Vj, called sheets, and each restriction pVj:VjU is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a U is evenly covered, and p1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×FB with F discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F2]

Let (X,TX) and (Y,TY) be topological spaces and let f:XY be a function. Continuity is as in def-continuous-map-top, injections, surjections and bijections as in def-injection-surjection-bijection. f is an open map if f[U] is open in Y for every open UX, a closed map if f[F] is closed in Y for every closed FX, and a homeomorphism if f is a continuous bijection whose inverse f1:YX is also continuous; the spaces are homeomorphic when such an f exists. (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

[F3]

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 X be a set. The six families below are topologies on X; that each really satisfies (T1), (T2) and (T3) is discharged in full after the list. Among those six is the discrete topology Tdisc:=P(X), in which every subset is open and hence every subset is also closed. (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies).

Proof

technique · direct
1.1

An evenly covered neighbourhood restricts the projection to a homeomorphism on each sheet, which gives the local-homeomorphism property.

givenF1F2F3
2.1

Intersect a sheet with a fibre to isolate its unique point.

step 1.1F1
3.1

Keep surjectivity as part of the covering-map definition rather than infer it from local data.

step 2.1F1
4.1

The preceding construction and implications establish the assertion.

step 3.1
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

The cardinality of a covering fibre is locally constant and is constant on a connected base

Statement

For a covering p:EB, the cardinality of p1(b) is locally constant as a function of bB. If B is connected, all fibres are equinumerous.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

A covering map is a continuous surjection p:EB such that every bB has an open neighbourhood U for which p1(U) is a disjoint union of open sets Vj, called sheets, and each restriction pVj:VjU is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a U is evenly covered, and p1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×FB with F discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F2]

Let (X,T) be a topological space (def-topological-space). A separation of X is an ordered pair (U,V) of open, nonempty, disjoint subsets of X with UV=X; X is disconnected when a separation of X exists and connected when none does. Since U and V are complementary each is clopen, so a separation is the same thing as a partition of X into two nonempty clopen pieces. A subset AX is a connected subset when the subspace (A,TA) is connected. (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).

[F3]

Let A and B be sets (def-injection-surjection-bijection for the terminology). A and B are equinumerous, written AB, if there exists a bijection f:AB; A is dominated by B, written AB, if there exists an injection f:AB. (Equinumerous sets, AB and AB).

Proof

technique · direct
1.1

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.

givenF1F3F2
2.1

The subsets on which a fixed fibre cardinal occurs are open; connectedness permits only one nonempty such subset.

step 1.1F1
3.1

The preceding construction and implications establish the assertion.

step 2.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Existence and uniqueness of path lifts through a covering map

Statement

Let p:EB be a covering, let α:IB be a path, and let e0E satisfy p(e0)=α(0). There is a unique path α~:IE with α~(0)=e0 and pα~=α.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

Let p:EB be a covering and f:YB continuous. A lift of f through p is a continuous map f~:YE with pf~=f. This includes lifts of paths IB and of homotopies Y×IB; an initial lift prescribes the restriction at time 0 (def-homotopy-relative-and-path-homotopy, def-path-connected). (Lifts of maps, paths, and homotopies through a covering map).

[F2]

Let (X,d) be a compact metric space (def-metric-compactness, def-metric-space) and let U be an open cover of X. Then there is a real δ>0, a Lebesgue number for U, such that every nonempty AX with diam(A)<δ (def-metric-bounded-diameter) satisfies AU for some UU. Diameters of nonempty subsets of X 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 δ>0 such that every nonempty subset of diameter less than δ lies inside a single member of the cover).

[F3]

Let X, Y and Z be topological spaces, with subspaces carrying the subspace topology (def-subspace-topology-top). Then: 1. Composites. If f:XY and g:YZ are continuous (def-continuous-map-top) then gf:XZ is continuous. 2. Open cover. Let f:XY be a function and let {Ui:iI} be a family of open subsets of X with iIUi=X. If fUi:UiY is continuous for every iI, then f is continuous. 3. Finite closed cover. Let f:XY be a function, let n1 and let F1,,Fn be closed subsets of X with F1Fn=X. If fFk:FkY is continuous for every k, then f 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).

[F4]

Let (X,T) be a topological space (def-topological-space). An open cover of (X,T) is a family UT of open sets with X=U; a subcover of U is a subfamily that is itself an open cover; and (X,T) 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

technique · direct
1.1

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.

givenF1F2F3F4
2.1

Agreement at subdivision endpoints gives a continuous pasted path; sheet uniqueness proves uniqueness, including constant paths.

step 1.1F3F1
3.1

The preceding construction and implications establish the assertion.

step 2.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Existence and uniqueness of homotopy lifts through a covering map

Statement

Let p:EB be a covering, H:Y×IB a homotopy, and H~0:YE a lift of H(,0). There is a unique lift H~:Y×IE of H extending H~0.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

Let p:EB be a covering and f:YB continuous. A lift of f through p is a continuous map f~:YE with pf~=f. This includes lifts of paths IB and of homotopies Y×IB; an initial lift prescribes the restriction at time 0 (def-homotopy-relative-and-path-homotopy, def-path-connected). (Lifts of maps, paths, and homotopies through a covering map).

[F2]

Let p:EB be a covering, let α:IB be a path, and let e0E satisfy p(e0)=α(0). There is a unique path α~:IE with α~(0)=e0 and pα~=α. (Existence and uniqueness of path lifts through a covering map).

[F3]

The product set. Let I be a set and let Xi be a set for each iI. The product is iIXi  :=  {x:x is a function with domain I and x(i)Xi for every iI}, and we write xi:=x(i), the i-th coordinate of x. 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 jI the j-th projection is πj:iIXiXj,πj(x):=xj.. The product topology TΠ on iXi is the initial topology of the projections: the topology generated by the subbasis {πi1[U]:iI, UTi}. Finite intersections of subbasic sets form a basis for it, and they are exactly the boxes iIUi with every Ui open in Xi and Ui=Xi for all but finitely many i. (The product set iIXi 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).

[F4]

Let X, Y and Z be topological spaces, with subspaces carrying the subspace topology (def-subspace-topology-top). Then: 1. Composites. If f:XY and g:YZ are continuous (def-continuous-map-top) then gf:XZ is continuous. 2. Open cover. Let f:XY be a function and let {Ui:iI} be a family of open subsets of X with iIUi=X. If fUi:UiY is continuous for every iI, then f is continuous. 3. Finite closed cover. Let f:XY be a function, let n1 and let F1,,Fn be closed subsets of X with F1Fn=X. If fFk:FkY is continuous for every k, then f 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).

[F5]

Let (X,T) be a topological space (def-topological-space). An open cover of (X,T) is a family UT of open sets with X=U; a subcover of U is a subfamily that is itself an open cover; and (X,T) 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

technique · direct
1.1

For a homotopy H:Y×IX 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 Y.

givenF1F2F5
2.1

Pasting gives a global lift, and the set of points where two lifts agree is open and closed on each vertical interval, yielding uniqueness.

step 1.1F1F4F3
3.1

The preceding construction and implications establish the assertion.

step 2.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

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.

[F1]

Let p:EB be a covering, H:Y×IB a homotopy, and H~0:YE a lift of H(,0). There is a unique lift H~:Y×IE of H extending H~0. (Existence and uniqueness of homotopy lifts through a covering map).

[F2]

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).

[F3]

Let (X,T) be a topological space (def-topological-space). A separation of X is an ordered pair (U,V) of open, nonempty, disjoint subsets of X with UV=X; X is disconnected when a separation of X exists and connected when none does. Since U and V are complementary each is clopen, so a separation is the same thing as a partition of X into two nonempty clopen pieces. A subset AX is a connected subset when the subspace (A,TA) is connected. (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).

Proof

technique · direct
1.1

Lift an endpoint-fixed homotopy starting from the chosen lift of one path.

givenF1F3
2.1

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.

step 1.1F2
3.1

The preceding construction and implications establish the assertion.

step 2.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

A covering map induces an injective homomorphism on fundamental groups

Statement

For a covering p:(E,e0)(B,b0), the induced homomorphism p:π1(E,e0)π1(B,b0) is injective.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

Let p:EB be a covering, H:Y×IB a homotopy, and H~0:YE a lift of H(,0). There is a unique lift H~:Y×IE of H extending H~0. (Existence and uniqueness of homotopy lifts through a covering map).

[F2]

Let f:XY be continuous and let x0X. Composition sends a loop α at x0 to the loop fα at f(x0). Using the loop classes and fundamental group of def-based-loops-and-fundamental-group, the proposed induced homomorphism is f:π1(X,x0)π1(Y,f(x0)),f([α]):=[fα]. 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).

[F3]

A topological space X is simply connected when it is nonempty and path-connected (def-path-connected) and, for every x0X, the group π1(X,x0) has exactly one element. (Simply connected topological spaces).

Proof

technique · direct
1.1

If a loop upstairs maps to a nullhomotopic loop downstairs, lift a nullhomotopy with the given loop as its initial edge.

givenF2F1F3
2.1

Uniqueness forces the opposite edge to be constant, yielding a nullhomotopy upstairs.

step 1.1F2
3.1

Preserve the chosen basepoints and the exact published definition of the induced map.

step 2.1F2
4.1

The preceding construction and implications establish the assertion.

step 3.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Two lifts from a connected space that agree at one point agree everywhere

Statement

Let Y be connected and let f,g:YE be lifts through the same covering of the same map YB. If f(y0)=g(y0) for some y0Y, then f=g.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

Let p:EB be a covering and f:YB continuous. A lift of f through p is a continuous map f~:YE with pf~=f. This includes lifts of paths IB and of homotopies Y×IB; an initial lift prescribes the restriction at time 0 (def-homotopy-relative-and-path-homotopy, def-path-connected). (Lifts of maps, paths, and homotopies through a covering map).

[F2]

Let (X,T) be a topological space (def-topological-space). A separation of X is an ordered pair (U,V) of open, nonempty, disjoint subsets of X with UV=X; X is disconnected when a separation of X exists and connected when none does. Since U and V are complementary each is clopen, so a separation is the same thing as a partition of X into two nonempty clopen pieces. A subset AX is a connected subset when the subspace (A,TA) is connected. (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).

[F3]

A covering map is a continuous surjection p:EB such that every bB has an open neighbourhood U for which p1(U) is a disjoint union of open sets Vj, called sheets, and each restriction pVj:VjU is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a U is evenly covered, and p1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×FB with F discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

Proof

technique · direct
1.1

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.

givenF3F1F2
2.1

Its complement is open by choosing disjoint sheets near a disagreement point.

step 1.1F3
3.1

Connectedness and the named agreement point force the equaliser to be the whole domain.

step 2.1F3
4.1

The preceding construction and implications establish the assertion.

step 3.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Lifting criterion for maps from path-connected locally path-connected spaces

Statement

Let Y be path-connected and locally path-connected, let f:(Y,y0)(B,b0) be based, and let p:(E,e0)(B,b0) be a covering. A based lift f~:(Y,y0)(E,e0) exists if and only if fπ1(Y,y0)pπ1(E,e0); when it exists it is unique.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

Let p:EB be a covering, let α:IB be a path, and let e0E satisfy p(e0)=α(0). There is a unique path α~:IE with α~(0)=e0 and pα~=α. (Existence and uniqueness of path lifts through a covering map).

[F2]

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).

[F3]

Let Y be connected and let f,g:YE be lifts through the same covering of the same map YB. If f(y0)=g(y0) for some y0Y, then f=g. (Two lifts from a connected space that agree at one point agree everywhere).

[F4]

Let f:XY be continuous and let x0X. Composition sends a loop α at x0 to the loop fα at f(x0). Using the loop classes and fundamental group of def-based-loops-and-fundamental-group, the proposed induced homomorphism is f:π1(X,x0)π1(Y,f(x0)),f([α]):=[fα]. 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).

[F5]

Let (X,T) be a topological space (def-topological-space) and let xX. Subsets carry the subspace topology (def-subspace-topology-top); connectedness is def-connected-space and path-connectedness is def-path-connected. X is locally connected at x when for every open U with xU there is an open connected V with xVU, and locally connected when this holds at every point; X is locally path-connected at x when for every open U with xU there is an open path-connected V with xVU, 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).

[F6]

Let f:(X,x0)(Y,y0) be continuous with f(x0)=y0. Then f([α])=[fα] is a well-defined group homomorphism, and for pointed continuous maps id=id and (gf)=gf (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

Proof

technique · direct
1.1

For a based map f:(Y,y0)(X,x0) with Y path-connected and locally path-connected, necessity follows by functoriality: if a based lift f~ exists then f=pf~, so f=pf~ by the composition law of [F6], whence fπ1(Y,y0)pπ1(E,e0). [F4] is the definition of the induced map and expressly leaves functoriality to [F6].

givenF5F1F2F4F6
2.1

For sufficiency, define the candidate lift at y by lifting f along any path from y0; the subgroup inclusion makes the endpoint independent of the chosen path.

step 1.1F1F2F5
3.1

Local path-connectedness and an evenly covered neighbourhood make the candidate continuous.

step 2.1F5F1F2
4.1

Uniqueness follows from connectedness.

step 3.1F3F5
5.1

The preceding construction and implications establish the assertion.

step 4.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

The pullback of a covering space along a continuous map

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

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.

[F1]

For a covering p:EB and a continuous map f:XB, define fE:={(x,e)X×E:f(x)=p(e)} with the subspace topology, and let fp:fEX be (x,e)x (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).

[F2]

A covering map is a continuous surjection p:EB such that every bB has an open neighbourhood U for which p1(U) is a disjoint union of open sets Vj, called sheets, and each restriction pVj:VjU is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a U is evenly covered, and p1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×FB with F discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F3]

The product set. Let I be a set and let Xi be a set for each iI. The product is iIXi  :=  {x:x is a function with domain I and x(i)Xi for every iI}, and we write xi:=x(i), the i-th coordinate of x. 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 jI the j-th projection is πj:iIXiXj,πj(x):=xj.. The product topology TΠ on iXi is the initial topology of the projections: the topology generated by the subbasis {πi1[U]:iI, UTi}. Finite intersections of subbasic sets form a basis for it, and they are exactly the boxes iIUi with every Ui open in Xi and Ui=Xi for all but finitely many i. (The product set iIXi 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).

[F4]

Let (X,T) be a topological space (def-topological-space) and let SX. The subspace topology (also relative topology) on S is TS:={US:UT}, the family of traces on S of the open sets of X. The pair (S,TS) is a subspace of X. A subset of S that lies in TS is said to be open in S, 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

technique · direct
1.1

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.

givenF2F1F4F3
2.1

The preceding construction and implications establish the assertion.

step 1.1
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

A composite of covering maps is a covering when the outer covering is finite-sheeted

Statement

If p:EB and q:BX are covering maps and q is finite-sheeted, then qp:EX is a covering map.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

A covering map is a continuous surjection p:EB such that every bB has an open neighbourhood U for which p1(U) is a disjoint union of open sets Vj, called sheets, and each restriction pVj:VjU is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a U is evenly covered, and p1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×FB with F discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

Proof

technique · direct
1.1

For coverings p:EB and q:BX, evenly cover a neighbourhood of x for q.

givenF1
2.1

There are only finitely many resulting q-sheets.

step 1.1F1
3.1

Around the unique point of each such sheet over x, choose a smaller neighbourhood evenly covered by p; intersect their finitely many images downstairs and restrict all sheets to that common neighbourhood.

step 2.1F1
4.1

The resulting two-level sheets evenly cover the composite.

step 3.1F1
5.1

Separate the empty base case, and record that the finite-sheet hypothesis is what permits the common intersection.

step 4.1F1
6.1

The preceding construction and implications establish the assertion.

step 5.1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-16Open item page →

The monodromy right action on a covering fibre and its equivalent left-action convention

Definition

Fix a covering p:EB, a basepoint b0B, and ep1(b0). For [α]π1(B,b0), define e[α] as the endpoint of the unique lift of α beginning at e (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 [α]e:=e[α]1 (Left group actions, transitive actions, and faithful actions).

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

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 e is exactly the intersection of the path component of e with that fibre.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

Fix a covering p:EB, a basepoint b0B, and ep1(b0). For [α]π1(B,b0), define e[α] as the endpoint of the unique lift of α beginning at e (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 [α]e:=e[α]1 (def-group-action). (The monodromy right action on a covering fibre and its equivalent left-action convention).

[F2]

For every pointed topological space (X,x0), the product [α][β]=[αβ] is well defined and makes π1(X,x0) a group. Its identity is the class of the constant loop cx0, and [α]1=[αˉ]. (Loop classes form the group π1(X,x0) under concatenation).

[F3]

Throughout, I:=[0,1]={tR:0t1} (def-interval) carries the subspace topology inherited from R 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 X from x to y is a continuous map γ:IX with γ(0)=x and γ(1)=y, where I:=[0,1] carries the subspace topology inherited from R; X is path-connected when any two of its points are joined by such a path. (Paths, path-connected spaces and path components).

Proof

technique · direct
1.1

Path reversal gives the inverse endpoint permutation and concatenation gives the right-action law under the library's convention that [α][β] traverses α first.

givenF1F2F3
2.1

A lifted loop is a path upstairs joining its starting and endpoint fibre points.

step 1.1F1F2F3
3.1

Conversely, project any path upstairs between fibre points to a loop downstairs.

step 2.1F1F2F3
4.1

Thus transitivity is equivalent to path-connectedness of the relevant covering component.

step 3.1F1F3
5.1

The preceding construction and implications establish the assertion.

step 4.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Deck transformations and the deck-transformation group of a covering

Definition

For a covering p:EB, a deck transformation is an isomorphism h:EE over B, so ph=p (Maps and isomorphisms of covering spaces over a fixed base). Deck transformations form the deck group Deck(p) under composition, and this group acts on E by evaluation (Group and abelian group, Left group actions, transitive actions, and faithful actions).

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

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.

[F1]

For a covering p:EB, a deck transformation is an isomorphism h:EE over B, so ph=p (def-map-and-isomorphism-of-covering-spaces). Deck transformations form the deck group Deck(p) under composition, and this group acts on E by evaluation (def-group, def-group-action). (Deck transformations and the deck-transformation group of a covering).

[F2]

Let Y be connected and let f,g:YE be lifts through the same covering of the same map YB. If f(y0)=g(y0) for some y0Y, then f=g. (Two lifts from a connected space that agree at one point agree everywhere).

[F3]

A left action of a group G on a set X (def-group-action) is free when gx=xg=e for every gG and xX. Equivalently, no nonidentity element of G fixes any point of X. (A free group action has no nonidentity element fixing a point).

Proof

technique · direct
1.1

Two deck transformations are lifts of the same projection.

givenF1F2
2.1

If they agree at one point, uniqueness of lifts from the connected total space makes them equal.

step 1.1F2F3
3.1

Applying this to a deck transformation and the identity shows that a fixed point forces the transformation to be the identity.

step 2.1F1F3
4.1

The preceding construction and implications establish the assertion.

step 3.1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-16Open item page →

Covering-space actions by disjoint translates of neighbourhoods

Definition

A left action of a group G on a space E by homeomorphisms is a covering-space action when every eE has an open neighbourhood U such that gUU= for every nonidentity gG (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 ege is a homeomorphism of E; the underlying set action alone would not make the translates gU open. This condition implies freeness (A free group action has no nonidentity element fixing a point) and makes the translates of U pairwise disjoint.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

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 G on E, the orbit map EE/G is a covering. If E is path-connected, the deck group of this covering consists exactly of the transformations supplied by G.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

A left action of a group G on a space E by homeomorphisms is a covering-space action when every eE has an open neighbourhood U such that gUU= for every nonidentity gG (def-group-action, def-homeomorphism-and-open-maps). Acting by homeomorphisms means that each map ege is a homeomorphism of E; the underlying set action alone would not make the translates gU open. This condition implies freeness (def-free-group-action) and makes the translates of U pairwise disjoint. (Covering-space actions by disjoint translates of neighbourhoods).

[F2]

A covering map is a continuous surjection p:EB such that every bB has an open neighbourhood U for which p1(U) is a disjoint union of open sets Vj, called sheets, and each restriction pVj:VjU is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a U is evenly covered, and p1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×FB with F discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F3]

The quotient topology. Let (X,T) be a topological space (def-topological-space), let Y be a set and let q:XY be a surjection (def-injection-surjection-bijection). The quotient topology on Y induced by q is the final topology of the one-element family (q) (def-initial-and-final-topology): Tq  :=  {VY:q1[V]T}. 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, CY is closed in Tq exactly when q1[C] is closed in X, because q1[YV]=Xq1[V]. (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection).

[F4]

For a covering p:EB, a deck transformation is an isomorphism h:EE over B, so ph=p (def-map-and-isomorphism-of-covering-spaces). Deck transformations form the deck group Deck(p) under composition, and this group acts on E by evaluation (def-group, def-group-action). (Deck transformations and the deck-transformation group of a covering).

[F5]

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).

[F6]

Let X and Y be topological spaces and let q:XY be continuous (def-continuous-map-top). Each of the following three conditions makes q a quotient map (def-quotient-topology). 1. q is a surjection and an open map (def-homeomorphism-and-open-maps). 2. q is a surjection and a closed map. 3. q admits a continuous section: a continuous s:YX with qs=idY. (Surjectivity of q 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

technique · direct
1.1

Let U be a neighbourhood whose nonidentity translates are disjoint. Each g acts by a homeomorphism of E by [F1], so every translate gU is open, and the full preimage of the orbit image of U is gGgU, 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.

givenF6F3F2F1
2.1

Each translate maps homeomorphically onto that quotient neighbourhood.

step 1.1F6F2F3
3.1

The action is free automatically, and when E is nonempty this embeds the acting group in the deck group: freeness makes ge=e force g=1, so distinct group elements give distinct translates. The nonemptiness is needed — on E= every translate is the identity, so a nontrivial G does not embed.

step 2.1F4F1F5
4.1

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.

step 3.1F4F5F1
5.1

The preceding construction and implications establish the assertion.

step 4.1
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Local path-connectedness lifts and descends along covering maps

Statement

For a covering p:EB, the total space E is locally path-connected if and only if the base B is locally path-connected.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

A covering map is a continuous surjection p:EB such that every bB has an open neighbourhood U for which p1(U) is a disjoint union of open sets Vj, called sheets, and each restriction pVj:VjU is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a U is evenly covered, and p1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×FB with F discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F2]

Let (X,T) be a topological space (def-topological-space) and let xX. Subsets carry the subspace topology (def-subspace-topology-top); connectedness is def-connected-space and path-connectedness is def-path-connected. X is locally connected at x when for every open U with xU there is an open connected V with xVU, and locally connected when this holds at every point; X is locally path-connected at x when for every open U with xU there is an open path-connected V with xVU, 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).

[F3]

Let (X,TX) and (Y,TY) be topological spaces and let f:XY be a function. Continuity is as in def-continuous-map-top, injections, surjections and bijections as in def-injection-surjection-bijection. f is an open map if f[U] is open in Y for every open UX, a closed map if f[F] is closed in Y for every closed FX, and a homeomorphism if f is a continuous bijection whose inverse f1:YX is also continuous; the spaces are homeomorphic when such an f exists. (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

Proof

technique · direct
1.1

Every point has a sheet homeomorphic to an open neighbourhood of its image.

givenF1F3
2.1

Local path-connectedness passes to open subspaces and across homeomorphisms, which proves both directions using surjectivity to choose a point over each basepoint.

step 1.1F1F2F3
3.1

The preceding construction and implications establish the assertion.

step 2.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Semilocally simply connected spaces with explicit basepoint convention

Definition

A space X is semilocally simply connected at xX when there is a neighbourhood U of x and a basepoint-preserving inclusion (U,x)(X,x) 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.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Universal covering spaces

Definition

A universal covering space of B is a covering map p:B~B whose total space B~ is simply connected (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings, Simply connected topological spaces).

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

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.

[F1]

A universal covering space of B is a covering map p:B~B whose total space B~ is simply connected (def-covering-map-and-evenly-covered-neighbourhoods, def-simply-connected). (Universal covering spaces).

[F2]

A space X is semilocally simply connected at xX when there is a neighbourhood U of x and a basepoint-preserving inclusion (U,x)(X,x) 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).

[F3]

For a covering p:(E,e0)(B,b0), the induced homomorphism p:π1(E,e0)π1(B,b0) is injective. (A covering map induces an injective homomorphism on fundamental groups).

[F4]

A topological space X is simply connected when it is nonempty and path-connected (def-path-connected) and, for every x0X, the group π1(X,x0) has exactly one element. (Simply connected topological spaces).

Proof

technique · direct
1.1

At a basepoint choose an evenly covered neighbourhood and a lift of that point.

givenF2F1
2.1

Any loop in the neighbourhood lifts to a loop in its sheet.

step 1.1F2
3.1

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.

step 2.1F2F3F1
4.1

No local path-connectedness is needed for this necessity direction.

step 3.1F4F2
5.1

The preceding construction and implications establish the assertion.

step 4.1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-16Open item page →

The based path-class model and basic sets for a universal cover

Definition

Fix a path-connected space X and x0X. Let X~ be the set of endpoint-fixed homotopy classes [α] of paths beginning at x0, and put p([α])=α(1). If U is an open path-connected neighbourhood of α(1) on which the inclusion-induced fundamental-group map is trivial, define B([α],U) to consist of the classes [αγ] with γ a path in U beginning at α(1). 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).

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

For a nonempty path-connected locally path-connected semilocally simply connected space, the path-class projection is a covering map

Statement

If X 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 X~ for which the endpoint projection p:X~X is a covering map.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

Fix a path-connected space X and x0X. Let X~ be the set of endpoint-fixed homotopy classes [α] of paths beginning at x0, and put p([α])=α(1). If U is an open path-connected neighbourhood of α(1) on which the inclusion-induced fundamental-group map is trivial, define B([α],U) to consist of the classes [αγ] with γ a path in U beginning at α(1). 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).

[F2]

A covering map is a continuous surjection p:EB such that every bB has an open neighbourhood U for which p1(U) is a disjoint union of open sets Vj, called sheets, and each restriction pVj:VjU is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a U is evenly covered, and p1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×FB with F discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F3]

A space X is semilocally simply connected at xX when there is a neighbourhood U of x and a basepoint-preserving inclusion (U,x)(X,x) 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).

[F4]

Let (X,T) be a topological space (def-topological-space) and let xX. Subsets carry the subspace topology (def-subspace-topology-top); connectedness is def-connected-space and path-connectedness is def-path-connected. X is locally connected at x when for every open U with xU there is an open connected V with xVU, and locally connected when this holds at every point; X is locally path-connected at x when for every open U with xU there is an open path-connected V with xVU, 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

technique · direct
1.1

Refine each semilocally simply connected neighbourhood to an open path-connected one.

givenF1F3F2F4
2.1

For a path class ending at its centre, append paths in that neighbourhood to obtain a basic sheet.

step 1.1F1F3F2
3.1

Triviality of the inclusion-induced fundamental group makes the endpoint description independent of the appended path, and distinct initial classes give disjoint sheets.

step 2.1F1F3F2
4.1

Verify that these basic sets form a topology and map homeomorphically onto the chosen neighbourhood.

step 3.1F1F2F3
5.1

The preceding construction and implications establish the assertion.

step 4.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

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.

[F1]

If X 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 X~ for which the endpoint projection p:X~X is a covering map. (For a nonempty path-connected locally path-connected semilocally simply connected space, the path-class projection is a covering map).

[F2]

A universal covering space of B is a covering map p:B~B whose total space B~ is simply connected (def-covering-map-and-evenly-covered-neighbourhoods, def-simply-connected). (Universal covering spaces).

[F3]

A topological space X is simply connected when it is nonempty and path-connected (def-path-connected) and, for every x0X, the group π1(X,x0) has exactly one element. (Simply connected topological spaces).

[F4]

For a covering p:(E,e0)(B,b0), the induced homomorphism p:π1(E,e0)π1(B,b0) is injective. (A covering map induces an injective homomorphism on fundamental groups).

Proof

technique · direct
1.1

Use the path-class projection, already proved to be a covering.

givenF1F2F3F4
2.1

The path-class space is nonempty and path-connected by truncating representatives.

step 1.1F1F3F2
3.1

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.

step 2.1F1F3F2
4.1

Thus the total space is simply connected.

step 3.1F2F3F1
5.1

The preceding construction and implications establish the assertion.

step 4.1
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

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 B be path-connected and locally path-connected. After basepoints over the same point are fixed, a universal cover of B admits a unique based continuous map over B to every connected covering of B; in particular any two universal covers of B are uniquely isomorphic over B.

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.

[F1]

A universal covering space of B is a covering map p:B~B whose total space B~ is simply connected (def-covering-map-and-evenly-covered-neighbourhoods, def-simply-connected). (Universal covering spaces).

[F2]

Let Y be path-connected and locally path-connected, let f:(Y,y0)(B,b0) be based, and let p:(E,e0)(B,b0) be a covering. A based lift f~:(Y,y0)(E,e0) exists if and only if fπ1(Y,y0)pπ1(E,e0); when it exists it is unique. (Lifting criterion for maps from path-connected locally path-connected spaces).

[F3]

Let Y be connected and let f,g:YE be lifts through the same covering of the same map YB. If f(y0)=g(y0) for some y0Y, then f=g. (Two lifts from a connected space that agree at one point agree everywhere).

[F4]

For a covering p:EB, the total space E is locally path-connected if and only if the base B is locally path-connected. (Local path-connectedness lifts and descends along covering maps).

Proof

technique · direct
1.1

Let the base be path-connected and locally path-connected and fix points over a common basepoint.

givenF4F2F1
2.1

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.

step 1.1F1F2F3
3.1

Applying this in both directions between two universal covers and using uniqueness of lifts makes the composites identities.

step 2.1F3F1F4
4.1

The preceding construction and implications establish the assertion.

step 3.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

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.

[F1]

For a covering p:EB, the total space E is locally path-connected if and only if the base B is locally path-connected. (Local path-connectedness lifts and descends along covering maps).

[F2]

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).

[F3]

A topological space X is simply connected when it is nonempty and path-connected (def-path-connected) and, for every x0X, the group π1(X,x0) has exactly one element. (Simply connected topological spaces).

[F4]

A covering map is a continuous surjection p:EB such that every bB has an open neighbourhood U for which p1(U) is a disjoint union of open sets Vj, called sheets, and each restriction pVj:VjU is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a U is evenly covered, and p1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×FB with F discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

Proof

technique · direct
1.1

Local path-connectedness lifts to the connected total space, making it path-connected.

givenF1F3F2
2.1

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.

step 1.1F2F3F1
3.1

Thus every fibre is a singleton, and a one-sheeted covering is a homeomorphism by its local sheet descriptions.

step 2.1F4F1F3
4.1

The preceding construction and implications establish the assertion.

step 3.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

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 p:(E,e0)(B,b0) with nonempty path-connected total space, put H=pπ1(E,e0). With traversal-order multiplication, the fibre p1(b0) is in bijection with the set of right cosets H\π1(B,b0)={H[α]:[α]π1(B,b0)}. 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.

[F1]

Fix a covering p:EB, a basepoint b0B, and ep1(b0). For [α]π1(B,b0), define e[α] as the endpoint of the unique lift of α beginning at e (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 [α]e:=e[α]1 (def-group-action). (The monodromy right action on a covering fibre and its equivalent left-action convention).

[F2]

For a covering p:(E,e0)(B,b0), the induced homomorphism p:π1(E,e0)π1(B,b0) is injective. (A covering map induces an injective homomorphism on fundamental groups).

[F3]

Monodromy acts on each covering fibre by bijections. Its orbit through e is exactly the intersection of the path component of e with that fibre. (Monodromy acts by fibre bijections, and its orbits are the intersections of path components with the fibre).

[F4]

Let G be a group and let HG be a subgroup (def-group, def-subgroup). For gG, the left coset and right coset of H represented by g are gH:={gh:hH},Hg:={hg:hH}. The element g is a representative of these cosets. The notation denotes subsets of G; it does not assert that either subset is a subgroup. (Left and right cosets gH and Hg of a subgroup).

[F5]

Let HG. The left coset set is G/H:={gH:gG}. By lem-coset-partition, its elements are exactly the blocks of the coset partition of G. The index of H in G is [G:H]:=G/H when G/H is finite, with finite cardinality as in def-finite-cardinality. If G/H is not finite, write [G:H]=. 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 G/H and the index [G:H] of a subgroup).

Proof

technique · direct
1.1

Fix a point in the fibre.

givenF3F1
2.1

Send a loop class to the endpoint of its lifted path.

step 1.1F1F3
3.1

Endpoint homotopy invariance makes this well defined; with traversal-order multiplication, two classes have the same endpoint exactly when their quotient [α][β]1 lies in the image H of the upstairs fundamental group, and [α][β]1H holds exactly when [β]H[α]. By the convention of [F4] the sets H[α] are right cosets, so the fibres of the endpoint map are precisely the members of H\π1(B,b0).

step 2.1F1F5F4F2
4.1

Path-connectedness of the total space gives surjectivity onto the fibre.

step 3.1F1F3
5.1

Translate the bijection into the published index convention. That convention defines [G:H] from the left coset set G/H, so use the clause of [F5] giving an explicit bijection between the left and right coset sets: H\π1(B,b0) and π1(B,b0)/H 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 .

step 4.1F5F3
6.1

The preceding construction and implications establish the assertion.

step 5.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

For a finite-sheeted covering, the total space is compact exactly when the base is compact

Statement

If p:EB is a finite-sheeted covering, then E is compact if and only if B is compact.

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

A covering map is a continuous surjection p:EB such that every bB has an open neighbourhood U for which p1(U) is a disjoint union of open sets Vj, called sheets, and each restriction pVj:VjU is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a U is evenly covered, and p1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×FB with F discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F2]

Let (X,T) be a topological space (def-topological-space). An open cover of (X,T) is a family UT of open sets with X=U; a subcover of U is a subfamily that is itself an open cover; and (X,T) 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).

[F3]

Let (X,TX) and (Y,TY) be topological spaces (def-topological-space), and let R carry its usual topology, the metric topology of dR(s,t)=st (lem-real-line-is-a-metric-space, def-metric-topology, def-metrizable-space). Then: 1. Continuous images. If f:XY is continuous (def-continuous-map-top) and (X,TX) is compact (def-compact-space), then f[X] is a compact subset of Y. More generally, if KX is a compact subset of X then f[K] is a compact subset of Y. 2. Extreme values. If (X,TX) is compact and nonempty and g:XR is continuous, then g[X] has a maximum and a minimum (def-max-min): there are xmax,xminX with g(xmin)    g(x)    g(xmax)for every xX. 3. Compact to Hausdorff. If (X,TX) is compact, (Y,TY) is Hausdorff (def-hausdorff-space) and f:XY is a continuous bijection, then f is a homeomorphism (def-homeomorphism-and-open-maps). Nonemptiness in claim 2 is a hypothesis and not an oversight: for X= 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

technique · direct
1.1

The forward direction is the continuous image theorem and uses surjectivity.

givenF3F1F2
2.1

For the reverse direction, call an open VB adapted to a given open cover upstairs when V is evenly covered and every sheet above V lies in a single member of that cover. Because each fibre is finite, every point of B lies in some adapted V: take an evenly covered neighbourhood, and shrink it finitely many times, once per sheet. Let V be the set of all adapted open sets, formed outright rather than by selecting one per basepoint, so no choice principle is used.

step 1.1F1F3
3.1

V covers B, so the finite-subcover clause of [F2] supplies finitely many members of V covering B; each contributes finitely many sheets, each inside one cover member, so finitely many cover members exhaust the total space.

step 2.1F1F2F3
4.1

The preceding construction and implications establish the assertion.

step 3.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16Open item page →

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 B, the deck group of a universal cover is isomorphic to π1(B,b0). 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.

[F1]

For a covering p:EB, a deck transformation is an isomorphism h:EE over B, so ph=p (def-map-and-isomorphism-of-covering-spaces). Deck transformations form the deck group Deck(p) under composition, and this group acts on E by evaluation (def-group, def-group-action). (Deck transformations and the deck-transformation group of a covering).

[F2]

Fix a covering p:EB, a basepoint b0B, and ep1(b0). For [α]π1(B,b0), define e[α] as the endpoint of the unique lift of α beginning at e (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 [α]e:=e[α]1 (def-group-action). (The monodromy right action on a covering fibre and its equivalent left-action convention).

[F3]

Let B be path-connected and locally path-connected. After basepoints over the same point are fixed, a universal cover of B admits a unique based continuous map over B to every connected covering of B; in particular any two universal covers of B are uniquely isomorphic over B. (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).

[F4]

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).

[F5]

For every pointed topological space (X,x0), the product [α][β]=[αβ] is well defined and makes π1(X,x0) a group. Its identity is the class of the constant loop cx0, and [α]1=[αˉ]. (Loop classes form the group π1(X,x0) under concatenation).

Proof

technique · direct
1.1

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.

givenF3F2F4F5
2.1

The universal-cover lifting criterion gives the unique deck transformation taking the chosen point to that endpoint.

step 1.1F1F3F4
3.1

Because the library multiplies loops in traversal order, [F2] makes the monodromy a right action, and no path reversal is needed. A deck transformation h satisfies h(xg)=h(x)g: since ph=p, composing h with the lift of a loop starting at x gives a lift of that loop starting at h(x), and lifts from a given point are unique, so the endpoints correspond. Writing ha for the deck transformation of step 2.1 with ha(e)=ea, this gives (hahb)(e)=ha(eb)=ha(e)b=(ea)b=e(ab)=hab(e), so hahb and hab agree at e and [F4] makes them equal. Hence aha is a homomorphism as it stands; assigning inverse classes instead would reverse products and give an antihomomorphism.

step 2.1F2F3F1F4
4.1

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.

step 3.1F2F3
5.1

The preceding construction and implications establish the assertion.

step 4.1

5 · Examples, counterexamples and false statements

None yet.

Sources