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 initial topology of a family of maps into spaces and the final topology of a family of maps out of spaces, and the subspace topology as the model initial topology
Definition
Two constructions are defined here, one for maps into spaces and one for maps out of spaces. Every further construction on this page is an instance of one of them.
Initial topology. Let be a set, let be an index set, let be a topological space for each (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison), and let be a function for each . The initial topology on induced by the family is
the topology generated by the preimages of the open sets of the (Basis and subbasis for a topology, and the topology generated by a family of sets).
This is well posed, and the obligation is discharged by the item cited. For an arbitrary family of subsets of , the family is a topology on , contains , and is contained in every topology on containing (Basis and subbasis for a topology, and the topology generated by a family of sets); no further verification is needed here. By A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis a basis for is the family of intersections of finitely many sets , the intersection of none being .
Final topology. Let be a set, let be a topological space for each , and let be a function for each . The final topology on induced by the family is
This is a topology, and the verification is carried out here rather than assumed. Preimage commutes with the three set operations named in the axioms: and , which gives (T1); for every family , which with (T2) in gives (T2); and , which with (T3) in gives (T3) (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).
Two degenerate cases, stated because they are used. For the initial topology is , the indiscrete topology, and the final topology is , the discrete topology, the defining condition being vacuous (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, Basis and subbasis for a topology, and the topology generated by a family of sets). For a family consisting of a single map the definitions read the same way with the index dropped.
The subspace topology is the model initial topology. Let be a space, let and let be the inclusion. Then for every , so the generating family for the initial topology of the one-element family is exactly (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). That family is already a topology, so generating adds nothing and the initial topology of is the subspace topology. Everything 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 proves about it is therefore quoted here and not reproved: its closed sets are the traces of the closed sets, a basis of traces to a basis of , the inclusion is continuous (Continuity of a map of topological spaces at a point and globally, For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and ), is the coarsest topology making continuous, and a map is continuous if and only if is.
Terminology. A family as above is the defining family of the initial topology, and likewise for the final one; both topologies depend on the whole family and not on any one member. The characteristic properties that make these two constructions worth naming are the subject of the next item.
Remarks
-
The direction of the arrows is what distinguishes the two. An initial topology is put on the source of its defining maps and is the coarsest making them continuous; a final topology is put on the target and is the finest making them continuous. Both facts are proved in the next item rather than built into the definitions above.
-
Why the initial topology is generated and the final one is not. The preimages need not be closed under unions or finite intersections, so a topology has to be generated from them; the final family is closed under both operations already, because preimage commutes with both, so it is a topology as it stands. The asymmetry is a fact about preimages and not a choice of presentation.
-
Both constructions are determined by a universal property, so they are unique once that property is stated. That is the content of the next item, and it is what lets the product, the coproduct and the quotient be treated as three instances of two constructions rather than as three separate theories.
Depends on
- Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
- Basis and subbasis for a topology, and the topology generated by a family of sets
- A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis
- Continuity of a map of topological spaces at a point and globally
- For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f(\overline{A}) \subseteq \overline{f(A)}$
- 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 discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies
Used by
- The disjoint union (coproduct) bigsqcupᵢ Xᵢ with the final topology of the canonical injections: a set is open exactly when each of its traces is Definition
- The product set ∏_i ∈ I Xᵢ 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 Definition
- The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection Definition
- The topology of pointwise convergence on Y^X, which is the product topology, and its restriction to C(X,Y) Definition
- 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 Theorem
- Characteristic properties: a map into a space with the initial topology is continuous iff every composite with the defining family is, a map out of a space with the final topology is continuous iff every composite with the defining family is, and the two topologies are respectively the coarsest and the finest making that family continuous Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 42 results over 17 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
- Initial topology (Wikipedia) (standard reference, not scraped)
- Final topology (Wikipedia) (standard reference, not scraped)
- J. Munkres, Topology, 2nd ed., §19 and §22 (standard reference, not scraped)