Alphabeta Math
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.

✓ 3 results · all verified · 1 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full by a delegated reviewing agent on the owner's instruction; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Covering Spaces and Lifting — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-09-26 (gpt-6-sol)Open item page →

Trivial coverings are products with a discrete fibre

Example

If X is any space and F is a nonempty discrete space, the projection X×F→X is a trivial covering with fibre F. If X=∅, the same holds for F=∅; for nonempty X, an empty fibre would violate surjectivity.

Facts & Assumptions

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

[F1]

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

[F2]

The product set. Let I be a set and let Xi be a set for each i∈I. The product is ∏i∈IXi  :=  { x:x is a function with domain I and x(i)∈Xi for every i∈I }, 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 j∈I the j-th projection is πj:∏i∈IXi→Xj,πj(x):=xj.. The product topology TΠ on ∏iXi is the initial topology of the projections: the topology generated by the subbasis {πi−1[U]:i∈I, U∈Ti}. Finite intersections of subbasic sets form a basis for it, and they are exactly the boxes ∏i∈IUi with every Ui open in Xi and Ui=Xi for all but finitely many i. (The product set ∏i∈IXi 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).

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

Verification

technique · direct
1.1givenF1F2F3

The projection p:X×F→X is continuous by the product topology. When F is nonempty, it is surjective. For every open U⊆X, p−1(U)=U×F=⨆f∈F(U×{f}). Each U×{f} is open because F is discrete, and p restricts to a homeomorphism from that sheet onto U, with inverse x↦(x,f). Hence every open U is evenly covered, as required by [F1].

2.1step 1.1F1F2

The fibre over x∈X is {x}×F, canonically identified with F. The identity map over X identifies this covering with the product projection, so it is trivial. If X=∅, the map ∅×F→∅ is a covering even when F=∅, since surjectivity and the evenly covered condition are vacuous. If X≠∅ and F=∅, the projection is not surjective.

3.1step 2.1∎

The preceding construction and implications establish the assertion.

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-16Open item page →

A surjective local homeomorphism need not be a covering map

Statement refuted

Let E=(0,2)⊔(1,2) and map both summands by inclusion to B=(0,2). This map is a surjective local homeomorphism but is not a covering map.

Facts & Assumptions

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

[F1]

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

[F2]

For a covering p:E→B, the cardinality of p−1(b) is locally constant as a function of b∈B. If B is connected, all fibres are equinumerous. (The cardinality of a covering fibre is locally constant and is constant on a connected base).

[F3]

The underlying set. Let I be a set and let Xi be a set for each i∈I. The disjoint union is ⨆i∈IXi  :=  ⋃i∈I(Xi×{i}), whose elements are the pairs (x,i) with i∈I and x∈Xi. For j∈I the j-th canonical injection is κj:Xj→⨆i∈IXi,κj(x):=(x,j). The construction is what makes the word "disjoint" honest. Each κj is injective (def-injection-surjection-bijection), since (x,j)=(x′,j) forces x=x′; the images κj[Xj]=Xj×{j} are pairwise disjoint, since the second coordinate determines j; and their union is the whole set. So no assumption that the Xi are disjoint as sets is needed, and none is made: the tag i separates the copies even when Xi=Xi′ for i≠i′. (The disjoint union (coproduct) ⨆iXi with the final topology of the canonical injections: a set is open exactly when each of its traces is).

[F4]

Throughout, R is the complete ordered field (def-complete-ordered-field, def-ordered-field) with its order (def-real-order). A subset I⊆R is order-convex when x,y∈I and x≤z≤y imply z∈I, and the intervals of R are the nine listed forms, among them [a,b]={x:a≤x≤b} and (a,b)={x:a<x<b}. (Intervals of R: the nine order-convex forms, nondegeneracy, and length).

Counterexample

technique · direct
1.1givenF3F4

Let the domain be the disjoint union of (0,2) and (1,2) and map both components by inclusion onto the base (0,2).

2.1step 1.1F1F3

The first component makes the map surjective and each inclusion is a local homeomorphism.

3.1step 2.1F1F2F3

