(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 "β-scheme on α".

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).1 is the domain and (inducedMap A).2 is the function.

Implementation Notes

We consider end-appending to be the fundamental way to build lists (say on β) inductively, as this interacts better with the topology on ℕ → β. As a result, functions like List.get? or Stream'.take do not have their intended meaning in this file. See instead PiNat.res.

References

• [kechris1995] (Chapters 6-7)

Tags

scheme, cantor scheme, lusin scheme, approximation.

noncomputable def CantorScheme.inducedMap {β : Type u_1} {α : Type u_2} (A : List β → Set α) : (s : Set (ℕ → β)) × (↑s → α)

From a β-scheme on α 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.

def CantorScheme.Antitone {β : Type u_1} {α : Type u_2} (A : List β → Set α) : Prop

A scheme is antitone if each set contains its children.

def CantorScheme.ClosureAntitone {β : Type u_1} {α : Type u_2} (A : List β → Set α) [TopologicalSpace α] : Prop

A useful strengthening of being antitone is to require that each set contains the closure of each of its children.

def CantorScheme.Disjoint {β : Type u_1} {α : Type u_2} (A : List β → Set α) : Prop

A scheme is disjoint if the children of each set of pairwise disjoint.

theorem CantorScheme.map_mem {β : Type u_1} {α : Type u_2} {A : List β → Set α} (x : ↑(inducedMap A).fst) (n : ℕ) : (inducedMap A).snd x ∈ A (PiNat.res (↑x) n)

If x is in the domain of the induced map of a scheme A, its image under this map is in each set along the corresponding branch.

theorem CantorScheme.ClosureAntitone.antitone {β : Type u_1} {α : Type u_2} {A : List β → Set α} [TopologicalSpace α] (hA : ClosureAntitone A) : CantorScheme.Antitone A

theorem CantorScheme.Antitone.closureAntitone {β : Type u_1} {α : Type u_2} {A : List β → Set α} [TopologicalSpace α] (hanti : CantorScheme.Antitone A) (hclosed : ∀ (l : List β), IsClosed (A l)) : ClosureAntitone A

theorem CantorScheme.Disjoint.map_injective {β : Type u_1} {α : Type u_2} {A : List β → Set α} (hA : CantorScheme.Disjoint A) : Function.Injective (inducedMap A).snd

A scheme where the children of each set are pairwise disjoint induces an injective map.

def CantorScheme.VanishingDiam {β : Type u_1} {α : Type u_2} (A : List β → Set α) [PseudoMetricSpace α] : Prop

A scheme on a metric space has vanishing diameter if diameter approaches 0 along each branch.

theorem CantorScheme.VanishingDiam.dist_lt {β : Type u_1} {α : Type u_2} {A : List β → Set α} [PseudoMetricSpace α] (hA : VanishingDiam A) (ε : ℝ) (ε_pos : 0 < ε) (x : ℕ → β) : ∃ (n : ℕ), ∀ y ∈ A (PiNat.res x n), ∀ z ∈ A (PiNat.res x n), dist y z < ε

theorem CantorScheme.VanishingDiam.map_continuous {β : Type u_1} {α : Type u_2} {A : List β → Set α} [PseudoMetricSpace α] [TopologicalSpace β] [DiscreteTopology β] (hA : VanishingDiam A) : Continuous (inducedMap A).snd

A scheme with vanishing diameter along each branch induces a continuous map.

theorem CantorScheme.ClosureAntitone.map_of_vanishingDiam {β : Type u_1} {α : Type u_2} {A : List β → Set α} [PseudoMetricSpace α] [CompleteSpace α] (hdiam : VanishingDiam A) (hanti : ClosureAntitone A) (hnonempty : ∀ (l : List β), (A l).Nonempty) : (inducedMap A).fst = Set.univ

A scheme on a complete space with vanishing diameter such that each set contains the closure of its children induces a total map.