💄 added Emilie to authors

Rubin.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Laurent Bartholdi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author : Laurent Bartholdi
+Author : Laurent Bartholdi and Émilie Burgun
 -/
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Finset.Card
@@ -24,10 +24,12 @@ import Rubin.SmulImage
 import Rubin.Support
 import Rubin.Topology
 import Rubin.RigidStabilizer
+-- import Rubin.RigidStabilizerBasis
 import Rubin.Period
 import Rubin.AlgebraicDisjointness
 import Rubin.RegularSupport
 import Rubin.RegularSupportBasis
+import Rubin.HomeoGroup
 import Rubin.Filter
 
 #align_import rubin
@@ -35,54 +37,33 @@ import Rubin.Filter
 namespace Rubin
 open Rubin.Tactic
 
+-- TODO: find a home
+theorem equiv_congr_ne {ι ι' : Type _} (e : ι ≃ ι') {x y : ι} : x ≠ y → e x ≠ e y :=
+  by
+  intro x_ne_y
+  by_contra h
+  apply x_ne_y
+  convert congr_arg e.symm h <;> simp only [Equiv.symm_apply_apply]
+#align equiv.congr_ne Rubin.equiv_congr_ne
+
 ----------------------------------------------------------------
 section Rubin
 
 ----------------------------------------------------------------
 section RubinActions
 
--- TODO: debate whether having this structure is relevant or not,
+structure RubinAction (G α : Type _) extends
--- since the instance inference engine doesn't play well with it.
+  Group G,
--- One alternative would be to lay out all of the properties as-is (without their class wrappers),
+  TopologicalSpace α,
--- then provide ways to reconstruct them in instances.
+  MulAction G α,
-structure RubinAction (G α : Type _) where
+  FaithfulSMul G α
-  group : Group G
+where
-  action : MulAction G α
-  topology : TopologicalSpace α
-  faithful : FaithfulSMul G α
   locally_compact : LocallyCompactSpace α
   hausdorff : T2Space α
   no_isolated_points : HasNoIsolatedPoints α
-  locally_dense : LocallyDense G α
+  locallyDense : LocallyDense G α
 #align rubin_action Rubin.RubinAction
 
-/--
-Constructs a RubinAction from ambient instances.
-If needed, missing instances can be passed as named parameters.
---/
-def RubinAction.mk' (G α : Type _)
-  [group : Group G] [topology : TopologicalSpace α] [hausdorff : T2Space α] [action : MulAction G α]
-  [faithful : FaithfulSMul G α] [locally_compact : LocallyCompactSpace α]
-  [no_isolated_points : HasNoIsolatedPoints α] [locally_dense : LocallyDense G α] :
-  RubinAction G α := ⟨
-    group,
-    action,
-    topology,
-    faithful,
-    locally_compact,
-    hausdorff,
-    no_isolated_points,
-    locally_dense
-  ⟩
-
-variable {G α : Type _}
-
-instance RubinAction.instGroup (act : RubinAction G α) : Group G := act.group
-
-instance RubinAction.instFaithful (act : RubinAction G α) : @FaithfulSMul G α (@MulAction.toSMul G α act.group.toMonoid act.action) := act.faithful
-
-instance RubinAction.topologicalSpace (act : RubinAction G α) : TopologicalSpace α := act.topology
-
 end RubinActions
 
 section AlgebraicDisjointness
