From 4b4a719d403a9260d423b27048a08ac545b08b2b Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Mon, 27 Nov 2023 18:28:34 +0100 Subject: [PATCH] :sparkles: Working proof of proposition 2.1 --- Rubin.lean | 149 ++++++++++++------------------- Rubin/AlgebraicDisjointness.lean | 16 +++- Rubin/RegularSupport.lean | 9 ++ Rubin/Topological.lean | 39 ++++++++ 4 files changed, 118 insertions(+), 95 deletions(-) diff --git a/Rubin.lean b/Rubin.lean index 58714d3..3e48a1c 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -198,87 +198,59 @@ by section proposition_2_1 +-- TODO: put in a different file and introduce some QoL theorems def AlgebraicSubgroup {G : Type _} [Group G] (f : G) : Set G := (fun g : G => g^12) '' { g : G | IsAlgebraicallyDisjoint f g } +def AlgebraicCentralizer {G: Type _} (α : Type _) [Group G] [MulAction G α] (f : G) : Set G := + Set.centralizer (AlgebraicSubgroup f) --- TODO: WIP, can't seem to be able to construct a set U that fulfills all the conditions -lemma open_disj_of_not_support_subset_rsupp {G α : Type _} - [Group G] [TopologicalSpace α] [ContinuousMulAction G α] [T2Space α] [h_fsm : FaithfulSMul G α] - [h_lm : LocallyMoving G α] +-- Given the statement `¬Support α h ⊆ RegularSupport α f`, +-- 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 α] [ContinuousMulAction 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 - have v_exists := by - rw [Set.not_subset] at not_support_subset_rsupp - exact not_support_subset_rsupp - let ⟨v, ⟨v_in_supp, v_notin_rsupp⟩⟩ := v_exists - - have v_notin_supp_f : v ∉ Support α f := by - intro h₁ - exact v_notin_rsupp (support_subset_regularSupport h₁) - - let U := interior (Support α h \ Support α f) - have U_open : IsOpen U := by simp - have U_subset_supp_h : U ⊆ Support α h := by - calc - U ⊆ (Support α h \ Support α f) := interior_subset - _ ⊆ Support α h := Set.diff_subset _ _ + let U := Support α h \ closure (RegularSupport α f) + have U_open : IsOpen U := by + unfold_let + rw [Set.diff_eq_compl_inter] + apply IsOpen.inter + · simp + · exact support_open _ + have U_subset_supp_h : U ⊆ Support α h := by simp; apply Set.diff_subset have U_disj_supp_f : Disjoint U (Support α f) := by - by_contra h_contra - rw [Set.not_disjoint_iff] at h_contra - let ⟨x, x_in_U, x_in_supp_F⟩ := h_contra - unfold_let at x_in_U - have x_in_diff := interior_subset x_in_U - exact x_in_diff.2 x_in_supp_F - - have U_nonempty : Set.Nonempty U := by - by_contra U_empty - rw [Set.not_nonempty_iff_eq_empty] at U_empty - have v_moved : h • v ≠ v := by rw [<-mem_support]; assumption - let ⟨W, ⟨W_open, v_in_W, W_subset_supp_h, W_disj_img⟩⟩ := disjoint_nbhd_in (support_open _) v_in_supp v_moved - let V := W \ {v} - have V_open : IsOpen V := W_open.sdiff isClosed_singleton - sorry - - use U - - -- Stuff I attempted so far: - -- let U := Support α h \ closure (Support α f) - -- have U_open : IsOpen U := by - -- apply IsOpen.sdiff - -- exact support_open h - -- simp - - -- let V := U \ {v} - -- have V_open : IsOpen V := by - -- apply IsOpen.sdiff - -- · apply IsOpen.sdiff - -- exact support_open h - -- simp - -- · exact isClosed_singleton - -- have U_subset_support : U ⊆ Support α h := Set.diff_subset _ _ - -- have V_subset_support : V ⊆ Support α h := by - -- -- Mathlib kind of letting me down on this one: - -- unfold_let - -- repeat rw [Set.diff_eq] - -- intro x x_in - -- exact x_in.left.left - -- have V_disj_support : Disjoint V (Support α f) := by - -- intro S - -- simp - -- intro S_subset - -- intro S_support - -- intro x x_in_S - -- have h₁ := S_subset x_in_S - -- simp at h₁ - -- have h₂ := S_support x_in_S - -- simp at h₂ - -- have h₃ := not_mem_of_not_mem_closure h₁.left.right - -- exact h₃ h₂ - - -- use V - + apply Set.disjoint_of_subset_right + · exact subset_closure + · simp + rw [Set.diff_eq_compl_inter] + apply Disjoint.inter_left + apply Disjoint.closure_right; swap; simp + + rw [Set.disjoint_compl_left_iff_subset] + apply subset_trans + exact subset_closure + apply closure_mono + apply support_subset_regularSupport + + have U_nonempty : Set.Nonempty U; swap + exact ⟨U, U_subset_supp_h, U_nonempty, U_open, U_disj_supp_f⟩ + + -- We prove that U isn't empty by contradiction: + -- if it is empty, then `Support α h \ closure (RegularSupport α f) = ∅`, + -- so we can show that `Support α h ⊆ RegularSupport α f`, + -- contradicting with our initial hypothesis. + by_contra U_empty + apply not_support_subset_rsupp + show Support α h ⊆ RegularSupport α f + + apply subset_of_diff_closure_regular_empty + · apply regularSupport_regular + · exact support_open _ + · rw [Set.not_nonempty_iff_eq_empty] at U_empty + exact U_empty lemma nontrivial_pow_from_exponent_eq_zero {G : Type _} [Group G] (exp_eq_zero : Monoid.exponent G = 0) : @@ -321,50 +293,41 @@ lemma proposition_2_1 {G α : Type _} [Group G] [TopologicalSpace α] [ContinuousMulAction G α] [T2Space α] [LocallyMoving G α] [h_faithful : FaithfulSMul G α] (f : G) : - Set.centralizer (AlgebraicSubgroup f) = RigidStabilizer G (RegularSupport α f) := + AlgebraicCentralizer α f = RigidStabilizer G (RegularSupport α f) := by apply Set.eq_of_subset_of_subset swap { intro h h_in_rist simp at h_in_rist - let U := RegularSupport α f + unfold AlgebraicCentralizer rw [Set.mem_centralizer_iff] intro g g_in_S simp [AlgebraicSubgroup] at g_in_S let ⟨g', ⟨g'_alg_disj, g_eq_g'⟩⟩ := g_in_S have supp_disj := proposition_1_1_2 f g' g'_alg_disj (α := α) - have supp_αf_open : IsOpen (Support α f) := support_open f - have supp_αg_open : IsOpen (Support α g) := support_open g - - have rsupp_disj : Disjoint (RegularSupport α f) (Support α g) := by + apply Commute.eq + symm + apply commute_if_rigidStabilizer_and_disjoint (α := α) + · exact h_in_rist + · show Disjoint (RegularSupport α f) (Support α g) have cl_supp_disj : Disjoint (closure (Support α f)) (Support α g) - { - rw [<-g_eq_g'] - apply Set.disjoint_of_subset_left _ supp_disj - show closure (Support α f) ⊆ Support α f - -- TODO: figure out how to prove this - sorry - } + swap apply Set.disjoint_of_subset _ _ cl_supp_disj · rw [RegularSupport.def] exact interior_subset · rfl - - apply Commute.eq - symm - apply commute_if_rigidStabilizer_and_disjoint (α := α) - · exact h_in_rist - · exact rsupp_disj + · rw [<-g_eq_g'] + exact Disjoint.closure_left supp_disj (support_open _) } intro h h_in_centralizer by_contra h_notin_rist simp at h_notin_rist rw [rigidStabilizer_support] at h_notin_rist - let ⟨V, V_in_supp_h, V_nonempty, V_open, V_disj_supp_f⟩ := open_disj_of_not_support_subset_rsupp h_notin_rist + let ⟨V, V_in_supp_h, V_nonempty, V_open, V_disj_supp_f⟩ := open_set_from_supp_not_subset_rsupp h_notin_rist let ⟨v, v_in_V⟩ := V_nonempty have v_moved := V_in_supp_h v_in_V rw [mem_support] at v_moved diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean index d596760..43c228d 100644 --- a/Rubin/AlgebraicDisjointness.lean +++ b/Rubin/AlgebraicDisjointness.lean @@ -69,7 +69,8 @@ so that `⁅f₁, ⁅f₂, h⁆⁆` is a nontrivial element of `Centralizer(g, G Here the definition of `k ∈ Centralizer(g, G)` is directly unrolled as `Commute k g`. -This is a slightly stronger proposition that plain disjointness, a +This is a slightly weaker proposition than plain disjointness, +but it is easier to derive from the hypothesis of Rubin's theorem. -/ def AlgebraicallyDisjoint {G : Type _} [Group G] (f g : G) := ∀ (h : G), ¬Commute f h → AlgebraicallyDisjointElem f g h @@ -89,7 +90,18 @@ fun (h : G) (nc : ¬Commute f h) => { exact (mk_thm h nc).choose_spec.choose_spec.right.right.right } --- This is an idea of having a Prop version of AlgebraicallyDisjoint, but it sounds painful to work with +/-- +This definition simply wraps `AlgebraicallyDisjoint` as a `Prop`. +It is equivalent to it, although since `AlgebraicallyDisjoint` isn't a `Prop`, +an `↔` (iff) statement joining the two cannot be written. + +You should consider using it when proving `↔`/`∧` kinds of theorems, or when tools like `cases` are needed, +as the base `AlgebraicallyDisjoint` isn't a `Prop` and won't work with those. + +The two `Coe` and `CoeFn` instances provided around this type make it essentially transparent — +you can use an instance of `AlgebraicallyDisjoint` in place of a `IsAlgebraicallyDisjoint` and vice-versa. +You might need to add the odd `↑` (coe) operator to make Lean happy. +--/ def IsAlgebraicallyDisjoint {G : Type _} [Group G] (f g : G): Prop := ∀ (h : G), ¬Commute f h → ∃ (f₁ f₂ : G), ∃ (elem : AlgebraicallyDisjointElem f g h), elem.fst = f₁ ∧ elem.snd = f₂ diff --git a/Rubin/RegularSupport.lean b/Rubin/RegularSupport.lean index 0fbba5a..fcf44bf 100644 --- a/Rubin/RegularSupport.lean +++ b/Rubin/RegularSupport.lean @@ -30,6 +30,8 @@ theorem InteriorClosure.def (U : Set α) : InteriorClosure U = interior (closure @[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 @@ -38,6 +40,13 @@ 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 diff --git a/Rubin/Topological.lean b/Rubin/Topological.lean index 1cf63b2..11d5f29 100644 --- a/Rubin/Topological.lean +++ b/Rubin/Topological.lean @@ -2,6 +2,7 @@ import Mathlib.GroupTheory.Subgroup.Basic import Mathlib.GroupTheory.GroupAction.Basic import Mathlib.Topology.Basic import Mathlib.Topology.Homeomorph +import Mathlib.Data.Set.Basic import Rubin.RigidStabilizer import Rubin.MulActionExt @@ -100,6 +101,44 @@ lemma LocallyDense.nonEmpty {G α : Type _} [Group G] [TopologicalSpace α] [Loc 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 Rubin