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.

abbrev Cube (p : ℕ) : Type :=
  ↥(Set.pi Set.univ (fun _ : Fin p => Set.Icc (0 : ℝ) 1))
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
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
1 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.