From 29fc8990a87ad6291cd1bc1e79e26bb2dc0ca218 Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Fri, 1 Dec 2023 21:35:23 +0100
Subject: [PATCH] :sparkles: Prove the two-way monotonicity of rigid
 stabilizers in group homeomorphisms

I knew this proof that group homeomorphisms are faithful would come in handy :3
---
 Rubin.lean                 |   5 +
 Rubin/HomeoGroup.lean      | 284 ++++++++++++++++++++++++-------------
 Rubin/RigidStabilizer.lean |  34 +++++
 Rubin/Support.lean         |  38 ++++-
 4 files changed, 259 insertions(+), 102 deletions(-)

diff --git a/Rubin.lean b/Rubin.lean
index abe08d3..97610b0 100644
--- a/Rubin.lean
+++ b/Rubin.lean
@@ -25,6 +25,7 @@ import Rubin.RigidStabilizer
 import Rubin.Period
 import Rubin.AlgebraicDisjointness
 import Rubin.RegularSupport
+import Rubin.HomeoGroup
 
 #align_import rubin
 
@@ -701,6 +702,10 @@ by
 
 end RegularSupport
 
+section HomeoGroup
+
+
+end HomeoGroup
 
 -- variables [topological_space α] [topological_space β] [continuous_mul_action G α] [continuous_mul_action G β]
 -- noncomputable theorem rubin (hα : rubin_action G α) (hβ : rubin_action G β) : equivariant_homeomorph G α β := sorry
diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean
index 680de8c..685e1d2 100644
--- a/Rubin/HomeoGroup.lean
+++ b/Rubin/HomeoGroup.lean
@@ -2,6 +2,7 @@ import Mathlib.Logic.Equiv.Defs
 import Mathlib.Topology.Basic
 import Mathlib.Topology.Homeomorph
 
+import Rubin.LocallyDense
 import Rubin.Topology
 import Rubin.RegularSupport
 
@@ -141,6 +142,8 @@ instance homeoGroup_mulAction₁_faithful : FaithfulSMul (HomeoGroup α) α wher
 
 namespace Rubin
 
+section AssociatedPoset.Prelude
+
 variable {α : Type _}
 variable [TopologicalSpace α]
 variable [DecidableEq α]
@@ -168,75 +171,9 @@ def AssociatedPosetSeed.val (S : AssociatedPosetSeed α) : Set α := AssociatedP
 
 theorem AssociatedPosetSeed.val_def (S : AssociatedPosetSeed α) : S.val = AssociatedPosetElem S.seed := rfl
 
-/--
-A partially-ordered set, associated to Rubin's proof.
-Any element in that set is made up of a `seed`,
-such that `val = AssociatedPosetElem seed` and `Set.Nonempty val`.
-
-Actions on this set are first defined in terms of `AssociatedPosetSeed`,
-as the proofs otherwise get hairy with `Exists.choose`.
---/
-structure AssociatedPoset (α : Type _) [TopologicalSpace α] where
-  val : Set α
-  val_has_seed : ∃ po_seed : AssociatedPosetSeed α, po_seed.val = val
-
-theorem AssociatedPoset.eq_iff_val_eq (S T : AssociatedPoset α) : S = T ↔ S.val = T.val := by
-  rw [mk.injEq]
-
-def AssociatedPoset.fromSeed (seed : AssociatedPosetSeed α) : AssociatedPoset α := ⟨
-  seed.val,
-  ⟨seed, seed.val_def⟩
-⟩
-
-noncomputable def AssociatedPoset.full_seed (S : AssociatedPoset α) : AssociatedPosetSeed α :=
-  (Exists.choose S.val_has_seed)
-
-noncomputable def AssociatedPoset.seed (S : AssociatedPoset α) : Finset (HomeoGroup α) :=
-  S.full_seed.seed
-
-@[simp]
-theorem AssociatedPoset.full_seed_seed (S : AssociatedPoset α) : S.full_seed.seed = S.seed := rfl
-
-@[simp]
-theorem AssociatedPoset.fromSeed_val (seed : AssociatedPosetSeed α) :
-  (AssociatedPoset.fromSeed seed).val = seed.val :=
-by
-  unfold fromSeed
-  simp
-
-@[simp]
-theorem AssociatedPoset.val_from_seed (S : AssociatedPoset α) : AssociatedPosetElem S.seed = S.val := by
-  unfold seed full_seed
-  rw [<-AssociatedPosetSeed.val_def]
-  rw [Exists.choose_spec S.val_has_seed]
-
-@[simp]
-theorem AssociatedPoset.val_from_seed₂ (S : AssociatedPoset α) : S.full_seed.val = S.val := by
-  unfold full_seed
-  rw [AssociatedPosetSeed.val_def]
-  nth_rw 2 [<-AssociatedPoset.val_from_seed]
-  unfold seed full_seed
-  rfl
-
--- Allows one to prove properties of AssociatedPoset without jumping through `Exists.choose`-shaped hoops
-theorem AssociatedPoset.prop_from_val {p : Set α → Prop}
-  (any_seed : ∀ po_seed : AssociatedPosetSeed α, p po_seed.val) :
-  ∀ (S : AssociatedPoset α), p S.val :=
-by
-  intro S
-  rw [<-AssociatedPoset.val_from_seed]
-  have res := any_seed S.full_seed
-  rw [AssociatedPoset.val_from_seed₂] at res
-  rw [AssociatedPoset.val_from_seed]
-  exact res
-
 @[simp]
 theorem AssociatedPosetSeed.nonempty (S : AssociatedPosetSeed α) : Set.Nonempty S.val := S.val_nonempty
 
