(Topological) Schemes and their induced maps #
In topology, and especially descriptive set theory, one often constructs functions
(ℕ → β) → α,
where α is some topological space and β is a discrete space, as an appropriate limit of some map
List β → Set α. We call the latter type of map a "
This file develops the basic, abstract theory of these schemes and the functions they induce.
Main Definitions #
CantorScheme.inducedMap A: The aforementioned "limit" of a scheme
A : List β → Set α. This is a partial function from
ℕ → βto
a, implemented here as an object of type
Σ s : Set (ℕ → β), s → α. That is,
(inducedMap A).1is the domain and
(inducedMap A).2is the function.
Implementation Notes #
We consider end-appending to be the fundamental way to build lists (say on
as this interacts better with the topology on
ℕ → β.
As a result, functions like
Stream'.take do not have their intended meaning
in this file. See instead
- [kechris1995] (Chapters 6-7)
scheme, cantor scheme, lusin scheme, approximation.
A, we define a partial function from
(ℕ → β) to
which sends each infinite sequence
x to an element of the intersection along the
branch corresponding to
x, if it exists.
We call this the map induced by the scheme.
x is in the domain of the induced map of a scheme
its image under this map is in each set along the corresponding branch.
A scheme with vanishing diameter along each branch induces a continuous map.
A scheme on a complete space with vanishing diameter such that each set contains the closure of its children induces a total map.