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 circle as with basepoint
Definition
Use the canonical copy of inside fixed in Integer part: for every real there is exactly one integer with . For , put
This is an equivalence relation. Indeed, ; if , then ; and if , then . The closure facts used here are part of the additive-group structure supplied by The integers form a commutative ring, and the quotient-set construction is that of The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection.
Let denote the equivalence class of . Let be the canonical projection, . Thus
Let carry the quotient topology induced by . The circle is with the quotient topology induced by and basepoint ; moreover and for every real and integer .
The last assertions follow directly from the displayed fibre criterion: exactly when , while .
Depends on
- The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection
- The integers as equivalence classes of pairs of naturals
- The integers form a commutative ring
- Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$
Used by
- ℝ/ℤ is not simply connected Corollary
- An interval of length one need not embed under p:ℝ→ℝ/ℤ Counterexample
- The degree of a based circle loop Definition
- The standard circle loops ωₙ(t)=[nt] for n∈ℤ Definition
- A covering quotient of a simply connected space need not be simply connected Example
- A loop that traverses the circle once and then pauses is homotopic to the standard loop Example
- A surjective circle loop can have degree zero and be nullhomotopic Example
- FALSE: every continuous self-map of the circle is nullhomotopic False statement
- Based circle loops of equal degree are path-homotopic Lemma
- Lifts of circle-loop concatenations and reversals Lemma
- The quotient map is open, and every interval shorter than one embeds in ℝ/ℤ Lemma
- ℝ/ℤ is compact and path-connected Proposition
- ℝ/ℤ is Hausdorff Proposition
- Agreement with the published quotient model of ℝ/ℤ Remark
- [t]↦(cos 2π t,sin 2π t) is a homeomorphism from ℝ/ℤ to the unit circle Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 77 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Jonathan Wise, Math 6210 Lecture Notes, Week 3, Sections 3.1 and 3.4 (standard reference, not scraped)