From 652e1a0773c5eda404fc82e830c885d5188b1d32 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Fri, 1 Dec 2023 13:21:23 +0100 Subject: [PATCH] :truck: Move a bunch of definitions around, making Topology importable from more files --- Rubin.lean | 14 ++-- Rubin/AlgebraicDisjointness.lean | 108 ++-------------------------- Rubin/HomeoGroup.lean | 3 +- Rubin/LocallyDense.lean | 118 ++++++++++++++++++++++++++++++ Rubin/MulActionExt.lean | 24 +++++++ Rubin/RegularSupport.lean | 11 +-- Rubin/SmulImage.lean | 15 ++++ Rubin/Support.lean | 35 +++++++++ Rubin/Topological.lean | 120 ------------------------------- Rubin/Topology.lean | 54 ++++++++++++++ 10 files changed, 265 insertions(+), 237 deletions(-) create mode 100644 Rubin/LocallyDense.lean delete mode 100644 Rubin/Topological.lean create mode 100644 Rubin/Topology.lean diff --git a/Rubin.lean b/Rubin.lean index a01b4f3..abe08d3 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -20,7 +20,7 @@ import Rubin.Tactic import Rubin.MulActionExt import Rubin.SmulImage import Rubin.Support -import Rubin.Topological +import Rubin.Topology import Rubin.RigidStabilizer import Rubin.Period import Rubin.AlgebraicDisjointness @@ -69,6 +69,7 @@ section AlgebraicDisjointness variable {G α : Type _} variable [TopologicalSpace α] variable [Group G] +variable [MulAction G α] variable [ContinuousMulAction G α] variable [FaithfulSMul G α] @@ -350,7 +351,8 @@ end AlgebraicDisjointness section RegularSupport -lemma lemma_2_2 (G: Type _) {α : Type _} [Group G] [TopologicalSpace α] [ContinuousMulAction G α] [FaithfulSMul G α] +lemma lemma_2_2 (G: Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] + [ContinuousMulAction G α] [FaithfulSMul G α] [T2Space α] [h_lm : LocallyMoving G α] {U : Set α} (U_open : IsOpen U) (U_nonempty : Set.Nonempty U) : Monoid.exponent (RigidStabilizer G U) = 0 := @@ -494,7 +496,7 @@ def AlgebraicCentralizer {G: Type _} [Group G] (f : G) : Subgroup G := -- we construct an open subset within `Support α h \ RegularSupport α f`, -- and we show that it is non-empty, open and (by construction) disjoint from `Support α f`. lemma open_set_from_supp_not_subset_rsupp {G α : Type _} - [Group G] [TopologicalSpace α] [ContinuousMulAction G α] [T2Space α] + [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] [T2Space α] {f h : G} (not_support_subset_rsupp : ¬Support α h ⊆ RegularSupport α f): ∃ V : Set α, V ⊆ Support α h ∧ Set.Nonempty V ∧ IsOpen V ∧ Disjoint V (Support α f) := by @@ -550,7 +552,7 @@ by lemma proposition_2_1 {G α : Type _} - [Group G] [TopologicalSpace α] [ContinuousMulAction G α] [T2Space α] + [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] [T2Space α] [LocallyMoving G α] [h_faithful : FaithfulSMul G α] (f : G) : AlgebraicCentralizer f = RigidStabilizer G (RegularSupport α f) := @@ -637,7 +639,7 @@ by -- Small lemma for remark 2.3 theorem rigidStabilizer_inter_bot_iff_regularSupport_disj {G α : Type _} - [Group G] [TopologicalSpace α] [ContinuousMulAction G α] [LocallyMoving G α] [FaithfulSMul G α] + [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] [LocallyMoving G α] [FaithfulSMul G α] {f g : G} : RigidStabilizer G (RegularSupport α f) ⊓ RigidStabilizer G (RegularSupport α g) = ⊥ ↔ Disjoint (RegularSupport α f) (RegularSupport α g) := @@ -684,7 +686,7 @@ We could prove that the intersection of the algebraic centralizers of `f` and `g purely within group theory, and then apply this theorem to know that their support in `α` will be disjoint. --/ -lemma remark_2_3 {G α : Type _} [Group G] [TopologicalSpace α] [T2Space α] +lemma remark_2_3 {G α : Type _} [Group G] [TopologicalSpace α] [T2Space α] [MulAction G α] [ContinuousMulAction G α] [FaithfulSMul G α] [LocallyMoving G α] {f g : G} : (AlgebraicCentralizer f) ⊓ (AlgebraicCentralizer g) = ⊥ → Disjoint (Support α f) (Support α g) := by diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean index 2f04139..b5450ef 100644 --- a/Rubin/AlgebraicDisjointness.lean +++ b/Rubin/AlgebraicDisjointness.lean @@ -9,33 +9,13 @@ import Mathlib.Tactic.IntervalCases import Rubin.RigidStabilizer import Rubin.SmulImage -import Rubin.Topological +import Rubin.Topology import Rubin.FaithfulAction import Rubin.Period +import Rubin.LocallyDense namespace Rubin -class LocallyMoving (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] := - locally_moving: ∀ U : Set α, IsOpen U → Set.Nonempty U → RigidStabilizer G U ≠ ⊥ -#align is_locally_moving Rubin.LocallyMoving - -namespace LocallyMoving - -theorem get_nontrivial_rist_elem {G α : Type _} - [Group G] - [TopologicalSpace α] - [MulAction G α] - [h_lm : LocallyMoving G α] - {U: Set α} - (U_open : IsOpen U) - (U_nonempty : U.Nonempty) : - ∃ x : G, x ∈ RigidStabilizer G U ∧ x ≠ 1 := -by - have rist_ne_bot := h_lm.locally_moving U U_open U_nonempty - exact (or_iff_right rist_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) - -end LocallyMoving - structure AlgebraicallyDisjointElem {G : Type _} [Group G] (f g h : G) := non_commute: ¬Commute f h fst : G @@ -138,94 +118,14 @@ instance coeAlgebraicallyDisjoint : Coe (AlgebraicallyDisjoint f g) (IsAlgebraic end IsAlgebraicallyDisjoint -@[simp] -theorem orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) : - MulAction.orbit (⊥ : Subgroup G) p = {p} := - by - ext1 - rw [MulAction.mem_orbit_iff] - constructor - · rintro ⟨⟨_, g_bot⟩, g_to_x⟩ - rw [← g_to_x, Set.mem_singleton_iff, Subgroup.mk_smul] - exact (Subgroup.mem_bot.mp g_bot).symm ▸ one_smul _ _ - exact fun h => ⟨1, Eq.trans (one_smul _ p) (Set.mem_singleton_iff.mp h).symm⟩ -#align orbit_bot Rubin.orbit_bot - +-- TODO: find a better home for these lemmas variable {G α : Type _} variable [Group G] variable [TopologicalSpace α] +variable [MulAction G α] variable [ContinuousMulAction G α] variable [FaithfulSMul G α] -instance dense_locally_moving [T2Space α] - [H_nip : HasNoIsolatedPoints α] - (H_ld : LocallyDense G α) : - LocallyMoving G α -where - locally_moving := by - intros U _ H_nonempty - by_contra h_rs - have ⟨elem, ⟨_, some_in_orbit⟩⟩ := H_ld.nonEmpty H_nonempty - -- Note: This is automatic now :) - -- have H_nebot := has_no_isolated_points_neBot elem - rw [h_rs] at some_in_orbit - simp at some_in_orbit - -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 (g • x) x x_moved - let U := (g⁻¹ •'' V) ∩ W - use U - constructor - { - -- NOTE: if this is common, then we should make a tactic for solving IsOpen goals - exact IsOpen.inter (img_open_open g⁻¹ V V_open) W_open - } - constructor - { - simp - rw [mem_inv_smulImage] - trivial - } - { - apply Set.disjoint_of_subset - · apply Set.inter_subset_right - · intro y hy; show y ∈ V - - rw [<-smul_inv_smul g y] - rw [<-mem_inv_smulImage] - - rw [mem_smulImage] at hy - simp at hy - - exact hy.left - · exact disjoint_V_W.symm - } - -lemma disjoint_nbhd_in [T2Space α] {g : G} {x : α} {V : Set α} - (V_open : IsOpen V) (x_in_V : x ∈ V) (x_moved : g • x ≠ x) : - ∃ U : Set α, IsOpen U ∧ x ∈ U ∧ U ⊆ V ∧ Disjoint U (g •'' U) := -by - have ⟨W, W_open, x_in_W, disjoint_W_img⟩ := disjoint_nbhd x_moved - use W ∩ V - simp - constructor - { - apply IsOpen.inter <;> assumption - } - constructor - { - constructor <;> assumption - } - show Disjoint (W ∩ V) (g •'' W ∩ V) - apply Set.disjoint_of_subset - · exact Set.inter_subset_left W V - · show g •'' W ∩ V ⊆ g •'' W - rewrite [smulImage_inter] - exact Set.inter_subset_left _ _ - · exact disjoint_W_img - -- Kind of a boring lemma but okay lemma rewrite_Union (f : Fin 2 × Fin 2 → Set α) : (⋃(i : Fin 2 × Fin 2), f i) = (f (0,0) ∪ f (0,1)) ∪ (f (1,0) ∪ f (1,1)) := diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean index e97ae99..288f6c6 100644 --- a/Rubin/HomeoGroup.lean +++ b/Rubin/HomeoGroup.lean @@ -2,8 +2,7 @@ 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.Topology import Rubin.RegularSupport structure HomeoGroup (α : Type _) [TopologicalSpace α] extends diff --git a/Rubin/LocallyDense.lean b/Rubin/LocallyDense.lean new file mode 100644 index 0000000..4483b78 --- /dev/null +++ b/Rubin/LocallyDense.lean @@ -0,0 +1,118 @@ +import Mathlib.GroupTheory.Subgroup.Basic +import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.Topology.Basic + +import Rubin.RigidStabilizer + +namespace Rubin + +open Topology + +class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] := + isLocallyDense: + ∀ U : Set α, + ∀ p ∈ U, + p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) +#align is_locally_dense Rubin.LocallyDense + +lemma LocallyDense.nonEmpty {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α]: + ∀ {U : Set α}, + 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⟩ + +class LocallyMoving (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] := + locally_moving: ∀ U : Set α, IsOpen U → Set.Nonempty U → RigidStabilizer G U ≠ ⊥ +#align is_locally_moving Rubin.LocallyMoving + +theorem LocallyMoving.get_nontrivial_rist_elem {G α : Type _} + [Group G] + [TopologicalSpace α] + [MulAction G α] + [h_lm : LocallyMoving G α] + {U: Set α} + (U_open : IsOpen U) + (U_nonempty : U.Nonempty) : + ∃ x : G, x ∈ RigidStabilizer G U ∧ x ≠ 1 := +by + have rist_ne_bot := h_lm.locally_moving U U_open U_nonempty + exact (or_iff_right rist_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) + +variable {G α : Type _} +variable [Group G] +variable [TopologicalSpace α] +variable [MulAction G α] +variable [ContinuousMulAction G α] +variable [FaithfulSMul G α] + +instance dense_locally_moving [T2Space α] + [H_nip : HasNoIsolatedPoints α] + [H_ld : LocallyDense G α] : + LocallyMoving G α +where + locally_moving := by + intros U _ H_nonempty + by_contra h_rs + have ⟨elem, ⟨_, some_in_orbit⟩⟩ := H_ld.nonEmpty H_nonempty + rw [h_rs] at some_in_orbit + simp at some_in_orbit + +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 (g • x) x x_moved + let U := (g⁻¹ •'' V) ∩ W + use U + constructor + { + -- NOTE: if this is common, then we should make a tactic for solving IsOpen goals + exact IsOpen.inter (img_open_open g⁻¹ V V_open) W_open + } + constructor + { + simp + rw [mem_inv_smulImage] + trivial + } + { + apply Set.disjoint_of_subset + · apply Set.inter_subset_right + · intro y hy; show y ∈ V + + rw [<-smul_inv_smul g y] + rw [<-mem_inv_smulImage] + + rw [mem_smulImage] at hy + simp at hy + + exact hy.left + · exact disjoint_V_W.symm + } + +lemma disjoint_nbhd_in [T2Space α] {g : G} {x : α} {V : Set α} + (V_open : IsOpen V) (x_in_V : x ∈ V) (x_moved : g • x ≠ x) : + ∃ U : Set α, IsOpen U ∧ x ∈ U ∧ U ⊆ V ∧ Disjoint U (g •'' U) := +by + have ⟨W, W_open, x_in_W, disjoint_W_img⟩ := disjoint_nbhd x_moved + use W ∩ V + simp + constructor + { + apply IsOpen.inter <;> assumption + } + constructor + { + constructor <;> assumption + } + show Disjoint (W ∩ V) (g •'' W ∩ V) + apply Set.disjoint_of_subset + · exact Set.inter_subset_left W V + · show g •'' W ∩ V ⊆ g •'' W + rewrite [smulImage_inter] + exact Set.inter_subset_left _ _ + · exact disjoint_W_img + + +end Rubin diff --git a/Rubin/MulActionExt.lean b/Rubin/MulActionExt.lean index 2a87a84..86be76b 100644 --- a/Rubin/MulActionExt.lean +++ b/Rubin/MulActionExt.lean @@ -80,4 +80,28 @@ by apply h_f.eq_of_smul_eq_smul exact h +@[simp] +theorem orbit_bot {G : Type _} [Group G] {H : Subgroup G} (H_eq_bot : H = ⊥): + ∀ (g : G), MulAction.orbit H g = {g} := +by + intro g + ext x + rw [MulAction.mem_orbit_iff] + simp + rw [H_eq_bot] + simp + constructor <;> tauto + +@[simp] +theorem orbit_bot₂ {G : Type _} [Group G] {α : Type _} [MulAction G α] (H : Subgroup G) (H_eq_bot : H = ⊥): + ∀ (x : α), MulAction.orbit H x = {x} := +by + intro g + ext x + rw [MulAction.mem_orbit_iff] + simp + rw [H_eq_bot] + simp + constructor <;> tauto + end Rubin diff --git a/Rubin/RegularSupport.lean b/Rubin/RegularSupport.lean index 28e6233..2830afd 100644 --- a/Rubin/RegularSupport.lean +++ b/Rubin/RegularSupport.lean @@ -6,8 +6,9 @@ import Mathlib.Topology.Separation import Rubin.Tactic import Rubin.Support -import Rubin.Topological +import Rubin.Topology import Rubin.InteriorClosure +import Rubin.RigidStabilizer namespace Rubin @@ -46,6 +47,7 @@ section RegularSupport_continuous variable {G α : Type _} variable [Group G] variable [TopologicalSpace α] +variable [MulAction G α] variable [ContinuousMulAction G α] theorem support_subset_regularSupport [T2Space α] {g : G} : @@ -91,14 +93,13 @@ by exact rs_subset #align mem_regular_support Rubin.regularSupport_subset_of_rigidStabilizer -end RegularSupport_continuous - -theorem regularSupport_smulImage {G α : Type _} [Group G] [TopologicalSpace α] [ContinuousMulAction G α] - {f g : G} : +theorem regularSupport_smulImage {f g : G} : f •'' (RegularSupport α g) = RegularSupport α (f * g * f⁻¹) := by unfold RegularSupport rw [support_conjugate] rw [interiorClosure_smulImage _ _ (continuousMulAction_elem_continuous α f)] +end RegularSupport_continuous + end Rubin diff --git a/Rubin/SmulImage.lean b/Rubin/SmulImage.lean index 79fa3bc..02bd491 100644 --- a/Rubin/SmulImage.lean +++ b/Rubin/SmulImage.lean @@ -1,8 +1,10 @@ import Mathlib.Data.Finset.Basic import Mathlib.GroupTheory.Subgroup.Basic import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.Topology.Basic import Rubin.MulActionExt +import Rubin.Topology namespace Rubin @@ -283,4 +285,17 @@ by exact h_notin_V #align distinct_images_from_disjoint Rubin.smulImage_distinct_of_disjoint_pow + +theorem continuousMulAction_elem_continuous {G : Type _} (α : Type _) + [Group G] [TopologicalSpace α] [MulAction G α] [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 + + end Rubin diff --git a/Rubin/Support.lean b/Rubin/Support.lean index 340acf1..dc52237 100644 --- a/Rubin/Support.lean +++ b/Rubin/Support.lean @@ -2,6 +2,7 @@ import Mathlib.Data.Finset.Basic import Mathlib.GroupTheory.Commutator import Mathlib.GroupTheory.Subgroup.Basic import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.Topology.Basic import Rubin.MulActionExt import Rubin.SmulImage @@ -258,4 +259,38 @@ theorem support_eq: Support α f = Support α g ↔ ∀ (x : α), (f • x = x | inl h₁ => exfalso; exact gx_ne_x h₁.right | inr h₁ => exact h₁.left +section Continuous + +variable {G α : Type _} +variable [Group G] +variable [TopologicalSpace α] +variable [MulAction G α] +variable [ContinuousMulAction G α] + +theorem img_open_open (g : G) (U : Set α) (h : IsOpen U): IsOpen (g •'' U) := + by + rw [Rubin.smulImage_eq_inv_preimage] + exact Continuous.isOpen_preimage (Rubin.ContinuousMulAction.continuous g⁻¹) U h + +#align img_open_open Rubin.img_open_open + +theorem support_open (g : G) [TopologicalSpace α] [T2Space α] + [ContinuousMulAction G α] : IsOpen (Support α g) := + by + apply isOpen_iff_forall_mem_open.mpr + intro x 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 + ⟨V ∩ (g⁻¹ •'' U), fun y yW => + Disjoint.ne_of_mem + disjoint_U_V + (mem_inv_smulImage.mp (Set.mem_of_mem_inter_right yW)) + (Set.mem_of_mem_inter_left yW), + IsOpen.inter open_V (Rubin.img_open_open g⁻¹ U open_U), + ⟨x_in_V, mem_inv_smulImage.mpr gx_in_U⟩ + ⟩ +#align support_open Rubin.support_open + +end Continuous + end Rubin diff --git a/Rubin/Topological.lean b/Rubin/Topological.lean deleted file mode 100644 index 0fd12cf..0000000 --- a/Rubin/Topological.lean +++ /dev/null @@ -1,120 +0,0 @@ -import Mathlib.GroupTheory.Subgroup.Basic -import Mathlib.GroupTheory.GroupAction.Basic -import Mathlib.Topology.Basic -import Mathlib.Topology.Homeomorph -import Mathlib.Data.Set.Basic - -import Rubin.RigidStabilizer -import Rubin.MulActionExt -import Rubin.SmulImage -import Rubin.Support - -namespace Rubin - -section Continuity - -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 - equivariant : is_equivariant G toFun -#align equivariant_homeomorph Rubin.EquivariantHomeomorph - -variable {G α β : Type _} -variable [Group G] -variable [TopologicalSpace α] [TopologicalSpace β] - -theorem equivariant_fun [MulAction G α] [MulAction G β] - (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 α β) : - is_equivariant G h.invFun := - by - intro g x - symm - 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 - -variable [ContinuousMulAction G α] - -theorem img_open_open (g : G) (U : Set α) (h : IsOpen U): IsOpen (g •'' U) := - by - rw [Rubin.smulImage_eq_inv_preimage] - exact Continuous.isOpen_preimage (Rubin.ContinuousMulAction.continuous g⁻¹) U h - -#align img_open_open Rubin.img_open_open - -theorem support_open (g : G) [TopologicalSpace α] [T2Space α] - [ContinuousMulAction G α] : IsOpen (Support α g) := - by - apply isOpen_iff_forall_mem_open.mpr - intro x 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 - ⟨V ∩ (g⁻¹ •'' U), fun y yW => - Disjoint.ne_of_mem - disjoint_U_V - (mem_inv_smulImage.mp (Set.mem_of_mem_inter_right yW)) - (Set.mem_of_mem_inter_left yW), - IsOpen.inter open_V (Rubin.img_open_open g⁻¹ U open_U), - ⟨x_in_V, mem_inv_smulImage.mpr gx_in_U⟩ - ⟩ -#align support_open Rubin.support_open - -end Continuity - --- TODO: come up with a name -section LocallyDense -open Topology - -/-- -Note: `𝓝[≠] x` is notation for `nhdsWithin x {[x]}ᶜ`, ie. the neighborhood of x not containing itself. - ---/ -class HasNoIsolatedPoints (α : Type _) [TopologicalSpace α] := - nhbd_ne_bot : ∀ x : α, 𝓝[≠] x ≠ ⊥ -#align has_no_isolated_points Rubin.HasNoIsolatedPoints - -instance has_no_isolated_points_neBot {α : Type _} [TopologicalSpace α] [h_nip: HasNoIsolatedPoints α] (x: α): Filter.NeBot (𝓝[≠] x) where - ne' := h_nip.nhbd_ne_bot x - -class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] extends MulAction G α := - isLocallyDense: - ∀ U : Set α, - ∀ p ∈ U, - p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) -#align is_locally_dense Rubin.LocallyDense - -lemma LocallyDense.nonEmpty {G α : Type _} [Group G] [TopologicalSpace α] [LocallyDense G α]: - ∀ {U : Set α}, - 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⟩ - -end LocallyDense - - -end Rubin diff --git a/Rubin/Topology.lean b/Rubin/Topology.lean new file mode 100644 index 0000000..ca0c595 --- /dev/null +++ b/Rubin/Topology.lean @@ -0,0 +1,54 @@ +import Mathlib.GroupTheory.Subgroup.Basic +import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.Topology.Basic +import Mathlib.Topology.Homeomorph +import Mathlib.Data.Set.Basic + +import Rubin.MulActionExt + +namespace Rubin + +class ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] where + continuous : ∀ g : G, Continuous (fun x: α => g • x) +#align continuous_mul_action Rubin.ContinuousMulAction + +-- TODO: give this a notation? +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 + +variable {G α β : Type _} +variable [Group G] +variable [TopologicalSpace α] [TopologicalSpace β] + +theorem equivariant_fun [MulAction G α] [MulAction G β] + (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 α β) : + is_equivariant G h.invFun := + by + intro g x + symm + 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 + +open Topology + +/-- +Note: `𝓝[≠] x` is notation for `nhdsWithin x {[x]}ᶜ`, ie. the neighborhood of x not containing itself. +--/ +class HasNoIsolatedPoints (α : Type _) [TopologicalSpace α] := + nhbd_ne_bot : ∀ x : α, 𝓝[≠] x ≠ ⊥ +#align has_no_isolated_points Rubin.HasNoIsolatedPoints + +instance has_no_isolated_points_neBot {α : Type _} [TopologicalSpace α] [h_nip: HasNoIsolatedPoints α] (x: α): Filter.NeBot (𝓝[≠] x) where + ne' := h_nip.nhbd_ne_bot x + +end Rubin