-@[simp]
-theorem AssociatedPoset.nonempty : ∀ (S : AssociatedPoset α), Set.Nonempty S.val :=
-  AssociatedPoset.prop_from_val AssociatedPosetSeed.nonempty
-
 @[simp]
 theorem AssociatedPosetSeed.regular (S : AssociatedPosetSeed α) : Regular S.val := by
   rw [S.val_def]
@@ -254,10 +191,6 @@ theorem AssociatedPosetSeed.regular (S : AssociatedPosetSeed α) : Regular S.val
     rw [<-Heq]
     exact regularSupport_regular α g
 
-@[simp]
-theorem AssociatedPoset.regular : ∀ (S : AssociatedPoset α), Regular S.val :=
-  AssociatedPoset.prop_from_val AssociatedPosetSeed.regular
-
 lemma AssociatedPosetElem.mul_seed (seed : Finset (HomeoGroup α)) [DecidableEq (HomeoGroup α)] (f : HomeoGroup α):
   AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' AssociatedPosetElem seed :=
 by
@@ -298,6 +231,7 @@ by
   rw [<-AssociatedPosetElem.mul_seed]
   rw [AssociatedPosetSeed.smul_seed]
 
+-- We define a "preliminary" group action from `HomeoGroup α` to `AssociatedPosetSeed`
 instance homeoGroup_mulAction₂ : MulAction (HomeoGroup α) (AssociatedPosetSeed α) where
   one_smul := by
     intro S