@@ -463,6 +444,7 @@ by
       apply ge_antisymm
       {
         apply Period.notfix_le_period'
+        · exact n_pos
         · apply Period.period_pos'
           · exact Set.nonempty_of_mem p_in_U
           · exact exp_ne_zero
@@ -2100,7 +2082,8 @@ by
   exact RubinSpace.lim_mk α F
 
 theorem RubinSpace.lim_continuous : Continuous (RubinSpace.lim (G := G) (α := α)) := by
-  rw [(RegularSupportBasis.isBasis G α).continuous_iff]
+  -- TODO: rename to continuous_iff when upgrading mathlib
+  apply (RegularSupportBasis.isBasis G α).continuous
   intro S S_in_basis
   apply TopologicalSpace.isOpen_generateFrom_of_mem
   rw [RubinFilterBasis.mem_iff]
@@ -2334,7 +2317,6 @@ theorem RubinFilter.mul_smul (g h : G) (F : RubinFilter G) : (F.smul g).smul h =
   rw [Filter.map_map, <-MulAut.coe_mul]
   rw [Filter.InBasis.map_basis_toOrderIsoSet _ F.filter.in_basis]
 
--- Note: awfully slow to compile (since it isn't noncomputable, it gets compiled down to IR)
 def RubinSpace.smul (Q : RubinSpace G) (g : G) : RubinSpace G :=
   Quotient.map (fun F => F.smul g) (fun _ _ F_eqv => RubinFilter.smul_eqv_of_eqv g F_eqv) Q
 
@@ -2362,9 +2344,9 @@ instance : MulAction G (RubinSpace G) where
 
 theorem RubinSpace.smul_def (g : G) (Q : RubinSpace G) : g • Q = Q.smul g := rfl
 
-noncomputable def RubinSpace.equivariantHomeomorph : EquivariantHomeomorph G (RubinSpace G) α where
+noncomputable def rubin' : EquivariantHomeomorph G (RubinSpace G) α where
   toHomeomorph := RubinSpace.homeomorph (G := G) α
-  toFun_equivariant' := by
+  equivariant := by
     intro g Q
     simp [RubinSpace.homeomorph]
     rw [RubinSpace.smul_def]
@@ -2372,20 +2354,15 @@ noncomputable def RubinSpace.equivariantHomeomorph : EquivariantHomeomorph G (Ru
     rw [<-F_eq, RubinSpace.smul_mk, RubinSpace.lim_mk, RubinSpace.lim_mk]
     rw [RubinFilter.smul_lim]
 
-end Equivariant
+variable {β : Type _}
+variable [TopologicalSpace β] [MulAction G β]
+
+theorem rubin (hα : RubinAction G α) (hβ : RubinAction G β) : EquivariantHomeomorph G α β := by
+  let h₁ := @rubin'
+  let h₂ := @rubin' (α := β) -- why doesn't this work?
+  exact h₂.trans h₁.symm
 
-variable (G : Type _)
+end Equivariant
-variable [Group G] [Nontrivial G]
-variable (α : Type _) [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] [HasNoIsolatedPoints α]
-variable [MulAction G α] [FaithfulSMul G α] [ContinuousConstSMul G α] [LocallyDense G α]
-variable (β : Type _) [TopologicalSpace β] [T2Space β] [LocallyCompactSpace β] [HasNoIsolatedPoints β]
-variable [MulAction G β] [FaithfulSMul G β] [ContinuousConstSMul G β] [LocallyDense G β]
-
-noncomputable def rubin : EquivariantHomeomorph G α β :=
-  let α_nonempty : Nonempty α := by rwa [LocallyMoving.nonempty_iff_nontrivial G]
-  let β_nonempty : Nonempty β := by rwa [LocallyMoving.nonempty_iff_nontrivial G]
-  (RubinSpace.equivariantHomeomorph (G := G) (α := α)).inv.trans
-    (RubinSpace.equivariantHomeomorph (G := G) (α := β))
 
 end Rubin
 

Rubin/HomeoGroup.lean

@@ -0,0 +1,257 @@
+import Mathlib.Logic.Equiv.Defs
+import Mathlib.Topology.Basic
+import Mathlib.Topology.Homeomorph
+import Mathlib.Topology.Algebra.ConstMulAction
+
+import Rubin.LocallyDense
+import Rubin.Topology
+import Rubin.Support
+import Rubin.RegularSupport
+
+structure HomeoGroup (α : Type _) [TopologicalSpace α] extends Homeomorph α α
+
+variable {α : Type _}
+variable [TopologicalSpace α]
+
+def HomeoGroup.coe : HomeoGroup α -> Homeomorph α α := HomeoGroup.toHomeomorph
+
+def HomeoGroup.from : Homeomorph α α -> HomeoGroup α := HomeoGroup.mk
+
+instance homeoGroup_coe : Coe (HomeoGroup α) (Homeomorph α α) where
+  coe := HomeoGroup.coe
+
+instance homeoGroup_coe₂ : Coe (Homeomorph α α) (HomeoGroup α) where
+  coe := HomeoGroup.from
+
+def HomeoGroup.toPerm : HomeoGroup α → Equiv.Perm α := fun g => g.coe.toEquiv
+
+instance homeoGroup_coe_perm : Coe (HomeoGroup α) (Equiv.Perm α) where
+  coe := HomeoGroup.toPerm
+
+@[simp]
+theorem HomeoGroup.toPerm_def (g : HomeoGroup α) : g.coe.toEquiv = (g : Equiv.Perm α) := rfl
+
+@[simp]
+theorem HomeoGroup.mk_coe (g : HomeoGroup α) : HomeoGroup.mk (g.coe) = g := rfl
+
+@[simp]
+theorem HomeoGroup.eq_iff_coe_eq {f g : HomeoGroup α} : f.coe = g.coe ↔ f = g := by
+  constructor
+  {
+    intro f_eq_g
+    rw [<-HomeoGroup.mk_coe f]
+    rw [f_eq_g]
+    simp
+  }
+  {
+    intro f_eq_g
+    unfold HomeoGroup.coe
+    rw [f_eq_g]
+  }
+
+@[simp]
+theorem HomeoGroup.from_toHomeomorph (m : Homeomorph α α) : (HomeoGroup.from m).toHomeomorph = m := rfl
+
+instance homeoGroup_one : One (HomeoGroup α) where
+  one := HomeoGroup.from (Homeomorph.refl α)
+
+theorem HomeoGroup.one_def : (1 : HomeoGroup α) = (Homeomorph.refl α : HomeoGroup α) := rfl
+
+instance homeoGroup_inv : Inv (HomeoGroup α) where
+  inv := fun g => HomeoGroup.from (g.coe.symm)
+
+@[simp]
+theorem HomeoGroup.inv_def (g : HomeoGroup α) : (Homeomorph.symm g.coe : HomeoGroup α) = g⁻¹ := rfl
+
+theorem HomeoGroup.coe_inv {g : HomeoGroup α} : HomeoGroup.coe (g⁻¹) = (HomeoGroup.coe g).symm := rfl
+
+instance homeoGroup_mul : Mul (HomeoGroup α) where
+  mul := fun a b => ⟨b.toHomeomorph.trans a.toHomeomorph⟩
+
+theorem HomeoGroup.coe_mul {f g : HomeoGroup α} : HomeoGroup.coe (f * g) = (HomeoGroup.coe g).trans (HomeoGroup.coe f) := rfl
+
+@[simp]
+theorem HomeoGroup.mul_def (f g : HomeoGroup α) : HomeoGroup.from ((HomeoGroup.coe g).trans (HomeoGroup.coe f)) = f * g := rfl
+
+instance homeoGroup_group : Group (HomeoGroup α) where
+  mul_assoc := by
+    intro a b c
+    rw [<-HomeoGroup.eq_iff_coe_eq]
+    repeat rw [HomeoGroup_coe_mul]
+    rfl
+  mul_one := by
+    intro a
+    rw [<-HomeoGroup.eq_iff_coe_eq]
+    rw [HomeoGroup.coe_mul]
+    rfl
+  one_mul := by
+    intro a
+    rw [<-HomeoGroup.eq_iff_coe_eq]
+    rw [HomeoGroup.coe_mul]
+    rfl
+  mul_left_inv := by
+    intro a
+    rw [<-HomeoGroup.eq_iff_coe_eq]
+    rw [HomeoGroup.coe_mul]
+    rw [HomeoGroup.coe_inv]
+    simp
+    rfl
+
+/--
+The HomeoGroup trivially has a continuous and faithful `MulAction` on the underlying topology `α`.
+--/
+instance homeoGroup_smul₁ : SMul (HomeoGroup α) α where
+  smul := fun g x => g.toFun x
+
+@[simp]
+theorem HomeoGroup.smul₁_def (f : HomeoGroup α) (x : α) : f.toFun x = f • x := rfl
+
+@[simp]
+theorem HomeoGroup.smul₁_def' (f : HomeoGroup α) (x : α) : f.toHomeomorph x = f • x := rfl
+
+@[simp]
+theorem HomeoGroup.coe_toFun_eq_smul₁ (f : HomeoGroup α) (x : α) : FunLike.coe (HomeoGroup.coe f) x = f • x := rfl
+
+instance homeoGroup_mulAction₁ : MulAction (HomeoGroup α) α where
+  one_smul := by
+    intro x
+    rfl
+  mul_smul := by
+    intro f g x
+    rfl
+
+instance homeoGroup_mulAction₁_continuous : ContinuousConstSMul (HomeoGroup α) α where
+  continuous_const_smul := by
+    intro h
+    constructor
+    intro S S_open
+    conv => {
+      congr; ext
+      congr; ext
+      rw [<-HomeoGroup.smul₁_def']
+    }
+    simp only [Homeomorph.isOpen_preimage]
+    exact S_open
+
+instance homeoGroup_mulAction₁_faithful : FaithfulSMul (HomeoGroup α) α where
+  eq_of_smul_eq_smul := by
+    intro f g hyp
+    rw [<-HomeoGroup.eq_iff_coe_eq]
+    ext x
+    simp
+    exact hyp x
+
+theorem HomeoGroup.smulImage_eq_image (g : HomeoGroup α) (S : Set α) :
+  g •'' S = ⇑g.toHomeomorph '' S := rfl
+
+section FromContinuousConstSMul
+
+variable {G : Type _} [Group G]
+variable [MulAction G α] [ContinuousConstSMul G α]
+
+/--
+`fromContinuous` is a structure-preserving transformation from a continuous `MulAction` to a `HomeoGroup`
+--/
+def HomeoGroup.fromContinuous (α : Type _) [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α]
+  (g : G) : HomeoGroup α :=
+  HomeoGroup.from (Homeomorph.smul g)
+
+@[simp]
+theorem HomeoGroup.fromContinuous_def (g : G) :
+  HomeoGroup.from (Homeomorph.smul g) = HomeoGroup.fromContinuous α g := rfl
+
+@[simp]
+theorem HomeoGroup.fromContinuous_smul (g : G) :
+  ∀ x : α, (HomeoGroup.fromContinuous α g) • x = g • x :=
+by
+  intro x
+  unfold fromContinuous
+  rw [<-HomeoGroup.smul₁_def', HomeoGroup.from_toHomeomorph]
+  unfold Homeomorph.smul
+  simp
+
+theorem HomeoGroup.fromContinuous_one :
+  HomeoGroup.fromContinuous α (1 : G) = (1 : HomeoGroup α) :=
+by
+  apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
+  simp
+
+theorem HomeoGroup.fromContinuous_mul (g h : G):
+  (HomeoGroup.fromContinuous α g) * (HomeoGroup.fromContinuous α h) = (HomeoGroup.fromContinuous α (g * h)) :=
+by
+  apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
+  intro x
+  rw [mul_smul]
+  simp
+  rw [mul_smul]
+
+theorem HomeoGroup.fromContinuous_inv (g : G):
+  HomeoGroup.fromContinuous α g⁻¹ = (HomeoGroup.fromContinuous α g)⁻¹ :=
+by
+  apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
+  intro x
+  group_action
+  rw [mul_smul]
+  simp
+
+theorem HomeoGroup.fromContinuous_eq_iff [FaithfulSMul G α] (g h : G):
+  (HomeoGroup.fromContinuous α g) = (HomeoGroup.fromContinuous α h) ↔ g = h :=
+by
+  constructor
+  · intro cont_eq
+    apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
+    intro x
+    rw [<-HomeoGroup.fromContinuous_smul g]
+    rw [cont_eq]
+    simp
+  · tauto
+
+@[simp]
+theorem HomeoGroup.fromContinuous_support (g : G) :
+  Rubin.Support α (HomeoGroup.fromContinuous α g) = Rubin.Support α g :=
+by
+  ext x
+  repeat rw [Rubin.mem_support]
+  rw [<-HomeoGroup.smul₁_def, <-HomeoGroup.fromContinuous_def]
+  rw [HomeoGroup.from_toHomeomorph]
+  rw [Homeomorph.smul]
+  simp only [Equiv.toFun_as_coe, MulAction.toPerm_apply]
+
+@[simp]
+theorem HomeoGroup.fromContinuous_regularSupport (g : G) :
+  Rubin.RegularSupport α (HomeoGroup.fromContinuous α g) = Rubin.RegularSupport α g :=
+by
+  unfold Rubin.RegularSupport
+  rw [HomeoGroup.fromContinuous_support]
+
+@[simp]
+theorem HomeoGroup.fromContinuous_smulImage (g : G) (V : Set α) :
+  (HomeoGroup.fromContinuous α g) •'' V = g •'' V :=
+by
+  repeat rw [Rubin.smulImage_def]
+  simp
+
+def HomeoGroup.fromContinuous_embedding (α : Type _) [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α]: G ↪ (HomeoGroup α) where
+  toFun := fun (g : G) => HomeoGroup.fromContinuous α g
+  inj' := by
+    intro g h fromCont_eq
+    simp at fromCont_eq
+    apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
+    intro x
+    rw [<-fromContinuous_smul, fromCont_eq, fromContinuous_smul]
+
+@[simp]
+theorem HomeoGroup.fromContinuous_embedding_toFun [FaithfulSMul G α] (g : G):
+  HomeoGroup.fromContinuous_embedding α g = HomeoGroup.fromContinuous α g := rfl
+
+def HomeoGroup.fromContinuous_monoidHom (α : Type _) [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α]: G →* (HomeoGroup α) where
+  toFun := fun (g : G) => HomeoGroup.fromContinuous α g
+  map_one' := by
+    simp
+    rw [fromContinuous_one]
+  map_mul' := by
+    simp
+    intros
+    rw [fromContinuous_mul]
+
+end FromContinuousConstSMul

Rubin/LocallyDense.lean

@@ -126,29 +126,13 @@ by
   let ⟨g, _, g_ne_one⟩ := (get_nontrivial_rist_elem (G := G) (α := α) isOpen_univ Set.univ_nonempty)
   use g
 
-theorem LocallyMoving.nontrivial (G α : Type _) [Group G] [TopologicalSpace α]
+theorem LocallyMoving.nontrivial {G α : Type _} [Group G] [TopologicalSpace α]
   [MulAction G α] [LocallyMoving G α] [Nonempty α] : Nontrivial G where
   exists_pair_ne := by
     use 1
     simp only [ne_comm]
     exact nontrivial_elem G α
 
-theorem LocallyMoving.nonempty_iff_nontrivial (G α : Type _) [Group G] [TopologicalSpace α]
-  [MulAction G α] [FaithfulSMul G α] [LocallyMoving G α] : Nonempty α ↔ Nontrivial G :=
-by
-  constructor
-  · intro; exact LocallyMoving.nontrivial G α
-  · intro nontrivial
-    by_contra α_empty
-    rw [not_nonempty_iff] at α_empty
-    let ⟨g, h, g_ne_h⟩ := nontrivial.exists_pair_ne
-    apply g_ne_h
-    apply FaithfulSMul.eq_of_smul_eq_smul (α := α)
-    intro a
-    exfalso
-    exact α_empty.false a
-
-
 variable {G α : Type _}
 variable [Group G]
 variable [TopologicalSpace α]
@@ -171,7 +155,7 @@ where
 lemma disjoint_nbhd [T2Space α] {g : G} {x : α} (x_moved: g • x ≠ x) :
   ∃ U: Set α, IsOpen U ∧ x ∈ U ∧ Disjoint U (g •'' U) :=
 by
-  have ⟨V, W, V_open, W_open, gx_in_V, x_in_W, disjoint_V_W⟩ := T2Space.t2 x_moved
+  have ⟨V, W, V_open, W_open, gx_in_V, x_in_W, disjoint_V_W⟩ := T2Space.t2 (g • x) x x_moved
   let U := (g⁻¹ •'' V) ∩ W
   use U
   constructor

Rubin/MulActionExt.lean

@@ -37,6 +37,22 @@ theorem smul_zpow_eq_of_smul_eq {x : α} {g : G} (n : ℤ) :
     exact res
 #align smul_zpow_eq_of_smul_eq Rubin.smul_zpow_eq_of_smul_eq
 
+-- TODO: turn this into a structure?
+def is_equivariant (G : Type _) {β : Type _} [Group G] [MulAction G α]
+    [MulAction G β] (f : α → β) :=
+  ∀ g : G, ∀ x : α, f (g • x) = g • f x
+#align is_equivariant Rubin.is_equivariant
+
+lemma is_equivariant_refl {G : Type _} [Group G] [MulAction G α] : is_equivariant G (id : α → α) := by
+  intro g x
+  rw [id_eq, id_eq]
+
+lemma is_equivariant_trans {G : Type _} [Group G] [MulAction G α] [MulAction G β] [MulAction G γ]
+  (h₁ : α → β) (h₂ : β → γ) (e₁ : is_equivariant G h₁) (e₂ : is_equivariant G h₂) :
+    is_equivariant G (h₂ ∘ h₁) := by
+   intro g x
+   rw [Function.comp_apply, Function.comp_apply, e₁, e₂]
+
 lemma disjoint_not_mem {α : Type _} {U V : Set α} (disj: Disjoint U V) :
   ∀ {x : α}, x ∈ U → x ∉ V :=
 by

Rubin/Period.lean

@@ -19,15 +19,13 @@ theorem period_le_fix {p : α} {g : G} {m : ℕ} (m_pos : m > 0)
     (gmp_eq_p : g ^ m • p = p) : 0 < Rubin.Period.period p g ∧ Rubin.Period.period p g ≤ m :=
   by
   constructor
-  · by_contra h'
+  · by_contra h'; have period_zero : Rubin.Period.period p g = 0; linarith;
-    have period_zero : Rubin.Period.period p g = 0 := by linarith
+    rcases Nat.sInf_eq_zero.1 period_zero with ⟨cont, h_1⟩ | h; linarith;
-    rcases Nat.sInf_eq_zero.1 period_zero with ⟨cont, _⟩ | h
+    exact Set.eq_empty_iff_forall_not_mem.mp h ↑m ⟨m_pos, gmp_eq_p⟩
-    · linarith
-    · exact Set.eq_empty_iff_forall_not_mem.mp h ↑m ⟨m_pos, gmp_eq_p⟩
   exact Nat.sInf_le ⟨m_pos, gmp_eq_p⟩
 #align period_le_fix Rubin.Period.period_le_fix
 
-theorem notfix_le_period {p : α} {g : G} {n : ℕ}
+theorem notfix_le_period {p : α} {g : G} {n : ℕ} (n_pos : n > 0)
     (period_pos : Rubin.Period.period p g > 0) (pmoves : ∀ i : ℕ, 0 < i → i < n → g ^ i • p ≠ p) :
     n ≤ Rubin.Period.period p g := by
   by_contra period_le
@@ -36,10 +34,10 @@ theorem notfix_le_period {p : α} {g : G} {n : ℕ}
       (Nat.sInf_mem (Nat.nonempty_of_pos_sInf period_pos)).2
 #align notfix_le_period Rubin.Period.notfix_le_period
 
-theorem notfix_le_period' {p : α} {g : G} {n : ℕ}
+theorem notfix_le_period' {p : α} {g : G} {n : ℕ} (n_pos : n > 0)
     (period_pos : 0 < Rubin.Period.period p g)
     (pmoves : ∀ i : Fin n, 0 < (i : ℕ) → g ^ (i : ℕ) • p ≠ p) : n ≤ Rubin.Period.period p g :=
-  Rubin.Period.notfix_le_period period_pos fun (i : ℕ) (i_pos : 0 < i) (i_lt_n : i < n) =>
+  Rubin.Period.notfix_le_period n_pos period_pos fun (i : ℕ) (i_pos : 0 < i) (i_lt_n : i < n) =>
     pmoves (⟨i, i_lt_n⟩ : Fin n) i_pos
 #align notfix_le_period' Rubin.Period.notfix_le_period'
 
@@ -67,7 +65,7 @@ theorem moves_within_period' {z : ℤ} (g : G) (x : α) :
   0 < z → z < period x g → g^z • x ≠ x :=
 by
   intro n_pos n_lt_period
-  rw [<-Int.natAbs_of_nonneg (Int.le_of_lt n_pos)]
+  rw [<-Int.ofNat_natAbs_eq_of_nonneg _ (Int.le_of_lt n_pos)]
   rw [zpow_ofNat]
   apply moves_within_period
   · rw [<-Int.natAbs_zero]
@@ -88,7 +86,7 @@ theorem periods_lemmas {U : Set α} (U_nonempty : Set.Nonempty U) {H : Subgroup
     (exp_ne_zero : Monoid.exponent H ≠ 0) :
     (Rubin.Period.periods U H).Nonempty ∧
       BddAbove (Rubin.Period.periods U H) ∧
-        ∃ (m : ℕ), m > 0 ∧ ∀ (p : α) (g : H), g ^ m • p = p :=
+        ∃ (m : ℕ) (m_pos : m > 0), ∀ (p : α) (g : H), g ^ m • p = p :=
 by
   rcases Monoid.exponentExists_iff_ne_zero.2 exp_ne_zero with ⟨m, m_pos, gm_eq_one⟩
   have gmp_eq_p : ∀ (p : α) (g : H), g ^ m • p = p := by
@@ -137,7 +135,7 @@ theorem zero_lt_period_le_Sup_periods {U : Set α} (U_nonempty : U.Nonempty)
         Rubin.Period.period (p : α) (g : G) ≤ sSup (Rubin.Period.periods U H) :=
 by
   rcases Rubin.Period.periods_lemmas U_nonempty exp_ne_zero with
-    ⟨_periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩
+    ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩
   intro p g
   have period_in_periods : Rubin.Period.period (p : α) (g : G) ∈ Rubin.Period.periods U H := by
     use p; use g

Rubin/RegularSupportBasis.lean

@@ -11,6 +11,7 @@ import Rubin.LocallyDense
 import Rubin.Topology
 import Rubin.Support
 import Rubin.RegularSupport
+import Rubin.HomeoGroup
 
 namespace Rubin
 

Rubin/RigidStabilizerBasis.lean

@@ -0,0 +1,268 @@
+/-
+This file describes [`RigidStabilizerBasis`], which are all non-trivial subgroups of `G` constructed
+by finite intersections of `RigidStabilizer G (RegularSupport α g)`.
+-/
+
+import Mathlib.Topology.Basic
+import Mathlib.Topology.Homeomorph
+
+import Rubin.RegularSupport
+import Rubin.RigidStabilizer
+
+namespace Rubin
+
+variable {G α : Type _}
+variable [Group G]
+variable [MulAction G α]
+variable [TopologicalSpace α]
+
+/--
+Finite intersections of rigid stabilizers of regular supports
+(which are equivalent to the rigid stabilizers of finite intersections of regular supports).
+-/
+def RigidStabilizerInter₀ {G: Type _} (α : Type _) [Group G] [MulAction G α] [TopologicalSpace α]
+  (S : Finset G) : Subgroup G :=
+  ⨅ (g ∈ S), RigidStabilizer G (RegularSupport α g)
+
+theorem RigidStabilizerInter₀.eq_sInter (S : Finset G) :
+  RigidStabilizerInter₀ α S = RigidStabilizer G (⋂ g ∈ S, (RegularSupport α g)) :=
+by
+  have img_eq : ⋂ g ∈ S, RegularSupport α g = ⋂₀ ((fun g : G => RegularSupport α g) '' S) :=
+    by simp only [Set.sInter_image, Finset.mem_coe]
+
+  rw [img_eq]
+  rw [rigidStabilizer_sInter]
+  unfold RigidStabilizerInter₀
+
+  ext x
+  repeat rw [Subgroup.mem_iInf]
+  constructor
+  · intro H T
+    rw [Subgroup.mem_iInf]
+    intro T_in_img
+    simp at T_in_img
+    let ⟨g, ⟨g_in_S, T_eq⟩⟩ := T_in_img
+    specialize H g
+    rw [Subgroup.mem_iInf] at H
+    rw [<-T_eq]
+    apply H; assumption
+  · intro H g
+    rw [Subgroup.mem_iInf]
+    intro g_in_S
+    specialize H (RegularSupport α g)
+    rw [Subgroup.mem_iInf] at H
+    simp at H
+    apply H g <;> tauto
+
+/--
+A predecessor structure to [`RigidStabilizerBasis`], where equality is defined on the choice of
+group elements who regular support's rigid stabilizer get intersected upon.
+--/
+structure RigidStabilizerBasis₀ (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α] where
+  seed : Finset G
+  val_ne_bot : RigidStabilizerInter₀ α seed ≠ ⊥
+
+def RigidStabilizerBasis₀.val (B : RigidStabilizerBasis₀ G α) : Subgroup G :=
+  RigidStabilizerInter₀ α B.seed
+
+theorem RigidStabilizerBasis₀.val_def (B : RigidStabilizerBasis₀ G α) : B.val = RigidStabilizerInter₀ α B.seed := rfl
+
+/--
+The set of all non-trivial subgroups of `G` constructed
+by finite intersections of `RigidStabilizer G (RegularSupport α g)`.
+--/
+def RigidStabilizerBasis (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α] : Set (Subgroup G) :=
+  { H.val | H : RigidStabilizerBasis₀ G α }
+
+theorem RigidStabilizerBasis.mem_iff (H : Subgroup G) :
+  H ∈ RigidStabilizerBasis G α ↔ ∃ B : RigidStabilizerBasis₀ G α, B.val = H := by rfl
+
+theorem RigidStabilizerBasis.mem_iff' (H : Subgroup G)
+  (H_ne_bot : H ≠ ⊥) :
+  H ∈ RigidStabilizerBasis G α ↔ ∃ seed : Finset G, RigidStabilizerInter₀ α seed = H :=
+by
+  rw [mem_iff]
+  constructor
+  · intro ⟨B, B_eq⟩
+    use B.seed
+    rw [RigidStabilizerBasis₀.val_def] at B_eq
+    exact B_eq
+  · intro ⟨seed, seed_eq⟩
+    let B := RigidStabilizerInter₀ α seed
+    have val_ne_bot : B ≠ ⊥ := by
+      unfold_let
+      rw [seed_eq]
+      exact H_ne_bot
+    use ⟨seed, val_ne_bot⟩
+    rw [<-seed_eq]
+    rfl
+
+def RigidStabilizerBasis.asSets (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α] : Set (Set G) :=
+  { (H.val : Set G) | H : RigidStabilizerBasis₀ G α }
+
+theorem RigidStabilizerBasis.mem_asSets_iff (S : Set G) :
+  S ∈ RigidStabilizerBasis.asSets G α ↔ ∃ H ∈ RigidStabilizerBasis G α, H.carrier = S :=
+by
+  unfold asSets RigidStabilizerBasis
+  simp
+  rfl
+
+theorem RigidStabilizerBasis.mem_iff_asSets (H : Subgroup G) :
+  H ∈ RigidStabilizerBasis G α ↔ (H : Set G) ∈ RigidStabilizerBasis.asSets G α :=
+by
+  unfold asSets RigidStabilizerBasis
+  simp
+
+variable [ContinuousConstSMul G α]
+
+lemma RigidStabilizerBasis.smulImage_mem₀ {H : Subgroup G} (H_in_ristBasis : H ∈ RigidStabilizerBasis G α)
+  (f : G) : ((fun g => f * g * f⁻¹) '' H.carrier) ∈ RigidStabilizerBasis.asSets G α :=
+by
+  have G_decidable : DecidableEq G := Classical.decEq _
+  rw [mem_iff] at H_in_ristBasis
+  let ⟨seed, H_eq⟩ := H_in_ristBasis
+  rw [mem_asSets_iff]
+
+  let new_seed := Finset.image (fun g => f * g * f⁻¹) seed.seed
+  have new_seed_ne_bot : RigidStabilizerInter₀ α new_seed ≠ ⊥ := by
+    rw [RigidStabilizerInter₀.eq_sInter]
+    unfold_let
+    simp [<-regularSupport_smulImage]
+    rw [<-ne_eq]
+    rw [<-smulImage_iInter_fin]
+
+    have val_ne_bot := seed.val_ne_bot
+    rw [Subgroup.ne_bot_iff_exists_ne_one] at val_ne_bot
+    let ⟨⟨g, g_in_ristInter⟩, g_ne_one⟩ := val_ne_bot
+    simp at g_ne_one
+
+    have fgf_in_ristInter₂ : f * g * f⁻¹ ∈ RigidStabilizer G (f •'' ⋂ x ∈ seed.seed, RegularSupport α x) := by
+      rw [rigidStabilizer_smulImage]
+      group
+      rw [RigidStabilizerInter₀.eq_sInter] at g_in_ristInter
+      exact g_in_ristInter
+
+    have fgf_ne_one : f * g * f⁻¹ ≠ 1 := by
+      intro h₁
+      have h₂ := congr_arg (fun x => x * f) h₁
+      group at h₂
+      have h₃ := congr_arg (fun x => f⁻¹ * x) h₂
+      group at h₃
+      exact g_ne_one h₃
+
+
+    rw [Subgroup.ne_bot_iff_exists_ne_one]
+    use ⟨f * g * f⁻¹, fgf_in_ristInter₂⟩
+    simp
+    rw [<-ne_eq]
+    exact fgf_ne_one
+
+  use RigidStabilizerInter₀ α new_seed
+  apply And.intro
+  exact ⟨⟨new_seed, new_seed_ne_bot⟩, rfl⟩
+  rw [RigidStabilizerInter₀.eq_sInter]
+  unfold_let
+  simp [<-regularSupport_smulImage]
+  rw [<-smulImage_iInter_fin]
+
+  ext x
+  simp only [Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup,
+    Subgroup.mem_toSubmonoid, Set.mem_image]
+  rw [rigidStabilizer_smulImage]
+  rw [<-H_eq, RigidStabilizerBasis₀.val_def, RigidStabilizerInter₀.eq_sInter]
+
+  constructor
+  · intro fxf_mem
+    use f⁻¹ * x * f
+    constructor
+    · exact fxf_mem
+    · group
+  · intro ⟨y, ⟨y_in_H, y_conj⟩⟩
+    rw [<-y_conj]
+    group
+    exact y_in_H
+
+def RigidStabilizerBasisMul (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α]
+  [ContinuousConstSMul G α] (f : G) (H : Subgroup G) : Subgroup G
+where
+  carrier := (fun g => f * g * f⁻¹) '' H.carrier
+  mul_mem' := by
+    intro a b a_mem b_mem
+    simp at a_mem
+    simp at b_mem
+    let ⟨a', a'_in_H, a'_eq⟩ := a_mem
+    let ⟨b', b'_in_H, b'_eq⟩ := b_mem
+    use a' * b'
+    constructor
+    · apply Subsemigroup.mul_mem' <;> simp <;> assumption
+    · simp
+      rw [<-a'_eq, <-b'_eq]
+      group
+  one_mem' := by
+    simp
+    use 1
+    constructor
+    exact Subgroup.one_mem H
+    group
+  inv_mem' := by
+    simp
+    intro g g_in_H
+    use g⁻¹
+    constructor
+    exact Subgroup.inv_mem H g_in_H
+    rw [mul_assoc]
+
+theorem RigidStabilizerBasisMul_mem (f : G) {H : Subgroup G} (H_in_basis : H ∈ RigidStabilizerBasis G α)
+  : RigidStabilizerBasisMul G α f H ∈ RigidStabilizerBasis G α :=
+by
+  rw [RigidStabilizerBasis.mem_iff_asSets]
+  unfold RigidStabilizerBasisMul
+  simp
+
+  apply RigidStabilizerBasis.smulImage_mem₀
+  assumption
+
+instance rigidStabilizerBasis_smul : SMul G (RigidStabilizerBasis G α) where
+  smul := fun g H => ⟨
+    RigidStabilizerBasisMul G α g H.val,
+    RigidStabilizerBasisMul_mem g H.prop
+  ⟩
+
+theorem RigidStabilizerBasis.smul_eq (g : G) {H: Subgroup G} (H_in_basis : H ∈ RigidStabilizerBasis G α) :
+  g • (⟨H, H_in_basis⟩ : RigidStabilizerBasis G α) = ⟨
+    RigidStabilizerBasisMul G α g H,
+    RigidStabilizerBasisMul_mem g H_in_basis
+  ⟩ := rfl
+
+theorem RigidStabilizerBasis.mem_smul (f g : G) {H: Subgroup G} (H_in_basis : H ∈ RigidStabilizerBasis G α):
+  f ∈ (g • (⟨H, H_in_basis⟩ : RigidStabilizerBasis G α)).val ↔ g⁻¹ * f * g ∈ H :=
+by
+  rw [RigidStabilizerBasis.smul_eq]
+  simp
+  rw [<-Subgroup.mem_carrier]
+  unfold RigidStabilizerBasisMul
+  simp
+  constructor
+  · intro ⟨x, x_in_H, f_eq⟩
+    rw [<-f_eq]
+    group
+    exact x_in_H
+  · intro gfg_in_H
+    use g⁻¹ * f * g
+    constructor
+    assumption
+    group
+
+instance rigidStabilizerBasis_mulAction : MulAction G (RigidStabilizerBasis G α) where
+  one_smul := by
+    intro ⟨H, H_in_ristBasis⟩
+    ext x
+    rw [RigidStabilizerBasis.mem_smul]
+    group
+  mul_smul := by
+    intro f g ⟨B, B_in_ristBasis⟩
+    ext x
+    repeat rw [RigidStabilizerBasis.mem_smul]
+    group
+
+end Rubin

Rubin/Support.lean

@@ -387,18 +387,16 @@ variable [ContinuousConstSMul G α]
 theorem support_isOpen (g : G) [T2Space α]: IsOpen (Support α g) := by
   apply isOpen_iff_forall_mem_open.mpr
   intro x xmoved
-  let ⟨U, V, open_U, open_V, gx_in_U, x_in_V, disjoint_U_V⟩ := T2Space.t2 xmoved
+  rcases T2Space.t2 (g • x) x xmoved with ⟨U, V, open_U, open_V, gx_in_U, x_in_V, disjoint_U_V⟩
-
+  exact
-  refine ⟨
+    ⟨V ∩ (g⁻¹ •'' U), fun y yW =>
-    V ∩ (g⁻¹ •'' U),
+      Disjoint.ne_of_mem
-    ?subset,
+        disjoint_U_V
-    IsOpen.inter open_V (smulImage_isOpen g⁻¹ open_U),
+        (mem_inv_smulImage.mp (Set.mem_of_mem_inter_right yW))
-    ⟨x_in_V, mem_inv_smulImage.mpr gx_in_U⟩
+        (Set.mem_of_mem_inter_left yW),
-  ⟩
+        IsOpen.inter open_V (smulImage_isOpen g⁻¹ open_U),
-  intro y ⟨yV, yU⟩
+        ⟨x_in_V, mem_inv_smulImage.mpr gx_in_U⟩
-  apply Disjoint.ne_of_mem disjoint_U_V _ yV
+    ⟩
-  rw [mem_inv_smulImage] at yU
-  exact yU
 
 end Continuous
 

Rubin/Topology.lean

@@ -1,6 +1,5 @@
 import Mathlib.GroupTheory.Subgroup.Basic
 import Mathlib.GroupTheory.GroupAction.Basic
-import Mathlib.GroupTheory.GroupAction.Hom
 import Mathlib.Topology.Basic
 import Mathlib.Topology.Homeomorph
 import Mathlib.Topology.Algebra.ConstMulAction
@@ -10,88 +9,53 @@ import Rubin.MulActionExt
 
 namespace Rubin
 
-section Equivariant
+-- TODO: coe to / extend MulActionHom
-
--- TODO: rename or remove?
-def IsEquivariant (G : Type _) {β : Type _} [Group G] [MulAction G α]
-    [MulAction G β] (f : α → β) :=
-  ∀ g : G, ∀ x : α, f (g • x) = g • f x
-
--- TODO: rename to MulActionHomeomorph
 structure EquivariantHomeomorph (G α β : Type _) [Group G] [TopologicalSpace α]
     [TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where
-  toFun_equivariant' : IsEquivariant G toFun
+  equivariant : is_equivariant G toFun
+#align equivariant_homeomorph Rubin.EquivariantHomeomorph
+
+@[inherit_doc]
+notation:25 α " ≃ₜ[" G "] " β => EquivariantHomeomorph G α β
 
-variable {G α β γ: Type*}
+variable {G α β : Type _}
 variable [Group G]
-variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ]
+variable [TopologicalSpace α] [TopologicalSpace β] [MulAction G α] [MulAction G β]
-variable [MulAction G α] [MulAction G β] [MulAction G γ]
 
-theorem EquivariantHomeomorph.toFun_equivariant (f : EquivariantHomeomorph G α β) :
+theorem equivariant_fun (h : EquivariantHomeomorph G α β) :
-  IsEquivariant G f.toHomeomorph :=
+    is_equivariant G h.toFun :=
-by
+  h.equivariant
-  show IsEquivariant G f.toFun
+#align equivariant_fun Rubin.equivariant_fun
-  exact f.toFun_equivariant'
-
-instance EquivariantHomeomorph.smulHomClass : SMulHomClass (EquivariantHomeomorph G α β) G α β where
-  coe := fun f => f.toFun
-  coe_injective' := by
-    show Function.Injective (fun f => f.toHomeomorph)
-    refine Function.Injective.comp FunLike.coe_injective ?mk_inj
-    intro f g
-    rw [mk.injEq]
-    tauto
-  map_smul := fun f => f.toFun_equivariant
 
-theorem EquivariantHomeomorph.invFun_equivariant
+theorem equivariant_inv (h : EquivariantHomeomorph G α β) :
-  (h : EquivariantHomeomorph G α β) :
+    is_equivariant G h.invFun :=
-  IsEquivariant G h.invFun :=
+  by
-by
   intro g x
   symm
-  let e := congr_arg h.invFun (h.toFun_equivariant' g (h.invFun x))
+  let e := congr_arg h.invFun (h.equivariant g (h.invFun x))
   rw [h.left_inv _, h.right_inv _] at e
   exact e
-
+#align equivariant_inv Rubin.equivariant_inv
-def EquivariantHomeomorph.trans (f₁ : EquivariantHomeomorph G α β) (f₂ : EquivariantHomeomorph G β γ) :
+
-  EquivariantHomeomorph G α γ
+protected def symm (h : α ≃ₜ[G] β) : β ≃ₜ[G] α where
-where
+  continuous_toFun := h.continuous_invFun
-  toHomeomorph := Homeomorph.trans f₁.toHomeomorph f₂.toHomeomorph
+  continuous_invFun := h.continuous_toFun
-  toFun_equivariant' := by
+  toEquiv := h.toEquiv.symm
-    intro g x
+  equivariant := equivariant_inv h
-    simp
+
-    rw [f₁.toFun_equivariant]
+protected def refl : α ≃ₜ[G] α where
-    rw [f₂.toFun_equivariant]
+  continuous_toFun := continuous_id
-
+  continuous_invFun := continuous_id
-@[simp]
+  toEquiv := Equiv.refl α
-theorem EquivariantHomeomorph.trans_toFun (f₁ : EquivariantHomeomorph G α β) (f₂ : EquivariantHomeomorph G β γ) :
+  equivariant := is_equivariant_refl
-  (f₁.trans f₂).toFun = f₂.toFun ∘ f₁.toFun :=
+
-by
+/-- Composition of two homeomorphisms. -/
-  simp [trans]
+protected def trans {γ  : Type _} [TopologicalSpace γ] [MulAction G γ]
-  rfl
+  (h₁ : α ≃ₜ[G] β) (h₂ : β ≃ₜ[G] γ) : α ≃ₜ[G] γ where
-
+  continuous_toFun := h₂.continuous_toFun.comp h₁.continuous_toFun
-@[simp]
+  continuous_invFun := h₁.continuous_invFun.comp h₂.continuous_invFun
-theorem EquivariantHomeomorph.trans_invFun (f₁ : EquivariantHomeomorph G α β) (f₂ : EquivariantHomeomorph G β γ) :
+  toEquiv := Equiv.trans h₁.toEquiv h₂.toEquiv
-  (f₁.trans f₂).invFun = f₁.invFun ∘ f₂.invFun :=
+  equivariant := is_equivariant_trans h₁.toFun h₂.toFun h₁.equivariant h₂.equivariant
-by
-  simp [trans]
-  rfl
-
-def EquivariantHomeomorph.inv (f : EquivariantHomeomorph G α β) :
-  EquivariantHomeomorph G β α
-where
-  toHomeomorph := f.symm
-  toFun_equivariant' := f.invFun_equivariant
-
-@[simp]
-theorem EquivariantHomeomorph.inv_toFun (f : EquivariantHomeomorph G α β) :
-  f.inv.toFun = f.invFun := rfl
-
-@[simp]
-theorem EquivariantHomeomorph.inv_invFun (f : EquivariantHomeomorph G α β) :
-  f.inv.invFun = f.toFun := rfl
-
-end Equivariant
 
 open Topology
 

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "d8610e1bcb91c013c3d868821c0ef28bf693be07",
+   "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
+   "rev": "3141402ba5a5f0372d2378fd75a481bc79a74ecf",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "31d41415d5782a196999d4fd8eeaef3cae386a5f",
+   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.24",
+   "inputRev": "v0.0.23",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "95f91f8e66f14c0eecde8da6dbfeff39d44cbd81",
+   "rev": "c0f7586a3e77660ff51b9156783aaf8eab9506de",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.4.0-rc1