Simplicity conjecture

DefinitionArea-preserving homeomorphisms of the disc supported in the interior#✓fully proved

Let \(\mathbb{D}\) be the closed unit disc in \(\mathbb{R}^2\) and let \(\omega\) be the restriction of Lebesgue measure to \(\mathbb{D}\). \(\mathrm{Homeo}_c(\mathbb{D}, \omega)\) is the subgroup of the group of homeomorphisms of \(\mathbb{D}\) consisting of the homeomorphisms \(\phi\) that preserve \(\omega\) and whose support, the closure of \(\{x \in \mathbb{D} : \phi(x) \neq x\}\), is contained in the open unit disc.

def Homeo : Subgroup (𝔻 ≃ₜ 𝔻) where
  carrier := {ϕ | MeasurePreserving ϕ volume volume ∧ fixedSupport ϕ ⊆ 𝔻ᵒ}
  one_mem' := ⟨MeasurePreserving.id _, by simp [one_def, fixedSupport_def]⟩
  inv_mem' {ϕ} := .imp (.symm ϕ.toMeasurableEquiv)
    (by simp [inv_def, fixedSupport_def, ← coe_symm_toEquiv])
  mul_mem' {ϕ ψ} := fun ⟨hϕ1, hϕ2⟩ ⟨hψ1, hψ2⟩ ↦ ⟨hϕ1.comp hψ1, by
    rw [fixedSupport_def] at hϕ2 hψ2 ⊢
    have : fixedPoints ϕ ∩ fixedPoints ψ ⊆ fixedPoints (ϕ * ψ) := inter_subset_fixedPoints_comp
    grw [← this, Set.compl_inter, closure_union, hϕ2, hψ2, Set.union_self]⟩

Used by 1

Used bySimplicity conjecture

TheoremSimplicity conjecture#●ready to prove

Let \(\mathbb{D} \subseteq \mathbb{R}^2\) be the closed unit disc and let \(\omega\) be the restriction of Lebesgue measure to \(\mathbb{D}\). The group \(\mathrm{Homeo}_c(\mathbb{D}, \omega)\) of homeomorphisms of \(\mathbb{D}\) that preserve \(\omega\) and whose support, the closure of the set of non-fixed points, lies in the open unit disc is not simple: it is trivial or it has a normal subgroup other than the trivial subgroup and the whole group.

public theorem_wanted theorem_1_2 : ¬ IsSimpleGroup Homeo

Sources

• D. Cristofaro-Gardiner, V. Humilière, and S. Seyfaddini, Proof of the simplicity conjecture, Annals of Math, 199 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_simplicity_conjecture of the lean-eval benchmark.

Uses 1

Statement usesArea-preserving homeomorphisms of the disc supported in the interior

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.