From 4d8a4d0f1a902222166cc7224b117bc355004164 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Sun, 26 Nov 2023 02:42:35 +0100 Subject: [PATCH] :sparkles: Transition over RegularSupport --- Rubin.lean | 85 +++------------- Rubin/AlgebraicDisjointness.lean | 25 +++-- Rubin/FaithfulAction.lean | 2 +- Rubin/OrbitClosure.lean | 12 --- Rubin/RegularSupport.lean | 169 +++++++++++++++++++++++++++++++ Rubin/RigidStabilizer.lean | 40 ++++++-- Rubin/Topological.lean | 8 +- 7 files changed, 231 insertions(+), 110 deletions(-) delete mode 100644 Rubin/OrbitClosure.lean create mode 100644 Rubin/RegularSupport.lean diff --git a/Rubin.lean b/Rubin.lean index 023f4d4..e924cec 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -24,6 +24,7 @@ import Rubin.Topological import Rubin.RigidStabilizer import Rubin.Period import Rubin.AlgebraicDisjointness +import Rubin.RegularSupport #align_import rubin @@ -63,82 +64,20 @@ where end RubinActions ----------------------------------------------------------------- -section Rubin.RegularSupport.RegularSupport - -variable [TopologicalSpace α] [Rubin.ContinuousMulAction G α] - -def RegularSupport.InteriorClosure (U : Set α) := - interior (closure U) -#align interior_closure Rubin.RegularSupport.InteriorClosure - -theorem RegularSupport.is_open_interiorClosure (U : Set α) : - IsOpen (Rubin.RegularSupport.InteriorClosure U) := - isOpen_interior -#align is_open_interior_closure Rubin.RegularSupport.is_open_interiorClosure +section proposition_2_1 -theorem RegularSupport.interiorClosure_mono {U V : Set α} : - U ⊆ V → Rubin.RegularSupport.InteriorClosure U ⊆ Rubin.RegularSupport.InteriorClosure V := - interior_mono ∘ closure_mono -#align interior_closure_mono Rubin.RegularSupport.interiorClosure_mono +variable {G α : Type _} +variable [Group G] +variable [MulAction G α] +variable [TopologicalSpace α] +variable [T2Space α] -def is_regular_open (U : Set α) := - Rubin.RegularSupport.InteriorClosure U = U -#align set.is_regular_open Rubin.is_regular_open +lemma proposition_2_1 (f : G) : + Set.centralizer { g^12 | (g : G) (_ : AlgebraicallyDisjoint f g) } = RigidStabilizer G (RegularSupport α f) := +by + sorry -theorem is_regular_def (U : Set α) : - is_regular_open U ↔ Rubin.RegularSupport.InteriorClosure U = U := by rfl -#align set.is_regular_def Rubin.is_regular_def - -theorem RegularSupport.IsOpen.in_closure {U : Set α} : IsOpen U → U ⊆ interior (closure U) := - by - intro U_open x x_in_U - apply interior_mono subset_closure - rw [U_open.interior_eq] - exact x_in_U -#align is_open.in_closure Rubin.RegularSupport.IsOpen.in_closure - -theorem RegularSupport.IsOpen.interiorClosure_subset {U : Set α} : - IsOpen U → U ⊆ Rubin.RegularSupport.InteriorClosure U := fun h => - (subset_interior_iff_isOpen.mpr h).trans (interior_mono subset_closure) -#align is_open.interior_closure_subset Rubin.RegularSupport.IsOpen.interiorClosure_subset - -theorem RegularSupport.regular_interior_closure (U : Set α) : - is_regular_open (Rubin.RegularSupport.InteriorClosure U) := - by - rw [is_regular_def] - apply Set.Subset.antisymm - exact interior_mono ((closure_mono interior_subset).trans (subset_of_eq closure_closure)) - exact (subset_of_eq interior_interior.symm).trans (interior_mono subset_closure) -#align regular_interior_closure Rubin.RegularSupport.regular_interior_closure - -def RegularSupport.RegularSupport (α : Type _) [TopologicalSpace α] [MulAction G α] (g : G) := - Rubin.RegularSupport.InteriorClosure (Support α g) -#align regular_support Rubin.RegularSupport.RegularSupport - -theorem RegularSupport.regularSupport_regular {g : G} : - is_regular_open (Rubin.RegularSupport.RegularSupport α g) := - Rubin.RegularSupport.regular_interior_closure _ -#align regular_regular_support Rubin.RegularSupport.regularSupport_regular - -theorem RegularSupport.support_subset_regularSupport [T2Space α] (g : G) : - Support α g ⊆ Rubin.RegularSupport.RegularSupport α g := - Rubin.RegularSupport.IsOpen.interiorClosure_subset (Rubin.support_open g) -#align support_in_regular_support Rubin.RegularSupport.support_subset_regularSupport - -theorem RegularSupport.mem_regularSupport (g : G) (U : Set α) : - is_regular_open U → g ∈ RigidStabilizer G U → Rubin.RegularSupport.RegularSupport α g ⊆ U := - fun U_ro g_moves => - (is_regular_def _).mp U_ro ▸ - Rubin.RegularSupport.interiorClosure_mono (rist_supported_in_set g_moves) -#align mem_regular_support Rubin.RegularSupport.mem_regularSupport - --- FIXME: Weird naming? -def RegularSupport.AlgebraicCentralizer (f : G) : Set G := - {h | ∃ g, h = g ^ 12 ∧ AlgebraicallyDisjoint f g} -#align algebraic_centralizer Rubin.RegularSupport.AlgebraicCentralizer - -end Rubin.RegularSupport.RegularSupport +end proposition_2_1 -- ---------------------------------------------------------------- -- section finite_exponent diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean index b36ff71..5f73116 100644 --- a/Rubin/AlgebraicDisjointness.lean +++ b/Rubin/AlgebraicDisjointness.lean @@ -88,6 +88,10 @@ fun (h : G) (nc : ¬Commute f h) => { exact (mk_thm h nc).choose_spec.choose_spec.right.right.right } +-- This is an idea of having a Prop version of AlgebraicallyDisjoint, but it sounds painful to work with +-- def IsAlgebraicallyDisjoint {G : Type _} [Group G] (f g : G): Prop := +-- ∀ (h : G), ¬Commute f h → ∃ (f₁ f₂ : G), ∃ (elem : AlgebraicallyDisjointElem f g h), elem.fst = f₁ ∧ elem.snd = f₂ + @[simp] theorem orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) : MulAction.orbit (⊥ : Subgroup G) p = {p} := @@ -190,6 +194,7 @@ by <;> simp only [h, true_or, or_true] · rintro ((h|h)|(h|h)) <;> exact ⟨_, h⟩ +-- TODO: move to Rubin.lean -- TODO: modify the proof to be less "let everything"-y, especially the first half -- TODO: use the new class thingy to write a cleaner proof? lemma proposition_1_1_1 [h_lm : LocallyMoving G α] [T2Space α] (f g : G) (supp_disjoint : Disjoint (Support α f) (Support α g)) : AlgebraicallyDisjoint f g := by @@ -208,7 +213,7 @@ lemma proposition_1_1_1 [h_lm : LocallyMoving G α] [T2Space α] (f g : G) (supp -- Re-use the Hausdoff property of α again, this time yielding W ⊆ V let ⟨y, y_moved⟩ := faithful_moves_point' α f₂_ne_one - have y_in_V := (rist_supported_in_set f₂_in_rist_V) (mem_support.mpr y_moved) + have y_in_V := (rigidStabilizer_support.mp f₂_in_rist_V) (mem_support.mpr y_moved) let ⟨W, W_open, y_in_W, W_in_V, disjoint_img_W⟩ := disjoint_nbhd_in V_open y_in_V y_moved -- Let f₁ be a nontrivial element of RigidStabilizer G W @@ -220,13 +225,13 @@ lemma proposition_1_1_1 [h_lm : LocallyMoving G α] [T2Space α] (f g : G) (supp · apply disjoint_commute (α := α) apply Set.disjoint_of_subset_left _ supp_disjoint calc - Support α f₁ ⊆ W := rist_supported_in_set f₁_in_rist_W + Support α f₁ ⊆ W := rigidStabilizer_support.mp f₁_in_rist_W W ⊆ V := W_in_V V ⊆ Support α f := V_in_support · apply disjoint_commute (α := α) apply Set.disjoint_of_subset_left _ supp_disjoint calc - Support α f₂ ⊆ V := rist_supported_in_set f₂_in_rist_V + Support α f₂ ⊆ V := rigidStabilizer_support.mp f₂_in_rist_V V ⊆ Support α f := V_in_support -- We claim that [f₁, [f₂, h]] is a nontrivial elelement of Centralizer G g @@ -237,14 +242,14 @@ lemma proposition_1_1_1 [h_lm : LocallyMoving G α] [T2Space α] (f g : G) (supp symm apply disjoint_support_comm f₂ h _ disjoint_img_V · exact W_in_V z_in_W - · exact rist_supported_in_set f₂_in_rist_V + · exact rigidStabilizer_support.mp f₂_in_rist_V constructor · -- then `k*f₁⁻¹*k⁻¹` is supported on k W = f₂ W, -- so [f₁,k] is supported on W ∪ f₂ W ⊆ V ⊆ support f, so commutes with g. apply disjoint_commute (α := α) apply Set.disjoint_of_subset_left _ supp_disjoint - have supp_f₁_subset_W := (rist_supported_in_set f₁_in_rist_W) + have supp_f₁_subset_W := (rigidStabilizer_support.mp f₁_in_rist_W) show Support α ⁅f₁, ⁅f₂, h⁆⁆ ⊆ Support α f calc @@ -259,14 +264,14 @@ lemma proposition_1_1_1 [h_lm : LocallyMoving G α] [T2Space α] (f g : G) (supp _ ⊆ V ∪ V := by apply Set.union_subset_union_right apply smulImage_subset_in_support f₂ W V W_in_V - exact rist_supported_in_set f₂_in_rist_V + exact rigidStabilizer_support.mp f₂_in_rist_V _ ⊆ V := by rw [Set.union_self] _ ⊆ Support α f := V_in_support · -- finally, [f₁,k] agrees with f₁ on W, so is not the identity. have h₄: ∀ z ∈ W, ⁅f₁, k⁆ • z = f₁ • z := by apply disjoint_support_comm f₁ k - exact rist_supported_in_set f₁_in_rist_W + exact rigidStabilizer_support.mp f₁_in_rist_W rw [<-smulImage_eq_of_smul_eq h₂] exact disjoint_img_W let ⟨z, z_in_W, z_moved⟩ := faithful_rigid_stabilizer_moves_point f₁_in_rist_W f₁_ne_one @@ -522,7 +527,7 @@ by symm apply disjoint_support_comm h f - · exact rist_supported_in_set h_in_ristV + · exact rigidStabilizer_support.mp h_in_ristV · exact V_disjoint_smulImage · exact z_in_V @@ -541,11 +546,11 @@ by Support α ⁅f₂, h⁆ ⊆ Support α h ∪ (f₂ •'' Support α h) := support_comm α f₂ h _ ⊆ V ∪ (f₂ •'' Support α h) := by apply Set.union_subset_union_left - exact rist_supported_in_set h_in_ristV + exact rigidStabilizer_support.mp h_in_ristV _ ⊆ V ∪ (f₂ •'' V) := by apply Set.union_subset_union_right apply smulImage_subset - exact rist_supported_in_set h_in_ristV + exact rigidStabilizer_support.mp h_in_ristV have support_h' : Support α h' ⊆ ⋃(i : Fin 2 × Fin 2), (f₁^(i.1.val) * f₂^(i.2.val)) •'' V := by rw [rewrite_Union] simp (config := {zeta := false}) diff --git a/Rubin/FaithfulAction.lean b/Rubin/FaithfulAction.lean index 3bc5782..d4ca12e 100644 --- a/Rubin/FaithfulAction.lean +++ b/Rubin/FaithfulAction.lean @@ -29,7 +29,7 @@ theorem faithful_rigid_stabilizer_moves_point {g : G} {U : Set α} : by intro g_rigid g_ne_one let ⟨x, xmoved⟩ := Rubin.faithful_moves_point' α g_ne_one - exact ⟨x, rist_supported_in_set g_rigid xmoved, xmoved⟩ + exact ⟨x, rigidStabilizer_support.mp g_rigid xmoved, xmoved⟩ #align faithful_rist_moves_point Rubin.faithful_rigid_stabilizer_moves_point theorem ne_one_support_nonempty {g : G} : g ≠ 1 → (Support α g).Nonempty := diff --git a/Rubin/OrbitClosure.lean b/Rubin/OrbitClosure.lean deleted file mode 100644 index f39d984..0000000 --- a/Rubin/OrbitClosure.lean +++ /dev/null @@ -1,12 +0,0 @@ -import Mathlib.GroupTheory.GroupAction.Basic -import Mathlib.GroupTheory.Subgroup.Basic -import Mathlib.Data.Finset.Basic - -import Rubin.Support - -namespace Rubin - -def OrbitClosure {G α : Type _} [Group G] [MulAction G α] (U : Set α) := - { g : G | Support α g ⊆ U} - -end Rubin diff --git a/Rubin/RegularSupport.lean b/Rubin/RegularSupport.lean new file mode 100644 index 0000000..2bc4dbf --- /dev/null +++ b/Rubin/RegularSupport.lean @@ -0,0 +1,169 @@ +import Mathlib.Data.Finset.Basic +import Mathlib.GroupTheory.Commutator +import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.Topology.Basic +import Mathlib.Topology.Separation + +import Rubin.Tactic +import Rubin.Support +import Rubin.Topological + +namespace Rubin + +section InteriorClosure + +variable {α : Type _} +variable [TopologicalSpace α] + +-- Defines a kind of "regularization" transformation made to sets, +-- by calling `closure` followed by `interior` on it. +-- +-- A set is then said to be regular if the InteriorClosure does not modify it. +def InteriorClosure (U : Set α) : Set α := + interior (closure U) +#align interior_closure Rubin.InteriorClosure + +@[simp] +theorem InteriorClosure.def (U : Set α) : InteriorClosure U = interior (closure U) := + by simp [InteriorClosure] + +@[simp] +theorem InteriorClosure.fdef : InteriorClosure = (interior ∘ (closure (α := α))) := by ext; simp + +def Regular (U : Set α) : Prop := + InteriorClosure U = U + +@[simp] +theorem Regular.def (U : Set α) : Regular U ↔ interior (closure U) = U := + by simp [Regular] +#align set.is_regular_def Rubin.Regular.def + +theorem interiorClosure_open (U : Set α) : IsOpen (InteriorClosure U) := by simp +#align is_open_interior_closure Rubin.interiorClosure_open + +theorem interiorClosure_subset {U : Set α} : + IsOpen U → U ⊆ InteriorClosure U := +by + intro h + apply subset_trans + exact subset_interior_iff_isOpen.mpr h + apply interior_mono + exact subset_closure +#align is_open.interior_closure_subset Rubin.interiorClosure_subset + +theorem interiorClosure_regular (U : Set α) : Regular (InteriorClosure U) := +by + apply Set.eq_of_subset_of_subset <;> unfold InteriorClosure + { + apply interior_mono + nth_rw 2 [<-closure_closure (s := U)] + apply closure_mono + exact interior_subset + } + { + nth_rw 1 [<-interior_interior] + apply interior_mono + exact subset_closure + } +#align regular_interior_closure Rubin.interiorClosure_regular + +theorem interiorClosure_mono (U V : Set α) : + U ⊆ V → InteriorClosure U ⊆ InteriorClosure V +:= interior_mono ∘ closure_mono +#align interior_closure_mono Rubin.interiorClosure_mono + +theorem monotone_interior_closure : Monotone (InteriorClosure (α := α)) +:= fun a b => + interiorClosure_mono a b + +theorem regular_open (U : Set α) : Regular U → IsOpen U := +by + intro h_reg + rw [<-h_reg] + simp + +theorem regular_interior (U : Set α) : Regular U → interior U = U := +by + intro h_reg + rw [<-h_reg] + simp + +end InteriorClosure + +section RegularSupport_def + +variable {G : Type _} +variable (α : Type _) +variable [Group G] +variable [MulAction G α] +variable [TopologicalSpace α] + +-- The "regular support" is the `Support` of `g : G` in `α` (aka the elements in `α` which are moved by `g`), +-- transformed with the interior closure. +def RegularSupport (g: G) : Set α := + InteriorClosure (Support α g) +#align regular_support Rubin.RegularSupport + +@[simp] +theorem RegularSupport.def {G : Type _} (α : Type _) + [Group G] [MulAction G α] [TopologicalSpace α] + (g: G) : RegularSupport α g = interior (closure (Support α g)) := +by + simp [RegularSupport] + +theorem regularSupport_open [MulAction G α] (g : G) : IsOpen (RegularSupport α g) := by + unfold RegularSupport + simp + +theorem regularSupport_regular [MulAction G α] (g : G) : Regular (RegularSupport α g) := by + apply interiorClosure_regular +#align regular_regular_support Rubin.regularSupport_regular + +end RegularSupport_def + +section RegularSupport_continuous + +variable {G α : Type _} +variable [Group G] +variable [TopologicalSpace α] +variable [ContinuousMulAction G α] + +theorem support_subset_regularSupport [T2Space α] {g : G} : + Support α g ⊆ RegularSupport α g := +by + apply interiorClosure_subset + apply support_open (α := α) (g := g) +#align support_in_regular_support Rubin.support_subset_regularSupport + +theorem regularSupport_subset {g : G} {U : Set α} : + Regular U → Support α g ⊆ U → RegularSupport α g ⊆ U := +by + intro U_reg h + rw [<-U_reg] + apply interiorClosure_mono + exact h + +theorem regularSupport_subset_of_rigidStabilizer {g : G} {U : Set α} (U_reg : Regular U) : + g ∈ RigidStabilizer G U → RegularSupport α g ⊆ U := +by + intro g_in_rist + apply regularSupport_subset + · assumption + · apply rigidStabilizer_support.mp + assumption + +theorem regularSupport_subset_iff_rigidStabilizer [T2Space α] {g : G} {U : Set α} (U_reg : Regular U) : + g ∈ RigidStabilizer G U ↔ RegularSupport α g ⊆ U := +by + constructor + · apply regularSupport_subset_of_rigidStabilizer U_reg + · intro rs_subset + rw [rigidStabilizer_support] + apply subset_trans + apply support_subset_regularSupport + exact rs_subset +#align mem_regular_support Rubin.regularSupport_subset_of_rigidStabilizer + +end RegularSupport_continuous + +end Rubin diff --git a/Rubin/RigidStabilizer.lean b/Rubin/RigidStabilizer.lean index 9e1748b..4277f7b 100644 --- a/Rubin/RigidStabilizer.lean +++ b/Rubin/RigidStabilizer.lean @@ -10,6 +10,7 @@ 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`. def RigidStabilizer (G : Type _) [Group G] [MulAction G α] (U : Set α) : Subgroup G where carrier := {g : G | ∀ (x) (_ : x ∉ U), g • x = x} @@ -22,17 +23,40 @@ variable {G α: Type _} variable [Group G] variable [MulAction G α] -theorem rist_supported_in_set {g : G} {U : Set α} : - g ∈ RigidStabilizer G U → Support α g ⊆ U := fun h x x_in_support => - by_contradiction (x_in_support ∘ h x) -#align rist_supported_in_set Rubin.rist_supported_in_set - -theorem rist_ss_rist {U V : Set α} (V_ss_U : V ⊆ U) : - (RigidStabilizer G V : Set G) ⊆ (RigidStabilizer G U : Set G) := +theorem rigidStabilizer_support {g : G} {U : Set α} : + g ∈ RigidStabilizer G U ↔ Support α g ⊆ U := +⟨ + fun h x x_in_support => + by_contradiction (x_in_support ∘ h x), by + intro support_sub + rw [<-Subgroup.mem_carrier] + unfold RigidStabilizer; simp + intro x x_notin_U + by_contra h + exact x_notin_U (support_sub h) +⟩ +#align rist_supported_in_set Rubin.rigidStabilizer_support + +theorem rigidStabilizer_mono {U V : Set α} (V_ss_U : V ⊆ U) : + (RigidStabilizer G V : Set G) ⊆ (RigidStabilizer G U : Set G) := +by intro g g_in_ristV x x_notin_U have x_notin_V : x ∉ V := by intro x_in_V; exact x_notin_U (V_ss_U x_in_V) exact g_in_ristV x x_notin_V -#align rist_ss_rist Rubin.rist_ss_rist +#align rist_ss_rist Rubin.rigidStabilizer_mono + +theorem monotone_rigidStabilizer : Monotone (RigidStabilizer (α := α) G) := fun _ _ => rigidStabilizer_mono + +theorem rigidStabilizer_to_subgroup_closure {g : G} {U : Set α} : + g ∈ RigidStabilizer G U → g ∈ Subgroup.closure { g : G | Support α g ⊆ U } := +by + rw [rigidStabilizer_support] + intro h + rw [Subgroup.mem_closure] + intro V orbit_subset_V + apply orbit_subset_V + simp + exact h end Rubin diff --git a/Rubin/Topological.lean b/Rubin/Topological.lean index c753d12..1cf63b2 100644 --- a/Rubin/Topological.lean +++ b/Rubin/Topological.lean @@ -12,6 +12,7 @@ namespace Rubin section Continuity +-- TODO: don't have this extend MulAction class ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] extends MulAction G α where continuous : ∀ g : G, Continuous (fun x: α => g • x) @@ -92,18 +93,13 @@ class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] extends MulAc p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) #align is_locally_dense Rubin.LocallyDense -namespace LocallyDense - -lemma nonEmpty {G α : Type _} [Group G] [TopologicalSpace α] [LocallyDense G α]: +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 Other end Rubin