PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Canonical associativity, symmetry, and unit maps for smash products

Statement

For based CGWH spaces $X, Y, Z$ , the formulas

$(x \land y) \land z ⟼ x \land (y \land z), x \land y ⟼ y \land x,$

and $S^{0} \land X \to X$ , $1 \land x \mapsto x$ , induce natural based homeomorphisms

$(X \land Y) \land Z ≅ X \land (Y \land Z), X \land Y ≅ Y \land X, S^{0} \land X ≅ X .$

These maps satisfy the usual pentagon, triangle, and symmetry coherence identities.

Facts & Assumptions

[F1]

Every product and quotient is formed with the CGWH convention of Smash product of based spaces.

[F2]

The published product-of-quotients lemma identifies an iterated quotient product with the corresponding quotient of the product (Compact-test exponential law and products of quotient maps).

[F3]

The coordinate reassociations and permutations of k-products are mutually inverse homeomorphisms.

[F4]

Maps constant on quotient classes descend uniquely and continuously (For a quotient map $q : X \to Y$ , a map out of $Y$ is continuous iff its composite with $q$ is; a continuous map on $X$ constant on the fibres of $q$ factors uniquely through $q$ ; and a composite of quotient maps is a quotient map).

Proof

Given: Based CGWH spaces $X, Y, Z$ as in the statement.

1.1

Put both triple smashes over one quotient. Let [F1, F2, F4] $W = (X \times Y \times {*_{Z}}) \cup (X \times {*_{Y}} \times Z) \cup ({*_{X}} \times Y \times Z) .$

By [F1] and [F2], both $(X \land Y) \land Z$ and $X \land (Y \land Z)$ are canonically the kified quotient of $X \times_{k} Y \times_{k} Z$ by $W$ . The identity on triples therefore descends by [F4] to the displayed associator, and the same construction in reverse gives its continuous inverse. [F1, F2, F4]

1.2

Descend the twist and unit maps. The transposition $(x, y) \mapsto (y, x)$ takes $X \lor Y$ onto $Y \lor X$ , so [F3, F4] give the symmetry homeomorphism and its inverse. Since the nonbasepoint of $S^{0}$ is an open-and-closed singleton, collapsing $S^{0} \lor X$ leaves precisely the copy ${1} \times X$ , giving $S^{0} \land X ≅ X$ .

F1F3F4

1.3

Check naturality and coherence. Naturality follows because every map above is induced by the corresponding coordinate map before quotienting. Each pentagon, triangle, or symmetry composite is induced by the same reassociation or permutation of the same product coordinates. Those maps agree before quotienting, hence their descended maps agree.

$□$

Depends on

Used by

Pairings and unital multiplication of sequential prespectra Definition
Sequential prespectra, spectra, and adjoint structure maps Definition
Suspension prespectra of spheres are shifts Example
A ring prespectrum gives a graded product on stable homotopy groups Proposition

Dependency tree · two levels

15 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

J. P. May, A Concise Course in Algebraic Topology (standard reference, not scraped)