Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)
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 adjunction space YfXY \cup_f X glued along a continuous map, and, for a nonempty space, the cone and the suspension as quotients of X×[0,1]X \times [0,1]

Definition

Throughout, [0,1][0,1] denotes the closed unit interval (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length) with the subspace topology inherited from the usual topology of R\mathbb{R} (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 absolute value makes R\mathbb{R} a metric space: d(x,y)=xyd(x,y) = |x-y| is a metric, its open balls are the intervals (xr,x+r)(x-r, x+r), and it is unbounded, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not), and X×[0,1]X \times [0,1] the binary product with the product topology (The product set iIXi\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). All three constructions below are quotients (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection) of a space already built on this page, and none of them needs anything further. The one exception is the degenerate case X=X = \varnothing: then X×[0,1]X \times [0,1] is empty, so the one-point cone and the two-point suspension stipulated below are not quotients of it, and they are fixed by that stipulation rather than by the construction.

Adjunction space. Let XX and YY be topological spaces, let AXA \subseteq X carry the subspace topology, and let f:AYf : A \to Y be continuous (Continuity of a map of topological spaces at a point and globally). Form the disjoint union YXY \sqcup X with its canonical injections κY\kappa_Y and κX\kappa_X (The disjoint union (coproduct) iXi\bigsqcup_i X_i with the final topology of the canonical injections: a set is open exactly when each of its traces is) and let f\sim_f be the relation on YXY \sqcup X whose classes are

Cy  :=  {κY(y)}{κX(a):aA, f(a)=y}(yY),{κX(x)}(xXA).C_y \;:=\; \{\kappa_Y(y)\} \cup \{\, \kappa_X(a) : a \in A,\ f(a) = y \,\} \quad (y \in Y), \qquad \{\kappa_X(x)\} \quad (x \in X \setminus A) .

These sets are pairwise disjoint and their union is YXY \sqcup X, since every element of YXY \sqcup X is κY(y)\kappa_Y(y) for exactly one yy, or κX(x)\kappa_X(x) for exactly one xx, and in the latter case lies in Cf(x)C_{f(x)} when xAx \in A and in its own singleton otherwise. A family of pairwise disjoint nonempty sets covering a set is the family of classes of exactly one equivalence relation, so f\sim_f is well defined. The adjunction space is the identification space

YfX  :=  (YX)/ ⁣fY \cup_f X \;:=\; (Y \sqcup X)/\!\sim_f

with the quotient topology of its canonical projection. It is said to be obtained by gluing XX to YY along ff: each point aAa \in A is identified with its image f(a)f(a), and nothing else is identified.

Collapsing a subset. For a space ZZ and a nonempty BZB \subseteq Z, write Z/BZ/B for the quotient of ZZ by the equivalence relation whose classes are BB and the singletons {z}\{z\}, zBz \notin B (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection): all of BB becomes one point and nothing else is identified.

Cone. The cone on a space XX is

CX  :=  (X×[0,1])/(X×{1}),CX \;:=\; \big(X \times [0,1]\big)\big/\big(X \times \{1\}\big) ,

the product of XX with the unit interval, with the whole top face collapsed to a single point, called the apex. The definition presupposes only that X×{1}X \times \{1\} is nonempty, which holds exactly when XX is nonempty; for X=X = \varnothing the product is empty, the quotient of the empty space is empty, and no apex is produced; this library nonetheless takes CC\varnothing to be the one-point space by convention, so that the apex always exists and every cone is nonempty. The convention is a stipulation, not a consequence of the description above, which gives the empty space.

Suspension. The suspension of XX is

ΣX  :=  (X×[0,1])/ ⁣,\Sigma X \;:=\; \big(X \times [0,1]\big)\big/\!\sim ,

where \sim has as classes X×{0}X \times \{0\}, X×{1}X \times \{1\}, and the singletons {(x,t)}\{(x,t)\} for 0<t<10 < t < 1. So both faces are collapsed, each to its own point, and the two resulting points are distinct as soon as XX is nonempty. For X=X = \varnothing this library takes Σ\Sigma\varnothing to be the two-point discrete space, one apex from each end, matching the convention that a suspension is two cones glued along XX; the alternative stipulation of a single point is also in use in the literature, and nothing here depends on the choice.

Mapping cone. For a continuous f:XYf : X \to Y the mapping cone is the adjunction space YfCXY \cup_{f'} CX, where CXCX is the cone, XX is identified with the subspace X×{0}X \times \{0\} of X×[0,1]X \times [0,1] and thence with its image in CXCX, and ff' is the corresponding map into YY. It is recorded here as the standard instance of the two constructions used together, and nothing below depends on it.

What is deliberately not asserted. These constructions produce spaces, and this page proves nothing about which of them are homeomorphic to which. The invariants that separate them, connectedness, compactness and the homotopy notions, are not available for general topological spaces at this point in the reading order: connectedness and compactness are developed here only for subsets of R\mathbb{R} (Separated sets, disconnection, and connected subset of R\mathbb{R}) and for metric spaces (Open cover, subcover, compact metric space, and compact subset of a metric space), and neither development applies to a quotient that has not been shown metrizable, while the homotopy notions are absent altogether. So no statement here says that two of these spaces are different, and none says that the cone or the suspension of a familiar space is any particular familiar space.

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 90 results over 13 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