diff --git a/Rubin.lean b/Rubin.lean index 360242a..b1efb1a 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -24,12 +24,13 @@ import Rubin.SmulImage import Rubin.Support import Rubin.Topology import Rubin.RigidStabilizer -import Rubin.RigidStabilizerBasis +-- import Rubin.RigidStabilizerBasis import Rubin.Period import Rubin.AlgebraicDisjointness import Rubin.RegularSupport import Rubin.RegularSupportBasis import Rubin.HomeoGroup +import Rubin.Filter #align_import rubin @@ -694,43 +695,250 @@ by repeat rw [<-proposition_2_1] exact alg_disj -#check proposition_2_1 -lemma rigidStabilizerInter_eq_algebraicCentralizerInter {S : Finset G} : - RigidStabilizerInter₀ α S = AlgebraicCentralizerInter₀ S := +-- lemma remark_2_3' {f g : G} : +-- (AlgebraicCentralizer f) ⊓ (AlgebraicCentralizer g) ≠ ⊥ → +-- Set.Nonempty ((RegularSupport α f) ∩ (RegularSupport α g)) := +-- by +-- intro alg_inter_neBot +-- repeat rw [proposition_2_1 (α := α)] at alg_inter_neBot +-- rw [ne_eq] at alg_inter_neBot + +-- rw [rigidStabilizer_inter_bot_iff_regularSupport_disj] at alg_inter_neBot +-- rw [Set.not_disjoint_iff_nonempty_inter] at alg_inter_neBot +-- exact alg_inter_neBot + +lemma rigidStabilizer_inter_eq_algebraicCentralizerInter {S : Finset G} : + G•[RegularSupport.FiniteInter α S] = AlgebraicCentralizerInter S := by - unfold RigidStabilizerInter₀ - unfold AlgebraicCentralizerInter₀ + unfold RegularSupport.FiniteInter + unfold AlgebraicCentralizerInter + rw [rigidStabilizer_iInter_regularSupport'] simp only [<-proposition_2_1] - -- conv => { - -- rhs - -- congr; intro; congr; intro - -- rw [proposition_2_1 (α := α)] - -- } - -theorem rigidStabilizerBasis_eq_algebraicCentralizerBasis : - AlgebraicCentralizerBasis G = RigidStabilizerBasis G α := + +lemma regularSupportInter_nonEmpty_iff_neBot {S : Finset G} [Nonempty α]: + AlgebraicCentralizerInter S ≠ ⊥ ↔ + Set.Nonempty (RegularSupport.FiniteInter α S) := by - apply le_antisymm <;> intro B B_mem - any_goals rw [RigidStabilizerBasis.mem_iff] - any_goals rw [AlgebraicCentralizerBasis.mem_iff] - any_goals rw [RigidStabilizerBasis.mem_iff] at B_mem - any_goals rw [AlgebraicCentralizerBasis.mem_iff] at B_mem + constructor + · rw [<-rigidStabilizer_inter_eq_algebraicCentralizerInter (α := α), ne_eq] + intro rist_neBot + by_contra eq_empty + rw [Set.not_nonempty_iff_eq_empty] at eq_empty + rw [eq_empty, rigidStabilizer_empty] at rist_neBot + exact rist_neBot rfl + · intro nonempty + intro eq_bot + rw [<-rigidStabilizer_inter_eq_algebraicCentralizerInter (α := α)] at eq_bot + rw [<-rigidStabilizer_empty (G := G) (α := α), rigidStabilizer_eq_iff] at eq_bot + · rw [eq_bot, Set.nonempty_iff_ne_empty] at nonempty + exact nonempty rfl + · apply RegularSupport.FiniteInter_regular + · simp - all_goals let ⟨⟨seed, B_ne_bot⟩, B_eq⟩ := B_mem +theorem AlgebraicCentralizerBasis.exists_rigidStabilizer_inv (H : Set G) [Nonempty α]: + ∃ S ∈ RegularSupportBasis G α, H ∈ AlgebraicCentralizerBasis G → H = G•[S] := +by + by_cases H_in_basis?: H ∈ AlgebraicCentralizerBasis G + swap + { + use Set.univ + constructor + rw [RegularSupportBasis.mem_iff] + constructor + · exact Set.univ_nonempty + · use ∅ + unfold RegularSupport.FiniteInter + simp + · intro H_in_basis + exfalso + exact H_in_basis? H_in_basis + } - any_goals rw [RigidStabilizerBasis₀.val_def] at B_eq - any_goals rw [AlgebraicCentralizerBasis₀.val_def] at B_eq - all_goals simp at B_eq - all_goals rw [<-B_eq] + have ⟨H_ne_one, ⟨seed, H_eq⟩⟩ := (AlgebraicCentralizerBasis.mem_iff H).mp H_in_basis? - rw [<-rigidStabilizerInter_eq_algebraicCentralizerInter (α := α)] at B_ne_bot - swap - rw [rigidStabilizerInter_eq_algebraicCentralizerInter (α := α)] at B_ne_bot + rw [H_eq, <-Subgroup.coe_bot, ne_eq, SetLike.coe_set_eq, <-ne_eq] at H_ne_one + + use RegularSupport.FiniteInter α seed + constructor + · rw [RegularSupportBasis.mem_iff] + constructor + · rw [<-regularSupportInter_nonEmpty_iff_neBot] + exact H_ne_one + · use seed + · intro _ - all_goals use ⟨seed, B_ne_bot⟩ + rw [rigidStabilizer_inter_eq_algebraicCentralizerInter] + exact H_eq - symm - all_goals apply rigidStabilizerInter_eq_algebraicCentralizerInter +theorem AlgebraicCentralizerBasis.mem_of_regularSupportBasis {S : Set α} + (S_in_basis : S ∈ RegularSupportBasis G α) : + (G•[S] : Set G) ∈ AlgebraicCentralizerBasis G := +by + rw [AlgebraicCentralizerBasis.subgroup_mem_iff] + rw [RegularSupportBasis.mem_iff] at S_in_basis + let ⟨S_nonempty, ⟨seed, S_eq⟩⟩ := S_in_basis + + have α_nonempty : Nonempty α := by + by_contra α_empty + rw [not_nonempty_iff] at α_empty + rw [Set.nonempty_iff_ne_empty] at S_nonempty + apply S_nonempty + exact Set.eq_empty_of_isEmpty S + + constructor + · rw [S_eq, rigidStabilizer_inter_eq_algebraicCentralizerInter] + rw [regularSupportInter_nonEmpty_iff_neBot (α := α)] + rw [<-S_eq] + exact S_nonempty + · use seed + rw [S_eq] + exact rigidStabilizer_inter_eq_algebraicCentralizerInter + +@[simp] +theorem AlgebraicCentralizerBasis.eq_rist_image [Nonempty α]: + (fun S => (G•[S] : Set G)) '' RegularSupportBasis G α = AlgebraicCentralizerBasis G := +by + ext H + constructor + · simp + intro S S_in_basis H_eq + rw [<-H_eq] + apply mem_of_regularSupportBasis S_in_basis + · intro H_in_basis + simp + let ⟨S, S_in_rsupp, H_eq⟩ := AlgebraicCentralizerBasis.exists_rigidStabilizer_inv (α := α) H + specialize H_eq H_in_basis + symm at H_eq + use S + +noncomputable def rigidStabilizer_inv [Nonempty α] (H : Set G) : Set α := + (AlgebraicCentralizerBasis.exists_rigidStabilizer_inv H).choose + +theorem rigidStabilizer_inv_eq [Nonempty α] {H : Set G} (H_in_basis : H ∈ AlgebraicCentralizerBasis G) : + H = G•[rigidStabilizer_inv (α := α) H] := +by + have spec := (AlgebraicCentralizerBasis.exists_rigidStabilizer_inv (α := α) H).choose_spec + exact spec.right H_in_basis + +theorem rigidStabilizer_in_basis [Nonempty α] (H : Set G) : + rigidStabilizer_inv (α := α) H ∈ RegularSupportBasis G α := +by + have spec := (AlgebraicCentralizerBasis.exists_rigidStabilizer_inv (α := α) H).choose_spec + exact spec.left + +theorem rigidStabilizer_inv_eq' [Nonempty α] {S : Set α} (S_in_basis : S ∈ RegularSupportBasis G α) : + rigidStabilizer_inv (α := α) (G := G) G•[S] = S := +by + have GS_in_basis : (G•[S] : Set G) ∈ AlgebraicCentralizerBasis G := by + exact AlgebraicCentralizerBasis.mem_of_regularSupportBasis S_in_basis + + have eq := rigidStabilizer_inv_eq GS_in_basis (α := α) + rw [SetLike.coe_set_eq, rigidStabilizer_eq_iff] at eq + · exact eq.symm + · exact RegularSupportBasis.regular S_in_basis + · exact RegularSupportBasis.regular (rigidStabilizer_in_basis _) + +variable [Nonempty α] [HasNoIsolatedPoints α] [LocallyDense G α] + +noncomputable def RigidStabilizer.order_iso_on (G α : Type _) [Group G] [Nonempty α] [TopologicalSpace α] [T2Space α] + [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] + [HasNoIsolatedPoints α] [LocallyDense G α] : OrderIsoOn (Set α) (Set G) (RegularSupportBasis G α) +where + toFun := fun S => G•[S] + invFun := fun H => rigidStabilizer_inv (α := α) H + + leftInv_on := by + intro S S_in_basis + simp + exact rigidStabilizer_inv_eq' S_in_basis + + rightInv_on := by + intro H H_in_basis + simp + simp at H_in_basis + symm + exact rigidStabilizer_inv_eq H_in_basis + + toFun_doubleMonotone := by + intro S S_in_basis T T_in_basis + simp + apply rigidStabilizer_subset_iff G (RegularSupportBasis.regular S_in_basis) (RegularSupportBasis.regular T_in_basis) + +@[simp] +theorem RigidStabilizer.order_iso_on_toFun: + (RigidStabilizer.order_iso_on G α).toFun = (fun S => (G•[S] : Set G)) := +by + simp [order_iso_on] + +@[simp] +theorem RigidStabilizer.order_iso_on_invFun: + (RigidStabilizer.order_iso_on G α).invFun = (fun S => rigidStabilizer_inv (α := α) S) := +by + simp [order_iso_on] + +noncomputable def RigidStabilizer.inv_order_iso_on (G α : Type _) [Group G] [Nonempty α] [TopologicalSpace α] [T2Space α] + [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] + [HasNoIsolatedPoints α] [LocallyDense G α] : OrderIsoOn (Set G) (Set α) (AlgebraicCentralizerBasis G) := + (RigidStabilizer.order_iso_on G α).inv.mk_of_subset + (subset_of_eq (AlgebraicCentralizerBasis.eq_rist_image (α := α) (G := G)).symm) + +@[simp] +theorem RigidStabilizer.inv_order_iso_on_toFun: + (RigidStabilizer.inv_order_iso_on G α).toFun = (fun S => rigidStabilizer_inv (α := α) S) := +by + simp [inv_order_iso_on, order_iso_on] + +@[simp] +theorem RigidStabilizer.inv_order_iso_on_invFun: + (RigidStabilizer.inv_order_iso_on G α).invFun = (fun S => (G•[S] : Set G)) := +by + simp [inv_order_iso_on, order_iso_on] + +-- TODO: mark simp theorems as local +@[simp] +theorem RegularSupportBasis.eq_inv_rist_image: + (fun H => rigidStabilizer_inv (α := α) H) '' AlgebraicCentralizerBasis G = RegularSupportBasis G α := +by + rw [<-AlgebraicCentralizerBasis.eq_rist_image (α := α) (G := G)] + rw [Set.image_image] + nth_rw 2 [<-OrderIsoOn.leftInv_image (RigidStabilizer.order_iso_on G α)] + rw [Function.comp_def] + rw [RigidStabilizer.order_iso_on] + +lemma RigidStabilizer_doubleMonotone : DoubleMonotoneOn (fun S => G•[S]) (RegularSupportBasis G α) := by + have res := (RigidStabilizer.order_iso_on G α).toFun_doubleMonotone + simp at res + exact res + +lemma RigidStabilizer_inv_doubleMonotone : DoubleMonotoneOn (fun S => rigidStabilizer_inv (α := α) S) (AlgebraicCentralizerBasis G) := by + have res := (RigidStabilizer.order_iso_on G α).invFun_doubleMonotone + simp at res + exact res + +lemma RigidStabilizer_rightInv {U : Set G} (U_in_basis : U ∈ AlgebraicCentralizerBasis G) : + G•[rigidStabilizer_inv (α := α) U] = U := +by + have res := (RigidStabilizer.order_iso_on G α).rightInv_on U + simp at res + exact res U_in_basis + +lemma RigidStabilizer_leftInv {U : Set α} (U_in_basis : U ∈ RegularSupportBasis G α) : + rigidStabilizer_inv (α := α) (G•[U] : Set G) = U := +by + have res := (RigidStabilizer.order_iso_on G α).leftInv_on U + simp at res + exact res U_in_basis + +theorem AlgebraicCentralizerBasis.mem_of_regularSupportBasis_inv {S : Set G} + (S_in_basis : rigidStabilizer_inv (α := α) S ∈ RegularSupportBasis G α) : + S ∈ AlgebraicCentralizerBasis G := +by + let ⟨T, T_in_basis, T_eq⟩ := (RegularSupportBasis.eq_inv_rist_image (G := G) (α := α)).symm ▸ S_in_basis + simp only at T_eq + + -- Note: currently not provable, we need to add another requirement to rigidStabilizer_inv + + sorry end RegularSupport @@ -1020,8 +1228,24 @@ by exact proposition_3_5_1 U_in_basis (F : Filter α) · exact proposition_3_5_2 (F : Filter α) +theorem proposition_3_5' {U : Set α} (U_in_basis : U ∈ RegularSupportBasis G α) + (F : UltrafilterInBasis (RegularSupportBasis G α)): + (∃ p ∈ U, ClusterPt p F) + ↔ ∃ V : RegularSupportBasis G α, V.val ⊆ U ∧ RSuppSubsets G V.val ⊆ RSuppOrbit F G•[U] := +by + constructor + · simp only [ + F.clusterPt_iff_le_nhds + (RegularSupportBasis.isBasis G α) + (RegularSupportBasis.closed_inter G α) + ] + exact proposition_3_5_1 U_in_basis (F : Filter α) + · exact proposition_3_5_2 (F : Filter α) + end Ultrafilter + +/- variable {G α : Type _} variable [Group G] @@ -1600,11 +1824,188 @@ theorem rubin' (hα : RubinAction G α) : EquivariantHomeomorph G α (RubinSpace sorry end Convert +-/ + + +section RubinFilter +variable {G : Type _} [Group G] +variable {α : Type _} [Nonempty α] [TopologicalSpace α] [HasNoIsolatedPoints α] [T2Space α] [LocallyCompactSpace α] +variable [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyDense G α] + +def AlgebraicSubsets (V : Set G) : Set (Set G) := + {W ∈ AlgebraicCentralizerBasis G | W ⊆ V} + +def AlgebraicOrbit (F : Filter G) (U : Set G) : Set (Set G) := + { (fun h => g * h * g⁻¹) '' W | (g ∈ U) (W ∈ F.sets ∩ AlgebraicCentralizerBasis G) } + +theorem AlgebraicOrbit.mem_iff (F : Filter G) (U : Set G) (S : Set G): + S ∈ AlgebraicOrbit F U ↔ ∃ g ∈ U, ∃ W ∈ F, W ∈ AlgebraicCentralizerBasis G ∧ S = (fun h => g * h * g⁻¹) '' W := +by + simp [AlgebraicOrbit] + simp only [and_assoc, eq_comm] +structure RubinFilter (G : Type _) [Group G] := + filter : UltrafilterInBasis (AlgebraicCentralizerBasis G) --- Topology can be generated from the disconnectedness of the filters + converges : ∃ V ∈ AlgebraicCentralizerBasis G, AlgebraicSubsets V ⊆ AlgebraicOrbit filter Set.univ +lemma RegularSupportBasis.empty_not_mem' : ∅ ∉ (RigidStabilizer.inv_order_iso_on G α).toFun '' AlgebraicCentralizerBasis G := by + simp + exact RegularSupportBasis.empty_not_mem _ _ + +lemma AlgebraicCentralizerBasis.empty_not_mem' : ∅ ∉ (RigidStabilizer.order_iso_on G α).toFun '' RegularSupportBasis G α := by + unfold RigidStabilizer.order_iso_on + rw [AlgebraicCentralizerBasis.eq_rist_image] + exact AlgebraicCentralizerBasis.empty_not_mem + +def RubinFilter.map (F : RubinFilter G) (α : Type _) + [TopologicalSpace α] [T2Space α] [Nonempty α] [HasNoIsolatedPoints α] + [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyDense G α] : UltrafilterInBasis (RegularSupportBasis G α) := + ( + F.filter.map_basis + AlgebraicCentralizerBasis.empty_not_mem + (RigidStabilizer.inv_order_iso_on G α) + RegularSupportBasis.empty_not_mem' + ).cast (by simp) + +def IsRubinFilterOf (A : UltrafilterInBasis (RegularSupportBasis G α)) (B : UltrafilterInBasis (AlgebraicCentralizerBasis G)) : Prop := + ∀ U ∈ RegularSupportBasis G α, U ∈ A ↔ (G•[U] : Set G) ∈ B + +theorem RubinFilter.map_isRubinFilterOf (F : RubinFilter G) : + IsRubinFilterOf (F.map α) F.filter := +by + intro U U_in_basis + unfold map + simp + have ⟨U', U'_in_basis, U'_eq⟩ := (RegularSupportBasis.eq_inv_rist_image (G := G) (α := α)).symm ▸ U_in_basis + simp only at U'_eq + rw [<-U'_eq] + rw [Filter.InBasis.map_mem_map_basis_of_basis_set _ RigidStabilizer_inv_doubleMonotone F.filter.in_basis U'_in_basis] + rw [RigidStabilizer_rightInv U'_in_basis] + rfl + +theorem RubinFilter.from_isRubinFilterOf' (F : UltrafilterInBasis (RegularSupportBasis G α)) : + IsRubinFilterOf F ((F.map_basis + (RegularSupportBasis.empty_not_mem G α) + (RigidStabilizer.order_iso_on G α) + AlgebraicCentralizerBasis.empty_not_mem' + ).cast (by simp)) := +by + intro U U_in_basis + simp + rw [Filter.InBasis.map_mem_map_basis_of_basis_set _ RigidStabilizer_doubleMonotone F.in_basis U_in_basis] + rfl + +theorem IsRubinFilterOf.mem_inv {A : UltrafilterInBasis (RegularSupportBasis G α)} + {B : UltrafilterInBasis (AlgebraicCentralizerBasis G)} + (filter_of : IsRubinFilterOf A B) {U : Set G} (U_in_basis : U ∈ AlgebraicCentralizerBasis G): + U ∈ B ↔ rigidStabilizer_inv U ∈ A := +by + rw [<-AlgebraicCentralizerBasis.eq_rist_image (α := α)] at U_in_basis + let ⟨V, V_in_basis, V_eq⟩ := U_in_basis + rw [<-V_eq, RigidStabilizer_leftInv V_in_basis] + symm + exact filter_of V V_in_basis + +theorem IsRubinFilterOf.mem_inter_inv {A : UltrafilterInBasis (RegularSupportBasis G α)} + {B : UltrafilterInBasis (AlgebraicCentralizerBasis G)} + (filter_of : IsRubinFilterOf A B) (U : Set G): + U ∈ B.filter.sets ∩ AlgebraicCentralizerBasis G ↔ rigidStabilizer_inv U ∈ A.filter.sets ∩ RegularSupportBasis G α := +by + constructor + · intro ⟨U_in_filter, U_in_basis⟩ + constructor + simp + rw [<-filter_of.mem_inv U_in_basis] + exact U_in_filter + exact rigidStabilizer_in_basis U + · intro ⟨iU_in_filter, iU_in_basis⟩ + have U_in_basis := AlgebraicCentralizerBasis.mem_of_regularSupportBasis_inv iU_in_basis + constructor + · simp + rw [filter_of.mem_inv U_in_basis] + exact iU_in_filter + · assumption + +theorem IsRubinFilterOf.subsets_ss_orbit {A : UltrafilterInBasis (RegularSupportBasis G α)} + {B : UltrafilterInBasis (AlgebraicCentralizerBasis G)} + (filter_of : IsRubinFilterOf A B) + {V : Set α} (V_in_basis : V ∈ RegularSupportBasis G α) + {W : Set α} (W_in_basis : W ∈ RegularSupportBasis G α) : + RSuppSubsets G W ⊆ RSuppOrbit A G•[V] ↔ AlgebraicSubsets (G•[W]) ⊆ AlgebraicOrbit B.filter G•[V] := +by + constructor + · intro rsupp_ss + unfold AlgebraicSubsets AlgebraicOrbit + intro U ⟨U_in_basis, U_ss_GW⟩ + let U' := rigidStabilizer_inv (α := α) U + have U'_in_basis : U' ∈ RegularSupportBasis G α := rigidStabilizer_in_basis U + have U'_ss_W : U' ⊆ W := by + rw [rigidStabilizer_subset_iff (G := G) (RegularSupportBasis.regular U'_in_basis) (RegularSupportBasis.regular W_in_basis)] + unfold_let + rw [<-SetLike.coe_subset_coe] + rw [RigidStabilizer_rightInv (G := G) (α := α) U_in_basis] + assumption + let ⟨g, g_in_GV, ⟨W, W_in_A, gW_eq_U⟩⟩ := rsupp_ss ⟨U'_in_basis, U'_ss_W⟩ + use g + constructor + { + simp + exact g_in_GV + } + + have dec_eq : DecidableEq G := Classical.typeDecidableEq _ + + have W_in_basis : W ∈ RegularSupportBasis G α := by + rw [smulImage_inv] at gW_eq_U + rw [gW_eq_U] + apply RegularSupportBasis.smulImage_in_basis + assumption + + use G•[W] + rw [filter_of.mem_inter_inv] + rw [RigidStabilizer_leftInv (G := G) (α := α) W_in_basis] + refine ⟨⟨W_in_A, W_in_basis⟩, ?W_eq_U⟩ + rw [rigidStabilizer_conj_image_eq, gW_eq_U] + unfold_let + exact RigidStabilizer_rightInv U_in_basis + sorry + +def RubinFilter.from (F : UltrafilterInBasis (RegularSupportBasis G α)) (F_converges : ∃ p : α, F ≤ nhds p) : RubinFilter G where + filter := (F.map_basis + (RegularSupportBasis.empty_not_mem G α) + (RigidStabilizer.order_iso_on G α) + AlgebraicCentralizerBasis.empty_not_mem' + ).cast (by simp) + + converges := by + let ⟨p, F_le_nhds⟩ := F_converges + + have F_clusterPt : ClusterPt p F := by + rw [UltrafilterInBasis.clusterPt_iff_le_nhds] + · assumption + · exact RegularSupportBasis.isBasis G α + · exact RegularSupportBasis.closed_inter G α + + have ⟨⟨W, W_in_basis⟩, W_ss_V, W_subsets_ss_GV_orbit⟩ := (proposition_3_5' (RegularSupportBasis.univ_mem G α) F).mp ⟨p, (Set.mem_univ p), F_clusterPt⟩ + simp only at W_ss_V + simp only at W_subsets_ss_GV_orbit + + use G•[W] + constructor + { + apply AlgebraicCentralizerBasis.mem_of_regularSupportBasis W_in_basis + } + + rw [<-Subgroup.coe_top, <-rigidStabilizer_univ (α := α) (G := G)] + rw [<-(RubinFilter.from_isRubinFilterOf' F).subsets_ss_orbit (RegularSupportBasis.univ_mem G α) W_in_basis] + assumption + + +end RubinFilter + +/- variable {β : Type _} variable [TopologicalSpace β] [MulAction G β] [ContinuousConstSMul G β] @@ -1614,6 +2015,7 @@ variable [TopologicalSpace β] [MulAction G β] [ContinuousConstSMul G β] theorem rubin (hα : RubinAction G α) (hβ : RubinAction G β) : EquivariantHomeomorph G α β := by -- by composing rubin' hα sorry +-/ end Rubin diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean index d273126..58f8afb 100644 --- a/Rubin/AlgebraicDisjointness.lean +++ b/Rubin/AlgebraicDisjointness.lean @@ -396,44 +396,33 @@ by /-- Finite intersections of [`AlgebraicCentralizer`]. --/ -def AlgebraicCentralizerInter₀ (S : Finset G) : Subgroup G := +def AlgebraicCentralizerInter (S : Finset G) : Subgroup G := ⨅ (g ∈ S), AlgebraicCentralizer g -structure AlgebraicCentralizerBasis₀ (G: Type _) [Group G] where - seed : Finset G - val_ne_bot : AlgebraicCentralizerInter₀ seed ≠ ⊥ - -def AlgebraicCentralizerBasis₀.val (B : AlgebraicCentralizerBasis₀ G) : Subgroup G := - AlgebraicCentralizerInter₀ B.seed - -theorem AlgebraicCentralizerBasis₀.val_def (B : AlgebraicCentralizerBasis₀ G) : - B.val = AlgebraicCentralizerInter₀ B.seed := rfl - -def AlgebraicCentralizerBasis (G : Type _) [Group G] : Set (Subgroup G) := - { H.val | H : AlgebraicCentralizerBasis₀ G } +def AlgebraicCentralizerBasis (G : Type _) [Group G] : Set (Set G) := + { S : Set G | S ≠ {1} ∧ ∃ seed : Finset G, + S = AlgebraicCentralizerInter seed + } -theorem AlgebraicCentralizerBasis.mem_iff (H : Subgroup G) : - H ∈ AlgebraicCentralizerBasis G ↔ ∃ B : AlgebraicCentralizerBasis₀ G, B.val = H := by rfl +theorem AlgebraicCentralizerBasis.mem_iff (S : Set G) : + S ∈ AlgebraicCentralizerBasis G ↔ + S ≠ {1} ∧ ∃ seed : Finset G, S = AlgebraicCentralizerInter seed +:= by rfl -theorem AlgebraicCentralizerBasis.mem_iff' (H : Subgroup G) - (H_ne_bot : H ≠ ⊥) : - H ∈ AlgebraicCentralizerBasis G ↔ ∃ seed : Finset G, AlgebraicCentralizerInter₀ seed = H := +theorem AlgebraicCentralizerBasis.subgroup_mem_iff (S : Subgroup G) : + (S : Set G) ∈ AlgebraicCentralizerBasis G ↔ + S ≠ ⊥ ∧ ∃ seed : Finset G, S = AlgebraicCentralizerInter seed := by - rw [mem_iff] - constructor - · intro ⟨B, B_eq⟩ - use B.seed - rw [AlgebraicCentralizerBasis₀.val_def] at B_eq - exact B_eq - · intro ⟨seed, seed_eq⟩ - let B := AlgebraicCentralizerInter₀ seed - have val_ne_bot : B ≠ ⊥ := by - unfold_let - rw [seed_eq] - exact H_ne_bot - use ⟨seed, val_ne_bot⟩ - rw [<-seed_eq] - rfl + rw [mem_iff, <-Subgroup.coe_bot, ne_eq, SetLike.coe_set_eq] + simp + +theorem AlgebraicCentralizerBasis.empty_not_mem : ∅ ∉ AlgebraicCentralizerBasis G := by + simp [AlgebraicCentralizerBasis] + intro _ _ + rw [<-ne_eq] + symm + rw [<-Set.nonempty_iff_ne_empty] + exact Subgroup.coe_nonempty _ end AlgebraicCentralizer diff --git a/Rubin/Filter.lean b/Rubin/Filter.lean index a049a3a..57921a9 100644 --- a/Rubin/Filter.lean +++ b/Rubin/Filter.lean @@ -32,6 +32,19 @@ by all_goals rw [f_double_mono] all_goals assumption +theorem DoubleMonotoneOn.injective' [PartialOrder α] [Preorder β] (f_double_mono : DoubleMonotoneOn f B) : + ∀ x ∈ B, ∀ y ∈ B, + f x = f y → x = y := +by + intro x x_in_B y y_in_B fx_eq_fy + have fx_eq : f x = Set.restrict B f ⟨x, x_in_B⟩ := by simp + have fy_eq : f y = Set.restrict B f ⟨y, y_in_B⟩ := by simp + + rw [fx_eq, fy_eq] at fx_eq_fy + apply (injective f_double_mono) at fx_eq_fy + simp at fx_eq_fy + exact fx_eq_fy + theorem DoubleMonotoneOn.subset_iff {B : Set (Set α)} {f : Set α → Set β} (f_double_mono : DoubleMonotoneOn f B) : ∀ s ∈ B, ∀ t ∈ B, s ⊆ t ↔ f s ⊆ f t := by @@ -66,6 +79,20 @@ where intro a a_in_T b b_in_T rw [F.toFun_doubleMonotone a (T_ss_S a_in_T) b (T_ss_S b_in_T)] +@[simp] +theorem OrderIsoOn.mk_of_subset_toFun [Preorder α] [Preorder β] (F : OrderIsoOn α β S) + {T : Set α} (T_ss_S : T ⊆ S) : (F.mk_of_subset T_ss_S).toFun = F.toFun := +by + unfold mk_of_subset + rfl + +@[simp] +theorem OrderIsoOn.mk_of_subset_invFun [Preorder α] [Preorder β] (F : OrderIsoOn α β S) + {T : Set α} (T_ss_S : T ⊆ S) : (F.mk_of_subset T_ss_S).invFun = F.invFun := +by + unfold mk_of_subset + rfl + theorem OrderIsoOn.invFun_doubleMonotone [Preorder α] [Preorder β] (F : OrderIsoOn α β S) : DoubleMonotoneOn F.invFun (F.toFun '' S) := by @@ -462,6 +489,22 @@ by rw [Filter.InBasis.mem_image_basis_of_injective_on _ _ map_double_mono.injective S_in_B] + +theorem Filter.InBasis.mem_map_basis' + (map : Set α → Set β) (map_double_mono : DoubleMonotoneOn map B) + (F_basis : Filter.InBasis F B) {x : Set β} (x_in_basis : x ∈ map '' B): + x ∈ (Filter.InBasis.map_basis F B map) ↔ ∃ y : Set α, y ∈ F ∧ y ∈ B ∧ map y = x := +by + let ⟨y, y_in_B, y_eq⟩ := x_in_basis + rw [<-y_eq] + rw [map_mem_map_basis_of_basis_set map map_double_mono F_basis y_in_B] + constructor + · intro y_in_F + use y + · intro ⟨z, z_in_F, z_in_B, z_eq_y⟩ + apply (map_double_mono.injective' z z_in_B y y_in_B) at z_eq_y + exact z_eq_y ▸ z_in_F + -- TODO: clean this up :c theorem Filter.InBasis.map_basis_comp {γ : Type _} (m₁ : OrderIsoOn (Set α) (Set β) B) (m₂ : OrderIsoOn (Set β) (Set γ) (m₁.toFun '' B)) @@ -1048,6 +1091,28 @@ where use S ultra := U.map_basis_ultra empty_notin_B map +@[simp] +theorem UltrafilterInBasis.mem_map_basis {β : Type _} + (empty_notin_B : ∅ ∉ B) + (map : OrderIsoOn (Set α) (Set β) B) + (empty_notin_mB : ∅ ∉ map.toFun '' B) + (U : UltrafilterInBasis B) + (S : Set β): + S ∈ U.map_basis empty_notin_B map empty_notin_mB ↔ S ∈ Filter.InBasis.map_basis U.filter B map.toFun := +by + rw [map_basis] + rfl + +@[simp] +theorem UltrafilterInBasis.map_basis_filter {β : Type _} + (empty_notin_B : ∅ ∉ B) + (map : OrderIsoOn (Set α) (Set β) B) + (empty_notin_mB : ∅ ∉ map.toFun '' B) + (U : UltrafilterInBasis B): + (U.map_basis empty_notin_B map empty_notin_mB).filter = Filter.InBasis.map_basis U.filter B map.toFun := +by + rw [map_basis] + /- theorem compl_not_mem_iff : sᶜ ∉ f ↔ s ∈ f := ⟨fun hsc => @@ -1128,3 +1193,31 @@ by specialize p_clusterPt T_in_nhds Tc_in_U rw [Set.inter_compl_self] at p_clusterPt exact Set.not_nonempty_empty p_clusterPt + +/-- +Allows substituting the expression for the basis in the type. +--/ +def UltrafilterInBasis.cast (U : UltrafilterInBasis B) {C : Set (Set α)} (B_eq_C : B = C) : + UltrafilterInBasis C where + filter := U.filter + ne_bot := U.ne_bot + in_basis := U.in_basis.mono (subset_of_eq B_eq_C) + ultra := by + nth_rw 1 [<-B_eq_C] + exact U.ultra + +@[simp] +theorem UltrafilterInBasis.mem_cast (U : UltrafilterInBasis B) {C : Set (Set α)} (B_eq_C : B = C) (S : Set α): + S ∈ U.cast B_eq_C ↔ S ∈ U := by rw [cast]; rfl + +@[simp] +theorem UltrafilterInBasis.le_cast (U : UltrafilterInBasis B) {C : Set (Set α)} (B_eq_C : B = C) (F : Filter α): + F ≤ U.cast B_eq_C ↔ F ≤ U := by rw [cast] + +@[simp] +theorem UltrafilterInBasis.cast_le (U : UltrafilterInBasis B) {C : Set (Set α)} (B_eq_C : B = C) (F : Filter α): + U.cast B_eq_C ≤ F ↔ U ≤ F := by rw [cast] + +@[simp] +theorem UltrafilterInBasis.cast_filter (U : UltrafilterInBasis B) {C : Set (Set α)} (B_eq_C : B = C): + (U.cast B_eq_C).filter = U.filter := by rw [cast] diff --git a/Rubin/InteriorClosure.lean b/Rubin/InteriorClosure.lean index ecfc0dc..2993e97 100644 --- a/Rubin/InteriorClosure.lean +++ b/Rubin/InteriorClosure.lean @@ -182,6 +182,14 @@ by rw [<-Set.diff_eq_empty] exact V_diff_cl_empty +theorem regular_empty (α : Type _) [TopologicalSpace α]: Regular (∅ : Set α) := +by + simp + +theorem regular_univ (α : Type _) [TopologicalSpace α]: Regular (Set.univ : Set α) := +by + simp + theorem regular_nbhd [T2Space α] {u v : α} (u_ne_v : u ≠ v): ∃ (U V : Set α), Regular U ∧ Regular V ∧ Disjoint U V ∧ u ∈ U ∧ v ∈ V := by diff --git a/Rubin/RegularSupportBasis.lean b/Rubin/RegularSupportBasis.lean index 0ac010f..d9fd0aa 100644 --- a/Rubin/RegularSupportBasis.lean +++ b/Rubin/RegularSupportBasis.lean @@ -44,13 +44,14 @@ by simp only [RegularSupportBasis, Set.mem_setOf_eq] @[simp] -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] +theorem RegularSupport.FiniteInter_regular (F : Finset G) : + Regular (RegularSupport.FiniteInter α F) := +by + rw [RegularSupport.FiniteInter_sInter] apply regular_sInter · have set_decidable : DecidableEq (Set α) := Classical.typeDecidableEq (Set α) - let fin : Finset (Set α) := seed.image ((fun g => RegularSupport α g)) + let fin : Finset (Set α) := F.image ((fun g => RegularSupport α g)) apply Set.Finite.ofFinset fin simp @@ -60,6 +61,12 @@ theorem RegularSupportBasis.regular {S : Set α} (S_mem_basis : S ∈ RegularSup rw [<-Heq] exact regularSupport_regular α g +@[simp] +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] + apply RegularSupport.FiniteInter_regular + variable [ContinuousConstSMul G α] [DecidableEq G] lemma RegularSupport.FiniteInter_conj (seed : Finset G) (f : G): @@ -104,6 +111,14 @@ by rw [RegularSupport.FiniteInter_conj] rw [<-S.prop.right.choose_spec] +theorem RegularSupportBasis.smulImage_in_basis {U : Set α} (U_in_basis : U ∈ RegularSupportBasis G α) + (f : G) : f •'' U ∈ RegularSupportBasis G α := +by + have eq := smul_eq f ⟨U, U_in_basis⟩ + simp only at eq + rw [<-eq] + exact Subtype.coe_prop _ + def RegularSupportBasis.fromSingleton [T2Space α] [FaithfulSMul G α] (g : G) (g_ne_one : g ≠ 1) : { S : Set α // S ∈ RegularSupportBasis G α } := let seed : Finset G := {g} ⟨ @@ -236,5 +251,42 @@ by exact rsupp_ss_clW exact clW_ss_U +theorem RegularSupportBasis.closed_inter (b1 b2 : Set α) + (b1_in_basis : b1 ∈ RegularSupportBasis G α) + (b2_in_basis : b2 ∈ RegularSupportBasis G α) + (inter_nonempty : Set.Nonempty (b1 ∩ b2)) : + (b1 ∩ b2) ∈ RegularSupportBasis G α := +by + unfold RegularSupportBasis + simp + constructor + assumption + + let ⟨_, ⟨s1, b1_eq⟩⟩ := b1_in_basis + let ⟨_, ⟨s2, b2_eq⟩⟩ := b2_in_basis + + have dec_eq : DecidableEq G := Classical.typeDecidableEq G + use s1 ∪ s2 + rw [RegularSupport.FiniteInter_sInter] + rw [Finset.coe_union, Set.image_union, Set.sInter_union] + repeat rw [<-RegularSupport.FiniteInter_sInter] + rw [b2_eq, b1_eq] + +theorem RegularSupportBasis.empty_not_mem : + ∅ ∉ RegularSupportBasis G α := +by + intro empty_mem + rw [RegularSupportBasis.mem_iff] at empty_mem + exact Set.not_nonempty_empty empty_mem.left + +theorem RegularSupportBasis.univ_mem [Nonempty α]: + Set.univ ∈ RegularSupportBasis G α := +by + rw [RegularSupportBasis.mem_iff] + constructor + exact Set.univ_nonempty + use ∅ + simp [RegularSupport.FiniteInter] + end Basis end Rubin diff --git a/Rubin/RigidStabilizer.lean b/Rubin/RigidStabilizer.lean index 5f81773..d4490cf 100644 --- a/Rubin/RigidStabilizer.lean +++ b/Rubin/RigidStabilizer.lean @@ -159,6 +159,13 @@ by rw [f_in_rist x (Set.not_mem_empty x)] simp +theorem rigidStabilizer_univ (G α: Type _) [Group G] [MulAction G α]: + G•[(Set.univ : Set α)] = ⊤ := +by + ext g + rw [rigidStabilizer_support] + simp + theorem rigidStabilizer_sInter (S : Set (Set α)) : G•[⋂₀ S] = ⨅ T ∈ S, G•[T] := by @@ -191,6 +198,18 @@ by rw [smulImage_subset_inv] simp +theorem rigidStabilizer_conj_image_eq (S : Set α) (f : G) : + (fun g => f * g * f⁻¹) '' G•[S] = G•[f •'' S] := +by + ext x + have f_eq : (fun g => f * g * f⁻¹) = (MulAut.conj f).toEquiv := by + ext x + simp + + rw [f_eq, Set.mem_image_equiv] + rw [MulEquiv.toEquiv_eq_coe, MulEquiv.coe_toEquiv_symm, MulAut.conj_symm_apply] + simp [rigidStabilizer_smulImage] + theorem orbit_rigidStabilizer_subset {p : α} {U : Set α} (p_in_U : p ∈ U): MulAction.orbit G•[U] p ⊆ U := by