From 03cec8913af82626c5cea9b525e4452475e5f9b1 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Thu, 30 Nov 2023 23:37:12 +0100 Subject: [PATCH] :sparkles: Start working on homeomorphic groups --- Rubin/HomeoGroup.lean | 186 +++++++++++++++++++++++++++++++++++++ Rubin/InteriorClosure.lean | 98 +++++++++++++++++++ Rubin/MulActionExt.lean | 9 ++ Rubin/RegularSupport.lean | 15 +++ Rubin/SmulImage.lean | 65 ++++++++++++- Rubin/Support.lean | 28 ++++++ Rubin/Topological.lean | 13 ++- 7 files changed, 411 insertions(+), 3 deletions(-) create mode 100644 Rubin/HomeoGroup.lean diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean new file mode 100644 index 0000000..e97ae99 --- /dev/null +++ b/Rubin/HomeoGroup.lean @@ -0,0 +1,186 @@ +import Mathlib.Logic.Equiv.Defs +import Mathlib.Topology.Basic +import Mathlib.Topology.Homeomorph + +-- TODO: extract ContinuousMulAction into its own file, or into MulActionExt? +import Rubin.Topological +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 : Rubin.ContinuousMulAction (HomeoGroup α) α where + continuous := 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 + +namespace Rubin + +variable {α : Type _} +variable [TopologicalSpace α] + +-- Note that the condition that the resulting set is non-empty is introduced later in `RegularInter` +-- TODO: rename!!! +def RegularInterElem (S : Finset (HomeoGroup α)): Set α := + ⋂₀ ((fun (g : HomeoGroup α) => RegularSupport α g) '' S) + +def RegularInter (α : Type _) [TopologicalSpace α]: Type* := + { S : Set α // + Set.Nonempty S + ∧ ∃ (seed : Finset (HomeoGroup α)), S = RegularInterElem seed + } + +@[simp] +theorem regularInter_open (S : RegularInter α) : Set.Nonempty S.val := S.prop.left + +@[simp] +theorem regularInter_regular (S : RegularInter α) : Regular S.val := by + have ⟨seed, S_from_seed⟩ := S.prop.right + rw [S_from_seed] + unfold RegularInterElem + + apply regular_sInter + · have set_decidable : DecidableEq (Set α) := Classical.typeDecidableEq (Set α) + let fin : Finset (Set α) := seed.image ((fun g => RegularSupport α g)) + + apply Set.Finite.ofFinset fin + simp + · intro S S_in_set + simp at S_in_set + let ⟨g, ⟨_, Heq⟩⟩ := S_in_set + rw [<-Heq] + exact regularSupport_regular α g + +-- TODO: +-- def RegularInter.smul : HomeoGroup α → RegularInter α -> RegularInter α + +-- instance homeoGroup_smul₂ : SMul (HomeoGroup α) (RegularInter α) where +-- smul := fun g x => + +end Rubin diff --git a/Rubin/InteriorClosure.lean b/Rubin/InteriorClosure.lean index 8fa36f7..a2a6b14 100644 --- a/Rubin/InteriorClosure.lean +++ b/Rubin/InteriorClosure.lean @@ -1,6 +1,8 @@ import Mathlib.Topology.Basic import Mathlib.Topology.Separation +import Rubin.SmulImage + namespace Rubin variable {α : Type _} @@ -189,4 +191,100 @@ by · exact (interiorClosure_subset U'_open) u_in_U' · exact (interiorClosure_subset V'_open) v_in_V' +theorem regular_inter {U V : Set α} : Regular U → Regular V → Regular (U ∩ V) := +by + intro U_reg V_reg + simp + have UV_open : IsOpen (U ∩ V) := IsOpen.inter U_reg.isOpen V_reg.isOpen + + apply Set.eq_of_subset_of_subset + · simp + constructor + · nth_rw 2 [<-U_reg] + apply interiorClosure_mono + simp + · nth_rw 2 [<-V_reg] + apply interiorClosure_mono + simp + · apply interiorClosure_subset + exact UV_open + +theorem regular_sInter {S : Set (Set α)} (S_finite : Set.Finite S) (all_reg : ∀ U ∈ S, Regular U): + Regular (⋂₀ S) := +Set.Finite.induction_on' S_finite (by simp) (by + intro U S' U_in_S _ _ IH + rw [Set.sInter_insert] + apply regular_inter + · exact all_reg _ U_in_S + · exact IH +) + +theorem smulImage_interior {G : Type _} [Group G] [MulAction G α] + (g : G) (U : Set α) + (g_continuous : ∀ S : Set α, IsOpen S → IsOpen (g •'' S) ∧ IsOpen (g⁻¹ •'' S)): + interior (g •'' U) = g •'' interior U := +by + unfold interior + rw [smulImage_sUnion] + simp + ext x + simp + constructor + · intro ⟨T, ⟨T_open, T_sub⟩, x_in_T⟩ + use g⁻¹ •'' T + repeat' apply And.intro + · exact (g_continuous T T_open).right + · rw [smulImage_subset_inv] + rw [inv_inv] + exact T_sub + · rw [smulImage_mul, mul_right_inv, one_smulImage] + exact x_in_T + · intro ⟨T, ⟨T_open, T_sub⟩, x_in_T⟩ + use g •'' T + repeat' apply And.intro + · exact (g_continuous T T_open).left + · apply smulImage_mono + exact T_sub + · exact x_in_T + +theorem smulImage_closure {G : Type _} [Group G] [MulAction G α] + (g : G) (U : Set α) + (g_continuous : ∀ S : Set α, IsOpen S → IsOpen (g •'' S) ∧ IsOpen (g⁻¹ •'' S)): + closure (g •'' U) = g •'' closure U := +by + have g_continuous' : ∀ S : Set α, IsClosed S → IsClosed (g •'' S) ∧ IsClosed (g⁻¹ •'' S) := by + intro S S_closed + rw [<-isOpen_compl_iff] at S_closed + repeat rw [<-isOpen_compl_iff] + repeat rw [smulImage_compl] + exact g_continuous _ S_closed + unfold closure + rw [smulImage_sInter] + simp + ext x + simp + constructor + · intro IH T' T T_closed U_ss_T T'_eq + rw [<-T'_eq] + clear T' T'_eq + apply IH + · exact (g_continuous' _ T_closed).left + · apply smulImage_mono + exact U_ss_T + · intro IH T T_closed gU_ss_T + apply IH + · exact (g_continuous' _ T_closed).right + · rw [<-smulImage_subset_inv] + exact gU_ss_T + · simp + +theorem interiorClosure_smulImage {G : Type _} [Group G] [MulAction G α] + (g : G) (U : Set α) + (g_continuous : ∀ S : Set α, IsOpen S → IsOpen (g •'' S) ∧ IsOpen (g⁻¹ •'' S)) : + InteriorClosure (g •'' U) = g •'' InteriorClosure U := +by + simp + rw [<-smulImage_interior _ _ g_continuous] + rw [<-smulImage_closure _ _ g_continuous] + end Rubin diff --git a/Rubin/MulActionExt.lean b/Rubin/MulActionExt.lean index c2d14a9..2a87a84 100644 --- a/Rubin/MulActionExt.lean +++ b/Rubin/MulActionExt.lean @@ -71,4 +71,13 @@ by rw [<-mul_smul, mul_right_inv, one_smul] } +lemma exists_smul_ne {G : Type _} (α : Type _) [Group G] [MulAction G α] [h_f : FaithfulSMul G α] + {f g : G} (f_ne_g : f ≠ g) : ∃ (x : α), f • x ≠ g • x := +by + by_contra h + rw [Classical.not_exists_not] at h + apply f_ne_g + apply h_f.eq_of_smul_eq_smul + exact h + end Rubin diff --git a/Rubin/RegularSupport.lean b/Rubin/RegularSupport.lean index 17437a7..28e6233 100644 --- a/Rubin/RegularSupport.lean +++ b/Rubin/RegularSupport.lean @@ -63,6 +63,13 @@ by apply interiorClosure_mono exact h +theorem regularSupport_subset_closure_support {g : G} : + RegularSupport α g ⊆ closure (Support α g) := +by + unfold RegularSupport + simp + exact interior_subset + theorem regularSupport_subset_of_rigidStabilizer {g : G} {U : Set α} (U_reg : Regular U) : g ∈ RigidStabilizer G U → RegularSupport α g ⊆ U := by @@ -86,4 +93,12 @@ by end RegularSupport_continuous +theorem regularSupport_smulImage {G α : Type _} [Group G] [TopologicalSpace α] [ContinuousMulAction G α] + {f g : G} : + f •'' (RegularSupport α g) = RegularSupport α (f * g * f⁻¹) := +by + unfold RegularSupport + rw [support_conjugate] + rw [interiorClosure_smulImage _ _ (continuousMulAction_elem_continuous α f)] + end Rubin diff --git a/Rubin/SmulImage.lean b/Rubin/SmulImage.lean index 2156d18..e9249d8 100644 --- a/Rubin/SmulImage.lean +++ b/Rubin/SmulImage.lean @@ -105,9 +105,18 @@ by repeat rw [<-smulImage_mul] exact SmulImage.congr g⁻¹ h -theorem smulImage_inv {g: G} {U V : Set α} (img_eq : g •'' U = g •'' V) : U = V := - SmulImage.inv_congr g img_eq +theorem smulImage_inv (g: G) (U V : Set α) : g •'' U = V ↔ U = g⁻¹ •'' V := by + nth_rw 2 [<-one_smulImage (G := G) U] + rw [<-mul_left_inv g, <-smulImage_mul] + constructor + · intro h + rw [SmulImage.congr] + exact h + · intro h + apply SmulImage.inv_congr at h + exact h +-- TODO: rename to smulImage_mono theorem smulImage_subset (g : G) {U V : Set α} : U ⊆ V → g •'' U ⊆ g •'' V := by intro h1 x @@ -115,6 +124,8 @@ theorem smulImage_subset (g : G) {U V : Set α} : U ⊆ V → g •'' U ⊆ g exact fun h2 => h1 h2 #align smul''_subset Rubin.smulImage_subset +def smulImage_mono (g : G) {U V : Set α} : U ⊆ V → g •'' U ⊆ g •'' V := smulImage_subset g + theorem smulImage_union (g : G) {U V : Set α} : g •'' U ∪ V = (g •'' U) ∪ (g •'' V) := by ext @@ -129,6 +140,56 @@ theorem smulImage_inter (g : G) {U V : Set α} : g •'' U ∩ V = (g •'' U) Rubin.mem_smulImage, Set.mem_inter_iff] #align smul''_inter Rubin.smulImage_inter +theorem smulImage_sUnion (g : G) {S : Set (Set α)} : g •'' (⋃₀ S) = ⋃₀ {g •'' T | T ∈ S} := +by + ext x + constructor + · intro h + rw [mem_smulImage, Set.mem_sUnion] at h + rw [Set.mem_sUnion] + let ⟨T, ⟨T_in_S, ginv_x_in_T⟩⟩ := h + simp + use T + constructor; trivial + rw [mem_smulImage] + exact ginv_x_in_T + · intro h + rw [Set.mem_sUnion] at h + rw [mem_smulImage, Set.mem_sUnion] + simp at h + let ⟨T, ⟨T_in_S, x_in_gT⟩⟩ := h + use T + constructor; trivial + rw [<-mem_smulImage] + exact x_in_gT + +theorem smulImage_sInter (g : G) {S : Set (Set α)} : g •'' (⋂₀ S) = ⋂₀ {g •'' T | T ∈ S} := +by + ext x + constructor + · intro h + rw [mem_smulImage, Set.mem_sInter] at h + rw [Set.mem_sInter] + simp + intro T T_in_S + rw [mem_smulImage] + exact h T T_in_S + · intro h + rw [Set.mem_sInter] at h + rw [mem_smulImage, Set.mem_sInter] + intro T T_in_S + rw [<-mem_smulImage] + simp at h + exact h T T_in_S + +@[simp] +theorem smulImage_compl (g : G) (U : Set α) : (g •'' U)ᶜ = g •'' Uᶜ := +by + ext x + rw [Set.mem_compl_iff] + repeat rw [mem_smulImage] + rw [Set.mem_compl_iff] + theorem smulImage_eq_inv_preimage {g : G} {U : Set α} : g •'' U = (g⁻¹ • ·) ⁻¹' U := by ext diff --git a/Rubin/Support.lean b/Rubin/Support.lean index 289df68..bca7744 100644 --- a/Rubin/Support.lean +++ b/Rubin/Support.lean @@ -229,4 +229,32 @@ by apply Set.eq_empty_iff_forall_not_mem.mp support_empty exact h +theorem support_eq: Support α f = Support α g ↔ ∀ (x : α), (f • x = x ∧ g • x = x) ∨ (f • x ≠ x ∧ g • x ≠ x) := by + constructor + · intro h + intro x + by_cases x_in? : x ∈ Support α f + · right + have gx_ne_x := by rw [h] at x_in?; exact x_in? + exact ⟨x_in?, gx_ne_x⟩ + · left + have fx_eq_x : f • x = x := by rw [<-not_mem_support]; exact x_in? + have gx_eq_x : g • x = x := by rw [<-not_mem_support, <-h]; exact x_in? + exact ⟨fx_eq_x, gx_eq_x⟩ + · intro h + ext x + constructor + · intro fx_ne_x + rw [mem_support] at fx_ne_x + rw [mem_support] + cases h x with + | inl h₁ => exfalso; exact fx_ne_x h₁.left + | inr h₁ => exact h₁.right + · intro gx_ne_x + rw [mem_support] at gx_ne_x + rw [mem_support] + cases h x with + | inl h₁ => exfalso; exact gx_ne_x h₁.right + | inr h₁ => exact h₁.left + end Rubin diff --git a/Rubin/Topological.lean b/Rubin/Topological.lean index b9712e2..d906f98 100644 --- a/Rubin/Topological.lean +++ b/Rubin/Topological.lean @@ -13,12 +13,23 @@ namespace Rubin section Continuity --- TODO: don't have this extend MulAction +-- TODO: don't have this extend MulAction and move this somewhere else class ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] extends MulAction G α where continuous : ∀ g : G, Continuous (fun x: α => g • x) #align continuous_mul_action Rubin.ContinuousMulAction +theorem continuousMulAction_elem_continuous {G : Type _} (α : Type _) + [Group G] [TopologicalSpace α] [hc : ContinuousMulAction G α] (g : G): + ∀ (S : Set α), IsOpen S → IsOpen (g •'' S) ∧ IsOpen ((g⁻¹) •'' S) := +by + intro S S_open + repeat rw [smulImage_eq_inv_preimage] + rw [inv_inv] + constructor + · exact (hc.continuous g⁻¹).isOpen_preimage _ S_open + · exact (hc.continuous g).isOpen_preimage _ S_open + -- TODO: give this a notation? structure EquivariantHomeomorph (G α β : Type _) [Group G] [TopologicalSpace α] [TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where