From 24dd2c4f0a2da14b265b8b7c052db5d570ab38b0 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Sun, 17 Dec 2023 17:01:03 +0100 Subject: [PATCH] :fire: New notation for RigidStabilizer and prove first lemma for proposition 3.5 --- Rubin.lean | 54 ++++++++++++++++---------------------- Rubin/LocallyDense.lean | 10 +++---- Rubin/RigidStabilizer.lean | 33 +++++++++++------------ Rubin/Topology.lean | 30 +++++++++++++++++++++ 4 files changed, 73 insertions(+), 54 deletions(-) diff --git a/Rubin.lean b/Rubin.lean index bf977d0..773e1ea 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -355,7 +355,7 @@ lemma lemma_2_2 (G: Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAc [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 := + Monoid.exponent G•[U] = 0 := by by_contra exp_ne_zero @@ -548,7 +548,7 @@ lemma proposition_2_1 {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] [T2Space α] [LocallyMoving G α] [h_faithful : FaithfulSMul G α] (f : G) : - AlgebraicCentralizer f = RigidStabilizer G (RegularSupport α f) := + AlgebraicCentralizer f = G•[RegularSupport α f] := by ext h @@ -634,7 +634,7 @@ by theorem rigidStabilizer_inter_bot_iff_regularSupport_disj {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] [LocallyMoving G α] [FaithfulSMul G α] {f g : G} : - RigidStabilizer G (RegularSupport α f) ⊓ RigidStabilizer G (RegularSupport α g) = ⊥ + G•[RegularSupport α f] ⊓ G•[RegularSupport α g] = ⊥ ↔ Disjoint (RegularSupport α f) (RegularSupport α g) := by rw [<-rigidStabilizer_inter] @@ -782,34 +782,23 @@ def RSuppOrbit {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] { g •'' W | (g ∈ H) (W ∈ F) } lemma moving_elem_of_open_subset_closure_orbit {U V : Set α} (U_open : IsOpen U) (U_nonempty : Set.Nonempty U) - {p : α} (p_in_V : p ∈ V) (U_ss_clOrbit : U ⊆ closure (MulAction.orbit (RigidStabilizer G V) p)) : - ∃ h : G, h ∈ RigidStabilizer G V ∧ h • p ∈ U := + {p : α} (U_ss_clOrbit : U ⊆ closure (MulAction.orbit G•[V] p)) : + ∃ h : G, h ∈ G•[V] ∧ h • p ∈ U := by - have U_ss_clV : U ⊆ closure V := by - apply subset_trans - exact U_ss_clOrbit - apply closure_mono - exact orbit_rigidStabilizer_subset p_in_V - - by_cases (RigidStabilizer G V) = ⊥ - case pos rist_bot => - rw [rist_bot] at U_ss_clOrbit - simp at U_ss_clOrbit - use 1 - constructor - exact Subgroup.one_mem _ - rw [one_smul] - let ⟨q, q_in_U⟩ := U_nonempty - rw [<-U_ss_clOrbit _ q_in_U] - assumption - case neg rist_ne_bot => - rw [<-ne_eq, Subgroup.ne_bot_iff_exists_ne_one] at rist_ne_bot - let ⟨⟨g, g_in_rist⟩, g_ne_one⟩ := rist_ne_bot - rw [ne_eq, Subgroup.mk_eq_one_iff, <-ne_eq] at g_ne_one + have p_in_orbit : p ∈ MulAction.orbit G•[V] p := by simp - -- Idea: show that `U ∩ Orb(p, G_U)` is nonempty? - sorry + have ⟨q, ⟨q_in_U, q_in_orbit⟩⟩ := inter_of_open_subset_of_closure + U_open U_nonempty ⟨p, p_in_orbit⟩ U_ss_clOrbit + rw [MulAction.mem_orbit_iff] at q_in_orbit + let ⟨⟨h, h_in_orbit⟩, hq_eq_p⟩ := q_in_orbit + simp at hq_eq_p + + use h + constructor + assumption + rw [hq_eq_p] + assumption lemma compact_subset_of_rsupp_basis [LocallyCompactSpace α] (U : RegularSupportBasis α): @@ -885,6 +874,8 @@ by simp at W_in_subsets let ⟨W_in_basis, W_subset_rsupp⟩ := W_in_subsets clear W_in_subsets g' g'_ne_one + unfold RSuppOrbit + simp -- We have that W is a subset of the closure of the orbit of G_U have W_ss_clOrbit : W ⊆ closure (MulAction.orbit (↥(RigidStabilizer G U.val)) p) := by @@ -899,9 +890,8 @@ by rw [<-closure_closure (s := MulAction.orbit _ _)] apply closure_mono assumption - unfold RSuppOrbit - simp + -- W is also open and nonempty... have W_open : IsOpen W := by let ⟨W', W'_eq⟩ := (RegularSupportBasis.mem_asSet _).mp W_in_basis rw [<-W'_eq] @@ -911,8 +901,8 @@ by rw [<-W'_eq] exact W'.nonempty - -- We get an element `h` such that `h • p ∈ W` and `h ∈ G_U` - let ⟨h, h_in_rist, hp_in_W⟩ := moving_elem_of_open_subset_closure_orbit W_open W_nonempty p_in_U W_ss_clOrbit + -- So we can get an element `h` such that `h • p ∈ W` and `h ∈ G_U` + let ⟨h, h_in_rist, hp_in_W⟩ := moving_elem_of_open_subset_closure_orbit W_open W_nonempty W_ss_clOrbit use h constructor diff --git a/Rubin/LocallyDense.lean b/Rubin/LocallyDense.lean index 688f45c..320dac6 100644 --- a/Rubin/LocallyDense.lean +++ b/Rubin/LocallyDense.lean @@ -29,7 +29,7 @@ class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G #align is_locally_dense Rubin.LocallyDense theorem LocallyDense.from_rigidStabilizer_in_nhds (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] : - (∀ U : Set α, IsOpen U → ∀ p ∈ U, closure (MulAction.orbit (RigidStabilizer G U) p) ∈ 𝓝 p) → + (∀ U : Set α, IsOpen U → ∀ p ∈ U, closure (MulAction.orbit G•[U] p) ∈ 𝓝 p) → LocallyDense G α := by intro hyp @@ -46,7 +46,7 @@ theorem LocallyDense.rigidStabilizer_in_nhds (G α : Type _) [Group G] [Topologi [MulAction G α] [LocallyDense G α] {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U) : - closure (MulAction.orbit (RigidStabilizer G U) p) ∈ 𝓝 p := + closure (MulAction.orbit G•[U] p) ∈ 𝓝 p := by rw [mem_nhds_iff] rw [<-mem_interior] @@ -56,7 +56,7 @@ lemma LocallyDense.elem_from_nonEmpty {G α : Type _} [Group G] [TopologicalSpac ∀ {U : Set α}, IsOpen U → Set.Nonempty U → - ∃ p ∈ U, p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) := + ∃ p ∈ U, p ∈ interior (closure (MulAction.orbit G•[U] p)) := by 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⟩ @@ -71,7 +71,7 @@ theorem get_moving_elem_in_rigidStabilizer (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [LocallyDense G α] [T1Space α] {p : α} [Filter.NeBot (𝓝[≠] p)] {U : Set α} (U_open : IsOpen U) (p_in_U : p ∈ U) : - ∃ g : G, g ∈ RigidStabilizer G U ∧ g • p ≠ p := + ∃ g : G, g ∈ G•[U] ∧ g • p ≠ p := by by_contra g_not_exist rw [<-Classical.not_forall_not] at g_not_exist @@ -112,7 +112,7 @@ theorem LocallyMoving.get_nontrivial_rist_elem {G α : Type _} {U: Set α} (U_open : IsOpen U) (U_nonempty : U.Nonempty) : - ∃ x : G, x ∈ RigidStabilizer G U ∧ x ≠ 1 := + ∃ x : G, x ∈ 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 _) diff --git a/Rubin/RigidStabilizer.lean b/Rubin/RigidStabilizer.lean index 76ac63a..c51e61e 100644 --- a/Rubin/RigidStabilizer.lean +++ b/Rubin/RigidStabilizer.lean @@ -11,7 +11,14 @@ def rigidStabilizer' (G : Type _) [Group G] [MulAction G α] (U : Set α) : Set {g : G | ∀ x : α, g • x = x ∨ x ∈ U} #align rigid_stabilizer' Rubin.rigidStabilizer' --- A subgroup of G for which `Support α g ⊆ U`, or in other words, all elements of `G` that don't move points outside of `U`. +/-- +A "rigid stabilizer" is a subgroup of `G` associated with a set `U` for which `Support α g ⊆ U` is true for all of its elements. + +In other words, a rigid stabilizer for a set `U` contains all elements of `G` that don't move points outside of `U`. + +The notation for this subgroup is `G•[U]`. +You might sometimes find an expression written as `↑G•[U]` when `G•[U]` is used as a set. +--/ def RigidStabilizer (G : Type _) [Group G] [MulAction G α] (U : Set α) : Subgroup G where carrier := {g : G | ∀ (x) (_ : x ∉ U), g • x = x} @@ -20,6 +27,8 @@ def RigidStabilizer (G : Type _) [Group G] [MulAction G α] (U : Set α) : Subgr one_mem' x _ := one_smul G x #align rigid_stabilizer Rubin.RigidStabilizer +notation:max G "•[" U "]" => RigidStabilizer G U + variable {G α: Type _} variable [Group G] variable [MulAction G α] @@ -50,7 +59,7 @@ by theorem monotone_rigidStabilizer : Monotone (RigidStabilizer (α := α) G) := fun _ _ => rigidStabilizer_mono theorem rigidStabilizer_compl [FaithfulSMul G α] {U : Set α} {f : G} (f_ne_one : f ≠ 1) : - f ∈ RigidStabilizer G (Uᶜ) → f ∉ RigidStabilizer G U := + f ∈ G•[Uᶜ] → f ∉ G•[U] := by intro f_in_rist_compl intro f_in_rist @@ -60,16 +69,6 @@ by have supp_empty : Support α f = ∅ := empty_of_subset_disjoint f_in_rist_compl.symm f_in_rist exact f_ne_one ((support_empty_iff f).mp supp_empty) --- TODO: remove? -theorem rigidStabilizer_to_subgroup_closure {U : Set α} : - RigidStabilizer G U = Subgroup.closure { h : G | Support α h ⊆ U } := -by - ext g - simp only [<-rigidStabilizer_support] - have set_eq : {h | h ∈ RigidStabilizer G U} = (RigidStabilizer G U : Set G) := rfl - rw [set_eq] - rw [Subgroup.closure_eq] - theorem commute_if_rigidStabilizer_and_disjoint {g h : G} {U : Set α} [FaithfulSMul G α] : g ∈ RigidStabilizer G U → Disjoint U (Support α h) → Commute g h := by @@ -129,7 +128,7 @@ by } theorem rigidStabilizer_inter (U V : Set α) : - RigidStabilizer G (U ∩ V) = RigidStabilizer G U ⊓ RigidStabilizer G V := + G•[U ∩ V] = G•[U] ⊓ G•[V] := by ext x simp @@ -137,7 +136,7 @@ by rw [Set.subset_inter_iff] theorem rigidStabilizer_empty (G α: Type _) [Group G] [MulAction G α] [FaithfulSMul G α]: - RigidStabilizer G (α := α) ∅ = ⊥ := + G•[(∅ : Set α)] = ⊥ := by rw [Subgroup.eq_bot_iff_forall] intro f f_in_rist @@ -149,7 +148,7 @@ by simp theorem rigidStabilizer_sInter (S : Set (Set α)) : - RigidStabilizer G (⋂₀ S) = ⨅ T ∈ S, RigidStabilizer G T := + G•[⋂₀ S] = ⨅ T ∈ S, G•[T] := by ext x rw [rigidStabilizer_support] @@ -172,7 +171,7 @@ by exact x_in_rist T_in_S theorem rigidStabilizer_smulImage (f g : G) (S : Set α) : - g ∈ RigidStabilizer G (f •'' S) ↔ f⁻¹ * g * f ∈ RigidStabilizer G S := + g ∈ G•[f •'' S] ↔ f⁻¹ * g * f ∈ G•[S] := by repeat rw [rigidStabilizer_support] nth_rw 3 [<-inv_inv f] @@ -181,7 +180,7 @@ by simp theorem orbit_rigidStabilizer_subset {p : α} {U : Set α} (p_in_U : p ∈ U): - MulAction.orbit (RigidStabilizer G U) p ⊆ U := + MulAction.orbit G•[U] p ⊆ U := by intro q q_in_orbit have ⟨⟨h, h_in_rist⟩, hp_eq_q⟩ := MulAction.mem_orbit_iff.mp q_in_orbit diff --git a/Rubin/Topology.lean b/Rubin/Topology.lean index 59b8561..fdd90c9 100644 --- a/Rubin/Topology.lean +++ b/Rubin/Topology.lean @@ -69,6 +69,36 @@ theorem equivariant_inv [MulAction G α] [MulAction G β] open Topology +-- Note: this sounds like a general enough theorem that it should already be in mathlib +lemma inter_of_open_subset_of_closure {α : Type _} [TopologicalSpace α] {U V : Set α} + (U_open : IsOpen U) (U_nonempty : Set.Nonempty U) (V_nonempty : Set.Nonempty V) + (U_ss_clV : U ⊆ closure V) : Set.Nonempty (U ∩ V) := +by + by_contra empty + rw [Set.not_nonempty_iff_eq_empty] at empty + rw [Set.nonempty_iff_ne_empty] at U_nonempty + apply U_nonempty + + have clV_diff_U_ss_V : V ⊆ closure V \ U := by + rw [Set.subset_diff] + constructor + exact subset_closure + symm + rw [Set.disjoint_iff_inter_eq_empty] + exact empty + have clV_diff_U_closed : IsClosed (closure V \ U) := by + apply IsClosed.sdiff + exact isClosed_closure + assumption + unfold closure at U_ss_clV + simp at U_ss_clV + specialize U_ss_clV (closure V \ U) clV_diff_U_closed clV_diff_U_ss_V + + rw [Set.subset_diff] at U_ss_clV + rw [Set.disjoint_iff_inter_eq_empty] at U_ss_clV + simp at U_ss_clV + exact U_ss_clV.right + /-- Note: `𝓝[≠] x` is notation for `nhdsWithin x {[x]}ᶜ`, ie. the neighborhood of x not containing itself. --/