From 7d92d98b602da50907147f0b684db7578742a020 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Sat, 30 Dec 2023 22:42:24 +0100 Subject: [PATCH] :tada: Finally reached the homeomorph stage! All that remains is to define the conjugation action on RubinSpace, and prove that the canonical homeomorph (lim/fromPoint) preserves that action. The tools should be in place to prove most of this, and I don't have to deal with open sets ever again. --- Rubin.lean | 243 ++++++++++++++++++++++++++++++- Rubin/AlgebraicDisjointness.lean | 36 +++++ Rubin/LocallyDense.lean | 7 + 3 files changed, 279 insertions(+), 7 deletions(-) diff --git a/Rubin.lean b/Rubin.lean index cfb5532..16d7573 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -1612,6 +1612,10 @@ end Convergence section Setoid +variable {α : Type} +variable [Nonempty α] [TopologicalSpace α] [T2Space α] [HasNoIsolatedPoints α] [LocallyCompactSpace α] +variable [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyDense G α] + /-- Two rubin filters are equivalent if they share the same behavior in regards to which set their converging point `p` lies in. --/ @@ -1709,6 +1713,16 @@ by rw [<-F₁.le_nhds_eq_lim _ _ F₁_le_nhds] rw [<-F₂.le_nhds_eq_lim _ _ F₂_le_nhds] +theorem RubinFilter.lim_eq_iff_eqv (F₁ F₂ : RubinFilter G): + F₁ ≈ F₂ ↔ F₁.lim α = F₂.lim α := +by + constructor + apply lim_eq_of_eqv + intro lim_eq + apply eqv_of_map_converges _ _ (F₁.lim α) + · exact le_nhds_lim α F₁ + · rw [lim_eq] + exact le_nhds_lim α F₂ lemma RubinFilter.fromPoint_converges' (p : α) : ∃ q : α, ( @@ -1747,6 +1761,17 @@ by apply UltrafilterInBasis.of_le · exact le_nhds_lim α F +lemma RubinFilter.lim_in_set (F : RubinFilter G) {S : Set α} (S_in_basis : S ∈ RegularSupportBasis G α) : + F.lim α ∈ S ↔ AlgebraicConvergent F.filter.filter G•[S] := +by + rw [<-(RubinFilter.map_isRubinFilterOf F (α := α)).converges_iff S_in_basis] + constructor + · intro lim_in_S + exact ⟨lim α F, lim_in_S, le_nhds_lim α F⟩ + · intro ⟨p, p_in_S, F_le_nhds⟩ + convert p_in_S + exact (le_nhds_eq_lim α F p F_le_nhds).symm + def RubinFilterBasis (G : Type _) [Group G] : Set (Set (RubinFilter G)) := (fun S : Set G => { F : RubinFilter G | AlgebraicConvergent F.filter S }) '' AlgebraicCentralizerBasis G @@ -1810,15 +1835,220 @@ instance : TopologicalSpace (RubinSpace G) := by unfold RubinSpace infer_instance +end Setoid + +end RubinFilter + + +section Basis + +variable {G : Type _} +variable [Group G] + +variable (α : Type) [α_nonempty : Nonempty α] + [TopologicalSpace α] [T2Space α] [HasNoIsolatedPoints α] [LocallyCompactSpace α] + [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyDense G α] + +lemma AlgebraicConvergent_mono {F : RubinFilter G} {S T : Set G} + (S_basis : S ∈ AlgebraicCentralizerBasis G) (T_basis : T ∈ AlgebraicCentralizerBasis G) + (S_ss_T : S ⊆ T) (F_converges : AlgebraicConvergent F.filter.filter S) : AlgebraicConvergent F.filter.filter T := +by + let ⟨S', S'_basis, S'_eq⟩ := (AlgebraicCentralizerBasis.eq_rist_image (G := G) (α := α)).symm ▸ S_basis + let ⟨T', T'_basis, T'_eq⟩ := (AlgebraicCentralizerBasis.eq_rist_image (G := G) (α := α)).symm ▸ T_basis + rw [<-S'_eq, <-RubinFilter.lim_in_set F S'_basis (α := α)] at F_converges + rw [<-T'_eq, <-RubinFilter.lim_in_set F T'_basis (α := α)] + have S'_ss_T' : S' ⊆ T' := by + rw [<-S'_eq, <-T'_eq] at S_ss_T + simp at S_ss_T + rw [<-rigidStabilizer_subset_iff] at S_ss_T + any_goals apply RegularSupportBasis.regular (α := α) (G := G) + all_goals assumption + apply S'_ss_T' + assumption + +theorem RubinFilterBasis.isBasis : TopologicalSpace.IsTopologicalBasis (RubinFilterBasis G) := by + constructor + · intro T₁ T₁_in_basis T₂ T₂_in_basis F ⟨F_in_T₁, F_in_T₂⟩ + let ⟨B₁, B₁_in_basis, B₁_mem⟩ := (mem_iff T₁).mp T₁_in_basis + let ⟨B₂, B₂_in_basis, B₂_mem⟩ := (mem_iff T₂).mp T₂_in_basis + + have F_conv₁ := (B₁_mem F).mp F_in_T₁ + have F_conv₂ := (B₂_mem F).mp F_in_T₂ + + let ⟨B₁', B₁'_in_basis, B₁'_eq⟩ := (AlgebraicCentralizerBasis.eq_rist_image (G := G) (α := α)).symm ▸ B₁_in_basis + let ⟨B₂', B₂'_in_basis, B₂'_eq⟩ := (AlgebraicCentralizerBasis.eq_rist_image (G := G) (α := α)).symm ▸ B₂_in_basis + simp only at B₁'_eq + simp only at B₂'_eq + + rw [<-B₁'_eq, <-RubinFilter.lim_in_set F B₁'_in_basis] at F_conv₁ + rw [<-B₂'_eq, <-RubinFilter.lim_in_set F B₂'_in_basis] at F_conv₂ + + have F_conv₃ : F.lim α ∈ B₁' ∩ B₂' := ⟨F_conv₁, F_conv₂⟩ + + have B₃_nonempty : (B₁' ∩ B₂').Nonempty := by use F.lim α + have B₃'_in_basis : B₁' ∩ B₂' ∈ RegularSupportBasis G α := by + apply RegularSupportBasis.closed_inter + all_goals assumption + + have B₃_eq : B₁ ∩ B₂ = G•[B₁' ∩ B₂'] := by + rw [rigidStabilizer_inter, Subgroup.coe_inf, B₁'_eq, B₂'_eq] + + have B₃_in_basis : B₁ ∩ B₂ ∈ AlgebraicCentralizerBasis G := by + rw [<-AlgebraicCentralizerBasis.eq_rist_image (α := α)] + use B₁' ∩ B₂' + simp + exact ⟨B₃'_in_basis, B₃_eq.symm⟩ + + have B₃_ne_bot : B₁ ∩ B₂ ≠ {1} := by + rw [B₃_eq, <-Subgroup.coe_bot, ne_eq, SetLike.coe_set_eq] + rw [rigidStabilizer_empty_iff _ (RegularSupportBasis.regular B₃'_in_basis)] + rwa [<-ne_eq, <-Set.nonempty_iff_ne_empty] + + use { F : RubinFilter G | AlgebraicConvergent F.filter (B₁ ∩ B₂) } + simp [RubinFilterBasis] + refine ⟨⟨B₁ ∩ B₂, ?B_in_basis, rfl⟩, ?F_conv₃, ?T₃_ss_T₁, ?T₃_ss_T₂⟩ + · apply AlgebraicCentralizerBasis.inter_closed + all_goals assumption + · rw [<-B₁'_eq, <-B₂'_eq, <-Subgroup.coe_inf, <-rigidStabilizer_inter] + rw [<-RubinFilter.lim_in_set F B₃'_in_basis] + exact ⟨F_conv₁, F_conv₂⟩ + · intro X + simp [B₁_mem] + apply AlgebraicConvergent_mono α B₃_in_basis B₁_in_basis + exact Set.inter_subset_left B₁ B₂ + · intro X + simp [B₂_mem] + apply AlgebraicConvergent_mono α B₃_in_basis B₂_in_basis + exact Set.inter_subset_right B₁ B₂ + · have univ_in_basis : Set.univ ∈ RubinFilterBasis G := by + rw [RubinFilterBasis.mem_iff] + use Set.univ + refine ⟨AlgebraicCentralizerBasis.univ_mem ?ex_nontrivial, ?F_in_univ⟩ + { + let ⟨x⟩ := α_nonempty + let ⟨g, _, g_moving⟩ := get_moving_elem_in_rigidStabilizer G (isOpen_univ (α := α)) (Set.mem_univ x) + use g + intro g_eq_one + rw [g_eq_one, one_smul] at g_moving + exact g_moving rfl + } + intro X + simp + exact X.converges + apply Set.eq_univ_of_univ_subset + exact Set.subset_sUnion_of_mem univ_in_basis + · rfl + +theorem RubinSpace.basis : TopologicalSpace.IsTopologicalBasis ( + Set.image (Quotient.mk') '' (RubinFilterBasis G) +) := by + refine TopologicalSpace.IsTopologicalBasis.quotientMap (RubinFilterBasis.isBasis α) (quotientMap_quotient_mk') ?open_map + + rw [(RubinFilterBasis.isBasis α).isOpenMap_iff] + + intro U U_in_basis + + apply TopologicalSpace.isOpen_generateFrom_of_mem + rw [RubinFilterBasis.mem_iff] + rw [RubinFilterBasis.mem_iff] at U_in_basis + let ⟨B, B_in_basis, B_mem⟩ := U_in_basis + simp + refine ⟨B, B_in_basis, ?mem⟩ + intro F + + let ⟨B', B'_in_basis, B'_eq⟩ := (AlgebraicCentralizerBasis.eq_rist_image (G := G) (α := α)).symm ▸ B_in_basis + simp only at B'_eq + + simp only [B_mem] + rw [<-B'_eq, <-RubinFilter.lim_in_set (α := α) (G := G)] + conv => { + lhs; congr; intro; + rw [<-RubinFilter.lim_in_set (α := α) (G := G) _ B'_in_basis] + } + swap + exact B'_in_basis + + constructor + · intro ⟨F', F'_lim, F'_eqv⟩ + rw [(by rfl : Setoid.r F' F ↔ F' ≈ F)] at F'_eqv + rw [RubinFilter.lim_eq_iff_eqv F' F (α := α)] at F'_eqv + rwa [<-F'_eqv] + · intro F_lim + exact ⟨F, F_lim, Setoid.refl F⟩ + +end Basis + +section Equivariant + +variable {G : Type _} [Group G] +variable (α : Type _) [TopologicalSpace α] [T2Space α] [HasNoIsolatedPoints α] [LocallyCompactSpace α] [Nonempty α] +variable [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyDense G α] + +@[simp] +lemma RubinSpace.lim_mk (F : RubinFilter G) : + RubinSpace.lim (α := α) (⟦F⟧ : RubinSpace G) = F.lim α := +by + unfold lim + simp + +@[simp] +lemma RubinSpace.lim_mk' (F : RubinFilter G) : + RubinSpace.lim (α := α) (Quotient.mk' F : RubinSpace G) = F.lim α := +by + rw [Quotient.mk'_eq_mk] + exact RubinSpace.lim_mk α F + theorem RubinSpace.lim_continuous : Continuous (RubinSpace.lim (G := G) (α := α)) := by - sorry + -- TODO: rename to continuous_iff when upgrading mathlib + apply (RegularSupportBasis.isBasis G α).continuous + intro S S_in_basis + apply TopologicalSpace.isOpen_generateFrom_of_mem + rw [RubinFilterBasis.mem_iff] + use G•[S] + refine ⟨AlgebraicCentralizerBasis.mem_of_regularSupportBasis S_in_basis, ?filters_mem⟩ + simp + simp [<-RubinFilter.lim_in_set _ S_in_basis] theorem RubinSpace.fromPoint_continuous : Continuous (RubinSpace.fromPoint (G := G) (α := α)) := by - sorry + apply (RubinSpace.basis (α := α)).continuous + simp + intro U U_in_basis + rw [RubinFilterBasis.mem_iff] at U_in_basis + let ⟨V, V_in_basis, U_mem⟩ := U_in_basis + -- TODO: automatize this + let ⟨V', V'_in_basis, V'_eq⟩ := (AlgebraicCentralizerBasis.eq_rist_image (G := G) (α := α)).symm ▸ V_in_basis + simp only at V'_eq + + rw [<-V'_eq] at U_mem + conv at U_mem => { + intro F + rw [<-F.lim_in_set V'_in_basis] + } + rw [(RegularSupportBasis.isBasis G α).isOpen_iff] + simp + intro x F F_in_U F_eqv_fromPoint_x + rw [U_mem] at F_in_U + have x_eq_F_lim : x = F.lim α := by + symm + rwa [Quotient.mk'_eq_mk, fromPoint, Quotient.eq, RubinFilter.lim_eq_iff_eqv (α := α), RubinFilter.fromPoint_lim] at F_eqv_fromPoint_x + + refine ⟨V', V'_in_basis, ?x_in_V', ?V'_ss_U⟩ + rwa [x_eq_F_lim] + + intro y y_in_V' + simp + + use RubinFilter.fromPoint (G := G) y + constructor + rwa [U_mem, RubinFilter.fromPoint_lim] + + rw [Quotient.mk'_eq_mk, RubinSpace.fromPoint] + +-- TODO: mind the type variables /-- The canonical homeomorphism from a topological space that a rubin action acts on to -the rubin space. +the rubin space associated with the group. --/ noncomputable def RubinSpace.homeomorph : Homeomorph (RubinSpace G) α where toFun := RubinSpace.lim @@ -1827,12 +2057,12 @@ noncomputable def RubinSpace.homeomorph : Homeomorph (RubinSpace G) α where left_inv := RubinSpace.fromPoint_lim right_inv := RubinSpace.lim_fromPoint - continuous_toFun := RubinSpace.lim_continuous - continuous_invFun := RubinSpace.fromPoint_continuous + continuous_toFun := RubinSpace.lim_continuous α + continuous_invFun := RubinSpace.fromPoint_continuous α instance : MulAction G (RubinSpace G) := sorry -end Setoid +end Equivariant -- theorem rubin' (hα : RubinAction G α) : EquivariantHomeomorph G α (RubinSpace G) where -- toFun := fun x => ⟦⟧ @@ -1840,7 +2070,6 @@ end Setoid -end RubinFilter /- variable {β : Type _} diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean index ecfa8e0..91099af 100644 --- a/Rubin/AlgebraicDisjointness.lean +++ b/Rubin/AlgebraicDisjointness.lean @@ -525,6 +525,14 @@ by rw [S_eq_fT] simp +theorem AlgebraicCentralizerBasis.univ_mem (ex_non_trivial : ∃ g : G, g ≠ 1): Set.univ ∈ AlgebraicCentralizerBasis G := by + rw [mem_iff] + constructor + symm + exact Set.nonempty_compl.mp ex_non_trivial + use ∅ + simp [AlgebraicCentralizerInter] + theorem AlgebraicCentralizerBasis.conj_mem {S : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G) (h : G) : (fun g => h * g * h⁻¹) '' S ∈ AlgebraicCentralizerBasis G := by @@ -559,6 +567,34 @@ by rw [<-SetLike.mem_coe, <-AlgebraicCentralizer.conj, conj_eq, Set.mem_image_equiv] } +theorem AlgebraicCentralizerBasis.inter_closed + {S T : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G) (T_in_basis : T ∈ AlgebraicCentralizerBasis G) + (ST_ne_bot : S ∩ T ≠ {1}) : + S ∩ T ∈ AlgebraicCentralizerBasis G := +by + let ⟨S', S_eq⟩ := to_subgroup S_in_basis + rw [S_eq] + rw [S_eq, subgroup_mem_iff] at S_in_basis + let ⟨S'_ne_bot, ⟨S'_seed, S'_eq⟩⟩ := S_in_basis + + let ⟨T', T_eq⟩ := to_subgroup T_in_basis + rw [T_eq] + rw [T_eq, subgroup_mem_iff] at T_in_basis + let ⟨T'_ne_bot, ⟨T'_seed, T'_eq⟩⟩ := T_in_basis + + rw [<-Subgroup.coe_inf, subgroup_mem_iff] + rw [S_eq, T_eq, <-Subgroup.coe_inf, <-Subgroup.coe_bot, ne_eq, SetLike.coe_set_eq, <-ne_eq] at ST_ne_bot + + have dec_eq : DecidableEq G := Classical.typeDecidableEq G + + refine ⟨ST_ne_bot, ⟨S'_seed ∪ T'_seed, ?inter_eq⟩⟩ + + unfold AlgebraicCentralizerInter + + simp only [<-Finset.mem_coe] + rw [Finset.coe_union, iInf_union] + rw [S'_eq, T'_eq] + rfl end AlgebraicCentralizer diff --git a/Rubin/LocallyDense.lean b/Rubin/LocallyDense.lean index 9edaf44..be947e5 100644 --- a/Rubin/LocallyDense.lean +++ b/Rubin/LocallyDense.lean @@ -280,5 +280,12 @@ by · intro H_eq rw [H_eq] +theorem rigidStabilizer_empty_iff (G : Type _) [Group G] {α : Type _} [TopologicalSpace α] + [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyMoving G α] + {U : Set α} (U_reg : Regular U) : + G•[U] = ⊥ ↔ U = ∅ := +by + rw [<-rigidStabilizer_empty (α := α) (G := G)] + exact rigidStabilizer_eq_iff G U_reg (regular_empty α) end Rubin