From 69ad593f4bea509e3223ef84d9286ee71d50fdc3 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Sat, 2 Dec 2023 15:10:29 +0100 Subject: [PATCH] :sparkles: Prove proposition 3.2 --- Rubin.lean | 49 +++++++++++++++++++++++++++++++++++++---- Rubin/HomeoGroup.lean | 49 +++++++++++++++++++++++++++++++++++++++++ Rubin/LocallyDense.lean | 44 ++++++++++++++++++++++++++---------- Rubin/Topology.lean | 28 +++++++++++++++++++++++ 4 files changed, 154 insertions(+), 16 deletions(-) diff --git a/Rubin.lean b/Rubin.lean index e4c66b3..a95b089 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -12,6 +12,7 @@ import Mathlib.GroupTheory.GroupAction.Basic import Mathlib.GroupTheory.Exponent import Mathlib.GroupTheory.Perm.Basic import Mathlib.Topology.Basic +import Mathlib.Topology.Bases import Mathlib.Topology.Compactness.Compact import Mathlib.Topology.Separation import Mathlib.Topology.Homeomorph @@ -706,11 +707,13 @@ section HomeoGroup open Topology -theorem proposition_3_2 {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] +-- TODO: clean this lemma to not mention W anymore? +lemma proposition_3_2_subset (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α] [ContinuousMulAction G α] {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U) : - ∃ (W : Set α), W ∈ 𝓝 p ∧ closure W ⊆ U ∧ ∃ (g : G), g ∈ RigidStabilizer G W ∧ p ∈ RegularSupport α g := + ∃ (W : Set α), W ∈ 𝓝 p ∧ closure W ⊆ U ∧ + ∃ (g : G), g ∈ RigidStabilizer G W ∧ p ∈ RegularSupport α g ∧ RegularSupport α g ⊆ closure W := by have U_in_nhds : U ∈ 𝓝 p := by rw [mem_nhds_iff] @@ -741,17 +744,55 @@ by have p_in_int_W : p ∈ interior W := W'_ss_int_W (mem_of_mem_nhds W'_in_nhds) - let ⟨g, g_in_rist, g_moves_p⟩ := get_moving_elem_in_rigidStabilizer G p_in_int_W + let ⟨g, g_in_rist, g_moves_p⟩ := get_moving_elem_in_rigidStabilizer G isOpen_interior p_in_int_W use g - constructor + repeat' apply And.intro · apply rigidStabilizer_mono interior_subset simp exact g_in_rist · rw [<-mem_support] at g_moves_p apply support_subset_regularSupport exact g_moves_p + · rw [rigidStabilizer_support] at g_in_rist + apply subset_trans + exact regularSupport_subset_closure_support + apply closure_mono + apply subset_trans + exact g_in_rist + exact interior_subset +theorem proposition_3_2 {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] + [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α] + [hc : ContinuousMulAction G α] : + TopologicalSpace.IsTopologicalBasis (AssociatedPoset.asSet α) := +by + -- Note: the name later changes to isTopologicalBasis_of_isOpen_of_nhds + apply TopologicalSpace.isTopologicalBasis_of_open_of_nhds + { + intro U U_in_poset + rw [AssociatedPoset.mem_asSet] at U_in_poset + let ⟨T, T_val⟩ := U_in_poset + rw [<-T_val] + exact T.regular.isOpen + } + intro p U p_in_U U_open + + let ⟨W, _, clW_ss_U, ⟨g, _, p_in_rsupp, rsupp_ss_clW⟩⟩ := proposition_3_2_subset G U_open p_in_U + use RegularSupport α g + repeat' apply And.intro + · rw [AssociatedPoset.mem_asSet'] + constructor + exact ⟨p, p_in_rsupp⟩ + use {(ContinuousMulAction.toHomeomorph α g : HomeoGroup α)} + unfold AssociatedPosetElem + simp + unfold RegularSupport + rw [<-homeoGroup_support_eq_support_toHomeomorph g] + · exact p_in_rsupp + · apply subset_trans + exact rsupp_ss_clW + exact clW_ss_U end HomeoGroup diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean index 685e1d2..8fb4b0a 100644 --- a/Rubin/HomeoGroup.lean +++ b/Rubin/HomeoGroup.lean @@ -4,6 +4,7 @@ import Mathlib.Topology.Homeomorph import Rubin.LocallyDense import Rubin.Topology +import Rubin.Support import Rubin.RegularSupport structure HomeoGroup (α : Type _) [TopologicalSpace α] extends @@ -140,6 +141,16 @@ instance homeoGroup_mulAction₁_faithful : FaithfulSMul (HomeoGroup α) α wher simp exact hyp x +theorem homeoGroup_support_eq_support_toHomeomorph {G : Type _} + [Group G] [MulAction G α] [Rubin.ContinuousMulAction G α] (g : G) : + Rubin.Support α g = Rubin.Support α (HomeoGroup.from (Rubin.ContinuousMulAction.toHomeomorph α g)) := +by + ext x + repeat rw [Rubin.mem_support] + rw [<-HomeoGroup.smul₁_def] + rw [HomeoGroup.from_toHomeomorph] + rw [Rubin.ContinuousMulAction.toHomeomorph_toFun] + namespace Rubin section AssociatedPoset.Prelude @@ -397,6 +408,44 @@ by apply smulImage_mono assumption +instance associatedPoset_coeSet : Coe (AssociatedPoset α) (Set α) where + coe := AssociatedPoset.val + +def asSet (α : Type _) [TopologicalSpace α]: Set (Set α) := + { S : Set α | ∃ T : AssociatedPoset α, T.val = S } + +theorem asSet_def : + AssociatedPoset.asSet α = { S : Set α | ∃ T : AssociatedPoset α, T.val = S } := rfl + +theorem mem_asSet (S : Set α) : + S ∈ AssociatedPoset.asSet α ↔ ∃ T : AssociatedPoset α, T.val = S := +by + rw [asSet_def] + simp + +theorem mem_asSet' (S : Set α) : + S ∈ AssociatedPoset.asSet α ↔ Set.Nonempty S ∧ ∃ seed : Finset (HomeoGroup α), S = AssociatedPosetElem seed := +by + rw [asSet_def] + simp + constructor + · intro ⟨T, T_eq⟩ + rw [<-T_eq] + constructor + simp + + let ⟨⟨seed, _⟩, eq⟩ := T.val_has_seed + rw [AssociatedPosetSeed.val_def] at eq + simp at eq + use seed + exact eq.symm + · intro ⟨S_nonempty, ⟨seed, val_from_seed⟩⟩ + rw [val_from_seed] at S_nonempty + use fromSeed ⟨seed, S_nonempty⟩ + rw [val_from_seed] + simp + rw [AssociatedPosetSeed.val_def] + end AssociatedPoset section Other diff --git a/Rubin/LocallyDense.lean b/Rubin/LocallyDense.lean index f672f77..688f45c 100644 --- a/Rubin/LocallyDense.lean +++ b/Rubin/LocallyDense.lean @@ -8,9 +8,22 @@ namespace Rubin open Topology +/-- +A group action is said to be "locally dense" if for any open set `U` and `p ∈ U`, +the closure of the orbit of `p` under the `RigidStabilizer G U` contains a neighborhood of `p`. + +The definition provided here is an equivalent one, that does not require using filters. +See [`LocallyDense.from_rigidStabilizer_in_nhds`] and [`LocallyDense.rigidStabilizer_in_nhds`] +to translate from/to the original definition. + +A weaker relationship, [`LocallyMoving`], is used whenever possible. +The main difference between the two is that `LocallyMoving` does not allow us to find a group member +`g ∈ G` such that `g • p ≠ p` — it only allows us to know that `∃ g ∈ RigidStabilizer G U, g ≠ 1`. +--/ class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] := isLocallyDense: ∀ U : Set α, + IsOpen U → ∀ p ∈ U, p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) #align is_locally_dense Rubin.LocallyDense @@ -21,10 +34,7 @@ theorem LocallyDense.from_rigidStabilizer_in_nhds (G α : Type _) [Group G] [Top by intro hyp constructor - intro U p p_in_U - - -- TODO: potentially add that requirement to LocallyDense? - have U_open : IsOpen U := sorry + intro U U_open p p_in_U have closure_in_nhds := hyp U U_open p p_in_U rw [mem_nhds_iff] at closure_in_nhds @@ -32,14 +42,24 @@ by rw [mem_interior] exact closure_in_nhds --- TODO: rename -lemma LocallyDense.nonEmpty {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α]: +theorem LocallyDense.rigidStabilizer_in_nhds (G α : Type _) [Group G] [TopologicalSpace α] + [MulAction G α] [LocallyDense G α] + {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U) +: + closure (MulAction.orbit (RigidStabilizer G U) p) ∈ 𝓝 p := +by + rw [mem_nhds_iff] + rw [<-mem_interior] + apply LocallyDense.isLocallyDense <;> assumption + +lemma LocallyDense.elem_from_nonEmpty {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α]: ∀ {U : Set α}, + IsOpen U → Set.Nonempty U → ∃ p ∈ U, p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) := by - intros U H_ne - exact ⟨H_ne.some, H_ne.some_mem, LocallyDense.isLocallyDense U H_ne.some H_ne.some_mem⟩ + intros U U_open H_ne + exact ⟨H_ne.some, H_ne.some_mem, LocallyDense.isLocallyDense U U_open H_ne.some H_ne.some_mem⟩ /-- This is a stronger statement than `LocallyMoving.get_nontrivial_rist_elem`, @@ -50,7 +70,7 @@ The condition that `Filer.NeBot (𝓝[≠] p)` is automatically satisfied by the theorem get_moving_elem_in_rigidStabilizer (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α] [T1Space α] {p : α} [Filter.NeBot (𝓝[≠] p)] - {U : Set α} (p_in_U : p ∈ U) : + {U : Set α} (U_open : IsOpen U) (p_in_U : p ∈ U) : ∃ g : G, g ∈ RigidStabilizer G U ∧ g • p ≠ p := by by_contra g_not_exist @@ -76,7 +96,7 @@ by rw [closure_singleton] rw [interior_singleton] - have p_in_regular_orbit := LocallyDense.isLocallyDense (G := G) U p p_in_U + have p_in_regular_orbit := LocallyDense.isLocallyDense (G := G) U U_open p p_in_U rw [regular_orbit_empty] at p_in_regular_orbit exact p_in_regular_orbit @@ -110,9 +130,9 @@ instance dense_locally_moving [T2Space α] LocallyMoving G α where locally_moving := by - intros U _ H_nonempty + intros U U_open H_nonempty by_contra h_rs - have ⟨elem, ⟨_, some_in_orbit⟩⟩ := H_ld.nonEmpty H_nonempty + have ⟨elem, ⟨_, some_in_orbit⟩⟩ := H_ld.elem_from_nonEmpty U_open H_nonempty rw [h_rs] at some_in_orbit simp at some_in_orbit diff --git a/Rubin/Topology.lean b/Rubin/Topology.lean index ca0c595..1efaf82 100644 --- a/Rubin/Topology.lean +++ b/Rubin/Topology.lean @@ -12,6 +12,34 @@ class ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] [MulAc continuous : ∀ g : G, Continuous (fun x: α => g • x) #align continuous_mul_action Rubin.ContinuousMulAction +def ContinuousMulAction.toHomeomorph {G : Type _} (α : Type _) + [Group G] [TopologicalSpace α] [MulAction G α] [hc : ContinuousMulAction G α] + (g : G) : Homeomorph α α +where + toFun := fun x => g • x + invFun := fun x => g⁻¹ • x + left_inv := by + intro y + simp + right_inv := by + intro y + simp + continuous_toFun := by + simp + exact hc.continuous _ + continuous_invFun := by + simp + exact hc.continuous _ + +theorem ContinuousMulAction.toHomeomorph_toFun {G : Type _} (α : Type _) + [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] + (g : G) : (ContinuousMulAction.toHomeomorph α g).toFun = fun x => g • x := rfl + + +theorem ContinuousMulAction.toHomeomorph_invFun {G : Type _} (α : Type _) + [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] + (g : G) : (ContinuousMulAction.toHomeomorph α g).invFun = fun x => g⁻¹ • x := rfl + -- TODO: give this a notation? structure EquivariantHomeomorph (G α β : Type _) [Group G] [TopologicalSpace α] [TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where