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.
Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints
Definition
Write with its usual subspace topology, as in Paths, path-connected spaces and path components. Let and be topological spaces, and let be continuous maps (Continuity of a map of topological spaces at a point and globally).
A homotopy from to is a continuous map
from the product space (The product set 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) such that and for every . When such an exists, and are homotopic, written .
Let carry the subspace topology (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace). The homotopy is a homotopy relative to , or a homotopy rel , when
Thus a homotopy rel can exist only when , and every ordinary homotopy is a homotopy rel . We write when a homotopy rel exists.
If are paths with the same initial point and the same terminal point (Paths, path-connected spaces and path components), a path homotopy from to relative to the endpoints is a homotopy rel . Explicitly,
The first coordinate parametrises the path and the second coordinate parametrises the deformation.
Remarks
- The adjective relative means pointwise fixed throughout the deformation, not merely mapped back into .
- A homotopy is a map on a product. A family of maps is not by itself a homotopy unless the joint map is continuous.
Depends on
- Continuity of a map of topological spaces at a point and globally
- The product set $\prod_{i \in I} X_i$ 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
- Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Paths, path-connected spaces and path components
Used by
- A closed contour path-homotopic to a constant loop has zero integral against every holomorphic function Corollary
- Homotopy relative to a fixed subspace, and path homotopy relative to endpoints, are equivalence relations Corollary
- The smooth and continuous homotopy categories of smooth manifolds have the same morphism sets Corollary
- Analytic continuation along a path by admissible chains Definition
- Based loops and the fundamental group Definition
- Cofibration and homotopy extension property Definition
- Compactly generated conventions for based homotopy Definition
- Fundamental groupoid of a space Definition
- Higher homotopy group by based cubes Definition
- Homotopy equivalences, homotopy inverses and spaces of the same homotopy type Definition
- Hurewicz and serre fibrations Definition
- Lifts of maps, paths, and homotopies through a covering map Definition
- Mapping cylinder and mapping cone Definition
- Nullhomotopic maps and contractible spaces Definition
- Relative homotopy classes and groups Definition
- Retractions and deformation retracts, with a deformation retraction required to fix the retract pointwise Definition
- The based path-class model and basic sets for a universal cover Definition
- The prism operator of a homotopy Definition
- A path between basepoints induces an isomorphism of fundamental groups Example
- The fundamental groupoid of a topological space Example
- The prism operator for a path homotopy Example
- Two paths can induce distinct change-of-basepoint isomorphisms on S¹∨ S¹ Example
- Two paths with the same endpoints in a convex subset of ℝⁿ are path homotopic relative to their endpoints Example
- A path homotopy over a two-set open cover admits a finite subordinate grid Lemma
- Contiguous simplicial maps have homotopic realizations Lemma
- Homotopy relative to a subspace is reflexive and symmetric Lemma
- Pointwise multiplication and concatenation of loops in a topological group agree up to homotopy Lemma
- The open star criterion produces a simplicial map Lemma
- Two homotopies relative to the same subspace concatenate after piecewise-linear reparametrisation Lemma
- Any two continuous maps into a nonempty convex subset of ℝⁿ are homotopic by straight lines Theorem
- Continuously homotopic smooth maps are smoothly homotopic Theorem
- Endpoint-fixed homotopic paths have equal holomorphic line integrals Theorem
- Fixed-endpoint homotopic paths give the same analytic continuation Theorem
- Loop classes form the group π₁(X,x₀) under concatenation Theorem
- Lower-dimensional sphere maps are based nullhomotopic Theorem
- Precomposition and postcomposition by continuous maps preserve homotopies, including their relative form Theorem
- Relative Whitney approximation for manifold-valued maps Theorem
- The transversality homotopy theorem Theorem
- Whitney approximation for manifold-valued maps Theorem
- π₁(X× Y,(x₀,y₀))≅π₁(X,x₀)×π₁(Y,y₀) Theorem
Dependency tree · two levels
26 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
- A. Hatcher, Algebraic Topology, Section 0 (standard reference, not scraped)