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 path space replacement of a map
Definition
For a continuous map , let with the ordinary compact-open topology. Define where is the constant path with value . These use the product and subspace topologies of A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice and 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. They are called the mapping-path space, its endpoint projection, and its constant-path inclusion.
Evaluation is continuous by Interval exponential law and quotient homotopies, so is continuous. The constant-path map is continuous by transposing ; pairing with and restricting to shows that is continuous. Also let ; this is continuous as a restricted product projection. No arbitrary selection of paths is part of these definitions.
For CGWH spaces use the kified path space, k-product and kified indicated subspace instead; the same interval exponential law supplies these maps. Empty gives empty . If is empty then the existence of already forces empty. For a one-point domain this is the space of paths starting at its specified image; for a one-point target it identifies with . The factorization and homotopy claims are proved next.
Depends on
- Interval exponential law and quotient homotopies
- A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice
- 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
Used by
- Homotopy fiber of a map Definition
- Mapping path factorization Theorem
Dependency tree · two levels
21 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 (standard reference, not scraped)