💥 tried to add rubin

Rubin.lean

@@ -2354,22 +2354,15 @@ noncomputable def rubin' : EquivariantHomeomorph G (RubinSpace G) α where
     rw [<-F_eq, RubinSpace.smul_mk, RubinSpace.lim_mk, RubinSpace.lim_mk]
     rw [RubinFilter.smul_lim]
 
-end Equivariant
-
--- theorem rubin' (hα : RubinAction G α) : EquivariantHomeomorph G α (RubinSpace G) where
---   toFun := fun x => ⟦⟧
---   invFun := fun S => sorry
-
-
-
-/-
 variable {β : Type _}
-variable [TopologicalSpace β] [MulAction G β] [ContinuousConstSMul G β]
+variable [TopologicalSpace β] [MulAction G β]
 
 theorem rubin (hα : RubinAction G α) (hβ : RubinAction G β) : EquivariantHomeomorph G α β := by
-  -- by composing rubin' hα
+  let h₁ := @rubin'
-  sorry
+  let h₂ := @rubin' (α := β) -- why doesn't this work?
--/
+  exact h₂.trans h₁.symm
+
+end Equivariant
 
 end Rubin
 

Rubin/MulActionExt.lean

@@ -43,6 +43,16 @@ def is_equivariant (G : Type _) {β : Type _} [Group G] [MulAction G α]
   ∀ 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/Topology.lean

@@ -9,25 +9,25 @@ import Rubin.MulActionExt
 
 namespace Rubin
 
--- TODO: give this a notation?
 -- TODO: coe to / extend MulActionHom
 structure EquivariantHomeomorph (G α β : Type _) [Group G] [TopologicalSpace α]
     [TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where
   equivariant : is_equivariant G toFun
 #align equivariant_homeomorph Rubin.EquivariantHomeomorph
 
+@[inherit_doc]
+notation:25 α " ≃ₜ[" G "] " β => EquivariantHomeomorph G α β
+
 variable {G α β : Type _}
 variable [Group G]
-variable [TopologicalSpace α] [TopologicalSpace β]
+variable [TopologicalSpace α] [TopologicalSpace β] [MulAction G α] [MulAction G β]
 
-theorem equivariant_fun [MulAction G α] [MulAction G β]
+theorem equivariant_fun (h : EquivariantHomeomorph G α β) :
-    (h : EquivariantHomeomorph G α β) :
     is_equivariant G h.toFun :=
   h.equivariant
 #align equivariant_fun Rubin.equivariant_fun
 
-theorem equivariant_inv [MulAction G α] [MulAction G β]
+theorem equivariant_inv (h : EquivariantHomeomorph G α β) :
-    (h : EquivariantHomeomorph G α β) :
     is_equivariant G h.invFun :=
   by
   intro g x
@@ -37,6 +37,26 @@ theorem equivariant_inv [MulAction G α] [MulAction G β]
   exact e
 #align equivariant_inv Rubin.equivariant_inv
 
+protected def symm (h : α ≃ₜ[G] β) : β ≃ₜ[G] α where
+  continuous_toFun := h.continuous_invFun
+  continuous_invFun := h.continuous_toFun
+  toEquiv := h.toEquiv.symm
+  equivariant := equivariant_inv h
+
+protected def refl : α ≃ₜ[G] α where
+  continuous_toFun := continuous_id
+  continuous_invFun := continuous_id
+  toEquiv := Equiv.refl α
+  equivariant := is_equivariant_refl
+
+/-- Composition of two homeomorphisms. -/
+protected def trans {γ  : Type _} [TopologicalSpace γ] [MulAction G γ]
+  (h₁ : α ≃ₜ[G] β) (h₂ : β ≃ₜ[G] γ) : α ≃ₜ[G] γ where
+  continuous_toFun := h₂.continuous_toFun.comp h₁.continuous_toFun
+  continuous_invFun := h₁.continuous_invFun.comp h₂.continuous_invFun
+  toEquiv := Equiv.trans h₁.toEquiv h₂.toEquiv
+  equivariant := is_equivariant_trans h₁.toFun h₂.toFun h₁.equivariant h₂.equivariant
+
 open Topology
 
 -- Note: this sounds like a general enough theorem that it should already be in mathlib