🔥 New notation for RigidStabilizer and prove first lemma for proposition 3.5

Rubin.lean

@@ -355,7 +355,7 @@ lemma lemma_2_2 (G: Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAc
   [ContinuousMulAction G α] [FaithfulSMul G α]
   [T2Space α] [h_lm : LocallyMoving G α]
   {U : Set α} (U_open : IsOpen U) (U_nonempty : Set.Nonempty U) :
-  Monoid.exponent (RigidStabilizer G U) = 0 :=
+  Monoid.exponent G•[U] = 0 :=
 by
   by_contra exp_ne_zero
 
@@ -548,7 +548,7 @@ lemma proposition_2_1 {G α : Type _}
   [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] [T2Space α]
   [LocallyMoving G α] [h_faithful : FaithfulSMul G α]
   (f : G) :
-  AlgebraicCentralizer f = RigidStabilizer G (RegularSupport α f) :=
+  AlgebraicCentralizer f = G•[RegularSupport α f] :=
 by
   ext h
 
@@ -634,7 +634,7 @@ by
 theorem rigidStabilizer_inter_bot_iff_regularSupport_disj {G α : Type _}
   [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] [LocallyMoving G α] [FaithfulSMul G α]
   {f g : G} :
-  RigidStabilizer G (RegularSupport α f) ⊓ RigidStabilizer G (RegularSupport α g) = ⊥
+  G•[RegularSupport α f] ⊓ G•[RegularSupport α g] = ⊥
   ↔ Disjoint (RegularSupport α f) (RegularSupport α g) :=
 by
   rw [<-rigidStabilizer_inter]
@@ -782,34 +782,23 @@ def RSuppOrbit {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
   { g •'' W | (g ∈ H) (W ∈ F) }
 
 lemma moving_elem_of_open_subset_closure_orbit {U V : Set α} (U_open : IsOpen U) (U_nonempty : Set.Nonempty U)
-  {p : α} (p_in_V : p ∈ V) (U_ss_clOrbit : U ⊆ closure (MulAction.orbit (RigidStabilizer G V) p)) :
-  ∃ h : G, h ∈ RigidStabilizer G V ∧ h • p ∈ U :=
+  {p : α} (U_ss_clOrbit : U ⊆ closure (MulAction.orbit G•[V] p)) :
+  ∃ h : G, h ∈ G•[V] ∧ h • p ∈ U :=
 by
-  have U_ss_clV : U ⊆ closure V := by
-    apply subset_trans
-    exact U_ss_clOrbit
-    apply closure_mono
-    exact orbit_rigidStabilizer_subset p_in_V
-
-  by_cases (RigidStabilizer G V) = ⊥
-  case pos rist_bot =>
-    rw [rist_bot] at U_ss_clOrbit
-    simp at U_ss_clOrbit
-    use 1
-    constructor
-    exact Subgroup.one_mem _
-    rw [one_smul]
-    let ⟨q, q_in_U⟩ := U_nonempty
-    rw [<-U_ss_clOrbit _ q_in_U]
-    assumption
-  case neg rist_ne_bot =>
-    rw [<-ne_eq, Subgroup.ne_bot_iff_exists_ne_one] at rist_ne_bot
-    let ⟨⟨g, g_in_rist⟩, g_ne_one⟩ := rist_ne_bot
-    rw [ne_eq, Subgroup.mk_eq_one_iff, <-ne_eq] at g_ne_one
+  have p_in_orbit : p ∈ MulAction.orbit G•[V] p := by simp
 
-    -- Idea: show that `U ∩ Orb(p, G_U)` is nonempty?
-    sorry
+  have ⟨q, ⟨q_in_U, q_in_orbit⟩⟩ := inter_of_open_subset_of_closure
+    U_open U_nonempty ⟨p, p_in_orbit⟩ U_ss_clOrbit
 
+  rw [MulAction.mem_orbit_iff] at q_in_orbit
+  let ⟨⟨h, h_in_orbit⟩, hq_eq_p⟩ := q_in_orbit
+  simp at hq_eq_p
+
+  use h
+  constructor
+  assumption
+  rw [hq_eq_p]
+  assumption
 
 lemma compact_subset_of_rsupp_basis [LocallyCompactSpace α]
   (U : RegularSupportBasis α):
@@ -885,6 +874,8 @@ by
       simp at W_in_subsets
       let ⟨W_in_basis, W_subset_rsupp⟩ := W_in_subsets
       clear W_in_subsets g' g'_ne_one
+      unfold RSuppOrbit
+      simp
 
       -- We have that W is a subset of the closure of the orbit of G_U
       have W_ss_clOrbit : W ⊆ closure (MulAction.orbit (↥(RigidStabilizer G U.val)) p) := by
@@ -899,9 +890,8 @@ by
             rw [<-closure_closure (s := MulAction.orbit _ _)]
             apply closure_mono
             assumption
-      unfold RSuppOrbit
-      simp
 
+      -- W is also open and nonempty...
       have W_open : IsOpen W := by
         let ⟨W', W'_eq⟩ := (RegularSupportBasis.mem_asSet _).mp W_in_basis
         rw [<-W'_eq]
@@ -911,8 +901,8 @@ by
         rw [<-W'_eq]
         exact W'.nonempty
 
-      -- We get an element `h` such that `h • p ∈ W` and `h ∈ G_U`
-      let ⟨h, h_in_rist, hp_in_W⟩ := moving_elem_of_open_subset_closure_orbit W_open W_nonempty p_in_U W_ss_clOrbit
+      -- So we can get an element `h` such that `h • p ∈ W` and `h ∈ G_U`
+      let ⟨h, h_in_rist, hp_in_W⟩ := moving_elem_of_open_subset_closure_orbit W_open W_nonempty W_ss_clOrbit
 
       use h
       constructor

Rubin/LocallyDense.lean

@@ -29,7 +29,7 @@ class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G
 #align is_locally_dense Rubin.LocallyDense
 
 theorem LocallyDense.from_rigidStabilizer_in_nhds (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :
-  (∀ U : Set α, IsOpen U → ∀ p ∈ U, closure (MulAction.orbit (RigidStabilizer G U) p) ∈ 𝓝 p) →
+  (∀ U : Set α, IsOpen U → ∀ p ∈ U, closure (MulAction.orbit G•[U] p) ∈ 𝓝 p) →
   LocallyDense G α :=
 by
   intro hyp
@@ -46,7 +46,7 @@ theorem LocallyDense.rigidStabilizer_in_nhds (G α : Type _) [Group G] [Topologi
   [MulAction G α] [LocallyDense G α]
   {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U)
 :
-  closure (MulAction.orbit (RigidStabilizer G U) p) ∈ 𝓝 p :=
+  closure (MulAction.orbit G•[U] p) ∈ 𝓝 p :=
 by
   rw [mem_nhds_iff]
   rw [<-mem_interior]
@@ -56,7 +56,7 @@ lemma LocallyDense.elem_from_nonEmpty {G α : Type _} [Group G] [TopologicalSpac
   ∀ {U : Set α},
   IsOpen U →
   Set.Nonempty U →
-  ∃ p ∈ U, p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) :=
+  ∃ p ∈ U, p ∈ interior (closure (MulAction.orbit G•[U] p)) :=
 by
   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⟩
@@ -71,7 +71,7 @@ theorem get_moving_elem_in_rigidStabilizer (G : Type _) {α : Type _}
   [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α]
   [T1Space α] {p : α} [Filter.NeBot (𝓝[≠] p)]
   {U : Set α} (U_open : IsOpen U) (p_in_U : p ∈ U) :
-  ∃ g : G, g ∈ RigidStabilizer G U ∧ g • p ≠ p :=
+  ∃ g : G, g ∈ G•[U] ∧ g • p ≠ p :=
 by
   by_contra g_not_exist
   rw [<-Classical.not_forall_not] at g_not_exist
@@ -112,7 +112,7 @@ theorem LocallyMoving.get_nontrivial_rist_elem {G α : Type _}
   {U: Set α}
   (U_open : IsOpen U)
   (U_nonempty : U.Nonempty) :
-  ∃ x : G, x ∈ RigidStabilizer G U ∧ x ≠ 1 :=
+  ∃ x : G, x ∈ G•[U] ∧ x ≠ 1 :=
 by
   have rist_ne_bot := h_lm.locally_moving U U_open U_nonempty
   exact (or_iff_right rist_ne_bot).mp (Subgroup.bot_or_exists_ne_one _)

Rubin/RigidStabilizer.lean

@@ -11,7 +11,14 @@ def rigidStabilizer' (G : Type _) [Group G] [MulAction G α] (U : Set α) : Set
   {g : G | ∀ x : α, g • x = x ∨ x ∈ U}
 #align rigid_stabilizer' Rubin.rigidStabilizer'
 
--- A subgroup of G for which `Support α g ⊆ U`, or in other words, all elements of `G` that don't move points outside of `U`.
+/--
+A "rigid stabilizer" is a subgroup of `G` associated with a set `U` for which `Support α g ⊆ U` is true for all of its elements.
+
+In other words, a rigid stabilizer for a set `U` contains all elements of `G` that don't move points outside of `U`.
+
+The notation for this subgroup is `G•[U]`.
+You might sometimes find an expression written as `↑G•[U]` when `G•[U]` is used as a set.
+--/
 def RigidStabilizer (G : Type _) [Group G] [MulAction G α] (U : Set α) : Subgroup G
     where
   carrier := {g : G | ∀ (x) (_ : x ∉ U), g • x = x}
@@ -20,6 +27,8 @@ def RigidStabilizer (G : Type _) [Group G] [MulAction G α] (U : Set α) : Subgr
   one_mem' x _ := one_smul G x
 #align rigid_stabilizer Rubin.RigidStabilizer
 
+notation:max G "•[" U "]" => RigidStabilizer G U
+
 variable {G α: Type _}
 variable [Group G]
 variable [MulAction G α]
@@ -50,7 +59,7 @@ by
 theorem monotone_rigidStabilizer : Monotone (RigidStabilizer (α := α) G) := fun _ _ => rigidStabilizer_mono
 
 theorem rigidStabilizer_compl [FaithfulSMul G α] {U : Set α} {f : G} (f_ne_one : f ≠ 1) :
-  f ∈ RigidStabilizer G (Uᶜ) → f ∉ RigidStabilizer G U :=
+  f ∈ G•[Uᶜ] → f ∉ G•[U] :=
 by
   intro f_in_rist_compl
   intro f_in_rist
@@ -60,16 +69,6 @@ by
   have supp_empty : Support α f = ∅ := empty_of_subset_disjoint f_in_rist_compl.symm f_in_rist
   exact f_ne_one ((support_empty_iff f).mp supp_empty)
 
--- TODO: remove?
-theorem rigidStabilizer_to_subgroup_closure {U : Set α} :
-  RigidStabilizer G U = Subgroup.closure { h : G | Support α h ⊆ U } :=
-by
-  ext g
-  simp only [<-rigidStabilizer_support]
-  have set_eq : {h | h ∈ RigidStabilizer G U} = (RigidStabilizer G U : Set G) := rfl
-  rw [set_eq]
-  rw [Subgroup.closure_eq]
-
 theorem commute_if_rigidStabilizer_and_disjoint {g h : G} {U : Set α} [FaithfulSMul G α] :
   g ∈ RigidStabilizer G U → Disjoint U (Support α h) → Commute g h :=
 by
@@ -129,7 +128,7 @@ by
   }
 
 theorem rigidStabilizer_inter (U V : Set α) :
-  RigidStabilizer G (U ∩ V) = RigidStabilizer G U ⊓ RigidStabilizer G V :=
+  G•[U ∩ V] = G•[U] ⊓ G•[V] :=
 by
   ext x
   simp
@@ -137,7 +136,7 @@ by
   rw [Set.subset_inter_iff]
 
 theorem rigidStabilizer_empty (G α: Type _) [Group G] [MulAction G α] [FaithfulSMul G α]:
-  RigidStabilizer G (α := α) ∅ = ⊥ :=
+  G•[(∅ : Set α)] = ⊥ :=
 by
   rw [Subgroup.eq_bot_iff_forall]
   intro f f_in_rist
@@ -149,7 +148,7 @@ by
   simp
 
 theorem rigidStabilizer_sInter (S : Set (Set α)) :
-  RigidStabilizer G (⋂₀ S) = ⨅ T ∈ S, RigidStabilizer G T :=
+  G•[⋂₀ S] = ⨅ T ∈ S, G•[T] :=
 by
   ext x
   rw [rigidStabilizer_support]
@@ -172,7 +171,7 @@ by
     exact x_in_rist T_in_S
 
 theorem rigidStabilizer_smulImage (f g : G) (S : Set α) :
-  g ∈ RigidStabilizer G (f •'' S) ↔ f⁻¹ * g * f ∈ RigidStabilizer G S :=
+  g ∈ G•[f •'' S] ↔ f⁻¹ * g * f ∈ G•[S] :=
 by
   repeat rw [rigidStabilizer_support]
   nth_rw 3 [<-inv_inv f]
@@ -181,7 +180,7 @@ by
   simp
 
 theorem orbit_rigidStabilizer_subset {p : α} {U : Set α} (p_in_U : p ∈ U):
-  MulAction.orbit (RigidStabilizer G U) p ⊆ U :=
+  MulAction.orbit G•[U] p ⊆ U :=
 by
   intro q q_in_orbit
   have ⟨⟨h, h_in_rist⟩, hp_eq_q⟩ := MulAction.mem_orbit_iff.mp q_in_orbit

Rubin/Topology.lean

@@ -69,6 +69,36 @@ theorem equivariant_inv [MulAction G α] [MulAction G β]
 
 open Topology
 
+-- Note: this sounds like a general enough theorem that it should already be in mathlib
+lemma inter_of_open_subset_of_closure {α : Type _} [TopologicalSpace α] {U V : Set α}
+  (U_open : IsOpen U) (U_nonempty : Set.Nonempty U) (V_nonempty : Set.Nonempty V)
+  (U_ss_clV : U ⊆ closure V) : Set.Nonempty (U ∩ V) :=
+by
+  by_contra empty
+  rw [Set.not_nonempty_iff_eq_empty] at empty
+  rw [Set.nonempty_iff_ne_empty] at U_nonempty
+  apply U_nonempty
+
+  have clV_diff_U_ss_V : V ⊆ closure V \ U := by
+    rw [Set.subset_diff]
+    constructor
+    exact subset_closure
+    symm
+    rw [Set.disjoint_iff_inter_eq_empty]
+    exact empty
+  have clV_diff_U_closed : IsClosed (closure V \ U) := by
+    apply IsClosed.sdiff
+    exact isClosed_closure
+    assumption
+  unfold closure at U_ss_clV
+  simp at U_ss_clV
+  specialize U_ss_clV (closure V \ U) clV_diff_U_closed clV_diff_U_ss_V
+
+  rw [Set.subset_diff] at U_ss_clV
+  rw [Set.disjoint_iff_inter_eq_empty] at U_ss_clV
+  simp at U_ss_clV
+  exact U_ss_clV.right
+
 /--
 Note: `𝓝[≠] x` is notation for `nhdsWithin x {[x]}ᶜ`, ie. the neighborhood of x not containing itself.
 --/