From 6ce7127efe01bf0a6845411f8580945a01ccc155 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Wed, 29 Nov 2023 20:47:29 +0100 Subject: [PATCH] :art: Small renames for consistency --- Rubin.lean | 8 +- Rubin/AlgebraicDisjointness.lean | 14 ++- Rubin/InteriorClosure.lean | 160 +++++++++++++++++++++++++++++++ Rubin/RegularSupport.lean | 90 +---------------- Rubin/SmulImage.lean | 41 ++++---- Rubin/Topological.lean | 66 ++++--------- 6 files changed, 212 insertions(+), 167 deletions(-) create mode 100644 Rubin/InteriorClosure.lean diff --git a/Rubin.lean b/Rubin.lean index 3e48a1c..d3012a9 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -58,7 +58,7 @@ structure RubinAction (G α : Type _) extends where locally_compact : LocallyCompactSpace α hausdorff : T2Space α - no_isolated_points : Rubin.has_no_isolated_points α + no_isolated_points : HasNoIsolatedPoints α locallyDense : LocallyDense G α #align rubin_action Rubin.RubinAction @@ -97,7 +97,7 @@ by rw [h_in_ristV _ x_notin_V] let ⟨q, q_in_V, hq_ne_q ⟩ := faithful_rigid_stabilizer_moves_point h_in_ristV h_ne_one have gpowi_q_notin_V : ∀ (i : Fin n), (i : ℕ) > 0 → g ^ (i : ℕ) • q ∉ V := by - apply smulImage_distinct_of_disjoint_exp n_pos disj + apply smulImage_distinct_of_disjoint_pow n_pos disj exact q_in_V -- We have (hg)^i q = g^i q for all 0 < i < n @@ -122,7 +122,7 @@ by let i'₂ : Fin n := ⟨Nat.succ i', i_lt_n⟩ have h_eq: Nat.succ i' = (i'₂ : ℕ) := by simp rw [h_eq] - apply smulImage_distinct_of_disjoint_exp + apply smulImage_distinct_of_disjoint_pow · exact n_pos · exact disj · exact q_in_V @@ -246,7 +246,7 @@ by apply not_support_subset_rsupp show Support α h ⊆ RegularSupport α f - apply subset_of_diff_closure_regular_empty + apply subset_from_diff_closure_eq_empty · apply regularSupport_regular · exact support_open _ · rw [Set.not_nonempty_iff_eq_empty] at U_empty diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean index 43c228d..c10819b 100644 --- a/Rubin/AlgebraicDisjointness.lean +++ b/Rubin/AlgebraicDisjointness.lean @@ -156,7 +156,7 @@ variable [ContinuousMulAction G α] variable [FaithfulSMul G α] instance dense_locally_moving [T2Space α] - (H_nip : has_no_isolated_points α) + [H_nip : HasNoIsolatedPoints α] (H_ld : LocallyDense G α) : LocallyMoving G α where @@ -164,7 +164,8 @@ where intros U _ H_nonempty by_contra h_rs have ⟨elem, ⟨_, some_in_orbit⟩⟩ := H_ld.nonEmpty H_nonempty - have H_nebot := has_no_isolated_points_neBot H_nip elem + -- Note: This is automatic now :) + -- have H_nebot := has_no_isolated_points_neBot elem rw [h_rs] at some_in_orbit simp at some_in_orbit @@ -326,9 +327,6 @@ lemma proposition_1_1_1 [h_lm : LocallyMoving G α] [T2Space α] (f g : G) (supp exact z_moved h₆ #align proposition_1_1_1 Rubin.proposition_1_1_1 -@[simp] lemma smulImage_mul {g h : G} {U : Set α} : g •'' (h •'' U) = (g*h) •'' U := - (mul_smulImage g h U) - lemma smul_inj_moves {ι : Type*} [Fintype ι] [T2Space α] {f : ι → G} {x : α} {i j : ι} (i_ne_j : i ≠ j) (f_smul_inj : Function.Injective (fun i : ι => (f i) • x)) : @@ -682,12 +680,12 @@ by clear f₁_commutes f₂_commutes have g_k_disjoint : Disjoint ((g^i.val)⁻¹ •'' (k •'' V)) ((g^j.val)⁻¹ •'' (k •'' V)) := by - repeat rw [mul_smulImage] + repeat rw [smulImage_mul] repeat rw [<-inv_pow] repeat rw [k_commutes.symm.inv_left.pow_left] - repeat rw [<-mul_smulImage k] + repeat rw [<-smulImage_mul k] repeat rw [inv_pow] - exact disjoint_smulImage k g_disjoint + exact smulImage_disjoint k g_disjoint apply Set.disjoint_left.mp g_k_disjoint · rw [mem_inv_smulImage] diff --git a/Rubin/InteriorClosure.lean b/Rubin/InteriorClosure.lean new file mode 100644 index 0000000..121e250 --- /dev/null +++ b/Rubin/InteriorClosure.lean @@ -0,0 +1,160 @@ +import Mathlib.Topology.Basic +import Mathlib.Topology.Separation + +namespace Rubin + +variable {α : Type _} +variable [TopologicalSpace α] + +/-- +Defines a kind of "regularization" transformation made to sets, +by calling `closure` followed by `interior` on those sets. + +A set is then said to be [`Regular`] if the InteriorClosure does not modify it. +--/ +def InteriorClosure (U : Set α) : Set α := + interior (closure U) +#align interior_closure Rubin.InteriorClosure + +@[simp] +theorem InteriorClosure.def (U : Set α) : InteriorClosure U = interior (closure U) := + by simp [InteriorClosure] + +@[simp] +theorem InteriorClosure.fdef : InteriorClosure = (interior ∘ (closure (α := α))) := by ext; simp + +/-- +A set `U` is said to be regular if the interior of the closure of `U` is equal to `U`. +Notably, a regular set is also open, and the interior of a regular set is equal to itself. +--/ +def Regular (U : Set α) : Prop := + InteriorClosure U = U + +@[simp] +theorem Regular.def (U : Set α) : Regular U ↔ interior (closure U) = U := + by simp [Regular] +#align set.is_regular_def Rubin.Regular.def + +@[simp] +theorem Regular.eq {U : Set α} (U_reg : Regular U) : interior (closure U) = U := + (Regular.def U).mp U_reg + +instance Regular.instCoe {U : Set α} : Coe (Regular U) (interior (closure U) = U) where + coe := Regular.eq + +/-- From this, the set of regular sets is the set of regular *open* sets. --/ +theorem regular_open (U : Set α) : Regular U → IsOpen U := +by + intro h_reg + rw [<-h_reg] + simp + +theorem Regular.isOpen {U : Set α} (U_regular : Regular U): IsOpen U := regular_open _ U_regular + +theorem regular_interior {U : Set α} : Regular U → interior U = U := +by + intro h_reg + rw [<-h_reg] + simp + +theorem interiorClosure_open (U : Set α) : IsOpen (InteriorClosure U) := by simp +#align is_open_interior_closure Rubin.interiorClosure_open + +theorem interiorClosure_subset {U : Set α} : + IsOpen U → U ⊆ InteriorClosure U := +by + intro h + apply subset_trans + exact subset_interior_iff_isOpen.mpr h + apply interior_mono + exact subset_closure +#align is_open.interior_closure_subset Rubin.interiorClosure_subset + +theorem interiorClosure_regular (U : Set α) : Regular (InteriorClosure U) := +by + apply Set.eq_of_subset_of_subset <;> unfold InteriorClosure + { + apply interior_mono + nth_rw 2 [<-closure_closure (s := U)] + apply closure_mono + exact interior_subset + } + { + nth_rw 1 [<-interior_interior] + apply interior_mono + exact subset_closure + } +#align regular_interior_closure Rubin.interiorClosure_regular + +theorem interiorClosure_mono (U V : Set α) : + U ⊆ V → InteriorClosure U ⊆ InteriorClosure V +:= interior_mono ∘ closure_mono +#align interior_closure_mono Rubin.interiorClosure_mono + +theorem monotone_interiorClosure : Monotone (InteriorClosure (α := α)) +:= fun a b => + interiorClosure_mono a b + +theorem compl_closure_regular_of_open {S : Set α} (S_open : IsOpen S) : Regular (closure S)ᶜ := by + apply Set.eq_of_subset_of_subset + · simp + apply closure_mono + rw [IsOpen.subset_interior_iff S_open] + exact subset_closure + · apply interiorClosure_subset + simp + +@[simp] +theorem interiorClosure_closure {S : Set α} (S_open : IsOpen S) : closure (InteriorClosure S) = closure S := +by + apply Set.eq_of_subset_of_subset + · simp + rw [<-Set.compl_subset_compl] + rw [<-(compl_closure_regular_of_open S_open)] + simp + rfl + · apply closure_mono + exact interiorClosure_subset S_open + +@[simp] +theorem interiorClosure_interior {S : Set α} : interior (InteriorClosure S) = (InteriorClosure S) := +regular_interior (interiorClosure_regular S) + +theorem disjoint_interiorClosure_left {U V : Set α} (V_open : IsOpen V) + (disj : Disjoint U V) : Disjoint (InteriorClosure U) V := +by + apply Set.disjoint_of_subset_left interior_subset + exact Disjoint.closure_left disj V_open + +theorem disjoint_interiorClosure_right {U V : Set α} (U_open : IsOpen U) + (disj : Disjoint U V) : Disjoint U (InteriorClosure V) := + (disjoint_interiorClosure_left U_open (Disjoint.symm disj)).symm + +theorem subset_from_diff_closure_eq_empty {U V : Set α} + (U_regular : Regular U) (V_open : IsOpen V) (V_diff_cl_empty : V \ closure U = ∅) : + V ⊆ U := +by + have V_eq_interior : interior V = V := IsOpen.interior_eq V_open + rw [<-V_eq_interior] + rw [<-U_regular] + apply interior_mono + rw [<-Set.diff_eq_empty] + exact V_diff_cl_empty + +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 + let ⟨U', V', U'_open, V'_open, u_in_U', v_in_V', disj⟩ := t2_separation u_ne_v + let U := InteriorClosure U' + let V := InteriorClosure V' + use U, V + repeat' apply And.intro + · apply interiorClosure_regular + · apply interiorClosure_regular + · apply disjoint_interiorClosure_left (interiorClosure_regular V').isOpen + apply disjoint_interiorClosure_right U'_open + exact disj + · exact (interiorClosure_subset U'_open) u_in_U' + · exact (interiorClosure_subset V'_open) v_in_V' + +end Rubin diff --git a/Rubin/RegularSupport.lean b/Rubin/RegularSupport.lean index fcf44bf..17437a7 100644 --- a/Rubin/RegularSupport.lean +++ b/Rubin/RegularSupport.lean @@ -7,98 +7,10 @@ import Mathlib.Topology.Separation import Rubin.Tactic import Rubin.Support import Rubin.Topological +import Rubin.InteriorClosure namespace Rubin -section InteriorClosure - -variable {α : Type _} -variable [TopologicalSpace α] - --- Defines a kind of "regularization" transformation made to sets, --- by calling `closure` followed by `interior` on it. --- --- A set is then said to be regular if the InteriorClosure does not modify it. -def InteriorClosure (U : Set α) : Set α := - interior (closure U) -#align interior_closure Rubin.InteriorClosure - -@[simp] -theorem InteriorClosure.def (U : Set α) : InteriorClosure U = interior (closure U) := - by simp [InteriorClosure] - -@[simp] -theorem InteriorClosure.fdef : InteriorClosure = (interior ∘ (closure (α := α))) := by ext; simp - --- A set `U` is said to be regular if the interior of the closure of `U` is equal to `U`. --- Notably, a regular set is also open, and the interior of a regular set is equal to itself. -def Regular (U : Set α) : Prop := - InteriorClosure U = U - -@[simp] -theorem Regular.def (U : Set α) : Regular U ↔ interior (closure U) = U := - by simp [Regular] -#align set.is_regular_def Rubin.Regular.def - -@[simp] -theorem Regular.eq {U : Set α} (U_reg : Regular U) : interior (closure U) = U := - (Regular.def U).mp U_reg - -instance Regular.instCoe {U : Set α} : Coe (Regular U) (interior (closure U) = U) where - coe := Regular.eq - -theorem interiorClosure_open (U : Set α) : IsOpen (InteriorClosure U) := by simp -#align is_open_interior_closure Rubin.interiorClosure_open - -theorem interiorClosure_subset {U : Set α} : - IsOpen U → U ⊆ InteriorClosure U := -by - intro h - apply subset_trans - exact subset_interior_iff_isOpen.mpr h - apply interior_mono - exact subset_closure -#align is_open.interior_closure_subset Rubin.interiorClosure_subset - -theorem interiorClosure_regular (U : Set α) : Regular (InteriorClosure U) := -by - apply Set.eq_of_subset_of_subset <;> unfold InteriorClosure - { - apply interior_mono - nth_rw 2 [<-closure_closure (s := U)] - apply closure_mono - exact interior_subset - } - { - nth_rw 1 [<-interior_interior] - apply interior_mono - exact subset_closure - } -#align regular_interior_closure Rubin.interiorClosure_regular - -theorem interiorClosure_mono (U V : Set α) : - U ⊆ V → InteriorClosure U ⊆ InteriorClosure V -:= interior_mono ∘ closure_mono -#align interior_closure_mono Rubin.interiorClosure_mono - -theorem monotone_interior_closure : Monotone (InteriorClosure (α := α)) -:= fun a b => - interiorClosure_mono a b - -theorem regular_open (U : Set α) : Regular U → IsOpen U := -by - intro h_reg - rw [<-h_reg] - simp - -theorem regular_interior (U : Set α) : Regular U → interior U = U := -by - intro h_reg - rw [<-h_reg] - simp - -end InteriorClosure - section RegularSupport_def variable {G : Type _} diff --git a/Rubin/SmulImage.lean b/Rubin/SmulImage.lean index 46d1a85..2156d18 100644 --- a/Rubin/SmulImage.lean +++ b/Rubin/SmulImage.lean @@ -66,14 +66,13 @@ by rw [mem_smulImage] rw [<-mul_smul, mul_left_inv, one_smul] --- TODO: rename to smulImage_mul @[simp] -theorem mul_smulImage (g h : G) (U : Set α) : g •'' (h •'' U) = (g * h) •'' U := +theorem smulImage_mul (g h : G) (U : Set α) : g •'' (h •'' U) = (g * h) •'' U := by ext rw [Rubin.mem_smulImage, Rubin.mem_smulImage, Rubin.mem_smulImage, ← mul_smul, mul_inv_rev] -#align mul_smul'' Rubin.mul_smulImage +#align mul_smul'' Rubin.smulImage_mul @[simp] theorem one_smulImage (U : Set α) : (1 : G) •'' U = U := @@ -82,7 +81,7 @@ theorem one_smulImage (U : Set α) : (1 : G) •'' U = U := rw [Rubin.mem_smulImage, inv_one, one_smul] #align one_smul'' Rubin.one_smulImage -theorem disjoint_smulImage (g : G) {U V : Set α} : +theorem smulImage_disjoint (g : G) {U V : Set α} : Disjoint U V → Disjoint (g •'' U) (g •'' V) := by intro disjoint_U_V @@ -91,13 +90,23 @@ theorem disjoint_smulImage (g : G) {U V : Set α} : intro x x_in_gU by_contra h exact (disjoint_U_V (mem_smulImage.mp x_in_gU)) (mem_smulImage.mp h) -#align disjoint_smul'' Rubin.disjoint_smulImage +#align disjoint_smul'' Rubin.smulImage_disjoint -namespace SmulImage -theorem congr (g : G) {U V : Set α} : U = V → g •'' U = g •'' V := +theorem SmulImage.congr (g : G) {U V : Set α} : U = V → g •'' U = g •'' V := congr_arg fun W : Set α => g •'' W #align smul''_congr Rubin.SmulImage.congr -end SmulImage + +theorem SmulImage.inv_congr (g: G) {U V : Set α} : g •'' U = g •'' V → U = V := +by + intro h + rw [<-one_smulImage (G := G) U] + rw [<-one_smulImage (G := G) V] + rw [<-mul_left_inv g] + repeat rw [<-smulImage_mul] + exact SmulImage.congr g⁻¹ h + +theorem smulImage_inv {g: G} {U V : Set α} (img_eq : g •'' U = g •'' V) : U = V := + SmulImage.inv_congr g img_eq theorem smulImage_subset (g : G) {U V : Set α} : U ⊆ V → g •'' U ⊆ g •'' V := by @@ -149,12 +158,12 @@ by constructor · intro h apply smulImage_subset f⁻¹ at h - rw [mul_smulImage] at h + rw [smulImage_mul] at h rw [mul_left_inv, one_smulImage] at h exact h · intro h apply smulImage_subset f at h - rw [mul_smulImage] at h + rw [smulImage_mul] at h rw [mul_right_inv, one_smulImage] at h exact h @@ -170,14 +179,14 @@ theorem smulImage_disjoint_mul {G α : Type _} [Group G] [MulAction G α] Disjoint (f •'' U) (g •'' V) ↔ Disjoint U ((f⁻¹ * g) •'' V) := by constructor · intro h - apply disjoint_smulImage f⁻¹ at h - repeat rw [mul_smulImage] at h + apply smulImage_disjoint f⁻¹ at h + repeat rw [smulImage_mul] at h rw [mul_left_inv, one_smulImage] at h exact h · intro h - apply disjoint_smulImage f at h - rw [mul_smulImage] at h + apply smulImage_disjoint f at h + rw [smulImage_mul] at h rw [<-mul_assoc] at h rw [mul_right_inv, one_mul] at h exact h @@ -200,7 +209,7 @@ by -- States that if `g^i •'' V` and `g^j •'' V` are disjoint for any `i ≠ j` and `x ∈ V` -- then `g^i • x` will always lie outside of `V`. -lemma smulImage_distinct_of_disjoint_exp {G α : Type _} [Group G] [MulAction G α] {g : G} {V : Set α} {n : ℕ} +lemma smulImage_distinct_of_disjoint_pow {G α : Type _} [Group G] [MulAction G α] {g : G} {V : Set α} {n : ℕ} (n_pos : 0 < n) (h_disj : ∀ (i j : Fin n), i ≠ j → Disjoint (g ^ (i : ℕ) •'' V) (g ^ (j : ℕ) •'' V)) : ∀ (x : α) (_hx : x ∈ V) (i : Fin n), 0 < (i : ℕ) → g ^ (i : ℕ) • (x : α) ∉ V := @@ -216,6 +225,6 @@ by have h_notin_V := Set.disjoint_left.mp (h_disj i (⟨0, n_pos⟩ : Fin n) i_ne_zero) h_contra simp only [pow_zero, one_smulImage] at h_notin_V exact h_notin_V -#align distinct_images_from_disjoint Rubin.smulImage_distinct_of_disjoint_exp +#align distinct_images_from_disjoint Rubin.smulImage_distinct_of_disjoint_pow end Rubin diff --git a/Rubin/Topological.lean b/Rubin/Topological.lean index 11d5f29..b9712e2 100644 --- a/Rubin/Topological.lean +++ b/Rubin/Topological.lean @@ -46,7 +46,7 @@ theorem equivariant_inv [MulAction G α] [MulAction G β] exact e #align equivariant_inv Rubin.equivariant_inv -variable [Rubin.ContinuousMulAction G α] +variable [ContinuousMulAction G α] theorem img_open_open (g : G) (U : Set α) (h : IsOpen U): IsOpen (g •'' U) := by @@ -56,7 +56,7 @@ theorem img_open_open (g : G) (U : Set α) (h : IsOpen U): IsOpen (g •'' U) := #align img_open_open Rubin.img_open_open theorem support_open (g : G) [TopologicalSpace α] [T2Space α] - [Rubin.ContinuousMulAction G α] : IsOpen (Support α g) := + [ContinuousMulAction G α] : IsOpen (Support α g) := by apply isOpen_iff_forall_mem_open.mpr intro x xmoved @@ -75,17 +75,19 @@ theorem support_open (g : G) [TopologicalSpace α] [T2Space α] end Continuity -- TODO: come up with a name -section Other +section LocallyDense open Topology --- Note: `𝓝[≠] x` is notation for `nhdsWithin x {[x]}ᶜ`, ie. the neighborhood of x not containing itself --- TODO: make this a class? -def has_no_isolated_points (α : Type _) [TopologicalSpace α] := - ∀ x : α, 𝓝[≠] x ≠ ⊥ -#align has_no_isolated_points Rubin.has_no_isolated_points +/-- +Note: `𝓝[≠] x` is notation for `nhdsWithin x {[x]}ᶜ`, ie. the neighborhood of x not containing itself. -instance has_no_isolated_points_neBot {α : Type _} [TopologicalSpace α] (h_nip: has_no_isolated_points α) (x: α): Filter.NeBot (𝓝[≠] x) where - ne' := h_nip x +--/ +class HasNoIsolatedPoints (α : Type _) [TopologicalSpace α] := + nhbd_ne_bot : ∀ x : α, 𝓝[≠] x ≠ ⊥ +#align has_no_isolated_points Rubin.HasNoIsolatedPoints + +instance has_no_isolated_points_neBot {α : Type _} [TopologicalSpace α] [h_nip: HasNoIsolatedPoints α] (x: α): Filter.NeBot (𝓝[≠] x) where + ne' := h_nip.nhbd_ne_bot x class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] extends MulAction G α := isLocallyDense: @@ -97,48 +99,12 @@ class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] extends MulAc lemma LocallyDense.nonEmpty {G α : Type _} [Group G] [TopologicalSpace α] [LocallyDense G α]: ∀ {U : Set α}, Set.Nonempty U → - ∃ p ∈ U, p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) := by + ∃ p ∈ U, p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) := +by intros U H_ne exact ⟨H_ne.some, H_ne.some_mem, LocallyDense.isLocallyDense U H_ne.some H_ne.some_mem⟩ --- Should be put into mathlib — it doesn't use constructive logic only, --- unlike (I assume) the inter_compl_nonempty_iff counterpart -lemma Set.inter_compl_empty_iff {α : Type _} (s t : Set α) : - s ∩ tᶜ = ∅ ↔ s ⊆ t := -by - constructor - { - intro h₁ - by_contra h₂ - rw [<-Set.inter_compl_nonempty_iff] at h₂ - rw [Set.nonempty_iff_ne_empty] at h₂ - exact h₂ h₁ - } - { - intro h₁ - by_contra h₂ - rw [<-ne_eq, <-Set.nonempty_iff_ne_empty] at h₂ - rw [Set.inter_compl_nonempty_iff] at h₂ - exact h₂ h₁ - } - -theorem subset_of_diff_closure_regular_empty {α : Type _} [TopologicalSpace α] {U V : Set α} - (U_regular : interior (closure U) = U) (V_open : IsOpen V) (V_diff_cl_empty : V \ closure U = ∅) : - V ⊆ U := -by - have V_eq_interior : interior V = V := IsOpen.interior_eq V_open - -- rw [<-V_eq_interior] - have V_subset_closure_U : V ⊆ closure U := by - rw [Set.diff_eq_compl_inter] at V_diff_cl_empty - rw [Set.inter_comm] at V_diff_cl_empty - rw [Set.inter_compl_empty_iff] at V_diff_cl_empty - exact V_diff_cl_empty - have res : interior V ⊆ interior (closure U) := interior_mono V_subset_closure_U - rw [U_regular] at res - rw [V_eq_interior] at res - exact res - - -end Other +end LocallyDense + end Rubin