ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11

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.

For a fixed space $X$ , product with $X$ defines an endofunctor of $T o p$

Example

Fix a topological space $X$ . The assignment $Y \mapsto X \times Y$ is an endofunctor of $T o p$ .

Facts & Assumptions

Given: A fixed topological space $X$ .

[L1]

Topological spaces and continuous maps form $T o p$ (Topological spaces and continuous maps form the large locally small category $T o p$ ).

[L2]

A map into a product is continuous exactly when its coordinate maps are continuous (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).

[L3]

An endofunctor must preserve identities and composition (Covariant functor, identity functor, composite functor, and contravariant functor).

Verification

technique · direct

1.1

Define $T_{X} (Y) = X \times Y$ with the product topology. For a continuous $f : Y \to Z$ , define $T_{X} (f) = 1_{X} \times f$ by $(x, y) \mapsto (x, f (y))$ .

2.1

Its coordinate maps are the first projection and $f$ after the second projection, so $T_{X} (f)$ is continuous by [L2].

step 1.1L2

2.2

Pointwise, $1_{X} \times 1_{Y} = 1_{X \times Y}$ and $(1_{X} \times g) (1_{X} \times f) = 1_{X} \times (g f)$ .

step 1.1

3.1

Thus $T_{X}$ sends every morphism of $T o p$ to a morphism and obeys the two functor equations. It is an endofunctor by [L3].

step 2.1step 2.2L1L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

Emily Riehl, Category Theory in Context, Example 1.3.3 (standard reference, not scraped)

For a fixed space XX, product with XX defines an endofunctor of TopTop