diff --git a/Rubin.lean b/Rubin.lean index 973b273..bf977d0 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -781,12 +781,35 @@ def RSuppSubsets {α : Type _} [TopologicalSpace α] (V : Set α) : Set (Set α) def RSuppOrbit {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] (F : Filter α) (H : Subgroup G) : Set (Set α) := { g •'' W | (g ∈ H) (W ∈ F) } -lemma moving_elem_of_open_subset_closure_orbit {U V : Set α} (U_open : IsOpen U) {p : α} - (U_ss_clOrbit : U ⊆ closure (MulAction.orbit (RigidStabilizer G V) p)) : +lemma moving_elem_of_open_subset_closure_orbit {U V : Set α} (U_open : IsOpen U) (U_nonempty : Set.Nonempty U) + {p : α} (p_in_V : p ∈ V) (U_ss_clOrbit : U ⊆ closure (MulAction.orbit (RigidStabilizer G V) p)) : ∃ h : G, h ∈ RigidStabilizer G V ∧ h • p ∈ U := by - -- Idea: can `Support α g ⊆ MulAction.orbit (RigidStabilizer G (RegularSupport α g)) p` be proven? - sorry + have U_ss_clV : U ⊆ closure V := by + apply subset_trans + exact U_ss_clOrbit + apply closure_mono + exact orbit_rigidStabilizer_subset p_in_V + + by_cases (RigidStabilizer G V) = ⊥ + case pos rist_bot => + rw [rist_bot] at U_ss_clOrbit + simp at U_ss_clOrbit + use 1 + constructor + exact Subgroup.one_mem _ + rw [one_smul] + let ⟨q, q_in_U⟩ := U_nonempty + rw [<-U_ss_clOrbit _ q_in_U] + assumption + case neg rist_ne_bot => + rw [<-ne_eq, Subgroup.ne_bot_iff_exists_ne_one] at rist_ne_bot + let ⟨⟨g, g_in_rist⟩, g_ne_one⟩ := rist_ne_bot + rw [ne_eq, Subgroup.mk_eq_one_iff, <-ne_eq] at g_ne_one + + -- Idea: show that `U ∩ Orb(p, G_U)` is nonempty? + sorry + lemma compact_subset_of_rsupp_basis [LocallyCompactSpace α] (U : RegularSupportBasis α): @@ -816,17 +839,29 @@ by -- Then, get a nontrivial element from that set let ⟨g, g_in_rist, g_ne_one⟩ := LocallyMoving.get_nontrivial_rist_elem (G := G) V_open ⟨p, p_in_V⟩ - -- Somehow, the regular support of g is within U - have rsupp_ss_U : RegularSupport α g ⊆ U.val := by - rw [RegularSupport, InteriorClosure] - - apply interiorClosure_subset_of_regular _ U.regular - rw [<-rigidStabilizer_support] - apply rigidStabilizer_mono _ g_in_rist + have V_ss_clU : V ⊆ closure U.val := by + apply subset_trans + exact V_ss_clOrbit + apply closure_mono + exact orbit_rigidStabilizer_subset p_in_U - show V ⊆ U.val - -- Would probably require showing that the orbit of the rigidstabilizer is a subset of U - sorry + -- The regular support of g is within U + have rsupp_ss_U : RegularSupport α g ⊆ U.val := by + rw [RegularSupport] + rw [rigidStabilizer_support] at g_in_rist + calc + InteriorClosure (Support α g) ⊆ InteriorClosure V := by + apply interiorClosure_mono + assumption + _ ⊆ InteriorClosure (closure U.val) := by + apply interiorClosure_mono + assumption + _ ⊆ InteriorClosure U.val := by + simp + rfl + _ ⊆ _ := by + apply subset_of_eq + exact U.regular -- Use as the chosen set RegularSupport g let g' : HomeoGroup α := HomeoGroup.fromContinuous α g @@ -877,7 +912,7 @@ by exact W'.nonempty -- We get an element `h` such that `h • p ∈ W` and `h ∈ G_U` - let ⟨h, h_in_rist, hp_in_W⟩ := moving_elem_of_open_subset_closure_orbit W_open W_ss_clOrbit + let ⟨h, h_in_rist, hp_in_W⟩ := moving_elem_of_open_subset_closure_orbit W_open W_nonempty p_in_U W_ss_clOrbit use h constructor @@ -936,9 +971,9 @@ by rw [<-gW_eq_V] assumption have gV'_compact : IsCompact (closure (g⁻¹ •'' V'.val)) := by - rw [smulImage_closure _ _ (continuousMulAction_elem_continuous α g⁻¹)] - -- TODO: smulImage_compact - sorry + rw [smulImage_closure] + apply smulImage_compact + assumption have ⟨p, p_lim⟩ := (proposition_3_4_2 F).mpr ⟨g⁻¹ •'' V'.val, ⟨gV'_in_F, gV'_compact⟩⟩ use p @@ -948,12 +983,9 @@ by rw [clusterPt_iff_forall_mem_closure] at p_lim specialize p_lim (g⁻¹ •'' V') gV'_in_F - rw [smulImage_closure _ _ (continuousMulAction_elem_continuous α g⁻¹)] at p_lim - rw [mem_smulImage, inv_inv] at p_lim + rw [smulImage_closure, mem_smulImage, inv_inv] at p_lim - rw [rigidStabilizer_support] at g_in_rist - rw [<-support_inv] at g_in_rist - have q := fixed_smulImage_in_support g⁻¹ g_in_rist + rw [rigidStabilizer_support, <-support_inv] at g_in_rist rw [<-fixed_smulImage_in_support g⁻¹ g_in_rist] rw [mem_smulImage, inv_inv] diff --git a/Rubin/InteriorClosure.lean b/Rubin/InteriorClosure.lean index dc2382e..7c0260e 100644 --- a/Rubin/InteriorClosure.lean +++ b/Rubin/InteriorClosure.lean @@ -226,72 +226,18 @@ Set.Finite.induction_on' S_finite (by simp) (by · exact IH ) -theorem smulImage_interior {G : Type _} [Group G] [MulAction G α] - (g : G) (U : Set α) - (g_continuous : ∀ S : Set α, IsOpen S → IsOpen (g •'' S) ∧ IsOpen (g⁻¹ •'' S)): - interior (g •'' U) = g •'' interior U := -by - unfold interior - rw [smulImage_sUnion] - simp - ext x - simp - constructor - · intro ⟨T, ⟨T_open, T_sub⟩, x_in_T⟩ - use g⁻¹ •'' T - repeat' apply And.intro - · exact (g_continuous T T_open).right - · rw [smulImage_subset_inv] - rw [inv_inv] - exact T_sub - · rw [smulImage_mul, mul_right_inv, one_smulImage] - exact x_in_T - · intro ⟨T, ⟨T_open, T_sub⟩, x_in_T⟩ - use g •'' T - repeat' apply And.intro - · exact (g_continuous T T_open).left - · apply smulImage_mono - exact T_sub - · exact x_in_T - -theorem smulImage_closure {G : Type _} [Group G] [MulAction G α] - (g : G) (U : Set α) - (g_continuous : ∀ S : Set α, IsOpen S → IsOpen (g •'' S) ∧ IsOpen (g⁻¹ •'' S)): - 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 - ext x - simp - constructor - · intro IH T' T T_closed U_ss_T T'_eq - rw [<-T'_eq] - clear T' T'_eq - apply IH - · exact (g_continuous' _ T_closed).left - · apply smulImage_mono - exact U_ss_T - · intro IH T T_closed gU_ss_T - apply IH - · exact (g_continuous' _ T_closed).right - · rw [<-smulImage_subset_inv] - exact gU_ss_T - · simp - -theorem interiorClosure_smulImage {G : Type _} [Group G] [MulAction G α] +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)) : InteriorClosure (g •'' U) = g •'' InteriorClosure U := by simp - rw [<-smulImage_interior _ _ g_continuous] - rw [<-smulImage_closure _ _ g_continuous] + 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) end Rubin diff --git a/Rubin/RegularSupport.lean b/Rubin/RegularSupport.lean index 2830afd..a3541c9 100644 --- a/Rubin/RegularSupport.lean +++ b/Rubin/RegularSupport.lean @@ -98,7 +98,7 @@ theorem regularSupport_smulImage {f g : G} : by unfold RegularSupport rw [support_conjugate] - rw [interiorClosure_smulImage _ _ (continuousMulAction_elem_continuous α f)] + rw [interiorClosure_smulImage] end RegularSupport_continuous diff --git a/Rubin/RigidStabilizer.lean b/Rubin/RigidStabilizer.lean index 891aca3..76ac63a 100644 --- a/Rubin/RigidStabilizer.lean +++ b/Rubin/RigidStabilizer.lean @@ -60,16 +60,15 @@ by have supp_empty : Support α f = ∅ := empty_of_subset_disjoint f_in_rist_compl.symm f_in_rist exact f_ne_one ((support_empty_iff f).mp supp_empty) -theorem rigidStabilizer_to_subgroup_closure {g : G} {U : Set α} : - g ∈ RigidStabilizer G U → g ∈ Subgroup.closure { g : G | Support α g ⊆ U } := +-- TODO: remove? +theorem rigidStabilizer_to_subgroup_closure {U : Set α} : + RigidStabilizer G U = Subgroup.closure { h : G | Support α h ⊆ U } := by - rw [rigidStabilizer_support] - intro h - rw [Subgroup.mem_closure] - intro V orbit_subset_V - apply orbit_subset_V - simp - exact h + ext g + simp only [<-rigidStabilizer_support] + have set_eq : {h | h ∈ RigidStabilizer G U} = (RigidStabilizer G U : Set G) := rfl + rw [set_eq] + rw [Subgroup.closure_eq] theorem commute_if_rigidStabilizer_and_disjoint {g h : G} {U : Set α} [FaithfulSMul G α] : g ∈ RigidStabilizer G U → Disjoint U (Support α h) → Commute g h := @@ -181,4 +180,15 @@ by rw [smulImage_subset_inv] simp +theorem orbit_rigidStabilizer_subset {p : α} {U : Set α} (p_in_U : p ∈ U): + MulAction.orbit (RigidStabilizer G U) p ⊆ U := +by + intro q q_in_orbit + have ⟨⟨h, h_in_rist⟩, hp_eq_q⟩ := MulAction.mem_orbit_iff.mp q_in_orbit + simp at hp_eq_q + rw [<-hp_eq_q] + rw [rigidStabilizer_support] at h_in_rist + rw [<-elem_moved_in_support' p h_in_rist] + assumption + end Rubin diff --git a/Rubin/SmulImage.lean b/Rubin/SmulImage.lean index d03c834..97b325f 100644 --- a/Rubin/SmulImage.lean +++ b/Rubin/SmulImage.lean @@ -56,6 +56,12 @@ theorem mem_smulImage {x : α} {g : G} {U : Set α} : x ∈ g •'' U ↔ g⁻¹ -- this is simply [`mem_smulImage`] paired with set extensionality. theorem smulImage_set {g: G} {U: Set α} : g •'' U = {x | g⁻¹ • x ∈ U} := Set.ext (fun _x => mem_smulImage) +@[simp] +theorem smulImage_preImage (g: G) (U: Set α) : (fun p => g • p) ⁻¹' U = g⁻¹ •'' U := by + ext x + simp + rw [mem_smulImage, inv_inv] + theorem mem_inv_smulImage {x : α} {g : G} {U : Set α} : x ∈ g⁻¹ •'' U ↔ g • x ∈ U := by let msi := @Rubin.mem_smulImage _ _ _ _ x g⁻¹ U @@ -335,7 +341,6 @@ 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) := @@ -347,5 +352,237 @@ by · 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) + {S : Set α} (S_open : IsOpen S) : IsOpen (g •'' S) := + (continuousMulAction_elem_continuous α g S S_open).left + +theorem smulImage_isClosed {G α : Type _} + [Group G] [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] (g : G) + {S : Set α} (S_open : IsClosed S) : IsClosed (g •'' S) := +by + rw [<-isOpen_compl_iff] + rw [<-isOpen_compl_iff] at S_open + rw [smulImage_compl] + 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)): + interior (g •'' U) = g •'' interior U := +by + unfold interior + rw [smulImage_sUnion] + simp + ext x + simp + constructor + · intro ⟨T, ⟨T_open, T_sub⟩, x_in_T⟩ + use g⁻¹ •'' T + repeat' apply And.intro + · exact (g_continuous T T_open).right + · rw [smulImage_subset_inv] + rw [inv_inv] + exact T_sub + · rw [smulImage_mul, mul_right_inv, one_smulImage] + exact x_in_T + · intro ⟨T, ⟨T_open, T_sub⟩, x_in_T⟩ + use g •'' T + repeat' apply And.intro + · exact (g_continuous T T_open).left + · 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)): + 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 + ext x + simp + constructor + · intro IH T' T T_closed U_ss_T T'_eq + rw [<-T'_eq] + clear T' T'_eq + apply IH + · exact (g_continuous' _ T_closed).left + · apply smulImage_mono + exact U_ss_T + · intro IH T T_closed gU_ss_T + apply IH + · exact (g_continuous' _ T_closed).right + · 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 + +variable {G α : Type _} +variable [Group G] [MulAction G α] + +/-- +An SMul can be extended to filters, while preserving the properties of `MulAction`. + +To avoid polluting the `SMul` instances for filters, those properties are made separate, +instead of implementing `MulAction G (Filter α)`. +--/ +def SmulFilter {G α : Type _} [SMul G α] (g : G) (F : Filter α) : Filter α := + Filter.map (fun p => g • p) F + +infixl:60 " •ᶠ " => Rubin.SmulFilter + +theorem smulFilter_def {G α : Type _} [SMul G α] (g : G) (F : Filter α) : + Filter.map (fun p => g • p) F = g •ᶠ F := rfl + +theorem smulFilter_neBot {G α : Type _} [SMul G α] (g : G) {F : Filter α} (F_neBot : Filter.NeBot F) : + Filter.NeBot (g •ᶠ F) := +by + rw [<-smulFilter_def] + exact Filter.map_neBot + +instance smulFilter_neBot' {G α : Type _} [SMul G α] {g : G} {F : Filter α} [F_neBot : Filter.NeBot F] : + Filter.NeBot (g •ᶠ F) := smulFilter_neBot g F_neBot + +theorem smulFilter_principal (g : G) (S : Set α) : + g •ᶠ Filter.principal S = Filter.principal (g •'' S) := +by + rw [<-smulFilter_def] + rw [Filter.map_principal] + rfl + +theorem mul_smulFilter (g h: G) (F : Filter α) : + (g * h) •ᶠ F = g •ᶠ (h •ᶠ F) := +by + repeat rw [<-smulFilter_def] + simp only [mul_smul] + rw [Filter.map_map] + rfl + +theorem one_smulFilter (G : Type _) [Group G] [MulAction G α] (F : Filter α) : + (1 : G) •ᶠ F = F := +by + rw [<-smulFilter_def] + simp only [one_smul] + exact Filter.map_id + +theorem mem_smulFilter_iff (g : G) (F : Filter α) (U : Set α) : + U ∈ g •ᶠ F ↔ g⁻¹ •'' U ∈ F := +by + rw [<-smulFilter_def, Filter.mem_map, smulImage_eq_inv_preimage, inv_inv] + +theorem smulFilter_mono (g : G) (F F' : Filter α) : + F ≤ F' ↔ g •ᶠ F ≤ g •ᶠ F' := +by + suffices ∀ (g : G) (F F' : Filter α), F ≤ F' → g •ᶠ F ≤ g •ᶠ F' by + constructor + apply this + intro H + specialize this g⁻¹ _ _ H + repeat rw [<-mul_smulFilter] at this + rw [mul_left_inv] at this + repeat rw [one_smulFilter] at this + exact this + intro g F F' F_le_F' + intro U U_in_gF + rw [mem_smulFilter_iff] at U_in_gF + rw [mem_smulFilter_iff] + apply F_le_F' + assumption + +theorem smulFilter_le_iff_le_inv (g : G) (F F' : Filter α) : + F ≤ g •ᶠ F' ↔ g⁻¹ •ᶠ F ≤ F' := +by + nth_rw 2 [<-one_smulFilter G F'] + rw [<-mul_left_inv g, mul_smulFilter] + exact smulFilter_mono g⁻¹ _ _ + +variable [TopologicalSpace α] + +theorem smulFilter_nhds (g : G) (p : α) [ContinuousMulAction G α]: + g •ᶠ 𝓝 p = 𝓝 (g • p) := +by + ext S + rw [<-smulFilter_def, Filter.mem_map, mem_nhds_iff, mem_nhds_iff] + simp + constructor + · intro ⟨T, T_ss_smulImage, T_open, p_in_T⟩ + use g •'' T + repeat' apply And.intro + · rw [smulImage_subset_inv] + assumption + · exact smulImage_isOpen g T_open + · simp + assumption + · intro ⟨T, T_ss_S, T_open, gp_in_T⟩ + use g⁻¹ •'' T + repeat' apply And.intro + · apply smulImage_mono + assumption + · exact smulImage_isOpen g⁻¹ T_open + · rw [mem_smulImage, inv_inv] + assumption + +theorem smulFilter_clusterPt (g : G) (F : Filter α) (x : α) [ContinuousMulAction 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 + constructor + apply this + intro gx_clusterPt_F + + rw [<-one_smul G x, <-mul_right_inv g, mul_smul] + nth_rw 1 [<-inv_inv g] + apply this + rw [<-mul_smulFilter, mul_left_inv, one_smulFilter] + assumption + intro g F x x_cp_gF + rw [clusterPt_iff_forall_mem_closure] + rw [clusterPt_iff_forall_mem_closure] at x_cp_gF + simp only [mem_smulFilter_iff] at x_cp_gF + intro S S_in_F + + rw [<-mem_inv_smulImage] + rw [<-smulImage_closure] + + apply x_cp_gF + rw [inv_inv, smulImage_mul, mul_left_inv, one_smulImage] + assumption + +theorem smulImage_compact [ContinuousMulAction G α] (g : G) {U : Set α} (U_compact : IsCompact U) : + IsCompact (g •'' U) := +by + intro F F_neBot F_le_principal + rw [<-smulFilter_principal, smulFilter_le_iff_le_inv] at F_le_principal + let ⟨x, x_in_U, x_clusterPt⟩ := U_compact F_le_principal + use g • x + constructor + · rw [mem_smulImage'] + assumption + · rw [smulFilter_clusterPt, inv_inv] at x_clusterPt + assumption +end Filters end Rubin diff --git a/Rubin/Support.lean b/Rubin/Support.lean index c93da6e..0725fdc 100644 --- a/Rubin/Support.lean +++ b/Rubin/Support.lean @@ -68,24 +68,6 @@ theorem fixed_of_disjoint {U : Set α} : not_mem_support.mp (Set.disjoint_left.mp disjoint_U_support x_in_U) #align fixed_of_disjoint Rubin.fixed_of_disjoint -theorem fixed_smulImage_in_support (g : G) {U : Set α} : - Support α g ⊆ U → g •'' U = U := - by - intro support_in_U - ext x - cases' @or_not (x ∈ Support α g) with xmoved xfixed - exact - ⟨fun _ => support_in_U xmoved, fun _ => - mem_smulImage.mpr (support_in_U (Rubin.inv_smul_mem_support xmoved))⟩ - rw [Rubin.mem_smulImage, smul_eq_iff_inv_smul_eq.mp (not_mem_support.mp xfixed)] -#align fixes_subset_within_support Rubin.fixed_smulImage_in_support - -theorem smulImage_subset_in_support (g : G) (U V : Set α) : - U ⊆ V → Support α g ⊆ V → g •'' U ⊆ V := fun U_in_V support_in_V => - Rubin.fixed_smulImage_in_support g support_in_V ▸ - smulImage_mono g U_in_V -#align moves_subset_within_support Rubin.smulImage_subset_in_support - theorem support_mul (g h : G) (α : Type _) [MulAction G α] : Support α (g * h) ⊆ Support α g ∪ Support α h := @@ -142,6 +124,19 @@ theorem support_pow (α : Type _) [MulAction G α] (g : G) (j : ℕ) : -- exact j_ih #align support_pow Rubin.support_pow +theorem support_zpow (α : Type _) [MulAction G α] (g : G) (j : ℤ) : + Support α (g ^ j) ⊆ Support α g := +by + cases j with + | ofNat n => + rw [Int.ofNat_eq_coe, zpow_coe_nat] + exact support_pow α g n + | negSucc n => + rw [Int.negSucc_eq, zpow_neg, support_inv, zpow_add, zpow_coe_nat, zpow_one] + nth_rw 2 [<-pow_one g] + rw [<-pow_add] + exact support_pow α g (n+1) + theorem support_comm (α : Type _) [MulAction G α] (g h : G) : Support α ⁅g, h⁆ ⊆ Support α h ∪ (g •'' Support α h) := @@ -294,6 +289,93 @@ by rw [Set.not_nonempty_iff_eq_empty] at supp_empty exact g_ne_one ((support_empty_iff _).mp supp_empty) +theorem elem_moved_in_support (g : G) (p : α) : + p ∈ Support α g ↔ g • p ∈ Support α g := +by + suffices ∀ (g : G) (p : α), p ∈ Support α g → g • p ∈ Support α g by + constructor + exact this g p + rw [<-support_inv] + intro H + rw [<-one_smul G p, <-mul_left_inv g, mul_smul] + exact this _ _ H + intro g p p_in_supp + by_contra gp_notin_supp + rw [<-support_inv, not_mem_support] at gp_notin_supp + rw [mem_support] at p_in_supp + apply p_in_supp + group_action at gp_notin_supp + exact gp_notin_supp.symm + +theorem elem_moved_in_support' {g : G} (p : α) {U : Set α} (support_in_U : Support α g ⊆ U): + p ∈ U ↔ g • p ∈ U := +by + by_cases p_in_supp? : p ∈ Support α g + · constructor + rw [elem_moved_in_support] at p_in_supp? + all_goals intro; exact support_in_U p_in_supp? + · rw [not_mem_support] at p_in_supp? + rw [p_in_supp?] + +theorem elem_moved_in_support_zpow {g : G} (p : α) (j : ℤ) {U : Set α} (support_in_U : Support α g ⊆ U): + p ∈ U ↔ g^j • p ∈ U := +by + by_cases p_in_supp? : p ∈ Support α g + · constructor + all_goals intro; apply support_in_U + swap; exact p_in_supp? + rw [<-elem_moved_in_support' p (support_zpow α g j)] + assumption + · rw [not_mem_support] at p_in_supp? + rw [smul_zpow_eq_of_smul_eq j p_in_supp?] + +theorem orbit_subset_support (g : G) (p : α) : + MulAction.orbit (Subgroup.closure {g}) p ⊆ Support α g ∪ {p} := +by + intro q q_in_orbit + rw [MulAction.mem_orbit_iff] at q_in_orbit + let ⟨⟨h, h_in_closure⟩, hp_eq_q⟩ := q_in_orbit + simp at hp_eq_q + rw [Subgroup.mem_closure_singleton] at h_in_closure + let ⟨n, g_pow_n_eq_h⟩ := h_in_closure + rw [<-hp_eq_q, <-g_pow_n_eq_h] + clear hp_eq_q g_pow_n_eq_h h_in_closure + + have union_superset : Support α g ⊆ Support α g ∪ {p} := by + simp only [Set.union_singleton, Set.subset_insert] + rw [<-elem_moved_in_support_zpow _ _ union_superset] + simp only [Set.union_singleton, Set.mem_insert_iff, true_or] + +theorem orbit_subset_of_support_subset (g : G) {p : α} {U : Set α} (p_in_U : p ∈ U) + (supp_ss_U : Support α g ⊆ U) : + MulAction.orbit (Subgroup.closure {g}) p ⊆ U := +by + apply subset_trans + exact orbit_subset_support g p + apply Set.union_subset + assumption + rw [Set.singleton_subset_iff] + assumption + +theorem fixed_smulImage_in_support (g : G) {U : Set α} : + Support α g ⊆ U → g •'' U = U := +by + intro support_in_U + ext x + rw [mem_smulImage] + symm + apply elem_moved_in_support' + rw [support_inv] + assumption +#align fixes_subset_within_support Rubin.fixed_smulImage_in_support + +theorem smulImage_subset_in_support (g : G) (U V : Set α) : + U ⊆ V → Support α g ⊆ V → g •'' U ⊆ V := fun U_in_V support_in_V => + Rubin.fixed_smulImage_in_support g support_in_V ▸ + smulImage_mono g U_in_V +#align moves_subset_within_support Rubin.smulImage_subset_in_support + + section Continuous variable {G α : Type _}