The fibre has one point at 1 and two immediately to its right, so local constancy of sheet number rules out a covering; equivalently, the second component supplies only a one-sided partial sheet above every neighbourhood of 1.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-16Open item page →

A covering over a disconnected base can have different sheet numbers on different components

Statement refuted

There is a covering of a two-point discrete space whose fibre over one point has one element and whose fibre over the other has two elements. Thus connectedness is necessary for global constancy of sheet number.

Facts & Assumptions

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

[F1]

For a covering p:E→B, the cardinality of p−1(b) is locally constant as a function of b∈B. If B is connected, all fibres are equinumerous. (The cardinality of a covering fibre is locally constant and is constant on a connected base).

[F2]

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

Counterexample

technique · direct
1.1givenF2

Map a three-point discrete space onto a two-point discrete space with one point over the first basepoint and two over the second.

2.1step 1.1F1F2

Each singleton base neighbourhood is evenly covered, while the fibre cardinal is not globally constant.

3.1step 2.1F1

This isolates exactly why connectedness appears in the sheet-number theorem.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-09-26 (gpt-6-sol)Open item page →

The quotient R→R/Z is a covering with integer translations as deck transformations

Example

For the quotient by integer translation, q:R→R/Z is a covering map, and every deck transformation is a unique translation x↦x+n with n∈Z.

Facts & Assumptions

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

[F1]

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

[F2]

For a covering p:E→B, a deck transformation is an isomorphism h:E→E over B, so p∘h=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).

[F3]

