Constructions of new topological spaces from old ones
This file constructs products, sums, subtypes and quotients of topological spaces and sets up their basic theory, such as criteria for maps into or out of these constructions to be continuous; descriptions of the open sets, neighborhood filters, and generators of these constructions; and their behavior with respect to embeddings and other specific classes of maps.
The constructed topologies are defined using induced and coinduced topologies
along with the complete lattice structure on topologies. Their universal properties
(for example, a map
X → Y × Z is continuous if and only if both projections
X → Y,
X → Z are) follow easily using order-theoretic descriptions of
continuity. With more work we can also extract descriptions of the open sets,
neighborhood filters and so on.
product, sum, disjoint union, subspace, quotient space
Embedding a factor into a product space (by fixing arbitrarily all the other coordinates) is continuous.