ExampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-09-26 (gpt-6-sol)

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.

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

Example

If $U$ is evenly covered by $p : E \to 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 \to B$ and a continuous map $f : X \to B$ , define $f^{*} E : = {(x, e) \in X \times E : f (x) = p (e)}$ with the subspace topology, and let $f^{*} p : f^{*} E \to X$ be $(x, e) \mapsto 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 \to B$ such that every $b \in B$ has an open neighbourhood $U$ for which $p^{- 1} (U)$ is a disjoint union of open sets $V_{j}$ , called sheets, and each restriction $p ∣_{V_{j}} : V_{j} \to 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 \times F \to 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 \times F \to X$ is a trivial covering with fibre $F$ . If $X = \emptyset$ , the same holds for $F = \emptyset$ ; 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 = \emptyset$ , its pullback is empty and is isomorphic over $U$ to $U \times \emptyset \to U$ , which is a trivial covering by [F3]. Hence assume $U \neq \emptyset$ . Choose an evenly covered decomposition $p^{- 1} (U) = ⨆_{j \in J} V_{j}$ as in [F2]. Surjectivity of $p$ makes $J$ nonempty. The pullback $f^{*} E$ is ${(u, e) : u = p (e) \in U}$ by [F1].

2.1step 1.1F1F2

Give $J$ the discrete topology. Define $h : U \times J \to f^{*} E$ by $h (u, j) = (u, (p ∣_{V_{j}})^{- 1} (u))$ . Each $e \in p^{- 1} (U)$ belongs to exactly one sheet $V_{j}$ , 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 \times {j}$ is continuous because $(p ∣_{V_{j}})^{- 1}$ is continuous. These slices cover $U \times J$ , so $h$ is continuous. The pullback subset ${(u, e) : e \in V_{j}, u = p (e)}$ is open in $f^{*} E$ , since $V_{j}$ is open in $E$ ; on it, $h^{- 1}$ has the continuous form $(u, e) \mapsto (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 \times J \to U$ is a trivial covering. The homeomorphism of step 3.1 identifies it with the pullback covering, proving the Example.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Allen Hatcher, Algebraic Topology, §1.3 (standard reference, not scraped)
Marco Gualtieri, MAT1300 Week 4 Term 2, §1.6 (standard reference, not scraped)
Omar Antolín Camarena, Proper local homeomorphisms and covering maps (standard reference, not scraped)