From 52b5b5523b9506506a7a11ee1bbed74af9e2e389 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Mon, 4 Dec 2023 00:37:06 +0100 Subject: [PATCH] :pencil: Add installation instructions and push to github --- README.md | 30 ++++++++++++++ Rubin.lean | 27 +++++++++++++ Rubin/HomeoGroup.lean | 3 ++ Rubin/Topology.lean | 93 ++++++++++++++++++++++++++++++++++++++++++- 4 files changed, 152 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 99ac129..ba5520c 100644 --- a/README.md +++ b/README.md @@ -1 +1,31 @@ # Lean4 port of the proof of Rubin's Theorem + +THis repository contains a (WIP) computer proof of Rubin's Theorem, +which states that two groups (which satisfy a few conditions) that act on a topological space have a homeomorphism between them, +such that the homeomorphism preserves the group structure. + +It is based on ["A short proof of Rubin's Theorem"](https://arxiv.org/abs/2203.05930) (James Belk, Luke Elliott and Franceso Matucci), +and a good part of the computer proof was written in Lean 3 by [Laurent Bartholdi](https://www.math.uni-sb.de/ag/bartholdi/). + +The eventual goal of this computer proof is to have it land into [Mathlib](https://github.com/leanprover-community/mathlib4). + +## Installation and running + +You will need an installation of [`elan`](https://github.com/leanprover/elan) and `git`. + +Then, simply run the following: + +```sh +# Clone this repository +git clone https://github.com/adri326/rubin-lean4 + +# Navigate to the folder created by git +cd rubin-lean4 + +# This will download mathlib, and try to download a set of pre-compiled .olean files, +# so you won't have to re-compile the entirety of mathlib again (which takes a good hour or two) +lake exe cache get + +# Build the code (if no errors are printed then Lean was happy) +lake build +``` diff --git a/Rubin.lean b/Rubin.lean index c2b6a1b..de2e557 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -793,6 +793,33 @@ by exact rsupp_ss_clW exact clW_ss_U +-- TODO: implement Membership on AssociatedPoset +-- TODO: wrap these things in some neat structures +theorem proposition_3_5 {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] + [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α] + [hc : ContinuousMulAction G α] + (U : AssociatedPoset α) (F: Filter α): + (∃ p ∈ U.val, F.HasBasis (fun S: Set α => S ∈ AssociatedPoset.asSet α ∧ p ∈ S) id) + ↔ ∃ V : AssociatedPoset α, V ≤ U ∧ {W : AssociatedPoset α | W ≤ V} ⊆ { g •'' W | (g ∈ RigidStabilizer G U.val) (W ∈ F) } + := +by + constructor + { + simp + intro p p_in_U filter_basis + have assoc_poset_basis : TopologicalSpace.IsTopologicalBasis (AssociatedPoset.asSet α) := by + exact proposition_3_2 (G := G) + have F_eq_nhds : F = 𝓝 p := by + have nhds_basis := assoc_poset_basis.nhds_hasBasis (a := p) + rw [<-filter_basis.filter_eq] + rw [<-nhds_basis.filter_eq] + have p_in_int_cl := h_ld.isLocallyDense U U.regular.isOpen p p_in_U + -- TODO: show that ∃ V ⊆ closure (orbit (rist G U) p) + + sorry + } + sorry + end HomeoGroup -- variables [topological_space α] [topological_space β] [continuous_mul_action G α] [continuous_mul_action G β] diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean index 8fb4b0a..de798d3 100644 --- a/Rubin/HomeoGroup.lean +++ b/Rubin/HomeoGroup.lean @@ -151,6 +151,9 @@ by rw [HomeoGroup.from_toHomeomorph] rw [Rubin.ContinuousMulAction.toHomeomorph_toFun] +theorem HomeoGroup.smulImage_eq_image (g : HomeoGroup α) (S : Set α) : + g •'' S = ⇑g.toHomeomorph '' S := rfl + namespace Rubin section AssociatedPoset.Prelude diff --git a/Rubin/Topology.lean b/Rubin/Topology.lean index 1efaf82..59b8561 100644 --- a/Rubin/Topology.lean +++ b/Rubin/Topology.lean @@ -73,10 +73,101 @@ open Topology Note: `𝓝[≠] x` is notation for `nhdsWithin x {[x]}ᶜ`, ie. the neighborhood of x not containing itself. --/ class HasNoIsolatedPoints (α : Type _) [TopologicalSpace α] := + -- TODO: rename to nhdsWithin_ne_bot nhbd_ne_bot : ∀ x : α, 𝓝[≠] x ≠ ⊥ #align has_no_isolated_points Rubin.HasNoIsolatedPoints -instance has_no_isolated_points_neBot {α : Type _} [TopologicalSpace α] [h_nip: HasNoIsolatedPoints α] (x: α): Filter.NeBot (𝓝[≠] x) where +instance has_no_isolated_points_neBot₁ {α : Type _} [TopologicalSpace α] [h_nip: HasNoIsolatedPoints α] + (x: α) : Filter.NeBot (𝓝[≠] x) where ne' := h_nip.nhbd_ne_bot x +theorem Filter.NeBot.choose {α : Type _} (F : Filter α) [Filter.NeBot F] : + ∃ S : Set α, S ∈ F := +by + have res := (Filter.inhabitedMem (α := α) (f := F)).default + exact ⟨res.val, res.prop⟩ + + +theorem TopologicalSpace.IsTopologicalBasis.contains_point {α : Type _} [TopologicalSpace α] + {B : Set (Set α)} (B_basis : TopologicalSpace.IsTopologicalBasis B) (p : α) : + ∃ S : Set α, S ∈ B ∧ p ∈ S := +by + have nhds_basis := B_basis.nhds_hasBasis (a := p) + + rw [Filter.hasBasis_iff] at nhds_basis + let ⟨S₁, S₁_in_nhds⟩ := Filter.NeBot.choose (𝓝 p) + let ⟨S, ⟨⟨S_in_B, p_in_S⟩, _⟩⟩ := (nhds_basis S₁).mp S₁_in_nhds + exact ⟨S, S_in_B, p_in_S⟩ + +-- The collection of all the sets in `B` (a topological basis of `α`), such that `p` is in them. +def TopologicalBasisContaining {α : Type _} [TopologicalSpace α] + {B : Set (Set α)} (B_basis : TopologicalSpace.IsTopologicalBasis B) (p : α) : FilterBasis α +where + sets := {b ∈ B | p ∈ b} + nonempty := by + let ⟨S, S_in_B, p_in_S⟩ := TopologicalSpace.IsTopologicalBasis.contains_point B_basis p + use S + simp + tauto + inter_sets := by + intro S T ⟨S_in_B, p_in_S⟩ ⟨T_in_B, p_in_T⟩ + + have S_in_nhds := B_basis.mem_nhds_iff.mpr ⟨S, S_in_B, ⟨p_in_S, Eq.subset rfl⟩⟩ + have T_in_nhds := B_basis.mem_nhds_iff.mpr ⟨T, T_in_B, ⟨p_in_T, Eq.subset rfl⟩⟩ + + have ST_in_nhds : S ∩ T ∈ 𝓝 p := Filter.inter_mem S_in_nhds T_in_nhds + rw [B_basis.mem_nhds_iff] at ST_in_nhds + let ⟨U, props⟩ := ST_in_nhds + use U + simp + simp at props + tauto + +theorem TopologicalBasisContaining.mem_iff {α : Type _} [TopologicalSpace α] + {B : Set (Set α)} (B_basis : TopologicalSpace.IsTopologicalBasis B) (p : α) (S : Set α) : + S ∈ TopologicalBasisContaining B_basis p ↔ S ∈ B ∧ p ∈ S := +by + rw [<-FilterBasis.mem_sets] + rfl + +theorem TopologicalBasisContaining.mem_nhds {α : Type _} [TopologicalSpace α] + {B : Set (Set α)} (B_basis : TopologicalSpace.IsTopologicalBasis B) (p : α) (S : Set α) : + S ∈ TopologicalBasisContaining B_basis p → S ∈ 𝓝 p := +by + rw [TopologicalBasisContaining.mem_iff] + rw [B_basis.mem_nhds_iff] + intro ⟨S_in_B, p_in_S⟩ + use S + +instance TopologicalBasisContaining.neBot {α : Type _} [TopologicalSpace α] + {B : Set (Set α)} (B_basis : TopologicalSpace.IsTopologicalBasis B) (p : α) : + Filter.NeBot (TopologicalBasisContaining B_basis p).filter where + ne' := by + intro empty_in + rw [<-Filter.empty_mem_iff_bot, FilterBasis.mem_filter_iff] at empty_in + let ⟨S, ⟨S_in_basis, S_ss_empty⟩⟩ := empty_in + rw [TopologicalBasisContaining.mem_iff] at S_in_basis + exact S_ss_empty S_in_basis.right + +-- Note: the definition of "convergence" in the article doesn't quite match with the definition of ClusterPt +-- Instead, `F ≤ nhds p` should be used. + +-- Note: Filter.HasBasis is a stronger statement than just FilterBasis - it defines a two-way relationship between a filter and a property; if the property is true for a set, then any superset of it is part of the filter, and vice-versa. +-- With this, it's impossible for there to be a finer filter satisfying the property, +-- as is evidenced by `filter_eq`: stripping away the `Filter` allows us to uniquely reconstruct it from the property itself. + +-- Proposition 3.3.1 trivially follows from `TopologicalSpace.IsTopologicalBasis.nhds_hasBasis` and `disjoint_nhds_nhds`: if `F.HasBasis (S → S ∈ B ∧ p ∈ S)` and `F.HasBasis (S → S ∈ B ∧ q ∈ S)`, +-- then one can prove that `F ≤ nhds x` and `F ≤ nhds y` ~> `F = ⊥` +-- Proposition 3.3.2 becomes simply `TopologicalSpace.IsTopologicalBasis.nhds_hasBasis` +-- Proposition 3.3.3 is a consequence of the structure of `HasBasis` + +-- Proposition 3.4.1 can maybe be proven with `TopologicalSpace.IsTopologicalBasis.mem_closure_iff`? + +-- The tricky part here though is that "F is an ultra(pre)filter on B" can't easily be expressed. +-- I should maybe define a Prop for it, and show that "F is an ultrafilter on B" + "F tends to a point p" +-- is equivalent to `TopologicalSpace.IsTopologicalBasis.nhds_hasBasis`. + +-- The alternative is to only work with `Filter`, and state conditions with `Filter.HasBasis`, +-- since that will force the filter to be an ultraprefilter on B. + end Rubin