The quotient topology. Let (X,T) be a topological space (def-topological-space), let Y be a set and let q:X→Y 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  :=  { V⊆Y:q−1[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, C⊆Y is closed in Tq exactly when q−1[C] is closed in X, because q−1[Y∖V]=X∖q−1[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]

On the set N×N of pairs of natural numbers, define (a,b)∼(c,d)  ⟺  a+d=b+c. This is an equivalence relation (lem-int-equivalence). The integers are the quotient Z:=(N×N)/∼, and we write [(a,b)] for the equivalence class of (a,b). (The integers as equivalence classes of pairs of naturals).

[F5]

Identify Z with its canonical copy inside R along the embeddings N→Z→Q→R; then for every real x there is exactly one integer m with m≤x<m+1, written ⌊x⌋ (Integer part: for every real x there is exactly one integer m with m≤x<m+1).

Verification

technique · direct
1.1givenF3F4F5

By [F5] the integers sit inside R as a subgroup under the ordered-field operations, so x∼y iff x−y∈Z is an equivalence relation on R; [F4] supplies only the abstract construction of Z and not its copy in R, so the embedding of [F5] is what makes the relation and the translations below meaningful. Take the quotient topology of [F3] on R/Z.

2.1step 1.1F3F4F5

For an open interval I of length below 1 the translates I+k, k∈Z, are pairwise disjoint, since two points of I differ by less than 1 while distinct integer translates differ by at least 1 in the order of [F5]; the preimage q−1(q[I])=⋃k∈Z(I+k) is then a union of open sets, so q[I] is open and evenly covered. Openness of I is required and not cosmetic: for I=[0,12] the preimage ⋃k∈Z[k,k+12] is not open, so q[I] is not even a neighbourhood.

3.1step 2.1F1F2F3

Each integer translation τn(x)=x+n is a homeomorphism satisfying qτn=q. The intervals in step 2.1 show that this is a covering-space action of Z on R. Since R is path-connected by straight-line paths, [F1] identifies the entire deck group with these translations. More explicitly, a deck transformation h has h(0)∈q−1(q(0))=Z; the translation τh(0) agrees with h at 0, and the one-point determination used in [F1] makes them equal. Distinct integers give distinct translations.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

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

The projected unit interval is not nullhomotopic in R/Z

Example

The loop t↦[t] in R/Z is not nullhomotopic.

Facts & Assumptions

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

[F1]

For the quotient by integer translation, q:R→R/Z is a covering map, and every deck transformation is a unique translation x↦x+n with n∈Z. (The quotient R→R/Z is a covering with integer translations as deck transformations).

[F2]

Let p:E→B be a covering, H:Y×I→B a homotopy, and H~0:Y→E a lift of H(−,0). There is a unique lift H~:Y×I→E of H extending H~0. (Existence and uniqueness of homotopy lifts through a covering map).

[F3]

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

Verification

technique · direct
1.1givenF3F1

The loop t↦[t] lifts from zero to the path t↦t, whose endpoint is one.

2.1step 1.1F3F2

If it had an endpoint-fixed nullhomotopy, homotopy lifting would keep the terminal lift in the discrete fibre while deforming the initial lift to the constant path at zero, forcing endpoints one and zero to agree.

3.1step 2.1F1

This proves essentiality without asserting π1(R/Z)≅Z.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-09-26 (gpt-6-sol)Open item page →

The maps [x]↦[mx] on R/Z are m-sheeted coverings for m≥1

Example

For every integer m≥1, the map Pm:R/Z→R/Z given by Pm([x])=[mx] is a well-defined m-sheeted covering.

Facts & Assumptions

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

[F1]

For the quotient by integer translation, q:R→R/Z is a covering map, and every deck transformation is a unique translation x↦x+n with n∈Z. (The quotient R→R/Z is a covering with integer translations as deck transformations).

[F2]

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

[F3]

For a covering p:E→B, the cardinality of p−1(b) is locally constant as a function of b∈B. If B is connected, all fibres are equinumerous. (The cardinality of a covering fibre is locally constant and is constant on a connected base).

[F4]

On the set N×N of pairs of natural numbers, define (a,b)∼(c,d)  ⟺  a+d=b+c. This is an equivalence relation (lem-int-equivalence). The integers are the quotient Z:=(N×N)/∼, and we write [(a,b)] for the equivalence class of (a,b). (The integers as equivalence classes of pairs of naturals).

[F5]

Let a,b∈Z with b>0. Then there exist integers q and r with a=qb+r and 0≤r<b, and this pair is unique (Division with remainder in Z: for a∈Z and b>0 there are unique q,r∈Z with a=qb+r and 0≤r<b).

Verification

technique · direct
1.1givenF1

If [x]=[x+n] with n∈Z, then [m(x+n)]=[mx], so Pm is well defined. Since Pm∘q=q∘(x↦mx) and q is a quotient map, Pm is continuous. It is surjective because Pm([y/m])=[y].

2.1F1F2F5step 1.1

Fix [a] and choose I=(a−δ,a+δ) with 0<δ<1/2. The quotient map q is open, since q−1(q(O))=⋃n∈Z(O+n) is open for every open O⊆R. Thus U=q(I) is open, and q∣I is a homeomorphism onto U. For 0≤r<m, put Vr=q((I+r)/m). Each Vr is open, and Pm∣Vr is a homeomorphism onto U, with inverse q(u)↦q((u+r)/m) for u∈I. If points from Vr and Vs coincide, then u−v+r−s is a multiple of m for some u,v∈I. Since ∣u−v∣<1 and r−s is an integer between −(m−1) and m−1, this forces r=s and u=v. Finally, if Pm([x])∈U, then mx=u+n for some u∈I and n∈Z; write n=km+r with 0≤r<m by [F5], giving [x]∈Vr. Hence Pm−1(U) is the disjoint union of exactly m sheets.

3.1step 2.1

At m=1 the map is the identity, so no zero-sheet or division-by-zero case is hidden.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-09-26 (gpt-6-sol)Open item page →

Pulling a covering back to an evenly covered open set gives a trivial covering

Example

If U is evenly covered by p:E→B, then the pullback of p along the inclusion U↪B is a trivial covering of U.

Facts & Assumptions

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

[F1]

For a covering p:E→B and a continuous map f:X→B, define f∗E:={(x,e)∈X×E:f(x)=p(e)} with the subspace topology, and let f∗p:f∗E→X 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:E→B such that every b∈B has an open neighbourhood U for which p−1(U) is a disjoint union of open sets Vj, called sheets, and each restriction p∣Vj:Vj→U is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a U is evenly covered, and p−1(b) is the fibre over b. A covering is trivial when it is isomorphic over B to a product projection B×F→B with F discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F3]

If X is any space and F is a nonempty discrete space, the projection X×F→X is a trivial covering with fibre F. If X=∅, the same holds for F=∅; for nonempty X, an empty fibre would violate surjectivity. (Trivial coverings are products with a discrete fibre).

Verification

technique · direct
1.1F1F2F3

Let f:U↪B be the inclusion. If U=∅, its pullback is empty and is isomorphic over U to U×∅→U, which is a trivial covering by [F3]. Hence assume U≠∅. Choose an evenly covered decomposition p−1(U)=⨆j∈JVj as in [F2]. Surjectivity of p makes J nonempty. The pullback f∗E is {(u,e):u=p(e)∈U} by [F1].

2.1step 1.1F1F2

Give J the discrete topology. Define h:U×J→f∗E by h(u,j)=(u,(p∣Vj)−1(u)). Each e∈p−1(U) belongs to exactly one sheet Vj, so the inverse is h−1(u,e)=(u,j) for that unique j. Both maps preserve the projection to U.

3.1step 1.1step 2.1F1F2

The restriction of h to each open slice U×{j} is continuous because (p∣Vj)−1 is continuous. These slices cover U×J, so h is continuous. The pullback subset {(u,e):e∈Vj, u=p(e)} is open in f∗E, since Vj is open in E; on it, h−1 has the continuous form (u,e)↦(u,j). These subsets cover f∗E, so h−1 is continuous. Thus h is a homeomorphism over U.

4.1step 3.1F3∎

By [F3], U×J→U is a trivial covering. The homeomorphism of step 3.1 identifies it with the pullback covering, proving the Example.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-09-26 (gpt-6-sol)Open item page →

The Hawaiian earring is locally path-connected but has no universal cover

Example

The Hawaiian earring is locally path-connected but is not semilocally simply connected at its wedge point. Consequently it has no universal cover.

Facts & Assumptions

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

[F1]

The loop t↦[t] in R/Z is not nullhomotopic. (The projected unit interval is not nullhomotopic in R/Z).

[F2]

If a space admits a universal covering, then it is semilocally simply connected. No local path-connectedness hypothesis is required. (A space admitting a universal covering is semilocally simply connected).

[F3]

A space X is semilocally simply connected at x∈X 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]

