diff --git a/Rubin.lean b/Rubin.lean index a0377d5..3a8189c 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -16,6 +16,7 @@ import Mathlib.Topology.Bases import Mathlib.Topology.Compactness.Compact import Mathlib.Topology.Separation import Mathlib.Topology.Homeomorph +import Mathlib.Topology.Algebra.ConstMulAction import Rubin.Tactic import Rubin.MulActionExt @@ -70,7 +71,7 @@ variable {G α : Type _} variable [TopologicalSpace α] variable [Group G] variable [MulAction G α] -variable [ContinuousMulAction G α] +variable [ContinuousConstSMul G α] variable [FaithfulSMul G α] -- TODO: modify the proof to be less "let everything"-y, especially the first half @@ -83,7 +84,7 @@ lemma proposition_1_1_1 [h_lm : LocallyMoving G α] [T2Space α] (f g : G) (supp have hx_ne_x := mem_support.mp x_in_supp_h -- Since α is Hausdoff, there is a nonempty V ⊆ Support α f, with h •'' V disjoint from V - have ⟨V, V_open, x_in_V, V_in_support, disjoint_img_V⟩ := disjoint_nbhd_in (support_open f) x_in_supp_f hx_ne_x + have ⟨V, V_open, x_in_V, V_in_support, disjoint_img_V⟩ := disjoint_nbhd_in (support_isOpen f) x_in_supp_f hx_ne_x -- let f₂ be a nontrivial element of the RigidStabilizer G V let ⟨f₂, f₂_in_rist_V, f₂_ne_one⟩ := h_lm.get_nontrivial_rist_elem V_open (Set.nonempty_of_mem x_in_V) @@ -204,7 +205,7 @@ by have five_points : Function.Injective (fun i : Fin 5 => g^(i : ℤ) • x) := by apply moves_1234_of_moves_12 exact (Set.inter_subset_right _ _ x_in_U) - have U_open: IsOpen U := (IsOpen.inter (support_open f) (support_open (g^12))) + have U_open: IsOpen U := (IsOpen.inter (support_isOpen f) (support_isOpen (g^12))) let ⟨V₀, V₀_open, x_in_V₀, V₀_in_support, disjoint_img_V₀⟩ := disjoint_nbhd_in U_open x_in_U fx_moves let ⟨V₁, V₁_open, x_in_V₁, disjoint_img_V₁⟩ := disjoint_nbhd_fin five_points @@ -350,7 +351,7 @@ end AlgebraicDisjointness section RegularSupport lemma lemma_2_2 (G: Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] - [ContinuousMulAction G α] [FaithfulSMul G α] + [ContinuousConstSMul G α] [FaithfulSMul G α] [T2Space α] [h_lm : LocallyMoving G α] {U : Set α} (U_open : IsOpen U) (U_nonempty : Set.Nonempty U) : Monoid.exponent G•[U] = 0 := @@ -487,7 +488,7 @@ by -- we construct an open subset within `Support α h \ RegularSupport α f`, -- and we show that it is non-empty, open and (by construction) disjoint from `Support α f`. lemma open_set_from_supp_not_subset_rsupp {G α : Type _} - [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] [T2Space α] + [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] [T2Space α] {f h : G} (not_support_subset_rsupp : ¬Support α h ⊆ RegularSupport α f): ∃ V : Set α, V ⊆ Support α h ∧ Set.Nonempty V ∧ IsOpen V ∧ Disjoint V (Support α f) := by @@ -497,7 +498,7 @@ by rw [Set.diff_eq_compl_inter] apply IsOpen.inter · simp - · exact support_open _ + · exact support_isOpen _ have U_subset_supp_h : U ⊆ Support α h := by simp; apply Set.diff_subset have U_disj_supp_f : Disjoint U (Support α f) := by apply Set.disjoint_of_subset_right @@ -526,7 +527,7 @@ by apply subset_from_diff_closure_eq_empty · apply regularSupport_regular - · exact support_open _ + · exact support_isOpen _ · rw [Set.not_nonempty_iff_eq_empty] at U_empty exact U_empty @@ -543,7 +544,7 @@ by lemma proposition_2_1 {G α : Type _} - [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] [T2Space α] + [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] [T2Space α] [LocallyMoving G α] [h_faithful : FaithfulSMul G α] (f : G) : AlgebraicCentralizer f = G•[RegularSupport α f] := @@ -575,7 +576,7 @@ by exact interior_subset · rfl · rw [<-g_eq_g'] - exact Disjoint.closure_left supp_disj (support_open _) + exact Disjoint.closure_left supp_disj (support_isOpen _) } intro h_in_centralizer @@ -630,7 +631,7 @@ by -- Small lemma for remark 2.3 theorem rigidStabilizer_inter_bot_iff_regularSupport_disj {G α : Type _} - [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] [LocallyMoving G α] [FaithfulSMul G α] + [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] [LocallyMoving G α] [FaithfulSMul G α] {f g : G} : G•[RegularSupport α f] ⊓ G•[RegularSupport α g] = ⊥ ↔ Disjoint (RegularSupport α f) (RegularSupport α g) := @@ -670,7 +671,7 @@ by variable {G α : Type _} variable [Group G] variable [TopologicalSpace α] [T2Space α] -variable [MulAction G α] [ContinuousMulAction G α] [FaithfulSMul G α] [LocallyMoving G α] +variable [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyMoving G α] /-- This demonstrates that the disjointness of the supports of two elements `f` and `g` @@ -685,7 +686,7 @@ lemma remark_2_3 {f g : G} : (AlgebraicCentralizer f) ⊓ (AlgebraicCentralizer g) = ⊥ → Disjoint (Support α f) (Support α g) := by intro alg_disj - rw [disjoint_interiorClosure_iff (support_open _) (support_open _)] + rw [disjoint_interiorClosure_iff (support_isOpen _) (support_isOpen _)] simp repeat rw [<-RegularSupport.def] rw [<-rigidStabilizer_inter_bot_iff_regularSupport_disj] @@ -738,7 +739,7 @@ section HomeoGroup open Topology variable {G α : Type _} [Group G] [TopologicalSpace α] [T2Space α] -variable [MulAction G α] [ContinuousMulAction G α] [FaithfulSMul G α] [LocallyMoving G α] +variable [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyMoving G α] example : TopologicalSpace G := TopologicalSpace.generateFrom (RigidStabilizerBasis.asSets G α) @@ -772,7 +773,7 @@ section Ultrafilter variable {G α : Type _} variable [Group G] variable [TopologicalSpace α] [T2Space α] -variable [MulAction G α] [ContinuousMulAction G α] [FaithfulSMul G α] [LocallyMoving G α] +variable [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyMoving G α] def RSuppSubsets {α : Type _} [TopologicalSpace α] (V : Set α) : Set (Set α) := {W ∈ RegularSupportBasis.asSet α | W ⊆ V} @@ -801,7 +802,7 @@ by lemma compact_subset_of_rsupp_basis (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] [T2Space α] - [MulAction G α] [ContinuousMulAction G α] + [MulAction G α] [ContinuousConstSMul G α] [LocallyCompactSpace α] [HasNoIsolatedPoints α] [LocallyDense G α] (U : RegularSupportBasis α): ∃ V : RegularSupportBasis α, (closure V.val) ⊆ U.val ∧ IsCompact (closure V.val) := @@ -1018,7 +1019,7 @@ end Ultrafilter variable {G α : Type _} variable [Group G] -variable [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] +variable [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] def IsRigidSubgroup (S : Set G) := S ≠ {1} ∧ ∃ T : Finset G, S = ⨅ (f ∈ T), AlgebraicCentralizer f @@ -1085,7 +1086,7 @@ theorem IsRigidSubgroup.algebraicCentralizerBasis_val {S : Set G} (S_rigid : IsR section toRegularSupportBasis variable (α : Type _) -variable [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] +variable [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] variable [FaithfulSMul G α] [T2Space α] [LocallyMoving G α] theorem IsRigidSubgroup.has_regularSupportBasis {S : Set G} (S_rigid : IsRigidSubgroup S) : @@ -1204,7 +1205,7 @@ section Equivalence open Topology variable (α : Type _) -variable [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] +variable [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] variable [FaithfulSMul G α] [T2Space α] [LocallyMoving G α] -- TODO: either see whether we actually need this step, or change these names to something memorable @@ -1383,7 +1384,7 @@ def RubinSpace (G : Type _) [Group G] := Quotient (RubinFilterSetoid G) variable {β : Type _} -variable [TopologicalSpace β] [MulAction G β] [ContinuousMulAction G β] +variable [TopologicalSpace β] [MulAction G β] [ContinuousConstSMul G β] instance : TopologicalSpace (RubinSpace G) := sorry diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean index 9f2af07..d273126 100644 --- a/Rubin/AlgebraicDisjointness.lean +++ b/Rubin/AlgebraicDisjointness.lean @@ -3,6 +3,7 @@ import Mathlib.GroupTheory.Subgroup.Basic import Mathlib.GroupTheory.Subgroup.Actions import Mathlib.GroupTheory.Commutator import Mathlib.Topology.Basic +import Mathlib.Topology.Algebra.ConstMulAction import Mathlib.Data.Fintype.Perm import Mathlib.Tactic.FinCases import Mathlib.Tactic.IntervalCases @@ -123,7 +124,7 @@ variable {G α : Type _} variable [Group G] variable [TopologicalSpace α] variable [MulAction G α] -variable [ContinuousMulAction G α] +variable [ContinuousConstSMul G α] variable [FaithfulSMul G α] -- Kind of a boring lemma but okay diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean index af73378..6d16930 100644 --- a/Rubin/HomeoGroup.lean +++ b/Rubin/HomeoGroup.lean @@ -1,6 +1,7 @@ import Mathlib.Logic.Equiv.Defs import Mathlib.Topology.Basic import Mathlib.Topology.Homeomorph +import Mathlib.Topology.Algebra.ConstMulAction import Rubin.LocallyDense import Rubin.Topology @@ -119,8 +120,8 @@ instance homeoGroup_mulAction₁ : MulAction (HomeoGroup α) α where intro f g x rfl -instance homeoGroup_mulAction₁_continuous : Rubin.ContinuousMulAction (HomeoGroup α) α where - continuous := by +instance homeoGroup_mulAction₁_continuous : ContinuousConstSMul (HomeoGroup α) α where + continuous_const_smul := by intro h constructor intro S S_open @@ -143,24 +144,21 @@ instance homeoGroup_mulAction₁_faithful : FaithfulSMul (HomeoGroup α) α wher theorem HomeoGroup.smulImage_eq_image (g : HomeoGroup α) (S : Set α) : g •'' S = ⇑g.toHomeomorph '' S := rfl -section ContinuousMulActionCoe +section FromContinuousConstSMul variable {G : Type _} [Group G] -variable [MulAction G α] [Rubin.ContinuousMulAction G α] +variable [MulAction G α] [ContinuousConstSMul G α] /-- `fromContinuous` is a structure-preserving transformation from a continuous `MulAction` to a `HomeoGroup` --/ -def HomeoGroup.fromContinuous (α : Type _) [TopologicalSpace α] [MulAction G α] [Rubin.ContinuousMulAction G α] +def HomeoGroup.fromContinuous (α : Type _) [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] (g : G) : HomeoGroup α := - HomeoGroup.from (Rubin.ContinuousMulAction.toHomeomorph α g) + HomeoGroup.from (Homeomorph.smul g) @[simp] theorem HomeoGroup.fromContinuous_def (g : G) : - HomeoGroup.from (Rubin.ContinuousMulAction.toHomeomorph α g) = HomeoGroup.fromContinuous α g := rfl - --- instance homeoGroup_coe_fromContinuous : Coe G (HomeoGroup α) where --- coe := fun g => HomeoGroup.fromContinuous α g + HomeoGroup.from (Homeomorph.smul g) = HomeoGroup.fromContinuous α g := rfl @[simp] theorem HomeoGroup.fromContinuous_smul (g : G) : @@ -169,7 +167,7 @@ by intro x unfold fromContinuous rw [<-HomeoGroup.smul₁_def', HomeoGroup.from_toHomeomorph] - unfold Rubin.ContinuousMulAction.toHomeomorph + unfold Homeomorph.smul simp theorem HomeoGroup.fromContinuous_one : @@ -216,7 +214,8 @@ by repeat rw [Rubin.mem_support] rw [<-HomeoGroup.smul₁_def, <-HomeoGroup.fromContinuous_def] rw [HomeoGroup.from_toHomeomorph] - rw [Rubin.ContinuousMulAction.toHomeomorph_toFun] + rw [Homeomorph.smul] + simp only [Equiv.toFun_as_coe, MulAction.toPerm_apply] @[simp] theorem HomeoGroup.fromContinuous_regularSupport (g : G) : @@ -232,7 +231,7 @@ by repeat rw [Rubin.smulImage_def] simp -def HomeoGroup.fromContinuous_embedding (α : Type _) [TopologicalSpace α] [MulAction G α] [Rubin.ContinuousMulAction G α] [FaithfulSMul G α]: G ↪ (HomeoGroup α) where +def HomeoGroup.fromContinuous_embedding (α : Type _) [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α]: G ↪ (HomeoGroup α) where toFun := fun (g : G) => HomeoGroup.fromContinuous α g inj' := by intro g h fromCont_eq @@ -245,7 +244,7 @@ def HomeoGroup.fromContinuous_embedding (α : Type _) [TopologicalSpace α] [Mul theorem HomeoGroup.fromContinuous_embedding_toFun [FaithfulSMul G α] (g : G): HomeoGroup.fromContinuous_embedding α g = HomeoGroup.fromContinuous α g := rfl -def HomeoGroup.fromContinuous_monoidHom (α : Type _) [TopologicalSpace α] [MulAction G α] [Rubin.ContinuousMulAction G α] [FaithfulSMul G α]: G →* (HomeoGroup α) where +def HomeoGroup.fromContinuous_monoidHom (α : Type _) [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α]: G →* (HomeoGroup α) where toFun := fun (g : G) => HomeoGroup.fromContinuous α g map_one' := by simp @@ -255,120 +254,4 @@ def HomeoGroup.fromContinuous_monoidHom (α : Type _) [TopologicalSpace α] [Mul intros rw [fromContinuous_mul] --- theorem HomeoGroup.fromContinuous_rigidStabilizer (U : Set α) [FaithfulSMul G α]: --- Rubin.RigidStabilizer (HomeoGroup α) U = Subgroup.map (HomeoGroup.fromContinuous_monoidHom α) (Rubin.RigidStabilizer G U) := --- by --- ext g --- rw [<-Subgroup.mem_carrier] --- unfold Rubin.RigidStabilizer --- simp --- sorry - -end ContinuousMulActionCoe - -namespace Rubin - -section Other - --- TODO: move this somewhere else -/-- -## Proposition 3.1 ---/ -theorem rigidStabilizer_subset_iff (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] - [MulAction G α] [ContinuousMulAction G α] [FaithfulSMul G α] - [h_lm : LocallyMoving G α] - {U V : Set α} (U_reg : Regular U) (V_reg : Regular V): - U ⊆ V ↔ RigidStabilizer G U ≤ RigidStabilizer G V := -by - constructor - exact rigidStabilizer_mono - intro rist_ss - - by_contra U_not_ss_V - - let W := U \ closure V - have W_nonempty : Set.Nonempty W := by - by_contra W_empty - apply U_not_ss_V - apply subset_from_diff_closure_eq_empty - · assumption - · exact U_reg.isOpen - · rw [Set.not_nonempty_iff_eq_empty] at W_empty - exact W_empty - have W_ss_U : W ⊆ U := by - simp - exact Set.diff_subset _ _ - have W_open : IsOpen W := by - unfold_let - rw [Set.diff_eq_compl_inter] - apply IsOpen.inter - simp - exact U_reg.isOpen - - have ⟨f, f_in_ristW, f_ne_one⟩ := h_lm.get_nontrivial_rist_elem W_open W_nonempty - - have f_in_ristU : f ∈ RigidStabilizer G U := by - exact rigidStabilizer_mono W_ss_U f_in_ristW - - have f_notin_ristV : f ∉ RigidStabilizer G V := by - apply rigidStabilizer_compl f_ne_one - apply rigidStabilizer_mono _ f_in_ristW - calc - W = U ∩ (closure V)ᶜ := by unfold_let; rw [Set.diff_eq_compl_inter, Set.inter_comm] - _ ⊆ (closure V)ᶜ := Set.inter_subset_right _ _ - _ ⊆ Vᶜ := by - rw [Set.compl_subset_compl] - exact subset_closure - - exact f_notin_ristV (rist_ss f_in_ristU) - -theorem rigidStabilizer_eq_iff (G : Type _) [Group G] {α : Type _} [TopologicalSpace α] - [MulAction G α] [ContinuousMulAction G α] [FaithfulSMul G α] [LocallyMoving G α] - {U V : Set α} (U_reg : Regular U) (V_reg : Regular V): - RigidStabilizer G U = RigidStabilizer G V ↔ U = V := -by - constructor - · intro rist_eq - apply le_antisymm <;> simp only [Set.le_eq_subset] - all_goals { - rw [rigidStabilizer_subset_iff G] <;> try assumption - rewrite [rist_eq] - rfl - } - · intro H_eq - rw [H_eq] - -theorem homeoGroup_rigidStabilizer_subset_iff {α : Type _} [TopologicalSpace α] - [h_lm : LocallyMoving (HomeoGroup α) α] - {U V : Set α} (U_reg : Regular U) (V_reg : Regular V): - U ⊆ V ↔ RigidStabilizer (HomeoGroup α) U ≤ RigidStabilizer (HomeoGroup α) V := -by - rw [rigidStabilizer_subset_iff (HomeoGroup α) U_reg V_reg] - -theorem homeoGroup_rigidStabilizer_eq_iff {α : Type _} [TopologicalSpace α] - [LocallyMoving (HomeoGroup α) α] - {U V : Set α} (U_reg : Regular U) (V_reg : Regular V): - RigidStabilizer (HomeoGroup α) U = RigidStabilizer (HomeoGroup α) V ↔ U = V := -by - constructor - · intro rist_eq - apply le_antisymm <;> simp only [Set.le_eq_subset] - all_goals { - rw [homeoGroup_rigidStabilizer_subset_iff] <;> try assumption - rewrite [rist_eq] - rfl - } - · intro H_eq - rw [H_eq] - -theorem homeoGroup_rigidStabilizer_injective {α : Type _} [TopologicalSpace α] [LocallyMoving (HomeoGroup α) α] - : Function.Injective (fun U : { S : Set α // Regular S } => RigidStabilizer (HomeoGroup α) U.val) := -by - intro ⟨U, U_reg⟩ - intro ⟨V, V_reg⟩ - simp - exact (homeoGroup_rigidStabilizer_eq_iff U_reg V_reg).mp - -end Other - -end Rubin +end FromContinuousConstSMul diff --git a/Rubin/InteriorClosure.lean b/Rubin/InteriorClosure.lean index 90fa5ea..ecfc0dc 100644 --- a/Rubin/InteriorClosure.lean +++ b/Rubin/InteriorClosure.lean @@ -226,21 +226,15 @@ Set.Finite.induction_on' S_finite (by simp) (by · exact IH ) -theorem interiorClosure_smulImage' {G : Type _} [Group G] [MulAction G α] - (g : G) (U : Set α) - (g_continuous : ∀ S : Set α, IsOpen S → IsOpen (g •'' S) ∧ IsOpen (g⁻¹ •'' S)) : +theorem interiorClosure_smulImage {G : Type _} [Group G] [MulAction G α] [ContinuousConstSMul G α] + (g : G) (U : Set α) : InteriorClosure (g •'' U) = g •'' InteriorClosure U := by simp - rw [<-smulImage_interior' _ _ g_continuous] - rw [<-smulImage_closure' _ _ g_continuous] - -theorem interiorClosure_smulImage {G : Type _} [Group G] [MulAction G α] [ContinuousMulAction G α] - (g : G) (U : Set α) : - InteriorClosure (g •'' U) = g •'' InteriorClosure U := - interiorClosure_smulImage' g U (continuousMulAction_elem_continuous α g) + rw [<-smulImage_interior] + rw [<-smulImage_closure] -theorem smulImage_regular {G : Type _} [Group G] [MulAction G α] [ContinuousMulAction G α] +theorem smulImage_regular {G : Type _} [Group G] [MulAction G α] [ContinuousConstSMul G α] (g : G) (U : Set α) : Regular U ↔ Regular (g •'' U) := by diff --git a/Rubin/LocallyDense.lean b/Rubin/LocallyDense.lean index 320dac6..1b7a534 100644 --- a/Rubin/LocallyDense.lean +++ b/Rubin/LocallyDense.lean @@ -1,8 +1,10 @@ import Mathlib.GroupTheory.Subgroup.Basic import Mathlib.GroupTheory.GroupAction.Basic import Mathlib.Topology.Basic +import Mathlib.Topology.Algebra.ConstMulAction import Rubin.RigidStabilizer +import Rubin.InteriorClosure namespace Rubin @@ -121,7 +123,7 @@ variable {G α : Type _} variable [Group G] variable [TopologicalSpace α] variable [MulAction G α] -variable [ContinuousMulAction G α] +variable [ContinuousConstSMul G α] variable [FaithfulSMul G α] instance dense_locally_moving [T2Space α] @@ -143,10 +145,8 @@ by let U := (g⁻¹ •'' V) ∩ W use U constructor - { - -- NOTE: if this is common, then we should make a tactic for solving IsOpen goals - exact IsOpen.inter (img_open_open g⁻¹ V V_open) W_open - } + exact IsOpen.inter (smulImage_isOpen g⁻¹ V_open) W_open + constructor { simp @@ -192,5 +192,79 @@ by exact Set.inter_subset_left _ _ · exact disjoint_W_img +/-- +## Proposition 3.1: + +If a group action is faithful, continuous and "locally moving", +then `U ⊆ V` if and only if `G•[U] ≤ G•[V]` when `U` and `V` are regular. +--/ +theorem rigidStabilizer_subset_iff (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] + [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] + [h_lm : LocallyMoving G α] + {U V : Set α} (U_reg : Regular U) (V_reg : Regular V): + U ⊆ V ↔ G•[U] ≤ G•[V] := +by + constructor + exact rigidStabilizer_mono + intro rist_ss + + by_contra U_not_ss_V + + let W := U \ closure V + have W_nonempty : Set.Nonempty W := by + by_contra W_empty + apply U_not_ss_V + apply subset_from_diff_closure_eq_empty + · assumption + · exact U_reg.isOpen + · rw [Set.not_nonempty_iff_eq_empty] at W_empty + exact W_empty + have W_ss_U : W ⊆ U := by + simp + exact Set.diff_subset _ _ + have W_open : IsOpen W := by + unfold_let + rw [Set.diff_eq_compl_inter] + apply IsOpen.inter + simp + exact U_reg.isOpen + + have ⟨f, f_in_ristW, f_ne_one⟩ := h_lm.get_nontrivial_rist_elem W_open W_nonempty + + have f_in_ristU : f ∈ RigidStabilizer G U := by + exact rigidStabilizer_mono W_ss_U f_in_ristW + + have f_notin_ristV : f ∉ RigidStabilizer G V := by + apply rigidStabilizer_compl f_ne_one + apply rigidStabilizer_mono _ f_in_ristW + calc + W = U ∩ (closure V)ᶜ := by unfold_let; rw [Set.diff_eq_compl_inter, Set.inter_comm] + _ ⊆ (closure V)ᶜ := Set.inter_subset_right _ _ + _ ⊆ Vᶜ := by + rw [Set.compl_subset_compl] + exact subset_closure + + exact f_notin_ristV (rist_ss f_in_ristU) + +/-- +A corollary of the previous theorem is that the rigid stabilizers of two regular sets `U` and `V` +are equal if and only if `U = V`. +--/ +theorem rigidStabilizer_eq_iff (G : Type _) [Group G] {α : Type _} [TopologicalSpace α] + [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyMoving G α] + {U V : Set α} (U_reg : Regular U) (V_reg : Regular V): + G•[U] = G•[V] ↔ U = V := +by + constructor + · intro rist_eq + apply le_antisymm <;> simp only [Set.le_eq_subset] + all_goals { + rw [rigidStabilizer_subset_iff G] <;> try assumption + rewrite [rist_eq] + rfl + } + · intro H_eq + rw [H_eq] + end Rubin diff --git a/Rubin/RegularSupport.lean b/Rubin/RegularSupport.lean index 1baa147..db9045b 100644 --- a/Rubin/RegularSupport.lean +++ b/Rubin/RegularSupport.lean @@ -48,13 +48,13 @@ variable {G α : Type _} variable [Group G] variable [TopologicalSpace α] variable [MulAction G α] -variable [ContinuousMulAction G α] +variable [ContinuousConstSMul G α] theorem support_subset_regularSupport [T2Space α] {g : G} : Support α g ⊆ RegularSupport α g := by apply interiorClosure_subset - apply support_open (α := α) (g := g) + apply support_isOpen (α := α) (g := g) #align support_in_regular_support Rubin.support_subset_regularSupport theorem regularSupport_subset {g : G} {U : Set α} : diff --git a/Rubin/RegularSupportBasis.lean b/Rubin/RegularSupportBasis.lean index 7c01623..ad8de1f 100644 --- a/Rubin/RegularSupportBasis.lean +++ b/Rubin/RegularSupportBasis.lean @@ -5,6 +5,7 @@ made up of finite intersections of `RegularSupport α g` for `g : HomeoGroup α` import Mathlib.Topology.Basic import Mathlib.Topology.Homeomorph +import Mathlib.Topology.Algebra.ConstMulAction import Rubin.LocallyDense import Rubin.Topology @@ -349,7 +350,7 @@ open Topology variable (G α : Type _) variable [Group G] variable [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] [HasNoIsolatedPoints α] -variable [MulAction G α] [LocallyDense G α] [ContinuousMulAction G α] +variable [MulAction G α] [LocallyDense G α] [ContinuousConstSMul G α] -- TODO: clean this lemma to not mention W anymore? lemma proposition_3_2_subset diff --git a/Rubin/RigidStabilizerBasis.lean b/Rubin/RigidStabilizerBasis.lean index 9c4de6f..6b41dea 100644 --- a/Rubin/RigidStabilizerBasis.lean +++ b/Rubin/RigidStabilizerBasis.lean @@ -113,7 +113,7 @@ by unfold asSets RigidStabilizerBasis simp -variable [ContinuousMulAction G α] +variable [ContinuousConstSMul G α] lemma RigidStabilizerBasis.smulImage_mem₀ {H : Subgroup G} (H_in_ristBasis : H ∈ RigidStabilizerBasis G α) (f : G) : ((fun g => f * g * f⁻¹) '' H.carrier) ∈ RigidStabilizerBasis.asSets G α := @@ -183,8 +183,7 @@ by exact y_in_H def RigidStabilizerBasisMul (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α] - [ContinuousMulAction G α] (f : G) (H : Subgroup G) - : Subgroup G + [ContinuousConstSMul G α] (f : G) (H : Subgroup G) : Subgroup G where carrier := (fun g => f * g * f⁻¹) '' H.carrier mul_mem' := by diff --git a/Rubin/SmulImage.lean b/Rubin/SmulImage.lean index 97b325f..8ca0819 100644 --- a/Rubin/SmulImage.lean +++ b/Rubin/SmulImage.lean @@ -341,24 +341,15 @@ by exact h_notin_V #align distinct_images_from_disjoint Rubin.smulImage_distinct_of_disjoint_pow -theorem continuousMulAction_elem_continuous {G : Type _} (α : Type _) - [Group G] [TopologicalSpace α] [MulAction G α] [hc : ContinuousMulAction G α] (g : G): - ∀ (S : Set α), IsOpen S → IsOpen (g •'' S) ∧ IsOpen ((g⁻¹) •'' S) := -by - intro S S_open - repeat rw [smulImage_eq_inv_preimage] - rw [inv_inv] - constructor - · exact (hc.continuous g⁻¹).isOpen_preimage _ S_open - · exact (hc.continuous g).isOpen_preimage _ S_open - theorem smulImage_isOpen {G α : Type _} - [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] (g : G) + [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] (g : G) {S : Set α} (S_open : IsOpen S) : IsOpen (g •'' S) := - (continuousMulAction_elem_continuous α g S S_open).left +by + rw [smulImage_eq_inv_preimage] + exact (continuous_id.const_smul g⁻¹).isOpen_preimage S S_open theorem smulImage_isClosed {G α : Type _} - [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] (g : G) + [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] (g : G) {S : Set α} (S_open : IsClosed S) : IsClosed (g •'' S) := by rw [<-isOpen_compl_iff] @@ -367,9 +358,8 @@ by apply smulImage_isOpen assumption -theorem smulImage_interior' {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] - (g : G) (U : Set α) - (g_continuous : ∀ S : Set α, IsOpen S → IsOpen (g •'' S) ∧ IsOpen (g⁻¹ •'' S)): +theorem smulImage_interior {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] + [hc : ContinuousConstSMul G α] (g : G) (U : Set α) : interior (g •'' U) = g •'' interior U := by unfold interior @@ -381,7 +371,7 @@ by · intro ⟨T, ⟨T_open, T_sub⟩, x_in_T⟩ use g⁻¹ •'' T repeat' apply And.intro - · exact (g_continuous T T_open).right + · exact smulImage_isOpen g⁻¹ T_open · rw [smulImage_subset_inv] rw [inv_inv] exact T_sub @@ -390,27 +380,15 @@ by · intro ⟨T, ⟨T_open, T_sub⟩, x_in_T⟩ use g •'' T repeat' apply And.intro - · exact (g_continuous T T_open).left + · exact smulImage_isOpen g T_open · apply smulImage_mono exact T_sub · exact x_in_T -theorem smulImage_interior {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] - [ContinuousMulAction G α] (g : G) (U : Set α) : - interior (g •'' U) = g •'' interior U := - smulImage_interior' g U (continuousMulAction_elem_continuous α g) - -theorem smulImage_closure' {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] - (g : G) (U : Set α) - (g_continuous : ∀ S : Set α, IsOpen S → IsOpen (g •'' S) ∧ IsOpen (g⁻¹ •'' S)): +theorem smulImage_closure {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] + [ContinuousConstSMul G α] (g : G) (U : Set α) : closure (g •'' U) = g •'' closure U := by - have g_continuous' : ∀ S : Set α, IsClosed S → IsClosed (g •'' S) ∧ IsClosed (g⁻¹ •'' S) := by - intro S S_closed - rw [<-isOpen_compl_iff] at S_closed - repeat rw [<-isOpen_compl_iff] - repeat rw [smulImage_compl] - exact g_continuous _ S_closed unfold closure rw [smulImage_sInter] simp @@ -421,21 +399,16 @@ by rw [<-T'_eq] clear T' T'_eq apply IH - · exact (g_continuous' _ T_closed).left + · exact smulImage_isClosed g T_closed · apply smulImage_mono exact U_ss_T · intro IH T T_closed gU_ss_T apply IH - · exact (g_continuous' _ T_closed).right + · exact smulImage_isClosed g⁻¹ T_closed · rw [<-smulImage_subset_inv] exact gU_ss_T · simp -theorem smulImage_closure {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] - [ContinuousMulAction G α] (g : G) (U : Set α) : - closure (g •'' U) = g •'' closure U := - smulImage_closure' g U (continuousMulAction_elem_continuous α g) - section Filters open Topology @@ -521,7 +494,7 @@ by variable [TopologicalSpace α] -theorem smulFilter_nhds (g : G) (p : α) [ContinuousMulAction G α]: +theorem smulFilter_nhds (g : G) (p : α) [ContinuousConstSMul G α]: g •ᶠ 𝓝 p = 𝓝 (g • p) := by ext S @@ -545,7 +518,7 @@ by · rw [mem_smulImage, inv_inv] assumption -theorem smulFilter_clusterPt (g : G) (F : Filter α) (x : α) [ContinuousMulAction G α] : +theorem smulFilter_clusterPt (g : G) (F : Filter α) (x : α) [ContinuousConstSMul G α] : ClusterPt x (g •ᶠ F) ↔ ClusterPt (g⁻¹ • x) F := by suffices ∀ (g : G) (F : Filter α) (x : α), ClusterPt x (g •ᶠ F) → ClusterPt (g⁻¹ • x) F by @@ -571,7 +544,7 @@ by rw [inv_inv, smulImage_mul, mul_left_inv, one_smulImage] assumption -theorem smulImage_compact [ContinuousMulAction G α] (g : G) {U : Set α} (U_compact : IsCompact U) : +theorem smulImage_compact [ContinuousConstSMul G α] (g : G) {U : Set α} (U_compact : IsCompact U) : IsCompact (g •'' U) := by intro F F_neBot F_le_principal diff --git a/Rubin/Support.lean b/Rubin/Support.lean index 931d300..aa880f2 100644 --- a/Rubin/Support.lean +++ b/Rubin/Support.lean @@ -3,6 +3,7 @@ import Mathlib.GroupTheory.Commutator import Mathlib.GroupTheory.Subgroup.Basic import Mathlib.GroupTheory.GroupAction.Basic import Mathlib.Topology.Basic +import Mathlib.Topology.Algebra.ConstMulAction import Rubin.MulActionExt import Rubin.SmulImage @@ -381,17 +382,9 @@ variable {G α : Type _} variable [Group G] variable [TopologicalSpace α] variable [MulAction G α] -variable [ContinuousMulAction G α] +variable [ContinuousConstSMul G α] -theorem img_open_open (g : G) (U : Set α) (h : IsOpen U): IsOpen (g •'' U) := - by - rw [Rubin.smulImage_eq_inv_preimage] - exact Continuous.isOpen_preimage (Rubin.ContinuousMulAction.continuous g⁻¹) U h - -#align img_open_open Rubin.img_open_open - -theorem support_open (g : G) [T2Space α]: IsOpen (Support α g) := - by +theorem support_isOpen (g : G) [T2Space α]: IsOpen (Support α g) := by apply isOpen_iff_forall_mem_open.mpr intro x xmoved rcases T2Space.t2 (g • x) x xmoved with ⟨U, V, open_U, open_V, gx_in_U, x_in_V, disjoint_U_V⟩ @@ -401,10 +394,9 @@ theorem support_open (g : G) [T2Space α]: IsOpen (Support α g) := disjoint_U_V (mem_inv_smulImage.mp (Set.mem_of_mem_inter_right yW)) (Set.mem_of_mem_inter_left yW), - IsOpen.inter open_V (Rubin.img_open_open g⁻¹ U open_U), + IsOpen.inter open_V (smulImage_isOpen g⁻¹ open_U), ⟨x_in_V, mem_inv_smulImage.mpr gx_in_U⟩ ⟩ -#align support_open Rubin.support_open end Continuous diff --git a/Rubin/Topology.lean b/Rubin/Topology.lean index e26c0b5..ee1990f 100644 --- a/Rubin/Topology.lean +++ b/Rubin/Topology.lean @@ -2,48 +2,13 @@ import Mathlib.GroupTheory.Subgroup.Basic import Mathlib.GroupTheory.GroupAction.Basic import Mathlib.Topology.Basic import Mathlib.Topology.Homeomorph +import Mathlib.Topology.Algebra.ConstMulAction import Mathlib.Data.Set.Basic import Rubin.MulActionExt namespace Rubin -/-- -Specificies that a group action is continuous, that is, for every group element `g`, `x ↦ g • x` is continuous. - -Note that this is a weaker statement than `ContinuousSMul`, as the group `G` is not required to be a topology. ---/ -class ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] where - continuous : ∀ g : G, Continuous (fun x: α => g • x) -#align continuous_mul_action Rubin.ContinuousMulAction - -def ContinuousMulAction.toHomeomorph {G : Type _} (α : Type _) - [Group G] [TopologicalSpace α] [MulAction G α] [hc : ContinuousMulAction G α] - (g : G) : Homeomorph α α -where - toFun := fun x => g • x - invFun := fun x => g⁻¹ • x - left_inv := by - intro y - simp - right_inv := by - intro y - simp - continuous_toFun := by - simp - exact hc.continuous _ - continuous_invFun := by - simp - exact hc.continuous _ - -theorem ContinuousMulAction.toHomeomorph_toFun {G : Type _} (α : Type _) - [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] - (g : G) : (ContinuousMulAction.toHomeomorph α g).toFun = fun x => g • x := rfl - -theorem ContinuousMulAction.toHomeomorph_invFun {G : Type _} (α : Type _) - [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] - (g : G) : (ContinuousMulAction.toHomeomorph α g).invFun = fun x => g⁻¹ • x := rfl - -- TODO: give this a notation? -- TODO: coe to / extend MulActionHom structure EquivariantHomeomorph (G α β : Type _) [Group G] [TopologicalSpace α]