From 9e6258bf5c362690113f4aeea6b5677e61b823d0 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Fri, 8 Dec 2023 14:37:12 +0100 Subject: [PATCH] :truck: Rename AssociatedPoset to RegularSupportBasis --- Rubin.lean | 97 +--------------- Rubin/HomeoGroup.lean | 264 +++++++++++++++++++++++++++++------------- 2 files changed, 190 insertions(+), 171 deletions(-) diff --git a/Rubin.lean b/Rubin.lean index 8f794dc..0fd1a8d 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -707,108 +707,21 @@ section HomeoGroup open Topology --- 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 ∧ RegularSupport α g ⊆ closure W := -by - have U_in_nhds : U ∈ 𝓝 p := by - rw [mem_nhds_iff] - use U - - let ⟨W', W'_in_nhds, W'_ss_U, W'_compact⟩ := local_compact_nhds U_in_nhds - - -- This feels like black magic, but okay - let ⟨W, _W_compact, W_closed, W'_ss_int_W, W_ss_U⟩ := exists_compact_closed_between W'_compact U_open W'_ss_U - have W_cl_eq_W : closure W = W := IsClosed.closure_eq W_closed - - have W_in_nhds : W ∈ 𝓝 p := by - rw [mem_nhds_iff] - use interior W - repeat' apply And.intro - · exact interior_subset - · simp - · exact W'_ss_int_W (mem_of_mem_nhds W'_in_nhds) - - use W - - repeat' apply And.intro - exact W_in_nhds - { - rw [W_cl_eq_W] - exact W_ss_U - } - - 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 isOpen_interior p_in_int_W - - use g - 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 - apply TopologicalSpace.isTopologicalBasis_of_isOpen_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 - --- TODO: implement Membership on AssociatedPoset +-- TODO: implement Membership on RegularSupportBasis -- TODO: wrap these things in some neat structures theorem proposition_3_5 {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α] [hc : ContinuousMulAction G α] - (U : AssociatedPoset α) (F: Filter α): - (∃ p ∈ U.val, F.HasBasis (fun S: Set α => S ∈ AssociatedPoset.asSet α ∧ p ∈ S) id) - ↔ ∃ V : AssociatedPoset α, V ≤ U ∧ {W : AssociatedPoset α | W ≤ V} ⊆ { g •'' W | (g ∈ RigidStabilizer G U.val) (W ∈ F) } + (U : RegularSupportBasis α) (F: Filter α): + (∃ p ∈ U.val, F.HasBasis (fun S: Set α => S ∈ RegularSupportBasis.asSet α ∧ p ∈ S) id) + ↔ ∃ V : RegularSupportBasis α, V ≤ U ∧ {W : RegularSupportBasis α | W ≤ V} ⊆ { g •'' W | (g ∈ RigidStabilizer G U.val) (W ∈ F) (_: W ∈ RegularSupportBasis.asSet α) } := by constructor { simp intro p p_in_U filter_basis - have assoc_poset_basis : TopologicalSpace.IsTopologicalBasis (AssociatedPoset.asSet α) := by - exact proposition_3_2 (G := G) + have assoc_poset_basis := RegularSupportBasis.isBasis G α have F_eq_nhds : F = 𝓝 p := by have nhds_basis := assoc_poset_basis.nhds_hasBasis (a := p) rw [<-filter_basis.filter_eq] diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean index de798d3..357ea39 100644 --- a/Rubin/HomeoGroup.lean +++ b/Rubin/HomeoGroup.lean @@ -7,8 +7,7 @@ import Rubin.Topology import Rubin.Support import Rubin.RegularSupport -structure HomeoGroup (α : Type _) [TopologicalSpace α] extends - Homeomorph α α +structure HomeoGroup (α : Type _) [TopologicalSpace α] extends Homeomorph α α variable {α : Type _} variable [TopologicalSpace α] @@ -156,7 +155,7 @@ theorem HomeoGroup.smulImage_eq_image (g : HomeoGroup α) (S : Set α) : namespace Rubin -section AssociatedPoset.Prelude +section RegularSupportBasis.Prelude variable {α : Type _} variable [TopologicalSpace α] @@ -165,33 +164,39 @@ variable [DecidableEq α] /-- Maps a "seed" of homeorphisms in α to the intersection of their regular support in α. -Note that the condition that the resulting set is non-empty is introduced later in `AssociatedPosetSeed` +Note that the condition that the resulting set is non-empty is introduced later in `RegularSupportBasis₀` --/ -def AssociatedPosetElem (S : Finset (HomeoGroup α)): Set α := - ⋂₀ ((fun (g : HomeoGroup α) => RegularSupport α g) '' S) +def RegularSupportInter₀ (S : Finset (HomeoGroup α)): Set α := + ⋂ (g ∈ S), RegularSupport α g + +theorem RegularSupportInter₀.eq_sInter (S : Finset (HomeoGroup α)) : + RegularSupportInter₀ S = ⋂₀ ((fun (g : HomeoGroup α) => RegularSupport α g) '' S) := +by + rw [Set.sInter_image] + rfl /-- -This is a predecessor type to `AssociatedPoset`, where equality is defined on the `seed` used, rather than the `val`. +This is a predecessor type to `RegularSupportBasis`, where equality is defined on the `seed` used, rather than the `val`. --/ -structure AssociatedPosetSeed (α : Type _) [TopologicalSpace α] where +structure RegularSupportBasis₀ (α : Type _) [TopologicalSpace α] where seed : Finset (HomeoGroup α) - val_nonempty : Set.Nonempty (AssociatedPosetElem seed) + val_nonempty : Set.Nonempty (RegularSupportInter₀ seed) -theorem AssociatedPosetSeed.eq_iff_seed_eq (S T : AssociatedPosetSeed α) : S = T ↔ S.seed = T.seed := by +theorem RegularSupportBasis₀.eq_iff_seed_eq (S T : RegularSupportBasis₀ α) : S = T ↔ S.seed = T.seed := by -- Spooky :3c rw [mk.injEq] -def AssociatedPosetSeed.val (S : AssociatedPosetSeed α) : Set α := AssociatedPosetElem S.seed +def RegularSupportBasis₀.val (S : RegularSupportBasis₀ α) : Set α := RegularSupportInter₀ S.seed -theorem AssociatedPosetSeed.val_def (S : AssociatedPosetSeed α) : S.val = AssociatedPosetElem S.seed := rfl +theorem RegularSupportBasis₀.val_def (S : RegularSupportBasis₀ α) : S.val = RegularSupportInter₀ S.seed := rfl @[simp] -theorem AssociatedPosetSeed.nonempty (S : AssociatedPosetSeed α) : Set.Nonempty S.val := S.val_nonempty +theorem RegularSupportBasis₀.nonempty (S : RegularSupportBasis₀ α) : Set.Nonempty S.val := S.val_nonempty @[simp] -theorem AssociatedPosetSeed.regular (S : AssociatedPosetSeed α) : Regular S.val := by +theorem RegularSupportBasis₀.regular (S : RegularSupportBasis₀ α) : Regular S.val := by rw [S.val_def] - unfold AssociatedPosetElem + rw [RegularSupportInter₀.eq_sInter] apply regular_sInter · have set_decidable : DecidableEq (Set α) := Classical.typeDecidableEq (Set α) @@ -205,10 +210,10 @@ theorem AssociatedPosetSeed.regular (S : AssociatedPosetSeed α) : Regular S.val rw [<-Heq] exact regularSupport_regular α g -lemma AssociatedPosetElem.mul_seed (seed : Finset (HomeoGroup α)) [DecidableEq (HomeoGroup α)] (f : HomeoGroup α): - AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' AssociatedPosetElem seed := +lemma RegularSupportInter₀.mul_seed (seed : Finset (HomeoGroup α)) [DecidableEq (HomeoGroup α)] (f : HomeoGroup α): + RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' RegularSupportInter₀ seed := by - unfold AssociatedPosetElem + unfold RegularSupportInter₀ simp conv => { rhs @@ -220,110 +225,110 @@ by variable [DecidableEq (HomeoGroup α)] /-- -A `HomeoGroup α` group element `f` acts on an `AssociatedPosetSeed α` set `S`, +A `HomeoGroup α` group element `f` acts on an `RegularSupportBasis₀ α` set `S`, by mapping each element `g` of `S.seed` to `f * g * f⁻¹` --/ -instance homeoGroup_smul₂ : SMul (HomeoGroup α) (AssociatedPosetSeed α) where +instance homeoGroup_smul₂ : SMul (HomeoGroup α) (RegularSupportBasis₀ α) where smul := fun f S => ⟨ (Finset.image (fun g => f * g * f⁻¹) S.seed), by - rw [AssociatedPosetElem.mul_seed] + rw [RegularSupportInter₀.mul_seed] simp exact S.val_nonempty ⟩ -theorem AssociatedPosetSeed.smul_seed (f : HomeoGroup α) (S : AssociatedPosetSeed α) : +theorem RegularSupportBasis₀.smul_seed (f : HomeoGroup α) (S : RegularSupportBasis₀ α) : (f • S).seed = (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl -theorem AssociatedPosetSeed.smul_val (f : HomeoGroup α) (S : AssociatedPosetSeed α) : - (f • S).val = AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl +theorem RegularSupportBasis₀.smul_val (f : HomeoGroup α) (S : RegularSupportBasis₀ α) : + (f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl -theorem AssociatedPosetSeed.smul_val' (f : HomeoGroup α) (S : AssociatedPosetSeed α) : +theorem RegularSupportBasis₀.smul_val' (f : HomeoGroup α) (S : RegularSupportBasis₀ α) : (f • S).val = f •'' S.val := by unfold val - rw [<-AssociatedPosetElem.mul_seed] - rw [AssociatedPosetSeed.smul_seed] + rw [<-RegularSupportInter₀.mul_seed] + rw [RegularSupportBasis₀.smul_seed] --- We define a "preliminary" group action from `HomeoGroup α` to `AssociatedPosetSeed` -instance homeoGroup_mulAction₂ : MulAction (HomeoGroup α) (AssociatedPosetSeed α) where +-- We define a "preliminary" group action from `HomeoGroup α` to `RegularSupportBasis₀` +instance homeoGroup_mulAction₂ : MulAction (HomeoGroup α) (RegularSupportBasis₀ α) where one_smul := by intro S - rw [AssociatedPosetSeed.eq_iff_seed_eq] - rw [AssociatedPosetSeed.smul_seed] + rw [RegularSupportBasis₀.eq_iff_seed_eq] + rw [RegularSupportBasis₀.smul_seed] simp mul_smul := by intro f g S - rw [AssociatedPosetSeed.eq_iff_seed_eq] - repeat rw [AssociatedPosetSeed.smul_seed] + rw [RegularSupportBasis₀.eq_iff_seed_eq] + repeat rw [RegularSupportBasis₀.smul_seed] rw [Finset.image_image] ext x simp group -end AssociatedPoset.Prelude +end RegularSupportBasis.Prelude /-- A partially-ordered set, associated to Rubin's proof. Any element in that set is made up of a `seed`, -such that `val = AssociatedPosetElem seed` and `Set.Nonempty val`. +such that `val = RegularSupportInter₀ seed` and `Set.Nonempty val`. -Actions on this set are first defined in terms of `AssociatedPosetSeed`, +Actions on this set are first defined in terms of `RegularSupportBasis₀`, as the proofs otherwise get hairy with a bunch of `Exists.choose` appearing. --/ -structure AssociatedPoset (α : Type _) [TopologicalSpace α] where +structure RegularSupportBasis (α : Type _) [TopologicalSpace α] where val : Set α - val_has_seed : ∃ po_seed : AssociatedPosetSeed α, po_seed.val = val + val_has_seed : ∃ po_seed : RegularSupportBasis₀ α, po_seed.val = val -namespace AssociatedPoset +namespace RegularSupportBasis variable {α : Type _} variable [TopologicalSpace α] variable [DecidableEq α] -theorem eq_iff_val_eq (S T : AssociatedPoset α) : S = T ↔ S.val = T.val := by +theorem eq_iff_val_eq (S T : RegularSupportBasis α) : S = T ↔ S.val = T.val := by rw [mk.injEq] -def fromSeed (seed : AssociatedPosetSeed α) : AssociatedPoset α := ⟨ +def fromSeed (seed : RegularSupportBasis₀ α) : RegularSupportBasis α := ⟨ seed.val, ⟨seed, seed.val_def⟩ ⟩ -noncomputable def full_seed (S : AssociatedPoset α) : AssociatedPosetSeed α := +noncomputable def full_seed (S : RegularSupportBasis α) : RegularSupportBasis₀ α := (Exists.choose S.val_has_seed) -noncomputable def seed (S : AssociatedPoset α) : Finset (HomeoGroup α) := +noncomputable def seed (S : RegularSupportBasis α) : Finset (HomeoGroup α) := S.full_seed.seed @[simp] -theorem full_seed_seed (S : AssociatedPoset α) : S.full_seed.seed = S.seed := rfl +theorem full_seed_seed (S : RegularSupportBasis α) : S.full_seed.seed = S.seed := rfl @[simp] -theorem fromSeed_val (seed : AssociatedPosetSeed α) : +theorem fromSeed_val (seed : RegularSupportBasis₀ α) : (fromSeed seed).val = seed.val := by unfold fromSeed simp @[simp] -theorem val_from_seed (S : AssociatedPoset α) : AssociatedPosetElem S.seed = S.val := by +theorem val_from_seed (S : RegularSupportBasis α) : RegularSupportInter₀ S.seed = S.val := by unfold seed full_seed - rw [<-AssociatedPosetSeed.val_def] + rw [<-RegularSupportBasis₀.val_def] rw [Exists.choose_spec S.val_has_seed] @[simp] -theorem val_from_seed₂ (S : AssociatedPoset α) : S.full_seed.val = S.val := by +theorem val_from_seed₂ (S : RegularSupportBasis α) : S.full_seed.val = S.val := by unfold full_seed - rw [AssociatedPosetSeed.val_def] + rw [RegularSupportBasis₀.val_def] nth_rw 2 [<-val_from_seed] unfold seed full_seed rfl --- Allows one to prove properties of AssociatedPoset without jumping through `Exists.choose`-shaped hoops +-- Allows one to prove properties of RegularSupportBasis without jumping through `Exists.choose`-shaped hoops theorem prop_from_val {p : Set α → Prop} - (any_seed : ∀ po_seed : AssociatedPosetSeed α, p po_seed.val) : - ∀ (S : AssociatedPoset α), p S.val := + (any_seed : ∀ po_seed : RegularSupportBasis₀ α, p po_seed.val) : + ∀ (S : RegularSupportBasis α), p S.val := by intro S rw [<-val_from_seed] @@ -333,45 +338,45 @@ by exact res @[simp] -theorem nonempty : ∀ (S : AssociatedPoset α), Set.Nonempty S.val := - prop_from_val AssociatedPosetSeed.nonempty +theorem nonempty : ∀ (S : RegularSupportBasis α), Set.Nonempty S.val := + prop_from_val RegularSupportBasis₀.nonempty @[simp] -theorem regular : ∀ (S : AssociatedPoset α), Regular S.val := - prop_from_val AssociatedPosetSeed.regular +theorem regular : ∀ (S : RegularSupportBasis α), Regular S.val := + prop_from_val RegularSupportBasis₀.regular variable [DecidableEq (HomeoGroup α)] -instance homeoGroup_smul₃ : SMul (HomeoGroup α) (AssociatedPoset α) where +instance homeoGroup_smul₃ : SMul (HomeoGroup α) (RegularSupportBasis α) where smul := fun f S => ⟨ f •'' S.val, by use f • S.full_seed - rw [AssociatedPosetSeed.smul_val'] + rw [RegularSupportBasis₀.smul_val'] simp ⟩ -theorem smul_val (f : HomeoGroup α) (S : AssociatedPoset α) : +theorem smul_val (f : HomeoGroup α) (S : RegularSupportBasis α) : (f • S).val = f •'' S.val := rfl -theorem smul_seed' (f : HomeoGroup α) (S : AssociatedPoset α) (seed : Finset (HomeoGroup α)) : - S.val = AssociatedPosetElem seed → - (f • S).val = AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) seed) := +theorem smul_seed' (f : HomeoGroup α) (S : RegularSupportBasis α) (seed : Finset (HomeoGroup α)) : + S.val = RegularSupportInter₀ seed → + (f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) seed) := by intro S_val_eq rw [smul_val] - rw [AssociatedPosetElem.mul_seed] + rw [RegularSupportInter₀.mul_seed] rw [S_val_eq] -theorem smul_seed (f : HomeoGroup α) (S : AssociatedPoset α) : - (f • S).val = AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) S.seed) := +theorem smul_seed (f : HomeoGroup α) (S : RegularSupportBasis α) : + (f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) S.seed) := by apply smul_seed' symm exact val_from_seed S -- Note: we could potentially implement MulActionHom -instance homeoGroup_mulAction₃ : MulAction (HomeoGroup α) (AssociatedPoset α) where +instance homeoGroup_mulAction₃ : MulAction (HomeoGroup α) (RegularSupportBasis α) where one_smul := by intro S rw [eq_iff_val_eq] @@ -383,14 +388,14 @@ instance homeoGroup_mulAction₃ : MulAction (HomeoGroup α) (AssociatedPoset α repeat rw [smul_val] rw [smulImage_mul] -instance associatedPoset_le : LE (AssociatedPoset α) where +instance associatedPoset_le : LE (RegularSupportBasis α) where le := fun S T => S.val ⊆ T.val -theorem le_def (S T : AssociatedPoset α) : S ≤ T ↔ S.val ⊆ T.val := by +theorem le_def (S T : RegularSupportBasis α) : S ≤ T ↔ S.val ⊆ T.val := by rw [iff_eq_eq] rfl -instance associatedPoset_partialOrder : PartialOrder (AssociatedPoset α) where +instance associatedPoset_partialOrder : PartialOrder (RegularSupportBasis α) where le_refl := fun S => (le_def S S).mpr (le_refl S.val) le_trans := fun S T U S_le_T S_le_U => (le_def S U).mpr (le_trans ((le_def _ _).mp S_le_T) @@ -403,7 +408,7 @@ instance associatedPoset_partialOrder : PartialOrder (AssociatedPoset α) where rw [eq_iff_val_eq] apply le_antisymm <;> assumption -theorem smul_mono {S T : AssociatedPoset α} (f : HomeoGroup α) (S_le_T : S ≤ T) : +theorem smul_mono {S T : RegularSupportBasis α} (f : HomeoGroup α) (S_le_T : S ≤ T) : f • S ≤ f • T := by rw [le_def] @@ -411,23 +416,23 @@ by apply smulImage_mono assumption -instance associatedPoset_coeSet : Coe (AssociatedPoset α) (Set α) where - coe := AssociatedPoset.val +instance associatedPoset_coeSet : Coe (RegularSupportBasis α) (Set α) where + coe := RegularSupportBasis.val def asSet (α : Type _) [TopologicalSpace α]: Set (Set α) := - { S : Set α | ∃ T : AssociatedPoset α, T.val = S } + { S : Set α | ∃ T : RegularSupportBasis α, T.val = S } theorem asSet_def : - AssociatedPoset.asSet α = { S : Set α | ∃ T : AssociatedPoset α, T.val = S } := rfl + RegularSupportBasis.asSet α = { S : Set α | ∃ T : RegularSupportBasis α, T.val = S } := rfl theorem mem_asSet (S : Set α) : - S ∈ AssociatedPoset.asSet α ↔ ∃ T : AssociatedPoset α, T.val = S := + S ∈ RegularSupportBasis.asSet α ↔ ∃ T : RegularSupportBasis α, 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 := + S ∈ RegularSupportBasis.asSet α ↔ Set.Nonempty S ∧ ∃ seed : Finset (HomeoGroup α), S = RegularSupportInter₀ seed := by rw [asSet_def] simp @@ -438,7 +443,7 @@ by simp let ⟨⟨seed, _⟩, eq⟩ := T.val_has_seed - rw [AssociatedPosetSeed.val_def] at eq + rw [RegularSupportBasis₀.val_def] at eq simp at eq use seed exact eq.symm @@ -447,12 +452,113 @@ by use fromSeed ⟨seed, S_nonempty⟩ rw [val_from_seed] simp - rw [AssociatedPosetSeed.val_def] + rw [RegularSupportBasis₀.val_def] + +instance membership : Membership α (RegularSupportBasis α) where + mem := fun x S => x ∈ S.val + +theorem mem_iff (x : α) (S : RegularSupportBasis α) : x ∈ S ↔ x ∈ (S : Set α) := iff_eq_eq ▸ rfl + +section Basis +open Topology + +-- 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 ∧ RegularSupport α g ⊆ closure W := +by + have U_in_nhds : U ∈ 𝓝 p := by + rw [mem_nhds_iff] + use U + + let ⟨W', W'_in_nhds, W'_ss_U, W'_compact⟩ := local_compact_nhds U_in_nhds + + -- This feels like black magic, but okay + let ⟨W, _W_compact, W_closed, W'_ss_int_W, W_ss_U⟩ := exists_compact_closed_between W'_compact U_open W'_ss_U + have W_cl_eq_W : closure W = W := IsClosed.closure_eq W_closed + + have W_in_nhds : W ∈ 𝓝 p := by + rw [mem_nhds_iff] + use interior W + repeat' apply And.intro + · exact interior_subset + · simp + · exact W'_ss_int_W (mem_of_mem_nhds W'_in_nhds) + + use W + + repeat' apply And.intro + exact W_in_nhds + { + rw [W_cl_eq_W] + exact W_ss_U + } -end AssociatedPoset + 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 isOpen_interior p_in_int_W + + use g + 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 + +/-- +## Proposition 3.2 : RegularSupportBasis is a topological basis of `α` +-/ +theorem isBasis (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] + [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α] + [hc : ContinuousMulAction G α] : + TopologicalSpace.IsTopologicalBasis (RegularSupportBasis.asSet α) := +by + apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds + { + intro U U_in_poset + rw [RegularSupportBasis.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 [RegularSupportBasis.mem_asSet'] + constructor + exact ⟨p, p_in_rsupp⟩ + use {(ContinuousMulAction.toHomeomorph α g : HomeoGroup α)} + unfold RegularSupportInter₀ + 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 Basis +end RegularSupportBasis section Other +/-- +## Proposition 3.1 +--/ theorem homeoGroup_rigidStabilizer_subset_iff {α : Type _} [TopologicalSpace α] [h_lm : LocallyMoving (HomeoGroup α) α] {U V : Set α} (U_reg : Regular U) (V_reg : Regular V):