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.
Mapping cone of a degree d circle map
Example
For let , . Its unreduced mapping cone has and . For d=0, ; for d=±1 the fundamental group and reduced homology vanish. All homology coefficients here are integers.
Facts & Assumptions
The unreduced cone attaches the cone on the source circle to the target. Mapping cylinder and mapping cone
Degree is the integral sphere-homology multiplier. Degree of a self map of an oriented sphere
Local degree is the multiplier on the local oriented punctured-pair groups. Local degree at an isolated preimage
Degree is the sum over a finite fibre. Global sphere degree is the sum of local degrees
In dimension one identity, constant and reflection degrees are 1,0,−1. Degree of identity constant reflection and antipodal sphere maps
The cellular boundary coefficient is the attaching incidence degree. Cellular boundary is the incidence degree matrix
Cellular homology equals singular homology. Cellular homology computes singular homology
An open path-connected cover with path-connected intersection gives the fundamental-group pushout. Seifert–van Kampen identifies the fundamental group with a group pushout
The standard winding class identifies π1(R/Z) with Z. is an isomorphism
Verification
Given: The spaces, maps, and hypotheses in the statement above.
The map identifies the quotient circle with the unit circle: it is a continuous bijection, and inverse angular charts are continuous on arcs, including arcs crossing the quotient seam. Give it the counterclockwise orientation. Then . For d>0 the fibre over 1 is , 0≤k<d. In positive angular coordinates at each preimage and at 1, the map is u↦du. Interpolating the positive coefficient d to 1 on a sufficiently small arc gives a homotopy of punctured pairs. Thus F3 identifies its local multiplier with that of an orientation-preserving circle rotation, namely +1 by the identity and rotation homotopy, or the singleton-fibre case of F4. For d<0 the same calculation reduces to angular reflection, whose degree is −1 by the circle clause of F5. Hence F4 gives degree d for every nonzero d. For d=0 the map is constant and F5 gives degree zero.
For the fundamental group take U to be the target circle together with cone heights s<2/3, and V to be cone heights s>1/3 including its tip. They are open in the quotient, their union is the cone space, and their intersection is a circle times (1/3,2/3). U retracts to the target by decreasing height, V contracts to the tip by increasing height, and the intersection retracts to its circle. All are path-connected. Choose the basepoint at source [0], height 1/2 and transport to the target vertex along the height segment. The overlap generator maps to a^d in π1(U) by F9 and trivially in π1(V). Thus F8 gives the presentation . This calculation does not infer H1 from π1.
The cone on the source circle is the disk via ; its boundary at s=0 attaches by f_d. Thus the mapping cone has one vertex, one loop edge and one 2-cell. F2 and step 1.1 identify its attaching coefficient in F6 as d, so its cellular complex is . Direct kernels and images give the stated H0,H1,H2 and vanishing above dimension two, and F7 identifies them with singular homology.
When d=0 the cellular map is zero, so H1=H2=Z and the group relation is empty. When d=±1 the cellular map is an isomorphism and the group relation kills a, giving the claimed vanishings. For instance d=−2 gives H1=π1=Z/2Z and H2=0. No inference of contractibility from these invariants is made.
Depends on
- Mapping cylinder and mapping cone
- Degree of a self map of an oriented sphere
- Local degree at an isolated preimage
- Global sphere degree is the sum of local degrees
- Degree of identity constant reflection and antipodal sphere maps
- Cellular boundary is the incidence degree matrix
- Cellular homology computes singular homology
- Seifert–van Kampen identifies the fundamental group with a group pushout
- $\operatorname{Deg}:\pi_1(\mathbb R/\mathbb Z,[0])\to(\mathbb Z,+)$ is an isomorphism
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
39 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
- May, A Concise Course in Algebraic Topology (standard reference, not scraped)
- Hatcher, Algebraic Topology, Example 2.32 (standard reference, not scraped)