From a87dc079d66507e3d68f305aa7e48655856870e3 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Thu, 21 Dec 2023 19:18:55 +0100 Subject: [PATCH] :poop: Messy draft code to work towards the end of the proof I need to change a bunch of things kind of everywhere and clean everything up before continuing --- README.md | 5 +- Rubin.lean | 385 ++++++++++++++++++++++++++++++- Rubin/AlgebraicDisjointness.lean | 49 +++- Rubin/HomeoGroup.lean | 67 +++++- Rubin/InteriorClosure.lean | 15 ++ Rubin/RegularSupport.lean | 25 ++ Rubin/RigidStabilizer.lean | 25 +- Rubin/Support.lean | 17 +- Rubin/Tactic.lean | 24 +- Rubin/Topology.lean | 7 +- 10 files changed, 576 insertions(+), 43 deletions(-) diff --git a/README.md b/README.md index ba5520c..9f3407e 100644 --- a/README.md +++ b/README.md @@ -1,8 +1,9 @@ # Lean4 port of the proof of Rubin's Theorem THis repository contains a (WIP) computer proof of Rubin's Theorem, -which states that two groups (which satisfy a few conditions) that act on a topological space have a homeomorphism between them, -such that the homeomorphism preserves the group structure. +which states that if a group acts on two topological spaces while satisfying enough conditions, +then there exists a homeomorphism between those two topological spaces, +such that the homeomorphism preserves the group structure of the group action. It is based on ["A short proof of Rubin's Theorem"](https://arxiv.org/abs/2203.05930) (James Belk, Luke Elliott and Franceso Matucci), and a good part of the computer proof was written in Lean 3 by [Laurent Bartholdi](https://www.math.uni-sb.de/ag/bartholdi/). diff --git a/Rubin.lean b/Rubin.lean index c2257b8..a0377d5 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -742,15 +742,6 @@ variable [MulAction G α] [ContinuousMulAction G α] [FaithfulSMul G α] [Locall example : TopologicalSpace G := TopologicalSpace.generateFrom (RigidStabilizerBasis.asSets G α) --- TODO: remove --- proposition_3_4_1 -example {α : Type _} [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] (F : Ultrafilter α) (p : α): - F ≤ 𝓝 p ↔ p ∈ ⋂ (S ∈ F), closure S := -by - rw [<-Ultrafilter.clusterPt_iff] - simp - exact clusterPt_iff_forall_mem_closure - theorem proposition_3_4_2 {α : Type _} [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] (F : Ultrafilter α): (∃ p : α, ClusterPt p F) ↔ ∃ S ∈ F, IsCompact (closure S) := by @@ -1024,13 +1015,385 @@ by end Ultrafilter -variable {G α β : Type _} +variable {G α : Type _} variable [Group G] variable [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] - [TopologicalSpace β] [MulAction G β] [ContinuousMulAction G β] + +def IsRigidSubgroup (S : Set G) := + S ≠ {1} ∧ ∃ T : Finset G, S = ⨅ (f ∈ T), AlgebraicCentralizer f + +def IsRigidSubgroup.toSubgroup {S : Set G} (S_rigid : IsRigidSubgroup S) : Subgroup G where + carrier := S + mul_mem' := by + let ⟨_, T, S_eq⟩ := S_rigid + simp only [S_eq, SetLike.mem_coe] + apply Subgroup.mul_mem + one_mem' := by + let ⟨_, T, S_eq⟩ := S_rigid + simp only [S_eq, SetLike.mem_coe] + apply Subgroup.one_mem + inv_mem' := by + let ⟨_, T, S_eq⟩ := S_rigid + simp only [S_eq, SetLike.mem_coe] + apply Subgroup.inv_mem + +theorem IsRigidSubgroup.mem_subgroup {S : Set G} (S_rigid : IsRigidSubgroup S) (g : G): + g ∈ S ↔ g ∈ S_rigid.toSubgroup := by rfl + +theorem IsRigidSubgroup.toSubgroup_neBot {S : Set G} (S_rigid : IsRigidSubgroup S) : + S_rigid.toSubgroup ≠ ⊥ := +by + intro eq_bot + rw [Subgroup.eq_bot_iff_forall] at eq_bot + simp only [<-mem_subgroup] at eq_bot + apply S_rigid.left + rw [Set.eq_singleton_iff_unique_mem] + constructor + · let ⟨S', S'_eq⟩ := S_rigid.right + rw [S'_eq, SetLike.mem_coe] + exact Subgroup.one_mem _ + · assumption + +lemma Subgroup.coe_eq (S T : Subgroup G) : + (S : Set G) = (T : Set G) ↔ S = T := +by + constructor + · intro h + ext x + repeat rw [<-Subgroup.mem_carrier] + have h₁ : ∀ S : Subgroup G, (S : Set G) = S.carrier := by intro h; rfl + repeat rw [h₁] at h + rw [h] + · intro h + rw [h] + +def IsRigidSubgroup.algebraicCentralizerBasis {S : Set G} (S_rigid : IsRigidSubgroup S) : AlgebraicCentralizerBasis G := ⟨ + S_rigid.toSubgroup, + by + rw [AlgebraicCentralizerBasis.mem_iff' _ (IsRigidSubgroup.toSubgroup_neBot S_rigid)] + let ⟨S', S'_eq⟩ := S_rigid.right + use S' + unfold AlgebraicCentralizerInter₀ + rw [<-Subgroup.coe_eq, <-S'_eq] + rfl +⟩ + +theorem IsRigidSubgroup.algebraicCentralizerBasis_val {S : Set G} (S_rigid : IsRigidSubgroup S) : + S_rigid.algebraicCentralizerBasis.val = S_rigid.toSubgroup := rfl + +section toRegularSupportBasis + +variable (α : Type _) +variable [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] +variable [FaithfulSMul G α] [T2Space α] [LocallyMoving G α] + +theorem IsRigidSubgroup.has_regularSupportBasis {S : Set G} (S_rigid : IsRigidSubgroup S) : + ∃ (U : RegularSupportBasis α), 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 + 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 + rw [rigidStabilizer_iInter_regularSupport'] + simp only [<-proposition_2_1] + +noncomputable def IsRigidSubgroup.toRegularSupportBasis {S : Set G} (S_rigid : IsRigidSubgroup S) : + RegularSupportBasis α +:= Exists.choose (IsRigidSubgroup.has_regularSupportBasis α S_rigid) + +theorem IsRigidSubgroup.toRegularSupportBasis_eq {S : Set G} (S_rigid : IsRigidSubgroup S): + G•[(S_rigid.toRegularSupportBasis α).val] = S := +by + exact Exists.choose_spec (IsRigidSubgroup.has_regularSupportBasis α S_rigid) + +theorem IsRigidSubgroup.toRegularSupportBasis_mono {S T : Set G} (S_rigid : IsRigidSubgroup S) + (T_rigid : IsRigidSubgroup T) : + S ⊆ T ↔ S_rigid.toRegularSupportBasis α ≤ T_rigid.toRegularSupportBasis α := +by + rw [RegularSupportBasis.le_def] + 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] := + by + simp + assumption + rw [IsRigidSubgroup.toRegularSupportBasis_eq (α := α) S_rigid] at Sr_ss_Tr' + rw [IsRigidSubgroup.toRegularSupportBasis_eq (α := α) T_rigid] at Sr_ss_Tr' + assumption + +theorem IsRigidSubgroup.toRegularSupportBasis_mono' {S T : Set G} (S_rigid : IsRigidSubgroup S) + (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 + +theorem IsRigidSubgroup.conj {U : Set G} (U_rigid : IsRigidSubgroup U) (g : G) : IsRigidSubgroup ((fun h => g * h * g⁻¹) '' U) := by + have conj_bijective : ∀ g : G, Function.Bijective (fun h => g * h * g⁻¹) := by + intro g + constructor + · intro x y; simp + · intro x + use g⁻¹ * x * g + group + + constructor + · intro H + apply U_rigid.left + have h₁ : (fun h => g * h * g⁻¹) '' {1} = {1} := by simp + rw [<-h₁] at H + apply (Set.image_eq_image (conj_bijective g).left).mp H + · let ⟨S, S_eq⟩ := U_rigid.right + have dec_eq : DecidableEq G := Classical.typeDecidableEq G + use Finset.image (fun h => g * h * g⁻¹) S + rw [S_eq] + simp + simp only [Set.image_iInter (conj_bijective _), AlgebraicCentralizer.conj] + +def AlgebraicSubsets (V : Set G) : Set (Subgroup G) := + {W ∈ AlgebraicCentralizerBasis G | W ≤ V} + +def AlgebraicOrbit (F : Ultrafilter G) (U : Set G) : Set (Subgroup G) := + { (W_rigid.conj g).toSubgroup | (g ∈ U) (W ∈ F) (W_rigid : IsRigidSubgroup W) } + +structure RubinFilter (G : Type _) [Group G] where + filter : Ultrafilter G + -- rigid_basis : ∀ S ∈ filter, ∃ T ⊆ S, IsRigidSubgroup T + converges : ∀ U ∈ filter, + IsRigidSubgroup U → + ∃ V : Set G, IsRigidSubgroup V ∧ V ⊆ U ∧ AlgebraicSubsets V ⊆ AlgebraicOrbit filter U + + -- Only really used to prove that ∀ S : Rigid, T : Rigid, S T ∈ F, S ∩ T : Rigid + ne_bot : {1} ∉ filter + +instance : Coe (RubinFilter G) (Ultrafilter G) where + coe := RubinFilter.filter + +section Equivalence +open Topology + +variable (α : Type _) +variable [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] +variable [FaithfulSMul G α] [T2Space α] [LocallyMoving G α] + +-- TODO: either see whether we actually need this step, or change these names to something memorable +-- This is an attempt to convert a RubinFilter G back to an Ultrafilter α +def RubinFilter.to_action_filter (F : RubinFilter G) : Filter α := + ⨅ (S : { S : Set G // S ∈ F.filter ∧ IsRigidSubgroup S }), (Filter.principal (S.prop.right.toRegularSupportBasis α)) + +instance RubinFilter.to_action_filter_neBot {F : RubinFilter G} [Nonempty α] : Filter.NeBot (F.to_action_filter α) := + by + unfold to_action_filter + rw [Filter.iInf_neBot_iff_of_directed] + · intro ⟨S, S_in_F, S_rigid⟩ + simp + · intro ⟨S, S_in_F, S_rigid⟩ ⟨T, T_in_F, T_rigid⟩ + simp + use S ∩ T + have ST_in_F : (S ∩ T) ∈ F.filter := by + rw [<-Ultrafilter.mem_coe] + apply Filter.inter_mem <;> assumption + have ST_subgroup : IsRigidSubgroup (S ∩ T) := by + constructor + swap + · let ⟨S_seed, S_eq⟩ := S_rigid.right + let ⟨T_seed, T_eq⟩ := T_rigid.right + have dec_eq : DecidableEq G := Classical.typeDecidableEq G + use S_seed ∪ T_seed + rw [Finset.iInf_union, S_eq, T_eq] + simp + · -- TODO: check if we can't prove this without using F.ne_bot; + -- we might be able to use convergence + intro ST_eq_bot + apply F.ne_bot + rw [<-ST_eq_bot] + exact ST_in_F + -- sorry + use ⟨ST_in_F, ST_subgroup⟩ + + repeat rw [<-IsRigidSubgroup.toRegularSupportBasis_mono' (α := α)] + constructor + exact Set.inter_subset_left S T + exact Set.inter_subset_right S T + +-- lemma RubinFilter.mem_to_action_filter' (F : RubinFilter G) (U : Set α) : +-- U ∈ F.to_action_filter α ↔ ∃ S : AlgebraicCentralizerBasis G, S.val ∈ F.filter, + +lemma RubinFilter.mem_to_action_filter (F : RubinFilter G) {U : Set G} (U_rigid : IsRigidSubgroup U) : + U ∈ F.filter ↔ (U_rigid.toRegularSupportBasis α : Set α) ∈ F.to_action_filter α := +by + unfold to_action_filter + constructor + · intro U_in_filter + apply Filter.mem_iInf_of_mem ⟨U, U_in_filter, U_rigid⟩ + intro x + simp + · sorry + +noncomputable def RubinFilter.to_action_ultrafilter (F : RubinFilter G) [Nonempty α]: Ultrafilter α := + Ultrafilter.of (F.to_action_filter α) + +theorem RubinFilter.to_action_ultrafilter_converges (F : RubinFilter G) [Nonempty α] [LocallyDense G α] [HasNoIsolatedPoints α] [LocallyCompactSpace α] {U : Set G} + (U_in_F : U ∈ F.filter) (U_rigid : IsRigidSubgroup U): + ∃ p ∈ (U_rigid.toRegularSupportBasis α).val, ClusterPt p (F.to_action_ultrafilter α) := +by + rw [proposition_3_5 (G := G)] + + let ⟨V, V_rigid, V_ss_U, algsubs_ss_algorb⟩ := F.converges U U_in_F U_rigid + let V' := V_rigid.toSubgroup + -- TODO: subst V' to simplify the proof? + + use V_rigid.toRegularSupportBasis α + constructor + { + rw [<-IsRigidSubgroup.toRegularSupportBasis_mono] + exact V_ss_U + } + + unfold RSuppSubsets RSuppOrbit + simp + intro S S_rsupp_basis S_ss_V + + 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_nonempty : Set.Nonempty S := by + let ⟨S', S'_eq⟩ := (RegularSupportBasis.mem_asSet S).mp S_rsupp_basis + rw [<-S'_eq] + exact S'.nonempty + + have GS_ss_V : G•[S] ≤ V := by + rw [<-V_rigid.toRegularSupportBasis_eq (α := α)] + simp + rw [<-rigidStabilizer_subset_iff G (α := α) S_regular (RegularSupportBasis.regular _)] + assumption + + -- TODO: show that G•[S] ∈ AlgebraicSubsets V + have GS_in_algsubs_V : G•[S] ∈ AlgebraicSubsets V := by + unfold AlgebraicSubsets + 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 + · 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 + + use g + constructor + { + rw [<-SetLike.mem_coe] + rw [U_rigid.toRegularSupportBasis_eq (α := α)] + assumption + } + + use W_rigid.toRegularSupportBasis α + constructor + · apply Ultrafilter.of_le + rw [<-RubinFilter.mem_to_action_filter] + assumption + · rw [<-rigidStabilizer_eq_iff G] + swap + { + rw [<-smulImage_regular (G := G)] + apply RegularSupportBasis.regular + } + swap + { + let ⟨S', S'_eq⟩ := (RegularSupportBasis.mem_asSet S).mp S_rsupp_basis + rw [<-S'_eq] + exact S'.regular + } + ext i + rw [rigidStabilizer_smulImage, <-Wconj_eq_GS, <-IsRigidSubgroup.mem_subgroup, <-SetLike.mem_coe, IsRigidSubgroup.toRegularSupportBasis_eq] + simp + constructor + · intro gig_in_W + use g⁻¹ * i * g + constructor; exact gig_in_W + group + · intro ⟨j, j_in_W, gjg_eq_i⟩ + rw [<-gjg_eq_i] + group + assumption + +end Equivalence + +-- TODO: prove that for every rubinfilter, there exists an associated ultrafilter on α that converges + +instance RubinFilterSetoid (G : Type _) [Group G] : Setoid (RubinFilter G) where + r F F' := ∀ (U : Set G), IsRigidSubgroup U → + ((∃ V : Set G, V ≤ U ∧ AlgebraicSubsets V ⊆ AlgebraicOrbit F U) + ↔ (∃ V' : Set G, V' ≤ U ∧ AlgebraicSubsets V' ⊆ AlgebraicOrbit F' U)) + iseqv := by + constructor + · intros + simp + · intro F F' h + intro U U_rigid + symm + exact h U U_rigid + · intro F₁ F₂ F₃ + intro h₁₂ h₂₃ + intro U U_rigid + specialize h₁₂ U U_rigid + specialize h₂₃ U U_rigid + exact Iff.trans h₁₂ h₂₃ + +def RubinSpace (G : Type _) [Group G] := Quotient (RubinFilterSetoid G) + +-- Topology can be generated from the disconnectedness of the filters + +variable {β : Type _} + +variable [TopologicalSpace β] [MulAction G β] [ContinuousMulAction G β] + + +instance : TopologicalSpace (RubinSpace G) := sorry + +instance : MulAction G (RubinSpace G) := sorry + +theorem rubin' (hα : RubinAction G α) : EquivariantHomeomorph G α (RubinSpace G) := by sorry 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 d99a500..9f2af07 100644 --- a/Rubin/AlgebraicDisjointness.lean +++ b/Rubin/AlgebraicDisjointness.lean @@ -149,7 +149,7 @@ lemma smul_inj_moves {ι : Type*} [Fintype ι] [T2Space α] apply i_ne_j apply f_smul_inj group_action - group_action at h + group at h exact h def smul_inj_nbhd {ι : Type*} [Fintype ι] [T2Space α] @@ -257,7 +257,7 @@ by unfold_let rw [h.1] rw [smul_eq_iff_eq_inv_smul] - group_action + group symm exact same_img } @@ -347,6 +347,51 @@ def AlgebraicSubgroup (f : G) : Set G := def AlgebraicCentralizer (f : G) : Subgroup G := Subgroup.centralizer (AlgebraicSubgroup f) +theorem AlgebraicSubgroup.conj (f g : G) : + (fun h => g * h * g⁻¹) '' AlgebraicSubgroup f = AlgebraicSubgroup (g * f * g⁻¹) := +by + unfold AlgebraicSubgroup + rw [Set.image_image] + have gxg12_eq : ∀ x : G, g * x^12 * g⁻¹ = (g * x * g⁻¹)^12 := by + simp + simp only [gxg12_eq] + ext x + sorry + -- unfold IsAlgebraicallyDisjoint + + +@[simp] +theorem AlgebraicCentralizer.conj (f g : G) : + (fun h => g * h * g⁻¹) '' AlgebraicCentralizer f = AlgebraicCentralizer (g * f * g⁻¹) := +by + unfold AlgebraicCentralizer + + ext x + simp [Subgroup.mem_centralizer_iff] + + constructor + · intro ⟨y, ⟨x_comm, x_eq⟩⟩ + intro h h_in_alg + rw [<-AlgebraicSubgroup.conj] at h_in_alg + simp at h_in_alg + let ⟨i, i_in_alg, gig_eq_h⟩ := h_in_alg + specialize x_comm i i_in_alg + rw [<-gig_eq_h, <-x_eq] + group + rw [mul_assoc _ i, x_comm, <-mul_assoc] + · intro x_comm + use g⁻¹ * x * g + group + simp + intro h h_in_alg + simp [<-AlgebraicSubgroup.conj] at x_comm + specialize x_comm h h_in_alg + have h₁ : g⁻¹ * x * g * h = g⁻¹ * (g * h * g⁻¹ * x) * g := by + rw [x_comm] + group + rw [h₁] + group + /-- Finite intersections of [`AlgebraicCentralizer`]. --/ diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean index ceaedb3..af73378 100644 --- a/Rubin/HomeoGroup.lean +++ b/Rubin/HomeoGroup.lean @@ -232,19 +232,53 @@ by repeat rw [Rubin.smulImage_def] simp +def HomeoGroup.fromContinuous_embedding (α : Type _) [TopologicalSpace α] [MulAction G α] [Rubin.ContinuousMulAction G α] [FaithfulSMul G α]: G ↪ (HomeoGroup α) where + toFun := fun (g : G) => HomeoGroup.fromContinuous α g + inj' := by + intro g h fromCont_eq + simp at fromCont_eq + apply FaithfulSMul.eq_of_smul_eq_smul (α := α) + intro x + rw [<-fromContinuous_smul, fromCont_eq, fromContinuous_smul] + +@[simp] +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 + toFun := fun (g : G) => HomeoGroup.fromContinuous α g + map_one' := by + simp + rw [fromContinuous_one] + map_mul' := by + simp + 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 homeoGroup_rigidStabilizer_subset_iff {α : Type _} [TopologicalSpace α] - [h_lm : LocallyMoving (HomeoGroup α) α] +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 (HomeoGroup α) U ≤ RigidStabilizer (HomeoGroup α) V := + U ⊆ V ↔ RigidStabilizer G U ≤ RigidStabilizer G V := by constructor exact rigidStabilizer_mono @@ -273,10 +307,10 @@ by have ⟨f, f_in_ristW, f_ne_one⟩ := h_lm.get_nontrivial_rist_elem W_open W_nonempty - have f_in_ristU : f ∈ RigidStabilizer (HomeoGroup α) U := by + have f_in_ristU : f ∈ RigidStabilizer G U := by exact rigidStabilizer_mono W_ss_U f_in_ristW - have f_notin_ristV : f ∉ RigidStabilizer (HomeoGroup α) V := by + have f_notin_ristV : f ∉ RigidStabilizer G V := by apply rigidStabilizer_compl f_ne_one apply rigidStabilizer_mono _ f_in_ristW calc @@ -288,6 +322,29 @@ by 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): diff --git a/Rubin/InteriorClosure.lean b/Rubin/InteriorClosure.lean index 7c0260e..90fa5ea 100644 --- a/Rubin/InteriorClosure.lean +++ b/Rubin/InteriorClosure.lean @@ -240,4 +240,19 @@ theorem interiorClosure_smulImage {G : Type _} [Group G] [MulAction G α] [Conti InteriorClosure (g •'' U) = g •'' InteriorClosure U := interiorClosure_smulImage' g U (continuousMulAction_elem_continuous α g) +theorem smulImage_regular {G : Type _} [Group G] [MulAction G α] [ContinuousMulAction G α] + (g : G) (U : Set α) : + Regular U ↔ Regular (g •'' U) := +by + suffices ∀ V : Set α, ∀ h : G, Regular V → Regular (h •'' V) by + constructor + apply this + have U_eq : g⁻¹ •'' (g •'' U) = U := by simp + nth_rw 2 [<-U_eq] + apply this + intro U g U_reg + unfold Regular + rw [interiorClosure_smulImage] + rw [U_reg] + end Rubin diff --git a/Rubin/RegularSupport.lean b/Rubin/RegularSupport.lean index a3541c9..1baa147 100644 --- a/Rubin/RegularSupport.lean +++ b/Rubin/RegularSupport.lean @@ -100,6 +100,31 @@ by rw [support_conjugate] rw [interiorClosure_smulImage] +theorem rigidStabilizer_iInter_regularSupport (F : Set G) : + G•[⋂ (g ∈ F), RegularSupport α g] = (⨅ (g ∈ F), G•[RegularSupport α g]) := +by + let S := { RegularSupport α g | g ∈ F } + have h₁ : ⋂ (g ∈ F), RegularSupport α g = ⋂₀ S := by + ext x + simp + have h₂ : ⨅ (g ∈ F), G•[RegularSupport α g] = ⨅ (s ∈ S), G•[s] := by + ext x + rw [<-sInf_image] + simp + rw [Subgroup.mem_iInf] + simp only [Subgroup.mem_iInf, and_imp, forall_apply_eq_imp_iff₂] + + rw [h₁, h₂] + rw [rigidStabilizer_sInter] + +theorem rigidStabilizer_iInter_regularSupport' (F : Finset G) : + G•[⋂ (g ∈ F), RegularSupport α g] = (⨅ (g ∈ F), G•[RegularSupport α g]) := +by + have h₁ : G•[⋂ (g ∈ F), RegularSupport α g] = G•[⋂ (g ∈ (F : Set G)), RegularSupport α g] := by simp + have h₂ : ⨅ (g ∈ F), G•[RegularSupport α g] = ⨅ (g ∈ (F : Set G)), G•[RegularSupport α g] := by simp + + rw [h₁, h₂, rigidStabilizer_iInter_regularSupport] + end RegularSupport_continuous end Rubin diff --git a/Rubin/RigidStabilizer.lean b/Rubin/RigidStabilizer.lean index c51e61e..5f81773 100644 --- a/Rubin/RigidStabilizer.lean +++ b/Rubin/RigidStabilizer.lean @@ -1,5 +1,6 @@ import Mathlib.Data.Finset.Basic import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.GroupTheory.GroupAction.FixingSubgroup import Rubin.Support import Rubin.MulActionExt @@ -11,6 +12,7 @@ def rigidStabilizer' (G : Type _) [Group G] [MulAction G α] (U : Set α) : Set {g : G | ∀ x : α, g • x = x ∨ x ∈ U} #align rigid_stabilizer' Rubin.rigidStabilizer' +-- TODO: rename to something else? Also check the literature on what this is called /-- A "rigid stabilizer" is a subgroup of `G` associated with a set `U` for which `Support α g ⊆ U` is true for all of its elements. @@ -33,6 +35,14 @@ variable {G α: Type _} variable [Group G] variable [MulAction G α] +theorem rigidStabilizer_eq_fixingSubgroup_compl (U : Set α) : + G•[U] = fixingSubgroup G Uᶜ := +by + ext g + rw [mem_fixingSubgroup_iff, <-Subgroup.mem_carrier] + unfold RigidStabilizer + simp + theorem rigidStabilizer_support {g : G} {U : Set α} : g ∈ RigidStabilizer G U ↔ Support α g ⊆ U := ⟨ @@ -104,6 +114,7 @@ by symm at gx_notin_support rw [fixes_inv] at gx_notin_support rw [<-gx_notin_support] + symm group_action rw [not_mem_support.mp x_notin_support] } @@ -118,8 +129,9 @@ by have hx_notin_support := disjoint_not_mem U_disj hx_in_U? rw [<-support_inv] at hx_notin_support rw [not_mem_support] at hx_notin_support + symm at hx_notin_support group_action at hx_notin_support - rw [<-hx_notin_support] + rw [hx_notin_support] exact x_fixed } { @@ -190,4 +202,15 @@ by rw [<-elem_moved_in_support' p h_in_rist] assumption +-- TODO: remov ethe need for FaithfulSMul? +theorem rigidStabilizer_neBot [FaithfulSMul G α] {U : Set α}: + G•[U] ≠ ⊥ → Set.Nonempty U := +by + intro ne_bot + by_contra empty + apply ne_bot + rw [Set.not_nonempty_iff_eq_empty] at empty + rw [empty] + exact rigidStabilizer_empty G α + end Rubin diff --git a/Rubin/Support.lean b/Rubin/Support.lean index 0725fdc..931d300 100644 --- a/Rubin/Support.lean +++ b/Rubin/Support.lean @@ -15,27 +15,25 @@ The support of a group action of `g: G` on `α` (here generalized to `SMul G α` is the set of values `x` in `α` for which `g • x ≠ x`. This can also be thought of as the complement of the fixpoints of `(g •)`, -which [`support_eq_not_fixed_by`] provides. +which [`support_eq_compl_fixedBy`] provides. --/ +-- TODO: rename to MulAction.support def Support {G : Type _} (α : Type _) [SMul G α] (g : G) := {x : α | g • x ≠ x} #align support Rubin.Support -theorem SmulSupport_def {G : Type _} (α : Type _) [SMul G α] {g : G} : - Support α g = {x : α | g • x ≠ x} := by tauto - variable {G α: Type _} variable [Group G] variable [MulAction G α] variable {f g : G} variable {x : α} -theorem support_eq_not_fixed_by : Support α g = (MulAction.fixedBy α g)ᶜ := by tauto -#align support_eq_not_fixed_by Rubin.support_eq_not_fixed_by +theorem support_eq_compl_fixedBy : Support α g = (MulAction.fixedBy α g)ᶜ := by tauto +#align support_eq_not_fixed_by Rubin.support_eq_compl_fixedBy -theorem support_compl_eq_fixed_by : (Support α g)ᶜ = MulAction.fixedBy α g := by +theorem fixedBy_eq_compl_support : MulAction.fixedBy α g = (Support α g)ᶜ := by rw [<-compl_compl (MulAction.fixedBy _ _)] - exact congr_arg (·ᶜ) support_eq_not_fixed_by + exact congr_arg (·ᶜ) support_eq_compl_fixedBy theorem mem_support : x ∈ Support α g ↔ g • x ≠ x := by tauto @@ -304,8 +302,9 @@ by rw [<-support_inv, not_mem_support] at gp_notin_supp rw [mem_support] at p_in_supp apply p_in_supp + symm at gp_notin_supp group_action at gp_notin_supp - exact gp_notin_supp.symm + exact gp_notin_supp theorem elem_moved_in_support' {g : G} (p : α) {U : Set α} (support_in_U : Support α g ⊆ U): p ∈ U ↔ g • p ∈ U := diff --git a/Rubin/Tactic.lean b/Rubin/Tactic.lean index 66c0605..448da6d 100644 --- a/Rubin/Tactic.lean +++ b/Rubin/Tactic.lean @@ -54,18 +54,18 @@ macro_rules tsub_self, <-mul_assoc, - one_pow, - one_zpow, - <-mul_zpow_neg_one, - zpow_zero, - mul_zpow, - zpow_sub, - <-zpow_ofNat, - <-zpow_neg_one, - <-zpow_mul, - <-zpow_add_one, - <-zpow_one_add, - <-zpow_add, + -- one_pow, + -- one_zpow, + -- <-mul_zpow_neg_one, + -- zpow_zero, + -- mul_zpow, + -- zpow_sub, + -- <-zpow_ofNat, + -- <-zpow_neg_one, + -- <-zpow_mul, + -- <-zpow_add_one, + -- <-zpow_one_add, + -- <-zpow_add, Int.ofNat_add, Int.ofNat_mul, diff --git a/Rubin/Topology.lean b/Rubin/Topology.lean index fdd90c9..e26c0b5 100644 --- a/Rubin/Topology.lean +++ b/Rubin/Topology.lean @@ -8,6 +8,11 @@ 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 @@ -35,12 +40,12 @@ 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 α] [TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where equivariant : is_equivariant G toFun