(Topological) Schemes and their induced maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

cantor_scheme.induced_map 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, (induced_map A).1 is the domain and (induced_map 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.nth or stream.take do not have their intended meaning in this file. See instead pi_nat.res.

References #

[Kec95] (Chapters 6-7)

Tags #

scheme, cantor scheme, lusin scheme, approximation.

source

noncomputable def cantor_scheme.induced_map {β : 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.

Equations

cantor_scheme.induced_map A = ⟨λ (x : ℕ → β), (⋂ (n : ℕ), A (pi_nat.res x n)).nonempty, λ (x : ↥(λ (x : ℕ → β), (⋂ (n : ℕ), A (pi_nat.res x n)).nonempty)), set.nonempty.some _⟩

source

@[protected]

def cantor_scheme.antitone {β : Type u_1} {α : Type u_2} (A : list β → set α) :

Prop

A scheme is antitone if each set contains its children.

Equations

cantor_scheme.antitone A = ∀ (l : list β) (a : β), A (a :: l) ⊆ A l

source

def cantor_scheme.closure_antitone {β : Type u_1} {α : Type u_2} (A : list β → set α) [topological_space α] :

Prop

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

Equations

cantor_scheme.closure_antitone A = ∀ (l : list β) (a : β), closure (A (a :: l)) ⊆ A l

source

@[protected]

def cantor_scheme.disjoint {β : Type u_1} {α : Type u_2} (A : list β → set α) :

Prop

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

Equations

cantor_scheme.disjoint A = ∀ (l : list β), pairwise (λ (a b : β), disjoint (A (a :: l)) (A (b :: l)))

source

theorem cantor_scheme.map_mem {β : Type u_1} {α : Type u_2} {A : list β → set α} (x : ↥((cantor_scheme.induced_map A).fst)) (n : ℕ) :

(cantor_scheme.induced_map A).snd x ∈ A (pi_nat.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.

source

@[protected]

theorem cantor_scheme.closure_antitone.antitone {β : Type u_1} {α : Type u_2} {A : list β → set α} [topological_space α] (hA : cantor_scheme.closure_antitone A) :

cantor_scheme.antitone A

source

@[protected]

theorem cantor_scheme.antitone.closure_antitone {β : Type u_1} {α : Type u_2} {A : list β → set α} [topological_space α] (hanti : cantor_scheme.antitone A) (hclosed : ∀ (l : list β), is_closed (A l)) :

cantor_scheme.closure_antitone A

source

theorem cantor_scheme.disjoint.map_injective {β : Type u_1} {α : Type u_2} {A : list β → set α} (hA : cantor_scheme.disjoint A) :

function.injective (cantor_scheme.induced_map A).snd

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

source

def cantor_scheme.vanishing_diam {β : Type u_1} {α : Type u_2} (A : list β → set α) [pseudo_metric_space α] :

Prop

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

Equations

cantor_scheme.vanishing_diam A = ∀ (x : ℕ → β), filter.tendsto (λ (n : ℕ), emetric.diam (A (pi_nat.res x n))) filter.at_top (nhds 0)

source

theorem cantor_scheme.vanishing_diam.dist_lt {β : Type u_1} {α : Type u_2} {A : list β → set α} [pseudo_metric_space α] (hA : cantor_scheme.vanishing_diam A) (ε : ℝ) (ε_pos : 0 < ε) (x : ℕ → β) :

∃ (n : ℕ), ∀ (y : α), y ∈ A (pi_nat.res x n) → ∀ (z : α), z ∈ A (pi_nat.res x n) → has_dist.dist y z < ε

source

theorem cantor_scheme.vanishing_diam.map_continuous {β : Type u_1} {α : Type u_2} {A : list β → set α} [pseudo_metric_space α] [topological_space β] [discrete_topology β] (hA : cantor_scheme.vanishing_diam A) :

continuous (cantor_scheme.induced_map A).snd

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

source

theorem cantor_scheme.closure_antitone.map_of_vanishing_diam {β : Type u_1} {α : Type u_2} {A : list β → set α} [pseudo_metric_space α] [complete_space α] (hdiam : cantor_scheme.vanishing_diam A) (hanti : cantor_scheme.closure_antitone A) (hnonempty : ∀ (l : list β), (A l).nonempty) :

(cantor_scheme.induced_map 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.