From 3753948ac81930814b4d4f8b10838c0d2989209f Mon Sep 17 00:00:00 2001
From: Laurent Bartholdi <laurent.bartholdi@gmail.com>
Date: Sun, 7 Jan 2024 22:22:06 +0100
Subject: [PATCH] :boom: tried to add rubin

---
 Rubin.lean              | 19 ++++++-------------
 Rubin/MulActionExt.lean | 10 ++++++++++
 Rubin/Topology.lean     | 32 ++++++++++++++++++++++++++------
 3 files changed, 42 insertions(+), 19 deletions(-)

diff --git a/Rubin.lean b/Rubin.lean
index 2d95869..35038de 100644
--- a/Rubin.lean
+++ b/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α
-  sorry
--/
+  let h₁ := @rubin'
+  let h₂ := @rubin' (α := β) -- why doesn't this work?
+  exact h₂.trans h₁.symm
+
+end Equivariant
 
 end Rubin
 
diff --git a/Rubin/MulActionExt.lean b/Rubin/MulActionExt.lean
index 86be76b..cdbe560 100644
--- a/Rubin/MulActionExt.lean
+++ b/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
diff --git a/Rubin/Topology.lean b/Rubin/Topology.lean
index ee1990f..2bf3676 100644
--- a/Rubin/Topology.lean
+++ b/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 β]
-    (h : EquivariantHomeomorph G α β) :
+theorem equivariant_fun (h : EquivariantHomeomorph G α β) :
     is_equivariant G h.toFun :=
   h.equivariant
 #align equivariant_fun Rubin.equivariant_fun
 
-theorem equivariant_inv [MulAction G α] [MulAction G β]
-    (h : EquivariantHomeomorph G α β) :
+theorem equivariant_inv (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