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.
Topological spaces and continuous maps form the large locally small category
Statement
Topological spaces and continuous maps form a large locally small category .
Facts & Assumptions
Given: Topological spaces and continuous maps , .
A topology is the structure in Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison, and identity maps and composites of continuous maps are continuous by the inverse-image definition in Continuity of a map of topological spaces at a point and globally.
The functions between fixed sets form the set (The set of all functions ); category size is as in Category, object, morphism, domain, codomain, identity, composition, and hom-collection and Small, locally small, and large categories, and the ordinals form a proper class (Burali-Forti: there is no set of all ordinals).
Proof
Identity maps and are continuous by [L1], while associativity and unit equations are those of function composition.
Consequently spaces and continuous maps form a category, and each hom-collection is a set of functions between fixed underlying sets.
Every singleton , for an ordinal , has its unique topology; these give distinct space objects, so [L2] makes large and locally small.
Depends on
- Category, object, morphism, domain, codomain, identity, composition, and hom-collection
- Small, locally small, and large categories
- Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
- Continuity of a map of topological spaces at a point and globally
- The set $B^{A}$ of all functions $A \to B$
- Burali-Forti: there is no set of all ordinals
Used by
- For a fixed space X, product with X defines an endofunctor of Top Example
- Open-set and closed-set functors on Topᵒᵖ are naturally isomorphic by complements Example
- Underlying-set and structure-forgetting functors among Grp, Ring, Vect_F, R-Mod, Top, and Set Example
- The fundamental group is a functor π₁:Top_*toGrp Proposition
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 32 results over 11 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
- Emily Riehl, Category Theory in Context, Chapter 1 (standard reference, not scraped)