Dimension-raising open maps
TheoremKolmogorov's open map raising dimension#●ready to prove
An interior (open) mapping can raise dimension: there are compact metrizable spaces \(X\) and \(Y\), where \(X\) has small inductive dimension exactly \(1\) and \(Y\) has small inductive dimension exactly \(2\), and a continuous open surjective map \(f \colon X \to Y\). A space has small inductive dimension exactly \(n\) when its small inductive dimension is at most \(n\) but not at most \(n - 1\).
theorem_wanted kolmogorovInteriorMapRaisesDimension :
∃ (X Y : Type) (_ : TopologicalSpace X) (_ : TopologicalSpace Y) (_ : CompactSpace X)
(_ : CompactSpace Y) (_ : TopologicalSpace.MetrizableSpace X)
(_ : TopologicalSpace.MetrizableSpace Y),
HasSmallInductiveDimensionLE X 1 ∧ ¬ HasSmallInductiveDimensionLE X 0 ∧
HasSmallInductiveDimensionLE Y 2 ∧ ¬ HasSmallInductiveDimensionLE Y 1 ∧
∃ f : X → Y, Continuous f ∧ IsOpenMap f ∧ Function.Surjective f
Sources
- S. Eilenberg, Problem 136 of the Scottish Book, asking whether an interior mapping can increase dimension; answered affirmatively by A. Kolmogorov, Annals of Mathematics 38 (1937), pp. 34-38, who gave an example of a continuous interior mapping raising dimension from 1 to 2, as recorded in the typescript Ad 136.
AbbreviationThe p-dimensional cube#✓fully proved
For \(p \in \mathbb{N}\), the cube \(I^p = [0,1]^p\) is the set of points of \(\mathbb{R}^p\) all of whose coordinates lie in \([0,1]\), with the subspace topology.
Used by 1
TheoremOpen maps can raise the dimension of a cube#●ready to prove
There are natural numbers \(p < q\) and a continuous, open, surjective map \(f \colon I^p \to I^q\), where \(I^p = [0,1]^p\) and \(I^q = [0,1]^q\) are the \(p\)- and \(q\)-dimensional cubes.
Keldysh constructed such maps, refuting the claim of Scottish Book Problem 187, part (3), that no open (interior) continuous map of a \(p\)-dimensional cube onto a \(q\)-dimensional cube exists for \(p < q\).
theorem_wanted scottishBook187c_refuted :
∃ p q : ℕ, p < q ∧ ∃ f : Cube p → Cube q, Continuous f ∧ IsOpenMap f ∧
Function.Surjective f
abbrev Cube (p : ℕ) : Type :=
↥(Set.pi Set.univ (fun _ : Fin p => Set.Icc (0 : ℝ) 1))
WantedExt/Topology/ScottishBook187cWanted.lean:25
Sources
- P. Alexandroff, Problem 187 part (3) of the Scottish Book, typescript pp. 82–83; see the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015).
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.