📝 Add installation instructions and push to github

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
+```

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 β]

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

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