@@ -313,57 +247,207 @@ instance homeoGroup_mulAction₂ : MulAction (HomeoGroup α) (AssociatedPosetSee
     simp
     group
 
-def AssociatedPoset.smul_from_seed (f : HomeoGroup α) (S : AssociatedPoset α) : AssociatedPoset α :=
-  AssociatedPoset.fromSeed (f • S.full_seed)
+end AssociatedPoset.Prelude
+
+
+/--
+A partially-ordered set, associated to Rubin's proof.
+Any element in that set is made up of a `seed`,
+such that `val = AssociatedPosetElem seed` and `Set.Nonempty val`.
+
+Actions on this set are first defined in terms of `AssociatedPosetSeed`,
+as the proofs otherwise get hairy with a bunch of `Exists.choose` appearing.
+--/
+structure AssociatedPoset (α : Type _) [TopologicalSpace α] where
+  val : Set α
+  val_has_seed : ∃ po_seed : AssociatedPosetSeed α, po_seed.val = val
+
+namespace AssociatedPoset
+
+variable {α : Type _}
+variable [TopologicalSpace α]
+variable [DecidableEq α]
+
+theorem eq_iff_val_eq (S T : AssociatedPoset α) : S = T ↔ S.val = T.val := by
+  rw [mk.injEq]
+
+def fromSeed (seed : AssociatedPosetSeed α) : AssociatedPoset α := ⟨
+  seed.val,
+  ⟨seed, seed.val_def⟩
+⟩
+
+noncomputable def full_seed (S : AssociatedPoset α) : AssociatedPosetSeed α :=
+  (Exists.choose S.val_has_seed)
+
+noncomputable def seed (S : AssociatedPoset α) : Finset (HomeoGroup α) :=
+  S.full_seed.seed
+
+@[simp]
+theorem full_seed_seed (S : AssociatedPoset α) : S.full_seed.seed = S.seed := rfl
+
+@[simp]
+theorem fromSeed_val (seed : AssociatedPosetSeed α) :
+  (fromSeed seed).val = seed.val :=
+by
+  unfold fromSeed
+  simp
+
+@[simp]
+theorem val_from_seed (S : AssociatedPoset α) : AssociatedPosetElem S.seed = S.val := by
+  unfold seed full_seed
+  rw [<-AssociatedPosetSeed.val_def]
+  rw [Exists.choose_spec S.val_has_seed]
+
+@[simp]
+theorem val_from_seed₂ (S : AssociatedPoset α) : S.full_seed.val = S.val := by
+  unfold full_seed
+  rw [AssociatedPosetSeed.val_def]
+  nth_rw 2 [<-val_from_seed]
+  unfold seed full_seed
+  rfl
+
+-- Allows one to prove properties of AssociatedPoset without jumping through `Exists.choose`-shaped hoops
+theorem prop_from_val {p : Set α → Prop}
+  (any_seed : ∀ po_seed : AssociatedPosetSeed α, p po_seed.val) :
+  ∀ (S : AssociatedPoset α), p S.val :=
+by
+  intro S
+  rw [<-val_from_seed]
+  have res := any_seed S.full_seed
+  rw [val_from_seed₂] at res
+  rw [val_from_seed]
+  exact res
+
+@[simp]
+theorem nonempty : ∀ (S : AssociatedPoset α), Set.Nonempty S.val :=
+  prop_from_val AssociatedPosetSeed.nonempty
+
+@[simp]
+theorem regular : ∀ (S : AssociatedPoset α), Regular S.val :=
+  prop_from_val AssociatedPosetSeed.regular
+
+variable [DecidableEq (HomeoGroup α)]
 
--- TODO: use smulImage instead?
 instance homeoGroup_smul₃ : SMul (HomeoGroup α) (AssociatedPoset α) where
-  smul := AssociatedPoset.smul_from_seed
+  smul := fun f S => ⟨
+    f •'' S.val,
+    by
+      use f • S.full_seed
+      rw [AssociatedPosetSeed.smul_val']
+      simp
+  ⟩
 
-theorem AssociatedPoset.smul_fromSeed (f : HomeoGroup α) (S : AssociatedPoset α) :
-  f • S = AssociatedPoset.fromSeed (f • S.full_seed) := rfl
+theorem smul_val (f : HomeoGroup α) (S : AssociatedPoset α) :
+  (f • S).val = f •'' S.val := rfl
 
-theorem AssociatedPoset.smul_seed' (f : HomeoGroup α) (S : AssociatedPoset α) (seed : Finset (HomeoGroup α)) :
+theorem smul_seed' (f : HomeoGroup α) (S : AssociatedPoset α) (seed : Finset (HomeoGroup α)) :
   S.val = AssociatedPosetElem seed →
   (f • S).val = AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) seed) :=
 by
   intro S_val_eq
+  rw [smul_val]
+  rw [AssociatedPosetElem.mul_seed]
+  rw [S_val_eq]
 
-  rw [AssociatedPoset.smul_fromSeed]
-  rw [AssociatedPoset.fromSeed_val]
-  rw [AssociatedPosetSeed.smul_val]
-  repeat rw [AssociatedPosetElem.mul_seed]
-  rw [<-S_val_eq]
-  rw [AssociatedPoset.full_seed_seed]
-  rw [<-AssociatedPoset.val_from_seed]
-
-theorem AssociatedPoset.smul_seed (f : HomeoGroup α) (S : AssociatedPoset α) :
+theorem smul_seed (f : HomeoGroup α) (S : AssociatedPoset α) :
   (f • S).val = AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) S.seed) :=
 by
-  apply AssociatedPoset.smul_seed'
+  apply smul_seed'
   symm
-  exact AssociatedPoset.val_from_seed S
-
-theorem AssociatedPoset.smul_val (f : HomeoGroup α) (S : AssociatedPoset α) :
-  (f • S).val = f •'' S.val :=
-by
-  rw [AssociatedPoset.smul_fromSeed]
-  rw [AssociatedPoset.fromSeed_val]
-  rw [<-AssociatedPoset.val_from_seed₂]
-  exact AssociatedPosetSeed.smul_val' _ _
+  exact val_from_seed S
 
