From 68158749237a7794d8b1b2765b27de156aacfbe5 Mon Sep 17 00:00:00 2001 From: laurentbartholdi Date: Mon, 27 Nov 2023 15:47:59 +0100 Subject: [PATCH] A quick fix to prop 2.1, just to test --- Rubin/Rubin.lean | 412 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 412 insertions(+) create mode 100644 Rubin/Rubin.lean diff --git a/Rubin/Rubin.lean b/Rubin/Rubin.lean new file mode 100644 index 0000000..0d620f2 --- /dev/null +++ b/Rubin/Rubin.lean @@ -0,0 +1,412 @@ +/- +Copyright (c) 2023 Laurent Bartholdi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author : Laurent Bartholdi +-/ +import Mathlib.Data.Finset.Basic +import Mathlib.Data.Finset.Card +import Mathlib.Data.Fintype.Perm +import Mathlib.GroupTheory.Subgroup.Basic +import Mathlib.GroupTheory.Commutator +import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.GroupTheory.Exponent +import Mathlib.GroupTheory.Perm.Basic +import Mathlib.Topology.Basic +import Mathlib.Topology.Compactness.Compact +import Mathlib.Topology.Separation +import Mathlib.Topology.Homeomorph + +import Rubin.Tactic +import Rubin.MulActionExt +import Rubin.SmulImage +import Rubin.Support +import Rubin.Topological +import Rubin.RigidStabilizer +import Rubin.Period +import Rubin.AlgebraicDisjointness +import Rubin.RegularSupport + +#align_import rubin + +namespace Rubin +open Rubin.Tactic + +-- TODO: find a home +theorem equiv_congr_ne {ι ι' : Type _} (e : ι ≃ ι') {x y : ι} : x ≠ y → e x ≠ e y := + by + intro x_ne_y + by_contra h + apply x_ne_y + convert congr_arg e.symm h <;> simp only [Equiv.symm_apply_apply] +#align equiv.congr_ne Rubin.equiv_congr_ne + +---------------------------------------------------------------- +section Rubin + +variable {G α β : Type _} [Group G] + +---------------------------------------------------------------- +section RubinActions + +variable [TopologicalSpace α] [TopologicalSpace β] + +structure RubinAction (G α : Type _) extends + Group G, + TopologicalSpace α, + MulAction G α, + FaithfulSMul G α +where + locally_compact : LocallyCompactSpace α + hausdorff : T2Space α + no_isolated_points : Rubin.has_no_isolated_points α + locallyDense : LocallyDense G α +#align rubin_action Rubin.RubinAction + +end RubinActions + +lemma lemma_2_2 (G: Type _) {α : Type _} [Group G] [TopologicalSpace α] [ContinuousMulAction G α] [FaithfulSMul G α] + [T2Space α] [h_lm : LocallyMoving G α] + {U : Set α} (U_open : IsOpen U) (U_nonempty : Set.Nonempty U) : + Monoid.exponent (RigidStabilizer G U) = 0 := +by + by_contra exp_ne_zero + + let ⟨p, ⟨g, g_in_ristU⟩, n, p_in_U, n_pos, hpgn, n_eq_Sup⟩ := Period.period_from_exponent U U_nonempty exp_ne_zero + simp at hpgn + let ⟨V', V'_open, p_in_V', disj'⟩ := disjoint_nbhd_fin (smul_injective_within_period hpgn) + + let V := U ∩ V' + have V_open : IsOpen V := U_open.inter V'_open + have p_in_V : p ∈ V := ⟨p_in_U, p_in_V'⟩ + have disj : ∀ (i j : Fin n), i ≠ j → Disjoint (g ^ (i : ℕ) •'' V) (g ^ (j : ℕ) •'' V) := by + intro i j i_ne_j + apply Set.disjoint_of_subset + · apply smulImage_subset + apply Set.inter_subset_right + · apply smulImage_subset + apply Set.inter_subset_right + exact disj' i j i_ne_j + + let ⟨h, h_in_ristV, h_ne_one⟩ := h_lm.get_nontrivial_rist_elem V_open (Set.nonempty_of_mem p_in_V) + have hg_in_ristU : h * g ∈ RigidStabilizer G U := by + simp [RigidStabilizer] + intro x x_notin_U + rw [mul_smul] + rw [g_in_ristU _ x_notin_U] + have x_notin_V : x ∉ V := fun x_in_V => x_notin_U x_in_V.left + 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 + exact q_in_V + + -- We have (hg)^i q = g^i q for all 0 < i < n + have hgpow_eq_gpow : ∀ (i : Fin n), (h * g) ^ (i : ℕ) • q = g ^ (i : ℕ) • q := by + intro ⟨i, i_lt_n⟩ + simp + induction i with + | zero => simp + | succ i' IH => + have i'_lt_n: i' < n := Nat.lt_of_succ_lt i_lt_n + have IH := IH i'_lt_n + rw [smul_succ] + rw [IH] + rw [smul_succ] + rw [mul_smul] + rw [<-smul_succ] + + -- We can show that `g^(Nat.succ i') • q ∉ V`, + -- which means that with `h` in `RigidStabilizer G V`, `h` fixes that point + apply h_in_ristV (g^(Nat.succ i') • q) + + 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 + · exact n_pos + · exact disj + · exact q_in_V + · simp + + -- Combined with `g^i • q ≠ q`, this yields `(hg)^i • q ≠ q` for all `0 < i < n` + have hgpow_moves : ∀ (i : Fin n), 0 < (i : ℕ) → (h*g)^(i : ℕ) • q ≠ q := by + intro ⟨i, i_lt_n⟩ i_pos + simp at i_pos + rw [hgpow_eq_gpow] + simp + by_contra h' + apply gpowi_q_notin_V ⟨i, i_lt_n⟩ + exact i_pos + simp (config := {zeta := false}) only [] + rw [h'] + exact q_in_V + + -- This even holds for `i = n` + have hgpown_moves : (h * g) ^ n • q ≠ q := by + -- Rewrite (hg)^n • q = h * g^n • q + rw [<-Nat.succ_pred n_pos.ne.symm] + rw [pow_succ] + have h_eq := hgpow_eq_gpow ⟨Nat.pred n, Nat.pred_lt_self n_pos⟩ + simp at h_eq + rw [mul_smul, h_eq, <-mul_smul, mul_assoc, <-pow_succ] + rw [<-Nat.succ_eq_add_one, Nat.succ_pred n_pos.ne.symm] + + -- We first eliminate `g^n • q` by proving that `n = Period g q` + have period_gq_eq_n : Period.period q g = n := by + apply ge_antisymm + { + apply Period.notfix_le_period' + · exact n_pos + · apply Period.period_pos' + · exact Set.nonempty_of_mem p_in_U + · exact exp_ne_zero + · exact q_in_V.left + · exact g_in_ristU + · intro i i_pos + rw [<-hgpow_eq_gpow] + apply hgpow_moves i i_pos + } + { + rw [n_eq_Sup] + apply Period.period_le_Sup_periods' + · exact Set.nonempty_of_mem p_in_U + · exact exp_ne_zero + · exact q_in_V.left + · exact g_in_ristU + } + + rw [mul_smul, <-period_gq_eq_n] + rw [Period.pow_period_fix] + -- Finally, we have `h • q ≠ q` + exact hq_ne_q + + -- Finally, we derive a contradiction + have ⟨period_hg_pos, period_hg_le_n⟩ := Period.zero_lt_period_le_Sup_periods U_nonempty exp_ne_zero ⟨q, q_in_V.left⟩ ⟨h * g, hg_in_ristU⟩ + simp at period_hg_pos + simp at period_hg_le_n + rw [<-n_eq_Sup] at period_hg_le_n + cases (lt_or_eq_of_le period_hg_le_n) with + | inl period_hg_lt_n => + apply hgpow_moves ⟨Period.period q (h * g), period_hg_lt_n⟩ + exact period_hg_pos + simp + apply Period.pow_period_fix + | inr period_hg_eq_n => + apply hgpown_moves + rw [<-period_hg_eq_n] + apply Period.pow_period_fix + +section proposition_2_1 + +def AlgebraicSubgroup {G : Type _} [Group G] (f : G) : Set G := + (fun g : G => g^12) '' { g : G | IsAlgebraicallyDisjoint f g } + + +-- 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 α] + {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 _ _ + 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 + + +lemma nontrivial_pow_from_exponent_eq_zero {G : Type _} [Group G] + (exp_eq_zero : Monoid.exponent G = 0) : + ∀ (n : ℕ), n > 0 → ∃ g : G, g^n ≠ 1 := +by + intro n n_pos + rw [Monoid.exponent_eq_zero_iff] at exp_eq_zero + unfold Monoid.ExponentExists at exp_eq_zero + rw [<-Classical.not_forall_not, Classical.not_not] at exp_eq_zero + simp at exp_eq_zero + exact exp_eq_zero n n_pos + +lemma Commute.inv {G : Type _} [Group G] {f g : G} : Commute f g → Commute f g⁻¹ := by + unfold Commute SemiconjBy + intro h + have h₁ : f = g * f * g⁻¹ := by + nth_rw 1 [<-mul_one f] + rw [<-mul_right_inv g, <-mul_assoc] + rw [h] + nth_rw 2 [h₁] + group + +lemma Commute.inv_iff {G : Type _} [Group G] {f g : G} : Commute f g ↔ Commute f g⁻¹ := ⟨ + Commute.inv, + by + nth_rw 2 [<-inv_inv g] + apply Commute.inv +⟩ + +lemma Commute.inv_iff₂ {G : Type _} [Group G] {f g : G} : Commute f g ↔ Commute f⁻¹ g := ⟨ + Commute.symm ∘ Commute.inv_iff.mp ∘ Commute.symm, + Commute.symm ∘ Commute.inv_iff.mpr ∘ Commute.symm +⟩ + +lemma Commute.into {G : Type _} [Group G] {f g : G} : Commute f g → f * g = g * f := by + unfold Commute SemiconjBy + tauto + +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) := +by + apply Set.eq_of_subset_of_subset + swap + { + intro h h_in_rist + simp at h_in_rist + 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_disj' : Disjoint (Support α f) (Support α g) := by + rw [← g_eq_g'] + exact supp_disj + have rsupp_disj : Disjoint (RegularSupport α f) (Support α g) := by + have cl_supp_disj : Disjoint (closure (Support α f)) (Support α g) := by + exact Disjoint.closure_left supp_disj' (support_open g) + + 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 + } + + 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_V⟩ := V_nonempty + have v_moved := V_in_supp_h v_in_V + rw [mem_support] at v_moved + + have ⟨W, W_open, v_in_W, W_subset_support, disj_W_img⟩ := disjoint_nbhd_in V_open v_in_V v_moved + + have mono_exp := lemma_2_2 G W_open (Set.nonempty_of_mem v_in_W) + let ⟨⟨g, g_in_rist⟩, g12_ne_one⟩ := nontrivial_pow_from_exponent_eq_zero mono_exp 12 (by norm_num) + simp at g12_ne_one + + have disj_supports : Disjoint (Support α f) (Support α g) := by + apply Set.disjoint_of_subset_right + · apply rigidStabilizer_support.mp + exact g_in_rist + · apply Set.disjoint_of_subset_right + · exact W_subset_support + · exact V_disj_supp_f.symm + have alg_disj_f_g := proposition_1_1_1 _ _ disj_supports + have g12_in_algebraic_subgroup : g^12 ∈ AlgebraicSubgroup f := by + simp [AlgebraicSubgroup] + use g + constructor + exact ↑alg_disj_f_g + rfl + + have h_nc_g12 : ¬Commute (g^12) h := by + have supp_g12_sub_W : Support α (g^12) ⊆ W := by + rw [rigidStabilizer_support] at g_in_rist + calc + Support α (g^12) ⊆ Support α g := by apply support_pow + _ ⊆ W := g_in_rist + have supp_g12_disj_hW : Disjoint (Support α (g^12)) (h •'' W) := by + apply Set.disjoint_of_subset_left + swap + · exact disj_W_img + · exact supp_g12_sub_W + + exact not_commute_of_disj_support_smulImage + g12_ne_one + supp_g12_sub_W + supp_g12_disj_hW + + apply h_nc_g12 + exact h_in_centralizer _ g12_in_algebraic_subgroup + + +end proposition_2_1 +-- variables [topological_space α] [topological_space β] [continuous_mul_action G α] [continuous_mul_action G β] +-- noncomputable theorem rubin (hα : rubin_action G α) (hβ : rubin_action G β) : equivariant_homeomorph G α β := sorry +end Rubin + +end Rubin -- 2.43.0