The quotient topology. Let (X,T) be a topological space (def-topological-space), let Y be a set and let q:X→Y 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  :=  { V⊆Y:q−1[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, C⊆Y is closed in Tq exactly when q−1[C] is closed in X, because q−1[Y∖V]=X∖q−1[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).

Verification

technique · direct
1.1givenF1

Model the earring in R2 as H=⋃n≥1Cn, where Cn is the circle of radius 1/n centered at (1/n,0) and all circles meet at o=(0,0). Their diameters tend to zero. Each Cn is homeomorphic to R/Z, with the unit loop based at o.

2.1step 1.1F3F2

Away from the wedge point, sufficiently short open arcs are path-connected neighbourhoods.

3.1step 1.1step 2.1

At the wedge point, every open neighbourhood contains a smaller metric ball whose intersection with each circle is either an arc through the wedge point or the whole circle. It contains every sufficiently small circle, and all these pieces share the wedge point, so the ball is path-connected.

4.1step 1.1step 3.1F1F3

Every neighbourhood U of o contains some whole Cn. Define rn:H→Cn to be the identity on Cn and to send every other circle to o. This is continuous away from o because each nonzero point has a neighbourhood meeting only its own circle; it is continuous at o because ∣rn(z)∣≤∣z∣. The unit loop in Cn⊂U is essential in Cn by [F1], so its composite with the retraction cannot be nullhomotopic in H. Thus the inclusion-induced map from U to H is nontrivial, and semilocal simple connectedness fails at o.

5.1step 4.1F2

The necessity theorem then rules out a universal cover.

6.1step 5.1∎

The preceding construction and implications establish the assertion.

Sources