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.

The quotient $R \to R / Z$ is a covering with integer translations as deck transformations

Example

For the quotient by integer translation, $q : R \to R / Z$ is a covering map, and every deck transformation is a unique translation $x \mapsto x + n$ with $n \in 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 \to 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 \to B$ , a deck transformation is an isomorphism $h : E \to E$ over $B$ , so $p \circ 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 \to 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): $T_{q} : = {V \subseteq Y : q^{- 1} [V] \in 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 \subseteq Y$ is closed in $T_{q}$ 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 \times N$ of pairs of natural numbers, define $(a, b) \sim (c, d) ⟺ a + d = b + c .$ This is an equivalence relation (lem-int-equivalence). The integers are the quotient $Z : = (N \times N) / \sim,$ 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 \to Z \to Q \to R$ ; then for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ , written $⌊ x ⌋$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq 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 \sim y$ iff $x - y \in 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 \in 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 \in 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, \frac{1}{2}]$ the preimage $⋃_{k \in Z} [k, k + \frac{1}{2}]$ 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) \in 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.

Depends on

Used by

Dependency tree · two levels

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

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