+-- Note: we could potentially implement MulActionHom
 instance homeoGroup_mulAction₃ : MulAction (HomeoGroup α) (AssociatedPoset α) where
   one_smul := by
     intro S
-    rw [AssociatedPoset.eq_iff_val_eq]
-    repeat rw [AssociatedPoset.smul_val]
+    rw [eq_iff_val_eq]
+    repeat rw [smul_val]
     rw [one_smulImage]
   mul_smul := by
     intro S f g
-    rw [AssociatedPoset.eq_iff_val_eq]
-    repeat rw [AssociatedPoset.smul_val]
+    rw [eq_iff_val_eq]
+    repeat rw [smul_val]
     rw [smulImage_mul]
 
+instance associatedPoset_le : LE (AssociatedPoset α) where
+  le := fun S T => S.val ⊆ T.val
+
+theorem le_def (S T : AssociatedPoset α) : S ≤ T ↔ S.val ⊆ T.val := by
+  rw [iff_eq_eq]
+  rfl
+
+instance associatedPoset_partialOrder : PartialOrder (AssociatedPoset α) where
+  le_refl := fun S => (le_def S S).mpr (le_refl S.val)
+  le_trans := fun S T U S_le_T S_le_U => (le_def S U).mpr (le_trans
+    ((le_def _ _).mp S_le_T)
+    ((le_def _ _).mp S_le_U)
+  )
+  le_antisymm := by
+    intro S T S_le_T T_le_S
+    rw [le_def] at S_le_T
+    rw [le_def] at T_le_S
+    rw [eq_iff_val_eq]
+    apply le_antisymm <;> assumption
+
+theorem smul_mono {S T : AssociatedPoset α} (f : HomeoGroup α) (S_le_T : S ≤ T) :
+  f • S ≤ f • T :=
+by
+  rw [le_def]
+  repeat rw [smul_val]
+  apply smulImage_mono
+  assumption
+
+end AssociatedPoset
+
+section Other
+
+theorem homeoGroup_rigidStabilizer_subset_iff {α : Type _} [TopologicalSpace α]
+  [h_lm : LocallyMoving (HomeoGroup α) α]
+  {U V : Set α} (U_reg : Regular U) (V_reg : Regular V):
+  U ⊆ V ↔ RigidStabilizer (HomeoGroup α) U ≤ RigidStabilizer (HomeoGroup α) V :=
+by
+  constructor
+  exact rigidStabilizer_mono
+  intro rist_ss
+
+  by_contra U_not_ss_V
+
+  let W := U \ closure V
+  have W_nonempty : Set.Nonempty W := by
+    by_contra W_empty
+    apply U_not_ss_V
+    apply subset_from_diff_closure_eq_empty
+    · assumption
+    · exact U_reg.isOpen
+    · rw [Set.not_nonempty_iff_eq_empty] at W_empty
+      exact W_empty
+  have W_ss_U : W ⊆ U := by
+    simp
+    exact Set.diff_subset _ _
+  have W_open : IsOpen W := by
+    unfold_let
+    rw [Set.diff_eq_compl_inter]
+    apply IsOpen.inter
+    simp
+    exact U_reg.isOpen
+
+  have ⟨f, f_in_ristW, f_ne_one⟩ := h_lm.get_nontrivial_rist_elem W_open W_nonempty
+
+  have f_in_ristU : f ∈ RigidStabilizer (HomeoGroup α) U := by
+    exact rigidStabilizer_mono W_ss_U f_in_ristW
+
+  have f_notin_ristV : f ∉ RigidStabilizer (HomeoGroup α) V := by
+    apply rigidStabilizer_compl f_ne_one
+    apply rigidStabilizer_mono _ f_in_ristW
+    calc
+      W = U ∩ (closure V)ᶜ := by unfold_let; rw [Set.diff_eq_compl_inter, Set.inter_comm]
+      _ ⊆ (closure V)ᶜ := Set.inter_subset_right _ _
+      _ ⊆ Vᶜ := by
+        rw [Set.compl_subset_compl]
+        exact subset_closure
+
+  exact f_notin_ristV (rist_ss f_in_ristU)
 
+end Other
 
 end Rubin
