✨ Prove proposition 3.2

Rubin.lean

@@ -12,6 +12,7 @@ import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.GroupTheory.Exponent
 import Mathlib.GroupTheory.Perm.Basic
 import Mathlib.Topology.Basic
+import Mathlib.Topology.Bases
 import Mathlib.Topology.Compactness.Compact
 import Mathlib.Topology.Separation
 import Mathlib.Topology.Homeomorph
@@ -706,11 +707,13 @@ section HomeoGroup
 
 open Topology
 
-theorem proposition_3_2 {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
+-- TODO: clean this lemma to not mention W anymore?
+lemma proposition_3_2_subset (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
   [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α]
   [ContinuousMulAction G α]
   {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U) :
-  ∃ (W : Set α), W ∈ 𝓝 p ∧ closure W ⊆ U ∧ ∃ (g : G), g ∈ RigidStabilizer G W ∧ p ∈ RegularSupport α g :=
+  ∃ (W : Set α), W ∈ 𝓝 p ∧ closure W ⊆ U ∧
+  ∃ (g : G), g ∈ RigidStabilizer G W ∧ p ∈ RegularSupport α g ∧ RegularSupport α g ⊆ closure W :=
 by
   have U_in_nhds : U ∈ 𝓝 p := by
     rw [mem_nhds_iff]
@@ -741,17 +744,55 @@ by
 
   have p_in_int_W : p ∈ interior W := W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
 
-  let ⟨g, g_in_rist, g_moves_p⟩ := get_moving_elem_in_rigidStabilizer G p_in_int_W
+  let ⟨g, g_in_rist, g_moves_p⟩ := get_moving_elem_in_rigidStabilizer G isOpen_interior p_in_int_W
 
   use g
-  constructor
+  repeat' apply And.intro
   · apply rigidStabilizer_mono interior_subset
     simp
     exact g_in_rist
   · rw [<-mem_support] at g_moves_p
     apply support_subset_regularSupport
     exact g_moves_p
+  · rw [rigidStabilizer_support] at g_in_rist
+    apply subset_trans
+    exact regularSupport_subset_closure_support
+    apply closure_mono
+    apply subset_trans
+    exact g_in_rist
+    exact interior_subset
 
+theorem proposition_3_2 {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
+  [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α]
+  [hc : ContinuousMulAction G α] :
+  TopologicalSpace.IsTopologicalBasis (AssociatedPoset.asSet α) :=
+by
+  -- Note: the name later changes to isTopologicalBasis_of_isOpen_of_nhds
+  apply TopologicalSpace.isTopologicalBasis_of_open_of_nhds
+  {
+    intro U U_in_poset
+    rw [AssociatedPoset.mem_asSet] at U_in_poset
+    let ⟨T, T_val⟩ := U_in_poset
+    rw [<-T_val]
+    exact T.regular.isOpen
+  }
+  intro p U p_in_U U_open
+
+  let ⟨W, _, clW_ss_U, ⟨g, _, p_in_rsupp, rsupp_ss_clW⟩⟩ := proposition_3_2_subset G U_open p_in_U
+  use RegularSupport α g
+  repeat' apply And.intro
+  · rw [AssociatedPoset.mem_asSet']
+    constructor
+    exact ⟨p, p_in_rsupp⟩
+    use {(ContinuousMulAction.toHomeomorph α g : HomeoGroup α)}
+    unfold AssociatedPosetElem
+    simp
+    unfold RegularSupport
+    rw [<-homeoGroup_support_eq_support_toHomeomorph g]
+  · exact p_in_rsupp
+  · apply subset_trans
+    exact rsupp_ss_clW
+    exact clW_ss_U
 
 end HomeoGroup
 

Rubin/HomeoGroup.lean

@@ -4,6 +4,7 @@ import Mathlib.Topology.Homeomorph
 
 import Rubin.LocallyDense
 import Rubin.Topology
+import Rubin.Support
 import Rubin.RegularSupport
 
 structure HomeoGroup (α : Type _) [TopologicalSpace α] extends
@@ -140,6 +141,16 @@ instance homeoGroup_mulAction₁_faithful : FaithfulSMul (HomeoGroup α) α wher
     simp
     exact hyp x
 
+theorem homeoGroup_support_eq_support_toHomeomorph {G : Type _}
+  [Group G] [MulAction G α] [Rubin.ContinuousMulAction G α] (g : G) :
+  Rubin.Support α g = Rubin.Support α (HomeoGroup.from (Rubin.ContinuousMulAction.toHomeomorph α g)) :=
+by
+  ext x
+  repeat rw [Rubin.mem_support]
+  rw [<-HomeoGroup.smul₁_def]
+  rw [HomeoGroup.from_toHomeomorph]
+  rw [Rubin.ContinuousMulAction.toHomeomorph_toFun]
+
 namespace Rubin
 
 section AssociatedPoset.Prelude
@@ -397,6 +408,44 @@ by
   apply smulImage_mono
   assumption
 
+instance associatedPoset_coeSet : Coe (AssociatedPoset α) (Set α) where
+  coe := AssociatedPoset.val
+
+def asSet (α : Type _) [TopologicalSpace α]: Set (Set α) :=
+  { S : Set α | ∃ T : AssociatedPoset α, T.val = S }
+
+theorem asSet_def :
+  AssociatedPoset.asSet α = { S : Set α | ∃ T : AssociatedPoset α, T.val = S } := rfl
+
+theorem mem_asSet (S : Set α) :
+  S ∈ AssociatedPoset.asSet α ↔ ∃ T : AssociatedPoset α, T.val = S :=
+by
+  rw [asSet_def]
+  simp
+
+theorem mem_asSet' (S : Set α) :
+  S ∈ AssociatedPoset.asSet α ↔ Set.Nonempty S ∧ ∃ seed : Finset (HomeoGroup α), S = AssociatedPosetElem seed :=
+by
+  rw [asSet_def]
+  simp
+  constructor
+  · intro ⟨T, T_eq⟩
+    rw [<-T_eq]
+    constructor
+    simp
+
+    let ⟨⟨seed, _⟩, eq⟩ := T.val_has_seed
+    rw [AssociatedPosetSeed.val_def] at eq
+    simp at eq
+    use seed
+    exact eq.symm
+  · intro ⟨S_nonempty, ⟨seed, val_from_seed⟩⟩
+    rw [val_from_seed] at S_nonempty
+    use fromSeed ⟨seed, S_nonempty⟩
+    rw [val_from_seed]
+    simp
+    rw [AssociatedPosetSeed.val_def]
+
 end AssociatedPoset
 
 section Other

Rubin/LocallyDense.lean

@@ -8,9 +8,22 @@ namespace Rubin
 
 open Topology
 
+/--
+A group action is said to be "locally dense" if for any open set `U` and `p ∈ U`,
+the closure of the orbit of `p` under the `RigidStabilizer G U` contains a neighborhood of `p`.
+
+The definition provided here is an equivalent one, that does not require using filters.
+See [`LocallyDense.from_rigidStabilizer_in_nhds`] and [`LocallyDense.rigidStabilizer_in_nhds`]
+to translate from/to the original definition.
+
+A weaker relationship, [`LocallyMoving`], is used whenever possible.
+The main difference between the two is that `LocallyMoving` does not allow us to find a group member
+`g ∈ G` such that `g • p ≠ p` — it only allows us to know that `∃ g ∈ RigidStabilizer G U, g ≠ 1`.
+--/
 class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :=
   isLocallyDense:
     ∀ U : Set α,
+    IsOpen U →
     ∀ p ∈ U,
     p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p))
 #align is_locally_dense Rubin.LocallyDense
@@ -21,10 +34,7 @@ theorem LocallyDense.from_rigidStabilizer_in_nhds (G α : Type _) [Group G] [Top
 by
   intro hyp
   constructor
-  intro U p p_in_U
-
-  -- TODO: potentially add that requirement to LocallyDense?
-  have U_open : IsOpen U := sorry
+  intro U U_open p p_in_U
 
   have closure_in_nhds := hyp U U_open p p_in_U
   rw [mem_nhds_iff] at closure_in_nhds
@@ -32,14 +42,24 @@ by
   rw [mem_interior]
   exact closure_in_nhds
 
--- TODO: rename
-lemma LocallyDense.nonEmpty {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α]:
+theorem LocallyDense.rigidStabilizer_in_nhds (G α : Type _) [Group G] [TopologicalSpace α]
+  [MulAction G α] [LocallyDense G α]
+  {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U)
+:
+  closure (MulAction.orbit (RigidStabilizer G U) p) ∈ 𝓝 p :=
+by
+  rw [mem_nhds_iff]
+  rw [<-mem_interior]
+  apply LocallyDense.isLocallyDense <;> assumption
+
+lemma LocallyDense.elem_from_nonEmpty {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α]:
   ∀ {U : Set α},
+  IsOpen U →
   Set.Nonempty U →
   ∃ p ∈ U, p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) :=
 by
-  intros U H_ne
-  exact ⟨H_ne.some, H_ne.some_mem, LocallyDense.isLocallyDense U H_ne.some H_ne.some_mem⟩
+  intros U U_open H_ne
+  exact ⟨H_ne.some, H_ne.some_mem, LocallyDense.isLocallyDense U U_open H_ne.some H_ne.some_mem⟩
 
 /--
 This is a stronger statement than `LocallyMoving.get_nontrivial_rist_elem`,
@@ -50,7 +70,7 @@ The condition that `Filer.NeBot (𝓝[≠] p)` is automatically satisfied by the
 theorem get_moving_elem_in_rigidStabilizer (G : Type _) {α : Type _}
   [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α]
   [T1Space α] {p : α} [Filter.NeBot (𝓝[≠] p)]
-  {U : Set α} (p_in_U : p ∈ U) :
+  {U : Set α} (U_open : IsOpen U) (p_in_U : p ∈ U) :
   ∃ g : G, g ∈ RigidStabilizer G U ∧ g • p ≠ p :=
 by
   by_contra g_not_exist
@@ -76,7 +96,7 @@ by
     rw [closure_singleton]
     rw [interior_singleton]
 
-  have p_in_regular_orbit := LocallyDense.isLocallyDense (G := G) U p p_in_U
+  have p_in_regular_orbit := LocallyDense.isLocallyDense (G := G) U U_open p p_in_U
   rw [regular_orbit_empty] at p_in_regular_orbit
   exact p_in_regular_orbit
 
@@ -110,9 +130,9 @@ instance dense_locally_moving [T2Space α]
   LocallyMoving G α
 where
   locally_moving := by
-    intros U _ H_nonempty
+    intros U U_open H_nonempty
     by_contra h_rs
-    have ⟨elem, ⟨_, some_in_orbit⟩⟩ := H_ld.nonEmpty H_nonempty
+    have ⟨elem, ⟨_, some_in_orbit⟩⟩ := H_ld.elem_from_nonEmpty U_open H_nonempty
     rw [h_rs] at some_in_orbit
     simp at some_in_orbit
 

Rubin/Topology.lean

@@ -12,6 +12,34 @@ class ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] [MulAc
   continuous : ∀ g : G, Continuous (fun x: α => g • x)
 #align continuous_mul_action Rubin.ContinuousMulAction
 
+def ContinuousMulAction.toHomeomorph {G : Type _} (α : Type _)
+  [Group G] [TopologicalSpace α] [MulAction G α] [hc : ContinuousMulAction G α]
+  (g : G) : Homeomorph α α
+where
+  toFun := fun x => g • x
+  invFun := fun x => g⁻¹ • x
+  left_inv := by
+    intro y
+    simp
+  right_inv := by
+    intro y
+    simp
+  continuous_toFun := by
+    simp
+    exact hc.continuous _
+  continuous_invFun := by
+    simp
+    exact hc.continuous _
+
+theorem ContinuousMulAction.toHomeomorph_toFun {G : Type _} (α : Type _)
+  [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α]
+  (g : G) : (ContinuousMulAction.toHomeomorph α g).toFun = fun x => g • x := rfl
+
+
+theorem ContinuousMulAction.toHomeomorph_invFun {G : Type _} (α : Type _)
+  [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α]
+  (g : G) : (ContinuousMulAction.toHomeomorph α g).invFun = fun x => g⁻¹ • x := rfl
+
 -- TODO: give this a notation?
 structure EquivariantHomeomorph (G α β : Type _) [Group G] [TopologicalSpace α]
     [TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where