From 65e1ab7fc81cfce08091f0132aa82d528e2889d6 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Thu, 21 Dec 2023 23:28:48 +0100 Subject: [PATCH] :pencil: Refactor RegularSupportBasis --- Rubin.lean | 211 +++++++++--------- Rubin/RegularSupportBasis.lean | 381 +++++++-------------------------- 2 files changed, 180 insertions(+), 412 deletions(-) diff --git a/Rubin.lean b/Rubin.lean index 3a8189c..82bf1ff 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -741,8 +741,6 @@ open Topology variable {G α : Type _} [Group G] [TopologicalSpace α] [T2Space α] variable [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyMoving G α] -example : TopologicalSpace G := TopologicalSpace.generateFrom (RigidStabilizerBasis.asSets G α) - theorem proposition_3_4_2 {α : Type _} [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] (F : Ultrafilter α): (∃ p : α, ClusterPt p F) ↔ ∃ S ∈ F, IsCompact (closure S) := by @@ -775,8 +773,8 @@ variable [Group G] variable [TopologicalSpace α] [T2Space α] variable [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyMoving G α] -def RSuppSubsets {α : Type _} [TopologicalSpace α] (V : Set α) : Set (Set α) := - {W ∈ RegularSupportBasis.asSet α | W ⊆ V} +def RSuppSubsets (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] (V : Set α) : Set (Set α) := + {W ∈ RegularSupportBasis G α | W ⊆ V} def RSuppOrbit {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] (F : Filter α) (H : Subgroup G) : Set (Set α) := { g •'' W | (g ∈ H) (W ∈ F) } @@ -804,12 +802,14 @@ lemma compact_subset_of_rsupp_basis (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] [T2Space α] [MulAction G α] [ContinuousConstSMul G α] [LocallyCompactSpace α] [HasNoIsolatedPoints α] [LocallyDense G α] - (U : RegularSupportBasis α): - ∃ V : RegularSupportBasis α, (closure V.val) ⊆ U.val ∧ IsCompact (closure V.val) := + {U : Set α} (U_in_basis : U ∈ RegularSupportBasis G α): + ∃ V : RegularSupportBasis G α, (closure V.val) ⊆ U ∧ IsCompact (closure V.val) := by - let ⟨x, x_in_U⟩ := U.nonempty - let ⟨W, W_compact, x_in_intW, W_ss_U⟩ := exists_compact_subset U.regular.isOpen x_in_U - have ⟨V, V_in_basis, x_in_V, V_ss_intW⟩ := (RegularSupportBasis.isBasis G α).exists_subset_of_mem_open x_in_intW isOpen_interior + let ⟨⟨x, x_in_U⟩, _⟩ := (RegularSupportBasis.mem_iff U).mp U_in_basis + have U_regular : Regular U := RegularSupportBasis.regular U_in_basis + + let ⟨W, W_compact, x_in_intW, W_ss_U⟩ := exists_compact_subset U_regular.isOpen x_in_U + have ⟨V, V_in_basis, _, V_ss_intW⟩ := (RegularSupportBasis.isBasis G α).exists_subset_of_mem_open x_in_intW isOpen_interior have clV_ss_W : closure V ⊆ W := by calc @@ -823,10 +823,8 @@ by apply IsClosed.closure_eq exact W_compact.isClosed - rw [RegularSupportBasis.mem_asSet] at V_in_basis - let ⟨V', V'_val⟩ := V_in_basis - use V' - rw [V'_val] + use ⟨V, V_in_basis⟩ + simp constructor · exact subset_trans clV_ss_W W_ss_U @@ -839,18 +837,18 @@ This proposition gives an alternative definition for an ultrafilter to converge This alternative definition should be reconstructible entirely from the algebraic structure of `G`. --/ theorem proposition_3_5 [LocallyDense G α] [LocallyCompactSpace α] [HasNoIsolatedPoints α] - (U : RegularSupportBasis α) (F: Ultrafilter α): - (∃ p ∈ U.val, ClusterPt p F) - ↔ ∃ V : RegularSupportBasis α, V ≤ U ∧ RSuppSubsets V.val ⊆ RSuppOrbit F G•[U.val] := + {U : Set α} (U_in_basis : U ∈ RegularSupportBasis G α) (F: Ultrafilter α): + (∃ p ∈ U, ClusterPt p F) + ↔ ∃ V : RegularSupportBasis G α, V.val ⊆ U ∧ RSuppSubsets G V.val ⊆ RSuppOrbit F G•[U] := by constructor { simp intro p p_in_U p_clusterPt - have U_open : IsOpen U.val := U.regular.isOpen + have U_regular : Regular U := RegularSupportBasis.regular U_in_basis -- First, get a neighborhood of p that is a subset of the closure of the orbit of G_U - have clOrbit_in_nhds := LocallyDense.rigidStabilizer_in_nhds G α U_open p_in_U + have clOrbit_in_nhds := LocallyDense.rigidStabilizer_in_nhds G α U_regular.isOpen p_in_U rw [mem_nhds_iff] at clOrbit_in_nhds let ⟨V, V_ss_clOrbit, V_open, p_in_V⟩ := clOrbit_in_nhds clear clOrbit_in_nhds @@ -858,57 +856,50 @@ by -- Then, get a nontrivial element from that set let ⟨g, g_in_rist, g_ne_one⟩ := LocallyMoving.get_nontrivial_rist_elem (G := G) V_open ⟨p, p_in_V⟩ - have V_ss_clU : V ⊆ closure U.val := by + have V_ss_clU : V ⊆ closure U := by apply subset_trans exact V_ss_clOrbit apply closure_mono exact orbit_rigidStabilizer_subset p_in_U -- The regular support of g is within U - have rsupp_ss_U : RegularSupport α g ⊆ U.val := by + have rsupp_ss_U : RegularSupport α g ⊆ U := by rw [RegularSupport] rw [rigidStabilizer_support] at g_in_rist calc InteriorClosure (Support α g) ⊆ InteriorClosure V := by apply interiorClosure_mono assumption - _ ⊆ InteriorClosure (closure U.val) := by + _ ⊆ InteriorClosure (closure U) := by apply interiorClosure_mono assumption - _ ⊆ InteriorClosure U.val := by + _ ⊆ InteriorClosure U := by simp rfl _ ⊆ _ := by apply subset_of_eq - exact U.regular + exact U_regular - -- Use as the chosen set RegularSupport g - let g' : HomeoGroup α := HomeoGroup.fromContinuous α g - have g'_ne_one : g' ≠ 1 := by - simp - rw [<-HomeoGroup.fromContinuous_one (G := G)] - rw [HomeoGroup.fromContinuous_eq_iff] - exact g_ne_one - use RegularSupportBasis.fromSingleton g' g'_ne_one + let T := RegularSupportBasis.fromSingleton (α := α) g g_ne_one + have T_eq : T.val = RegularSupport α g := by + unfold_let + rw [RegularSupportBasis.fromSingleton_val] + use T.val - constructor + repeat' apply And.intro · -- This statement is equivalent to rsupp(g) ⊆ U - rw [RegularSupportBasis.le_def] - rw [RegularSupportBasis.fromSingleton_val] - unfold RegularSupportInter₀ - simp + rw [T_eq] exact rsupp_ss_U + · exact T.prop.left + · exact T.prop.right · intro W W_in_subsets - rw [RegularSupportBasis.fromSingleton_val] at W_in_subsets - unfold RSuppSubsets RegularSupportInter₀ at W_in_subsets - simp at W_in_subsets - let ⟨W_in_basis, W_subset_rsupp⟩ := W_in_subsets - clear W_in_subsets g' g'_ne_one + simp [RSuppSubsets, T_eq] at W_in_subsets + let ⟨W_in_basis, W_ss_W⟩ := W_in_subsets 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 + have W_ss_clOrbit : W ⊆ closure (MulAction.orbit G•[U] p) := by rw [rigidStabilizer_support] at g_in_rist calc W ⊆ RegularSupport α g := by assumption @@ -921,18 +912,11 @@ by apply closure_mono assumption - -- 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] - exact W'.regular.isOpen - have W_nonempty : Set.Nonempty W := by - let ⟨W', W'_eq⟩ := (RegularSupportBasis.mem_asSet _).mp W_in_basis - rw [<-W'_eq] - exact W'.nonempty + let ⟨W_nonempty, ⟨W_seed, W_eq⟩⟩ := W_in_basis + have W_regular := RegularSupportBasis.regular W_in_basis -- 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 + let ⟨h, h_in_rist, hp_in_W⟩ := moving_elem_of_open_subset_closure_orbit W_regular.isOpen W_nonempty W_ss_clOrbit use h constructor @@ -954,30 +938,33 @@ by rw [basis.mem_iff] use h⁻¹ •'' W repeat' apply And.intro - · rw [RegularSupportBasis.mem_asSet] - rw [RegularSupportBasis.mem_asSet] at W_in_basis - let ⟨W', W'_eq⟩ := W_in_basis - have dec_eq : DecidableEq (HomeoGroup α) := Classical.decEq _ - use (HomeoGroup.fromContinuous α h⁻¹) • W' - rw [RegularSupportBasis.smul_val, W'_eq] - simp + · rw [smulImage_nonempty] + assumption + · simp only [smulImage_inv, inv_inv] + have dec_eq : DecidableEq G := Classical.typeDecidableEq G + use Finset.image (fun g => h⁻¹ * g * h) W_seed + rw [<-RegularSupport.FiniteInter_conj, Finset.image_image] + have fn_eq_id : (fun g => h * g * h⁻¹) ∘ (fun g => h⁻¹ * g * h) = id := by + ext x + simp + group + rw [fn_eq_id, Finset.image_id] + exact W_eq · rw [mem_smulImage, inv_inv] exact hp_in_W · exact Eq.subset rfl } { - intro ⟨V, ⟨V_ss_U, subsets_ss_orbit⟩⟩ - rw [RegularSupportBasis.le_def] at V_ss_U + intro ⟨⟨V, V_in_basis⟩, ⟨V_ss_U, subsets_ss_orbit⟩⟩ + simp only at V_ss_U + simp only at subsets_ss_orbit -- Obtain a compact subset of V' in the basis - let ⟨V', clV'_ss_V, clV'_compact⟩ := compact_subset_of_rsupp_basis G V + let ⟨V', clV'_ss_V, clV'_compact⟩ := compact_subset_of_rsupp_basis G V_in_basis - have V'_in_subsets : V'.val ∈ RSuppSubsets V.val := by + have V'_in_subsets : V'.val ∈ RSuppSubsets G V := by unfold RSuppSubsets simp - constructor - unfold RegularSupportBasis.asSet - simp exact subset_trans subset_closure clV'_ss_V -- V' is in the orbit, so there exists a value `g ∈ G_U` such that `gV ∈ F` @@ -1090,36 +1077,36 @@ variable [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] variable [FaithfulSMul G α] [T2Space α] [LocallyMoving G α] theorem IsRigidSubgroup.has_regularSupportBasis {S : Set G} (S_rigid : IsRigidSubgroup S) : - ∃ (U : RegularSupportBasis α), G•[U.val] = S := + ∃ (U : RegularSupportBasis G α), G•[U.val] = S := by let ⟨S_ne_bot, ⟨T, S_eq⟩⟩ := S_rigid rw [S_eq] simp only [Subgroup.coe_eq] rw [S_eq, <-Subgroup.coe_bot, ne_eq, Subgroup.coe_eq, <-ne_eq] at S_ne_bot - let T' : Finset (HomeoGroup α) := Finset.map (HomeoGroup.fromContinuous_embedding α) T - have T'_rsupp_nonempty : Set.Nonempty (RegularSupportInter₀ T') := by - unfold RegularSupportInter₀ - simp only [proposition_2_1 (G := G) (α := α)] at S_ne_bot + + -- let T' : Finset (HomeoGroup α) := Finset.map (HomeoGroup.fromContinuous_embedding α) T + + let T' := RegularSupport.FiniteInter α T + + have T'_nonempty : Set.Nonempty T' := by + simp only [RegularSupport.FiniteInter, proposition_2_1 (G := G) (α := α)] at S_ne_bot rw [ne_eq, <-rigidStabilizer_iInter_regularSupport', <-ne_eq] at S_ne_bot - let ⟨x, x_in_iInter⟩ := rigidStabilizer_neBot S_ne_bot - use x - simp - simp at x_in_iInter - exact x_in_iInter - - let T'' := RegularSupportBasis.fromSeed ⟨T', T'_rsupp_nonempty⟩ - have T''_val : T''.val = RegularSupportInter₀ T' := rfl - use T'' - rw [T''_val] - unfold RegularSupportInter₀ - simp + exact rigidStabilizer_neBot S_ne_bot + + have T'_in_basis : T' ∈ RegularSupportBasis G α := by + constructor + assumption + use T + + use ⟨T', T'_in_basis⟩ + simp [RegularSupport.FiniteInter] rw [rigidStabilizer_iInter_regularSupport'] simp only [<-proposition_2_1] noncomputable def IsRigidSubgroup.toRegularSupportBasis {S : Set G} (S_rigid : IsRigidSubgroup S) : - RegularSupportBasis α + RegularSupportBasis G α := Exists.choose (IsRigidSubgroup.has_regularSupportBasis α S_rigid) theorem IsRigidSubgroup.toRegularSupportBasis_eq {S : Set G} (S_rigid : IsRigidSubgroup S): @@ -1127,20 +1114,29 @@ theorem IsRigidSubgroup.toRegularSupportBasis_eq {S : Set G} (S_rigid : IsRigidS by exact Exists.choose_spec (IsRigidSubgroup.has_regularSupportBasis α S_rigid) +theorem IsRigidSubgroup.toRegularSupportBasis_regular {S : Set G} (S_rigid : IsRigidSubgroup S): + Regular (S_rigid.toRegularSupportBasis α).val := +by + apply RegularSupportBasis.regular (G := G) + exact (toRegularSupportBasis α S_rigid).prop + +theorem IsRigidSubgroup.toRegularSupportBasis_nonempty {S : Set G} (S_rigid : IsRigidSubgroup S): + Set.Nonempty (S_rigid.toRegularSupportBasis α).val := +by + exact (Subtype.prop (S_rigid.toRegularSupportBasis α)).left + theorem IsRigidSubgroup.toRegularSupportBasis_mono {S T : Set G} (S_rigid : IsRigidSubgroup S) (T_rigid : IsRigidSubgroup T) : - S ⊆ T ↔ S_rigid.toRegularSupportBasis α ≤ T_rigid.toRegularSupportBasis α := + S ⊆ T ↔ (S_rigid.toRegularSupportBasis α : Set α) ⊆ T_rigid.toRegularSupportBasis α := by - rw [RegularSupportBasis.le_def] + rw [rigidStabilizer_subset_iff G (toRegularSupportBasis_regular _ S_rigid) (toRegularSupportBasis_regular _ T_rigid)] constructor · intro S_ss_T rw [<-IsRigidSubgroup.toRegularSupportBasis_eq (α := α) S_rigid] at S_ss_T rw [<-IsRigidSubgroup.toRegularSupportBasis_eq (α := α) T_rigid] at S_ss_T simp at S_ss_T - rw [<-rigidStabilizer_subset_iff G (RegularSupportBasis.regular _) (RegularSupportBasis.regular _)] at S_ss_T exact S_ss_T · intro Sr_ss_Tr - rw [rigidStabilizer_subset_iff G (RegularSupportBasis.regular _) (RegularSupportBasis.regular _)] at Sr_ss_Tr -- TODO: clean that up have Sr_ss_Tr' : (G•[(toRegularSupportBasis α S_rigid).val] : Set G) ⊆ G•[(toRegularSupportBasis α T_rigid).val] := @@ -1155,7 +1151,6 @@ theorem IsRigidSubgroup.toRegularSupportBasis_mono' {S T : Set G} (S_rigid : IsR (T_rigid : IsRigidSubgroup T) : S ⊆ T ↔ (S_rigid.toRegularSupportBasis α : Set α) ⊆ (T_rigid.toRegularSupportBasis α : Set α) := by - rw [<-RegularSupportBasis.le_def] rw [<-IsRigidSubgroup.toRegularSupportBasis_mono] end toRegularSupportBasis @@ -1219,6 +1214,7 @@ instance RubinFilter.to_action_filter_neBot {F : RubinFilter G} [Nonempty α] : rw [Filter.iInf_neBot_iff_of_directed] · intro ⟨S, S_in_F, S_rigid⟩ simp + apply IsRigidSubgroup.toRegularSupportBasis_nonempty · intro ⟨S, S_in_F, S_rigid⟩ ⟨T, T_in_F, T_rigid⟩ simp use S ∩ T @@ -1270,6 +1266,10 @@ theorem RubinFilter.to_action_ultrafilter_converges (F : RubinFilter G) [Nonempt ∃ p ∈ (U_rigid.toRegularSupportBasis α).val, ClusterPt p (F.to_action_ultrafilter α) := by rw [proposition_3_5 (G := G)] + swap + { + apply Subtype.prop (IsRigidSubgroup.toRegularSupportBasis α U_rigid) + } let ⟨V, V_rigid, V_ss_U, algsubs_ss_algorb⟩ := F.converges U U_in_F U_rigid let V' := V_rigid.toSubgroup @@ -1284,22 +1284,17 @@ by unfold RSuppSubsets RSuppOrbit simp - intro S S_rsupp_basis S_ss_V + intro S S_in_basis S_ss_V + -- let ⟨S', S'_eq⟩ := S_in_basis.right - have S_regular : Regular S := by - let ⟨S', S'_eq⟩ := (RegularSupportBasis.mem_asSet S).mp S_rsupp_basis - rw [<-S'_eq] - exact S'.regular + have S_regular : Regular S := RegularSupportBasis.regular S_in_basis - have S_nonempty : Set.Nonempty S := by - let ⟨S', S'_eq⟩ := (RegularSupportBasis.mem_asSet S).mp S_rsupp_basis - rw [<-S'_eq] - exact S'.nonempty + have S_nonempty : Set.Nonempty S := S_in_basis.left have GS_ss_V : G•[S] ≤ V := by rw [<-V_rigid.toRegularSupportBasis_eq (α := α)] simp - rw [<-rigidStabilizer_subset_iff G (α := α) S_regular (RegularSupportBasis.regular _)] + rw [<-rigidStabilizer_subset_iff G (α := α) S_regular (IsRigidSubgroup.toRegularSupportBasis_regular _ _)] assumption -- TODO: show that G•[S] ∈ AlgebraicSubsets V @@ -1308,11 +1303,10 @@ by simp constructor · rw [rigidStabilizerBasis_eq_algebraicCentralizerBasis (α := α)] - let ⟨S', S'_eq⟩ := (RegularSupportBasis.mem_asSet S).mp S_rsupp_basis - rw [<-S'_eq] - rw [RigidStabilizerBasis.mem_iff' _ (LocallyMoving.locally_moving _ S'.regular.isOpen S'.nonempty)] - - sorry + let ⟨S', S'_eq⟩ := S_in_basis.right + rw [RigidStabilizerBasis.mem_iff' _ (LocallyMoving.locally_moving _ S_regular.isOpen S_nonempty)] + use S' + rw [RigidStabilizerInter₀, S'_eq, RegularSupport.FiniteInter, rigidStabilizer_iInter_regularSupport'] · exact GS_ss_V let ⟨g, g_in_U, W, W_in_F, W_rigid, Wconj_eq_GS⟩ := algsubs_ss_algorb GS_in_algsubs_V @@ -1334,14 +1328,11 @@ by swap { rw [<-smulImage_regular (G := G)] - apply RegularSupportBasis.regular + apply IsRigidSubgroup.toRegularSupportBasis_regular } swap - { - let ⟨S', S'_eq⟩ := (RegularSupportBasis.mem_asSet S).mp S_rsupp_basis - rw [<-S'_eq] - exact S'.regular - } + exact S_regular + ext i rw [rigidStabilizer_smulImage, <-Wconj_eq_GS, <-IsRigidSubgroup.mem_subgroup, <-SetLike.mem_coe, IsRigidSubgroup.toRegularSupportBasis_eq] simp diff --git a/Rubin/RegularSupportBasis.lean b/Rubin/RegularSupportBasis.lean index ad8de1f..0ac010f 100644 --- a/Rubin/RegularSupportBasis.lean +++ b/Rubin/RegularSupportBasis.lean @@ -1,6 +1,6 @@ /- This files defines `RegularSupportBasis`, which is a basis of the topological space α, -made up of finite intersections of `RegularSupport α g` for `g : HomeoGroup α`. +made up of finite intersections of `RegularSupport α g` for `g : G`. -/ import Mathlib.Topology.Basic @@ -14,52 +14,43 @@ import Rubin.RegularSupport import Rubin.HomeoGroup namespace Rubin -section RegularSupportBasis.Prelude - -variable {α : Type _} -variable [TopologicalSpace α] -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 `RegularSupportBasis₀` --/ -def RegularSupportInter₀ (S : Finset (HomeoGroup α)): Set α := +def RegularSupport.FiniteInter {G : Type _} [Group G] (α : Type _) [TopologicalSpace α] [MulAction G α] (S : Finset G): Set α := ⋂ (g ∈ S), RegularSupport α g -theorem RegularSupportInter₀.eq_sInter (S : Finset (HomeoGroup α)) : - RegularSupportInter₀ S = ⋂₀ ((fun (g : HomeoGroup α) => RegularSupport α g) '' S) := +def RegularSupportBasis (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] : Set (Set α) := + { S : Set α | S.Nonempty ∧ ∃ (seed : Finset G), S = RegularSupport.FiniteInter α seed } + +variable {G : Type _} +variable {α : Type _} +variable [Group G] +variable [TopologicalSpace α] +variable [MulAction G α] + +theorem RegularSupport.FiniteInter_sInter (S : Finset G) : + RegularSupport.FiniteInter α S = ⋂₀ ((fun (g : G) => RegularSupport α g) '' S) := by rw [Set.sInter_image] rfl -/-- -This is a predecessor type to `RegularSupportBasis`, where equality is defined on the `seed` used, rather than the `val`. ---/ -structure RegularSupportBasis₀ (α : Type _) [TopologicalSpace α] where - seed : Finset (HomeoGroup α) - val_nonempty : Set.Nonempty (RegularSupportInter₀ seed) - -theorem RegularSupportBasis₀.eq_iff_seed_eq (S T : RegularSupportBasis₀ α) : S = T ↔ S.seed = T.seed := by - -- Spooky :3c - rw [mk.injEq] - -def RegularSupportBasis₀.val (S : RegularSupportBasis₀ α) : Set α := RegularSupportInter₀ S.seed - -theorem RegularSupportBasis₀.val_def (S : RegularSupportBasis₀ α) : S.val = RegularSupportInter₀ S.seed := rfl - -@[simp] -theorem RegularSupportBasis₀.nonempty (S : RegularSupportBasis₀ α) : Set.Nonempty S.val := S.val_nonempty +theorem RegularSupportBasis.mem_iff (S : Set α) : + S ∈ RegularSupportBasis G α ↔ S.Nonempty ∧ ∃ (seed : Finset G), S = RegularSupport.FiniteInter α seed := +by + simp only [RegularSupportBasis, Set.mem_setOf_eq] @[simp] -theorem RegularSupportBasis₀.regular (S : RegularSupportBasis₀ α) : Regular S.val := by - rw [S.val_def] - rw [RegularSupportInter₀.eq_sInter] +theorem RegularSupportBasis.regular {S : Set α} (S_mem_basis : S ∈ RegularSupportBasis G α) : Regular S := by + let ⟨_, ⟨seed, S_eq_inter⟩⟩ := (RegularSupportBasis.mem_iff S).mp S_mem_basis + rw [S_eq_inter, RegularSupport.FiniteInter_sInter] apply regular_sInter · have set_decidable : DecidableEq (Set α) := Classical.typeDecidableEq (Set α) - let fin : Finset (Set α) := S.seed.image ((fun g => RegularSupport α g)) + let fin : Finset (Set α) := seed.image ((fun g => RegularSupport α g)) apply Set.Finite.ofFinset fin simp @@ -69,10 +60,12 @@ theorem RegularSupportBasis₀.regular (S : RegularSupportBasis₀ α) : Regular rw [<-Heq] exact regularSupport_regular α g -lemma RegularSupportInter₀.mul_seed (seed : Finset (HomeoGroup α)) [DecidableEq (HomeoGroup α)] (f : HomeoGroup α): - RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' RegularSupportInter₀ seed := +variable [ContinuousConstSMul G α] [DecidableEq G] + +lemma RegularSupport.FiniteInter_conj (seed : Finset G) (f : G): + RegularSupport.FiniteInter α (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' RegularSupport.FiniteInter α seed := by - unfold RegularSupportInter₀ + unfold RegularSupport.FiniteInter simp conv => { rhs @@ -81,85 +74,46 @@ by rw [regularSupport_smulImage] } -variable [DecidableEq (HomeoGroup α)] - /-- -A `HomeoGroup α` group element `f` acts on an `RegularSupportBasis₀ α` set `S`, +A group element `f` acts on sets of `RegularSupportBasis G α`, by mapping each element `g` of `S.seed` to `f * g * f⁻¹` --/ -instance homeoGroup_smul₂ : SMul (HomeoGroup α) (RegularSupportBasis₀ α) where - smul := fun f S => ⟨ - (Finset.image (fun g => f * g * f⁻¹) S.seed), - by - rw [RegularSupportInter₀.mul_seed] - simp - exact S.val_nonempty - ⟩ - -theorem RegularSupportBasis₀.smul_seed (f : HomeoGroup α) (S : RegularSupportBasis₀ α) : - (f • S).seed = (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 RegularSupportBasis₀.smul_val' (f : HomeoGroup α) (S : RegularSupportBasis₀ α) : +noncomputable instance RegularSupportBasis.instSmul : SMul G (RegularSupportBasis G α) where + smul := fun f S => + let new_seed := (Finset.image (fun g => f * g * f⁻¹) S.prop.right.choose) + ⟨ + RegularSupport.FiniteInter α new_seed, + by + rw [RegularSupportBasis.mem_iff] + nth_rw 1 [RegularSupport.FiniteInter_conj, smulImage_nonempty] + rw [<-S.prop.right.choose_spec] + + constructor + · exact S.prop.left + · use new_seed + ⟩ + +theorem RegularSupportBasis.smul_eq' (f : G) (S : RegularSupportBasis G α) : + (f • S).val + = RegularSupport.FiniteInter α (Finset.image (fun g => f * g * f⁻¹) S.prop.right.choose) := rfl + +theorem RegularSupportBasis.smul_eq (f : G) (S : RegularSupportBasis G α) : (f • S).val = f •'' S.val := by - unfold val - rw [<-RegularSupportInter₀.mul_seed] - rw [RegularSupportBasis₀.smul_seed] - --- We define a "preliminary" group action from `HomeoGroup α` to `RegularSupportBasis₀` -instance homeoGroup_mulAction₂ : MulAction (HomeoGroup α) (RegularSupportBasis₀ α) where - one_smul := by - intro S - rw [RegularSupportBasis₀.eq_iff_seed_eq] - rw [RegularSupportBasis₀.smul_seed] - simp - mul_smul := by - intro f g S - rw [RegularSupportBasis₀.eq_iff_seed_eq] - repeat rw [RegularSupportBasis₀.smul_seed] - rw [Finset.image_image] - ext x - simp - group - -end RegularSupportBasis.Prelude - --- TODO: define RegularSupportBasis as a Set directly? -/-- -A partially-ordered set, associated to Rubin's proof. -Any element in that set is made up of a `seed`, -such that `val = RegularSupportInter₀ seed` and `Set.Nonempty val`. - -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 RegularSupportBasis (α : Type _) [TopologicalSpace α] where - val : Set α - val_has_seed : ∃ po_seed : RegularSupportBasis₀ α, po_seed.val = val - -namespace RegularSupportBasis - -variable {α : Type _} -variable [TopologicalSpace α] -variable [DecidableEq α] - -theorem eq_iff_val_eq (S T : RegularSupportBasis α) : S = T ↔ S.val = T.val := by - rw [mk.injEq] - -def fromSeed (seed : RegularSupportBasis₀ α) : RegularSupportBasis α := ⟨ - seed.val, - ⟨seed, seed.val_def⟩ -⟩ - -def fromSingleton [T2Space α] (g : HomeoGroup α) (g_ne_one : g ≠ 1) : RegularSupportBasis α := - let seed : RegularSupportBasis₀ α := ⟨ - {g}, + rw [RegularSupportBasis.smul_eq'] + rw [RegularSupport.FiniteInter_conj] + rw [<-S.prop.right.choose_spec] + +def RegularSupportBasis.fromSingleton [T2Space α] [FaithfulSMul G α] (g : G) (g_ne_one : g ≠ 1) : { S : Set α // S ∈ RegularSupportBasis G α } := + let seed : Finset G := {g} + ⟨ + RegularSupport.FiniteInter α seed, by - unfold RegularSupportInter₀ - simp + rw [RegularSupportBasis.mem_iff] + constructor + swap + use seed + rw [Set.nonempty_iff_ne_empty] intro rsupp_empty apply g_ne_one @@ -169,181 +123,34 @@ def fromSingleton [T2Space α] (g : HomeoGroup α) (g_ne_one : g ≠ 1) : Regula rw [<-not_mem_support] apply Set.not_mem_subset · apply support_subset_regularSupport - · rw [rsupp_empty] + · simp [RegularSupport.FiniteInter] at rsupp_empty + rw [rsupp_empty] exact Set.not_mem_empty x ⟩ - fromSeed seed - -theorem fromSingleton_val [T2Space α] (g : HomeoGroup α) (g_ne_one : g ≠ 1) : - (fromSingleton g g_ne_one).val = RegularSupportInter₀ {g} := rfl - -noncomputable def full_seed (S : RegularSupportBasis α) : RegularSupportBasis₀ α := - (Exists.choose S.val_has_seed) - -noncomputable def seed (S : RegularSupportBasis α) : Finset (HomeoGroup α) := - S.full_seed.seed - -instance : Coe (RegularSupportBasis₀ α) (RegularSupportBasis α) where - coe := fromSeed - -@[simp] -theorem full_seed_seed (S : RegularSupportBasis α) : S.full_seed.seed = S.seed := rfl - -@[simp] -theorem fromSeed_val (seed : RegularSupportBasis₀ α) : - (seed : RegularSupportBasis α).val = seed.val := -by - unfold fromSeed - simp - -@[simp] -theorem val_from_seed (S : RegularSupportBasis α) : RegularSupportInter₀ S.seed = S.val := by - unfold seed full_seed - rw [<-RegularSupportBasis₀.val_def] - rw [Exists.choose_spec S.val_has_seed] - -@[simp] -theorem val_from_seed₂ (S : RegularSupportBasis α) : S.full_seed.val = S.val := by - unfold full_seed - rw [RegularSupportBasis₀.val_def] - nth_rw 2 [<-val_from_seed] - unfold seed full_seed - rfl - --- 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 : RegularSupportBasis₀ α, p po_seed.val) : - ∀ (S : RegularSupportBasis α), p S.val := -by - intro S - rw [<-val_from_seed] - have res := any_seed S.full_seed - rw [val_from_seed₂] at res - rw [val_from_seed] - exact res - -@[simp] -theorem nonempty : ∀ (S : RegularSupportBasis α), Set.Nonempty S.val := - prop_from_val RegularSupportBasis₀.nonempty - -@[simp] -theorem regular : ∀ (S : RegularSupportBasis α), Regular S.val := - prop_from_val RegularSupportBasis₀.regular - -variable [DecidableEq (HomeoGroup α)] - -instance homeoGroup_smul₃ : SMul (HomeoGroup α) (RegularSupportBasis α) where - smul := fun f S => ⟨ - f •'' S.val, - by - use f • S.full_seed - rw [RegularSupportBasis₀.smul_val'] - simp - ⟩ - -theorem smul_val (f : HomeoGroup α) (S : RegularSupportBasis α) : - (f • S).val = f •'' S.val := rfl -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 [RegularSupportInter₀.mul_seed] - rw [S_val_eq] - -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 +theorem RegularSupportBasis.fromSingleton_val [T2Space α] [FaithfulSMul G α] (g : G) (g_ne_one : g ≠ 1) : + (fromSingleton g g_ne_one).val = RegularSupport α g := by simp [fromSingleton, RegularSupport.FiniteInter] -- Note: we could potentially implement MulActionHom -instance homeoGroup_mulAction₃ : MulAction (HomeoGroup α) (RegularSupportBasis α) where +noncomputable instance RegularSupportBasis.instMulAction : MulAction G (RegularSupportBasis G α) where one_smul := by intro S - rw [eq_iff_val_eq] - repeat rw [smul_val] + apply Subtype.eq + rw [RegularSupportBasis.smul_eq] rw [one_smulImage] mul_smul := by intro S f g - rw [eq_iff_val_eq] - repeat rw [smul_val] + apply Subtype.eq + repeat rw [RegularSupportBasis.smul_eq] rw [smulImage_mul] -instance associatedPoset_le : LE (RegularSupportBasis α) where - le := fun S T => S.val ⊆ T.val - -theorem le_def (S T : RegularSupportBasis α) : S ≤ T ↔ S.val ⊆ T.val := by - rw [iff_eq_eq] - rfl - -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) - ((le_def _ _).mp S_le_U) - ) - le_antisymm := by - intro S T S_le_T T_le_S - rw [le_def] at S_le_T - rw [le_def] at T_le_S - rw [eq_iff_val_eq] - apply le_antisymm <;> assumption - -theorem smul_mono {S T : RegularSupportBasis α} (f : HomeoGroup α) (S_le_T : S ≤ T) : - f • S ≤ f • T := +theorem RegularSupportBasis.smul_mono {S T : RegularSupportBasis G α} (f : G) (S_le_T : S.val ⊆ T.val) : + (f • S).val ⊆ (f • T).val := by - rw [le_def] - repeat rw [smul_val] + repeat rw [RegularSupportBasis.smul_eq] apply smulImage_mono assumption -instance associatedPoset_coeSet : Coe (RegularSupportBasis α) (Set α) where - coe := RegularSupportBasis.val - -def asSet (α : Type _) [TopologicalSpace α]: Set (Set α) := - { S : Set α | ∃ T : RegularSupportBasis α, T.val = S } - -theorem asSet_def : - RegularSupportBasis.asSet α = { S : Set α | ∃ T : RegularSupportBasis α, T.val = S } := rfl - -theorem mem_asSet (S : Set α) : - S ∈ RegularSupportBasis.asSet α ↔ ∃ T : RegularSupportBasis α, T.val = S := -by - rw [asSet_def] - simp - -theorem mem_asSet' (S : Set α) : - S ∈ RegularSupportBasis.asSet α ↔ Set.Nonempty S ∧ ∃ seed : Finset (HomeoGroup α), S = RegularSupportInter₀ seed := -by - rw [asSet_def] - simp - constructor - · intro ⟨T, T_eq⟩ - rw [<-T_eq] - constructor - simp - - let ⟨⟨seed, _⟩, eq⟩ := T.val_has_seed - rw [RegularSupportBasis₀.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 [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 @@ -408,56 +215,26 @@ by /-- ## Proposition 3.2 : RegularSupportBasis is a topological basis of `α` -/ -theorem isBasis : - TopologicalSpace.IsTopologicalBasis (RegularSupportBasis.asSet α) := +theorem RegularSupportBasis.isBasis : + TopologicalSpace.IsTopologicalBasis (RegularSupportBasis G α) := 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 + exact (RegularSupportBasis.regular U_in_poset).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 {HomeoGroup.fromContinuous α g} - unfold RegularSupportInter₀ - simp - · exact p_in_rsupp + · exact ⟨p, p_in_rsupp⟩ + · use {g} + simp [RegularSupport.FiniteInter] + · assumption · apply subset_trans exact rsupp_ss_clW exact clW_ss_U --- example (p : α): ∃ (S : Set α), S ∈ (RegularSupportBasis.asSet α) ∧ IsCompact (closure S) ∧ p ∈ S := --- by --- have h₁ := TopologicalSpace.IsTopologicalBasis.nhds_hasBasis (isBasis G α) (a := p) --- have h₂ := compact_basis_nhds p - --- rw [Filter.hasBasis_iff] at h₁ --- rw [Filter.hasBasis_iff] at h₂ - --- have T : Set α := sorry --- have T_in_nhds : T ∈ 𝓝 p := sorry - --- let ⟨U, ⟨⟨U_in_nhds, U_compact⟩, U_ss_T⟩⟩ := (h₂ T).mp T_in_nhds --- let ⟨V, ⟨⟨V_in_basis, p_in_V⟩, V_ss_T⟩⟩ := (h₁ U).mp U_in_nhds - --- use V --- (repeat' apply And.intro) <;> try assumption --- -- apply IsCompact.of_isClosed_subset - --- -- · assumption --- -- · sorry --- -- · assumption --- sorry - end Basis -end RegularSupportBasis end Rubin