Algebraic topology

Homotopy groups, singular homology and other algebraic invariants of spaces, with classical theorems such as Borsuk–Ulam, Hurewicz and Hopf invariant one.

• Adapting families of maps to open covers
• Bing's house with two rooms
• Homotopy groups of spheres
• Hurewicz theorem
• Solid condensed homology of CW complexes

TheoremAdams' theorem on spheres that are H-spaces#●ready to prove

For every natural number \(n\), the unit sphere \(S^n\) of the Euclidean space \(\mathbb{R}^{n+1}\) admits an H-space structure if and only if \(n = 0\), \(n = 1\), \(n = 3\) or \(n = 7\). Here an H-space structure on \(S^n\) is a continuous map \(\mu \colon S^n \times S^n \to S^n\) together with a point \(e \in S^n\) such that \(\mu(e, e) = e\) and the maps \(x \mapsto \mu(e, x)\) and \(x \mapsto \mu(x, e)\) are both homotopic to the identity relative to \(\{e\}\).

public theorem_wanted hSpace_sphere_iff (n : ℕ) :
    Nonempty (HSpace (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1)) ↔
      n = 0 ∨ n = 1 ∨ n = 3 ∨ n = 7

Sources

• J. F. Adams, 'On the non-existence of elements of Hopf invariant one', Ann. of Math. 72 (1960), 20-104; J. F. Adams and M. F. Atiyah, 'K-theory and the Hopf invariant', Quart. J. Math. Oxford 17 (1966), 31-38. See also A. Hatcher, 'Algebraic Topology', Section 4.B. Problem hSpace_sphere_iff of the lean-eval benchmark.

TheoremBorsuk–Ulam theorem#✓fully proved

Let \(n\) be a natural number and let \(S^n\) be the unit sphere in the Euclidean space \(\mathbb{R}^{n+1}\). For every continuous map \(f \colon S^n \to \mathbb{R}^n\) there is a point \(x \in S^n\) with \(f(x) = f(-x)\).

public theorem borsukUlam
    {n : ℕ} (f : sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1 → EuclideanSpace ℝ (Fin n))
    (hf : Continuous f) :
    ∃ x : sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1, f x = f (-x)

Sources

• K. Borsuk, Fund. Math. 20 (1933) 177–190 antipodal theorem; S. Ulam; J. Matoušek, Using the Borsuk–Ulam Theorem; Lean states EuclideanSpace ℝ (Fin (n+1)) to Fin n specialization.

Used by 1

Used byHam sandwich theorem

TheoremHam sandwich theorem#✓fully proved

Let \(n \ge 1\) and let \(\mu_1, \dots, \mu_n\) be finite Borel measures on the Euclidean space \(\mathbb{R}^n\), each absolutely continuous with respect to Lebesgue measure. Then there exist a unit vector \(v \in \mathbb{R}^n\) and a real number \(t\) such that for every \(i\), both closed half-spaces \(\{x : \langle v, x \rangle \le t\}\) and \(\{x : \langle v, x \rangle \ge t\}\) have \(\mu_i\)-measure equal to \(\mu_i(\mathbb{R}^n)/2\).

public theorem ham_sandwich
    {n : ℕ} (hn : 0 < n)
    [MeasurableSpace (EuclideanSpace ℝ (Fin n))]
    [BorelSpace (EuclideanSpace ℝ (Fin n))]
    (μ : Fin n → Measure (EuclideanSpace ℝ (Fin n)))
    (hfin : ∀ i, IsFiniteMeasure (μ i))
    (hac : ∀ i, μ i ≪ volume) :
    ∃ (v : EuclideanSpace ℝ (Fin n)) (t : ℝ), ‖v‖ = 1 ∧
      ∀ i : Fin n, μ i {x | ⟪v, x⟫_ℝ ≤ t} = μ i Set.univ / 2 ∧
        μ i {x | ⟪v, x⟫_ℝ ≥ t} = μ i Set.univ / 2

Sources

• A. H. Stone and J. W. Tukey, Duke Math. J. 9 (1942) 356–359 ham sandwich theorem; J. Matoušek, Using the Borsuk–Ulam Theorem; Lean states measure-theoretic Euclidean specialization with μ i ≪ volume making the bisecting hyperplane null.

Uses 1

Proof usesBorsuk–Ulam theorem

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.