diff --git a/Rubin/RigidStabilizer.lean b/Rubin/RigidStabilizer.lean
index 150017d..d443c4a 100644
--- a/Rubin/RigidStabilizer.lean
+++ b/Rubin/RigidStabilizer.lean
@@ -49,6 +49,17 @@ 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 :=
+by
+  intro f_in_rist_compl
+  intro f_in_rist
+  rw [rigidStabilizer_support] at f_in_rist_compl
+  rw [rigidStabilizer_support] at f_in_rist
+  rw [Set.subset_compl_iff_disjoint_left] at f_in_rist_compl
+  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)
+
 theorem rigidStabilizer_to_subgroup_closure {g : G} {U : Set α} :
   g ∈ RigidStabilizer G U → g ∈ Subgroup.closure { g : G | Support α g ⊆ U } :=
 by
@@ -138,4 +149,27 @@ by
   rw [f_in_rist x (Set.not_mem_empty x)]
   simp
 
+theorem rigidStabilizer_sInter (S : Set (Set α)) :
+  RigidStabilizer G (⋂₀ S) = ⨅ T ∈ S, RigidStabilizer G T :=
+by
+  ext x
+  rw [rigidStabilizer_support]
+  constructor
+  · intro supp_ss_sInter
+    rw [Subgroup.mem_iInf]
+    intro T
+    rw [Subgroup.mem_iInf]
+    intro T_in_S
+    rw [rigidStabilizer_support]
+    rw [Set.subset_sInter_iff] at supp_ss_sInter
+    exact supp_ss_sInter T T_in_S
+  · intro x_in_rist
+    rw [Set.subset_sInter_iff]
+    intro T T_in_S
+    rw [<-rigidStabilizer_support]
+    rw [Subgroup.mem_iInf] at x_in_rist
+    specialize x_in_rist T
+    rw [Subgroup.mem_iInf] at x_in_rist
+    exact x_in_rist T_in_S
+
 end Rubin
diff --git a/Rubin/Support.lean b/Rubin/Support.lean
index 0fa4174..c93da6e 100644
--- a/Rubin/Support.lean
+++ b/Rubin/Support.lean
@@ -46,6 +46,12 @@ theorem not_mem_support :
   rw [Rubin.mem_support, Classical.not_not]
 #align mem_not_support Rubin.not_mem_support
 
+theorem support_one : Support α (1 : G) = ∅ := by
+  rw [Set.eq_empty_iff_forall_not_mem]
+  intro x
+  rw [not_mem_support]
+  simp
+
 theorem smul_mem_support :
     x ∈ Support α g → g • x ∈ Support α g := fun h =>
   h ∘ smul_left_cancel g
@@ -259,6 +265,35 @@ theorem support_eq: Support α f = Support α g ↔ ∀ (x : α), (f • x = x 
       | inl h₁ => exfalso; exact gx_ne_x h₁.right
       | inr h₁ => exact h₁.left
 
+theorem support_empty_iff (g : G) [h_f : FaithfulSMul G α] :
+  Support α g = ∅ ↔ g = 1 :=
+by
+  constructor
+  · intro supp_empty
+    rw [Set.eq_empty_iff_forall_not_mem] at supp_empty
+    apply h_f.eq_of_smul_eq_smul
+    intro x
+    specialize supp_empty x
+    rw [not_mem_support] at supp_empty
+    simp
+    exact supp_empty
+  · intro g_eq_1
+    rw [g_eq_1]
+    exact support_one
+
+theorem support_nonempty_iff (g : G) [h_f : FaithfulSMul G α] :
+  Set.Nonempty (Support α g) ↔ g ≠ 1 :=
+by
+  constructor
+  · intro ⟨x, x_in_supp⟩
+    by_contra g_eq_1
+    rw [g_eq_1, support_one] at x_in_supp
+    exact x_in_supp
+  · intro g_ne_one
+    by_contra supp_empty
+    rw [Set.not_nonempty_iff_eq_empty] at supp_empty
+    exact g_ne_one ((support_empty_iff _).mp supp_empty)
+
 section Continuous
 
 variable {G α : Type _}
@@ -274,8 +309,7 @@ theorem img_open_open (g : G) (U : Set α) (h : IsOpen U): IsOpen (g •'' U) :=
 
 #align img_open_open Rubin.img_open_open
 
-theorem support_open (g : G) [TopologicalSpace α] [T2Space α]
-    [ContinuousMulAction G α] : IsOpen (Support α g) :=
+theorem support_open (g : G) [T2Space α]: IsOpen (Support α g) :=
   by
   apply isOpen_iff_forall_mem_open.mpr
   intro x xmoved