From d96318acc845d6434a4c2e911954c9b282069eb3 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Fri, 24 Nov 2023 00:36:26 +0100 Subject: [PATCH] :sparkles: Translate proposition 1.1.1 to lean4 --- Rubin.lean | 451 +------------------------------ Rubin/AlgebraicDisjointness.lean | 399 +++++++++++++++++++++++++++ Rubin/FaithfulAction.lean | 2 +- Rubin/Period.lean | 131 +++++++++ Rubin/Topological.lean | 62 ++++- 5 files changed, 586 insertions(+), 459 deletions(-) create mode 100644 Rubin/AlgebraicDisjointness.lean create mode 100644 Rubin/Period.lean diff --git a/Rubin.lean b/Rubin.lean index 47cd6c4..af7a6d3 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -22,6 +22,7 @@ import Rubin.SmulImage import Rubin.Support import Rubin.Topological import Rubin.RigidStabilizer +import Rubin.Period #align_import rubin @@ -42,55 +43,11 @@ section Rubin variable {G α β : Type _} [Group G] ----------------------------------------------------------------- -section Groups - -def is_algebraically_disjoint (f g : G) := - ∀ h : G, - ¬Commute f h → - ∃ f₁ f₂ : G, Commute f₁ g ∧ Commute f₂ g ∧ Commute ⁅f₁, ⁅f₂, h⁆⁆ g ∧ ⁅f₁, ⁅f₂, h⁆⁆ ≠ 1 -#align is_algebraically_disjoint Rubin.is_algebraically_disjoint - -end Groups - ----------------------------------------------------------------- -section Actions - -variable [MulAction G α] - -@[simp] -theorem orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) : - MulAction.orbit (⊥ : Subgroup G) p = {p} := - by - ext1 - rw [MulAction.mem_orbit_iff] - constructor - · rintro ⟨⟨_, g_bot⟩, g_to_x⟩ - rw [← g_to_x, Set.mem_singleton_iff, Subgroup.mk_smul] - exact (Subgroup.mem_bot.mp g_bot).symm ▸ one_smul _ _ - exact fun h => ⟨1, Eq.trans (one_smul _ p) (Set.mem_singleton_iff.mp h).symm⟩ -#align orbit_bot Rubin.orbit_bot - -end Actions - ---------------------------------------------------------------- section RubinActions -open Topology variable [TopologicalSpace α] [TopologicalSpace β] --- 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 - -def is_locally_dense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] := - ∀ U : Set α, - ∀ p ∈ U, - p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) -#align is_locally_dense Rubin.is_locally_dense - structure RubinAction (G α : Type _) extends Group G, TopologicalSpace α, @@ -100,413 +57,15 @@ where locally_compact : LocallyCompactSpace α hausdorff : T2Space α no_isolated_points : Rubin.has_no_isolated_points α - locallyDense : Rubin.is_locally_dense G α + locallyDense : LocallyDense G α #align rubin_action Rubin.RubinAction end RubinActions ----------------------------------------------------------------- -section Rubin.Period.period - -variable [MulAction G α] - -noncomputable def Period.period (p : α) (g : G) : ℕ := - sInf {n : ℕ | n > 0 ∧ g ^ n • p = p} -#align period Rubin.Period.period - -theorem Period.period_le_fix {p : α} {g : G} {m : ℕ} (m_pos : m > 0) - (gmp_eq_p : g ^ m • p = p) : 0 < Rubin.Period.period p g ∧ Rubin.Period.period p g ≤ m := - by - constructor - · by_contra h'; have period_zero : Rubin.Period.period p g = 0; linarith; - rcases Nat.sInf_eq_zero.1 period_zero with ⟨cont, h_1⟩ | h; linarith; - exact Set.eq_empty_iff_forall_not_mem.mp h ↑m ⟨m_pos, gmp_eq_p⟩ - exact Nat.sInf_le ⟨m_pos, gmp_eq_p⟩ -#align period_le_fix Rubin.Period.period_le_fix - -theorem Period.notfix_le_period {p : α} {g : G} {n : ℕ} (n_pos : n > 0) - (period_pos : Rubin.Period.period p g > 0) (pmoves : ∀ i : ℕ, 0 < i → i < n → g ^ i • p ≠ p) : - n ≤ Rubin.Period.period p g := by - by_contra period_le - exact - (pmoves (Rubin.Period.period p g) period_pos (not_le.mp period_le)) - (Nat.sInf_mem (Nat.nonempty_of_pos_sInf period_pos)).2 -#align notfix_le_period Rubin.Period.notfix_le_period - -theorem Period.notfix_le_period' {p : α} {g : G} {n : ℕ} (n_pos : n > 0) - (period_pos : Rubin.Period.period p g > 0) - (pmoves : ∀ i : Fin n, 0 < (i : ℕ) → g ^ (i : ℕ) • p ≠ p) : n ≤ Rubin.Period.period p g := - Rubin.Period.notfix_le_period n_pos period_pos fun (i : ℕ) (i_pos : 0 < i) (i_lt_n : i < n) => - pmoves (⟨i, i_lt_n⟩ : Fin n) i_pos -#align notfix_le_period' Rubin.Period.notfix_le_period' - -theorem Period.period_neutral_eq_one (p : α) : Rubin.Period.period p (1 : G) = 1 := - by - have : 0 < Rubin.Period.period p (1 : G) ∧ Rubin.Period.period p (1 : G) ≤ 1 := - Rubin.Period.period_le_fix (by norm_num : 1 > 0) - (by group_action : - (1 : G) ^ 1 • p = p) - linarith -#align period_neutral_eq_one Rubin.Period.period_neutral_eq_one - -def Period.periods (U : Set α) (H : Subgroup G) : Set ℕ := - {n : ℕ | ∃ (p : α) (g : H), p ∈ U ∧ Rubin.Period.period (p : α) (g : G) = n} -#align periods Rubin.Period.periods - --- TODO: split into multiple lemmas -theorem Period.periods_lemmas {U : Set α} (U_nonempty : Set.Nonempty U) {H : Subgroup G} - (exp_ne_zero : Monoid.exponent H ≠ 0) : - (Rubin.Period.periods U H).Nonempty ∧ - BddAbove (Rubin.Period.periods U H) ∧ - ∃ (m : ℕ) (m_pos : m > 0), ∀ (p : α) (g : H), g ^ m • p = p := - by - rcases Monoid.exponentExists_iff_ne_zero.2 exp_ne_zero with ⟨m, m_pos, gm_eq_one⟩ - have gmp_eq_p : ∀ (p : α) (g : H), g ^ m • p = p := by - intro p g; rw [gm_eq_one g]; - group_action - have periods_nonempty : (Rubin.Period.periods U H).Nonempty := by - use 1 - let p := Set.Nonempty.some U_nonempty; use p - use 1 - constructor - · exact Set.Nonempty.some_mem U_nonempty - · exact Rubin.Period.period_neutral_eq_one p - - have periods_bounded : BddAbove (Rubin.Period.periods U H) := by - use m; intro some_period hperiod; - rcases hperiod with ⟨p, g, hperiod⟩ - rw [← hperiod.2] - exact (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).2 - exact ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩ -#align period_lemma Rubin.Period.periods_lemmas - -theorem Period.period_from_exponent (U : Set α) (U_nonempty : U.Nonempty) {H : Subgroup G} - (exp_ne_zero : Monoid.exponent H ≠ 0) : - ∃ (p : α) (g : H) (n : ℕ), - p ∈ U ∧ n > 0 ∧ Rubin.Period.period (p : α) (g : G) = n ∧ n = sSup (Rubin.Period.periods U H) := - by - rcases Rubin.Period.periods_lemmas U_nonempty exp_ne_zero with - ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩ - rcases Nat.sSup_mem periods_nonempty periods_bounded with ⟨p, g, hperiod⟩ - use p - use g - use sSup (Rubin.Period.periods U H) - -- TODO: cleanup? - exact ⟨ - hperiod.1, - hperiod.2 ▸ (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).1, - hperiod.2, - rfl - ⟩ -#align period_from_exponent Rubin.Period.period_from_exponent - -theorem Period.zero_lt_period_le_Sup_periods {U : Set α} (U_nonempty : U.Nonempty) - {H : Subgroup G} (exp_ne_zero : Monoid.exponent H ≠ 0) : - ∀ (p : U) (g : H), - 0 < Rubin.Period.period (p : α) (g : G) ∧ - Rubin.Period.period (p : α) (g : G) ≤ sSup (Rubin.Period.periods U H) := - by - rcases Rubin.Period.periods_lemmas U_nonempty exp_ne_zero with - ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩ - intro p g - have period_in_periods : Rubin.Period.period (p : α) (g : G) ∈ Rubin.Period.periods U H := by - use p; use g - simp - exact - ⟨(Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).1, - le_csSup periods_bounded period_in_periods⟩ -#align zero_lt_period_le_Sup_periods Rubin.Period.zero_lt_period_le_Sup_periods - -theorem Period.pow_period_fix (p : α) (g : G) : g ^ Rubin.Period.period p g • p = p := - by - cases eq_zero_or_neZero (Rubin.Period.period p g) with - | inl h => rw [h]; simp - | inr h => - exact - (Nat.sInf_mem - (Nat.nonempty_of_pos_sInf - (Nat.pos_of_ne_zero (@NeZero.ne _ _ (Rubin.Period.period p g) h)))).2 -#align pow_period_fix Rubin.Period.pow_period_fix - -end Rubin.Period.period - ----------------------------------------------------------------- -section AlgebraicDisjointness - -variable [TopologicalSpace α] [Rubin.Topological.ContinuousMulAction G α] [FaithfulSMul G α] - -def Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpace α] - [MulAction G α] := - ∀ U : Set α, IsOpen U → Set.Nonempty U → RigidStabilizer G U ≠ ⊥ -#align is_locally_moving Rubin.Disjointness.IsLocallyMoving - --- lemma dense_locally_moving : t2_space α ∧ has_no_isolated_points α ∧ is_locally_dense G α → is_locally_moving G α := begin --- rintros ⟨t2α,nipα,ildGα⟩ U ioU neU, --- by_contra, --- have some_in_U := ildGα U neU.some neU.some_mem, --- rw [h,orbit_bot G neU.some,@closure_singleton α _ (@t2_space.t1_space α _ t2α) neU.some,@interior_singleton α _ neU.some (nipα neU.some)] at some_in_U, --- tauto --- end --- lemma disjoint_nbhd {g : G} {x : α} [t2_space α] : g • x ≠ x → ∃U : set α, is_open U ∧ x ∈ U ∧ disjoint U (g •'' U) := begin --- intro xmoved, --- rcases t2_space.t2 (g • x) x xmoved with ⟨V,W,open_V,open_W,gx_in_V,x_in_W,disjoint_V_W⟩, --- let U := (g⁻¹ •'' V) ∩ W, --- use U, --- split, --- exact is_open.inter (img_open_open g⁻¹ V open_V) open_W, --- split, --- exact ⟨mem_inv_smul''.mpr gx_in_V,x_in_W⟩, --- exact Set.disjoint_of_subset --- (Set.inter_subset_right (g⁻¹ •'' V) W) --- (λ y hy, smul_inv_smul g y ▸ mem_inv_smul''.mp (Set.mem_of_mem_inter_left (mem_smulImage.mp hy)) : g •'' U ⊆ V) --- disjoint_V_W.symm --- end --- lemma disjoint_nbhd_in {g : G} {x : α} [t2_space α] {V : set α} : is_open V → x ∈ V → g • x ≠ x → ∃U : set α, is_open U ∧ x ∈ U ∧ U ⊆ V ∧ disjoint U (g •'' U) := begin --- intros open_V x_in_V xmoved, --- rcases disjoint_nbhd xmoved with ⟨W,open_W,x_in_W,disjoint_W⟩, --- let U := W ∩ V, --- use U, --- split, --- exact is_open.inter open_W open_V, --- split, --- exact ⟨x_in_W,x_in_V⟩, --- split, --- exact Set.inter_subset_right W V, --- exact Set.disjoint_of_subset --- (Set.inter_subset_left W V) --- ((@smul''_inter _ _ _ _ g W V).symm ▸ Set.inter_subset_left (g •'' W) (g •'' V) : g •'' U ⊆ g •'' W) --- disjoint_W --- end --- lemma rewrite_Union (f : fin 2 × fin 2 → set α) : (⋃(i : fin 2 × fin 2), f i) = (f (0,0) ∪ f (0,1)) ∪ (f (1,0) ∪ f (1,1)) := begin --- ext, --- simp only [Set.mem_Union, Set.mem_union], --- split, --- { simp only [forall_exists_index], --- intro i, --- fin_cases i; simp {contextual := tt}, }, --- { rintro ((h|h)|(h|h)); exact ⟨_, h⟩, }, --- end --- lemma proposition_1_1_1 (f g : G) (locally_moving : is_locally_moving G α) [t2_space α] : disjoint (support α f) (support α g) → is_algebraically_disjoint f g := begin --- intros disjoint_f_g h hfh, --- let support_f := support α f, --- -- h is not the identity on support α f --- cases Set.not_disjoint_iff.mp (mt (@disjoint_commute G α _ _ _ _ _) hfh) with x hx, --- let x_in_support_f := hx.1, --- let hx_ne_x := mem_support.mp hx.2, --- -- so since α is Hausdoff there is V nonempty ⊆ support α f with h •'' V disjoint from V --- rcases disjoint_nbhd_in (support_open f) x_in_support_f hx_ne_x with ⟨V,open_V,x_in_V,V_in_support,disjoint_img_V⟩, --- let ristV_ne_bot := locally_moving V open_V (Set.nonempty_of_mem x_in_V), --- -- let f₂ be a nontrivial element of rigid_stabilizer G V --- rcases (or_iff_right ristV_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) with ⟨f₂,f₂_in_ristV,f₂_ne_one⟩, --- -- again since α is Hausdorff there is W nonempty ⊆ V with f₂ •'' W disjoint from W --- rcases faithful_moves_point' α f₂_ne_one with ⟨y,ymoved⟩, --- let y_in_V : y ∈ V := (rist_supported_in_set f₂_in_ristV) (mem_support.mpr ymoved), --- rcases disjoint_nbhd_in open_V y_in_V ymoved with ⟨W,open_W,y_in_W,W_in_V,disjoint_img_W⟩, --- -- let f₁ be a nontrivial element of rigid_stabilizer G W --- let ristW_ne_bot := locally_moving W open_W (Set.nonempty_of_mem y_in_W), --- rcases (or_iff_right ristW_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) with ⟨f₁,f₁_in_ristW,f₁_ne_one⟩, --- use f₁, use f₂, --- -- note that f₁,f₂ commute with g since their support is in support α f --- split, --- exact disjoint_commute (Set.disjoint_of_subset_left (Set.subset.trans (Set.subset.trans (rist_supported_in_set f₁_in_ristW) W_in_V) V_in_support) disjoint_f_g), --- split, --- exact disjoint_commute (Set.disjoint_of_subset_left (Set.subset.trans (rist_supported_in_set f₂_in_ristV) V_in_support) disjoint_f_g), --- -- we claim that [f₁,[f₂,h]] is a nontrivial element of centralizer G g --- let k := ⁅f₂,h⁆, --- -- first, h*f₂⁻¹*h⁻¹ is supported on h V, so k := [f₂,h] agrees with f₂ on V --- have h2 : ∀z ∈ W, f₂•z = k•z := λ z z_in_W, --- (disjoint_support_comm f₂ h (rist_supported_in_set f₂_in_ristV) disjoint_img_V z (W_in_V z_in_W)).symm, --- -- then k*f₁⁻¹*k⁻¹ is supported on k W = f₂ W, so [f₁,k] is supported on W ∪ f₂ W ⊆ V ⊆ support f, so commutes with g. --- have h3 : support α ⁅f₁,k⁆ ⊆ support α f := begin --- let := (support_comm α k f₁).trans (Set.union_subset_union (rist_supported_in_set f₁_in_ristW) (smul''_subset k $ rist_supported_in_set f₁_in_ristW)), --- rw [← commutator_element_inv,support_inv,(smul''_eq_of_smul_eq h2).symm] at this, --- exact (this.trans $ (Set.union_subset_union W_in_V (moves_subset_within_support f₂ W V W_in_V $ rist_supported_in_set f₂_in_ristV)).trans $ eq.subset V.union_self).trans V_in_support --- end, --- split, --- exact disjoint_commute (Set.disjoint_of_subset_left h3 disjoint_f_g), --- -- finally, [f₁,k] agrees with f₁ on W, so is not the identity. --- have h4 : ∀z ∈ W, ⁅f₁,k⁆•z = f₁•z := --- disjoint_support_comm f₁ k (rist_supported_in_set f₁_in_ristW) (smul''_eq_of_smul_eq h2 ▸ disjoint_img_W), --- rcases faithful_rist_moves_point f₁_in_ristW f₁_ne_one with ⟨z,z_in_W,z_moved⟩, --- by_contra h5, --- exact ((h4 z z_in_W).symm ▸ z_moved : ⁅f₁, k⁆ • z ≠ z) ((congr_arg (λg : G, g•z) h5).trans (one_smul G z)), --- end --- @[simp] lemma smul''_mul {g h : G} {U : set α} : g •'' (h •'' U) = (g*h) •'' U := --- (mul_smul'' g h U).symm --- lemma disjoint_nbhd_fin {ι : Type*} [fintype ι] {f : ι → G} {x : α} [t2_space α] : (λi : ι, f i • x).injective → ∃U : set α, is_open U ∧ x ∈ U ∧ (∀i j : ι, i ≠ j → disjoint (f i •'' U) (f j •'' U)) := begin --- intro f_injective, --- let disjoint_hyp := λi j (i_ne_j : i≠j), let x_moved : ((f j)⁻¹ * f i) • x ≠ x := begin --- by_contra, --- let := smul_congr (f j) h, --- rw [mul_smul, ← mul_smul,mul_right_inv,one_smul] at this, --- from i_ne_j (f_injective this), --- end in disjoint_nbhd x_moved, --- let ι2 := { p : ι×ι // p.1 ≠ p.2 }, --- let U := ⋂(p : ι2), (disjoint_hyp p.1.1 p.1.2 p.2).some, --- use U, --- split, --- exact is_open_Inter (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.1), --- split, --- exact Set.mem_Inter.mpr (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.2.1), --- intros i j i_ne_j, --- let U_inc := Set.Inter_subset (λ p : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some) ⟨⟨i,j⟩,i_ne_j⟩, --- let := (disjoint_smul'' (f j) (Set.disjoint_of_subset U_inc (smul''_subset ((f j)⁻¹ * (f i)) U_inc) (disjoint_hyp i j i_ne_j).some_spec.2.2)).symm, --- simp only [subtype.val_eq_coe, smul''_mul, mul_inv_cancel_left] at this, --- from this --- end --- lemma moves_inj {g : G} {x : α} {n : ℕ} (period_ge_n : ∀ (k : ℤ), 1 ≤ k → k < n → g ^ k • x ≠ x) : function.injective (λ (i : fin n), g ^ (i : ℤ) • x) := begin --- intros i j same_img, --- by_contra i_ne_j, --- let same_img' := congr_arg ((•) (g ^ (-(j : ℤ)))) same_img, --- simp only [inv_smul_smul] at same_img', --- rw [← mul_smul,← mul_smul,← zpow_add,← zpow_add,add_comm] at same_img', --- simp only [add_left_neg, zpow_zero, one_smul] at same_img', --- let ij := |(i:ℤ) - (j:ℤ)|, --- rw ← sub_eq_add_neg at same_img', --- have xfixed : g^ij • x = x := begin --- cases abs_cases ((i:ℤ) - (j:ℤ)), --- { rw ← h.1 at same_img', exact same_img' }, --- { rw [smul_eq_iff_inv_smul_eq,← zpow_neg,← h.1] at same_img', exact same_img' } --- end, --- have ij_ge_1 : 1 ≤ ij := int.add_one_le_iff.mpr (abs_pos.mpr $ sub_ne_zero.mpr $ norm_num.nat_cast_ne i j ↑i ↑j rfl rfl (fin.vne_of_ne i_ne_j)), --- let neg_le := int.sub_lt_sub_of_le_of_lt (nat.cast_nonneg i) (nat.cast_lt.mpr (fin.prop _)), --- rw zero_sub at neg_le, --- let le_pos := int.sub_lt_sub_of_lt_of_le (nat.cast_lt.mpr (fin.prop _)) (nat.cast_nonneg j), --- rw sub_zero at le_pos, --- have ij_lt_n : ij < n := abs_lt.mpr ⟨ neg_le, le_pos ⟩, --- exact period_ge_n ij ij_ge_1 ij_lt_n xfixed, --- end --- lemma int_to_nat (k : ℤ) (k_pos : k ≥ 1) : k = k.nat_abs := begin --- cases (int.nat_abs_eq k), --- { exact h }, --- { have : -(k.nat_abs : ℤ) ≤ 0 := neg_nonpos.mpr (int.nat_abs k).cast_nonneg, --- rw ← h at this, by_contra, linarith } --- end --- lemma moves_inj_N {g : G} {x : α} {n : ℕ} (period_ge_n' : ∀ (k : ℕ), 1 ≤ k → k < n → g ^ k • x ≠ x) : function.injective (λ (i : fin n), g ^ (i : ℕ) • x) := begin --- have period_ge_n : ∀ (k : ℤ), 1 ≤ k → k < n → g ^ k • x ≠ x, --- { intros k one_le_k k_lt_n, --- have one_le_k_nat : 1 ≤ k.nat_abs := ((int.coe_nat_le_coe_nat_iff 1 k.nat_abs).1 ((int_to_nat k one_le_k) ▸ one_le_k)), --- have k_nat_lt_n : k.nat_abs < n := ((int.coe_nat_lt_coe_nat_iff k.nat_abs n).1 ((int_to_nat k one_le_k) ▸ k_lt_n)), --- have := period_ge_n' k.nat_abs one_le_k_nat k_nat_lt_n, --- rw [(zpow_coe_nat g k.nat_abs).symm, (int_to_nat k one_le_k).symm] at this, --- exact this }, --- have := moves_inj period_ge_n, --- done --- end --- lemma moves_1234_of_moves_12 {g : G} {x : α} (xmoves : g^12 • x ≠ x) : function.injective (λi : fin 5, g^(i:ℤ) • x) := begin --- apply moves_inj, --- intros k k_ge_1 k_lt_5, --- by_contra xfixed, --- have k_div_12 : k * (12 / k) = 12 := begin --- interval_cases using k_ge_1 k_lt_5; norm_num --- end, --- have veryfixed : g^12 • x = x := begin --- let := smul_zpow_eq_of_smul_eq (12/k) xfixed, --- rw [← zpow_mul,k_div_12] at this, --- norm_cast at this --- end, --- exact xmoves veryfixed --- end --- lemma proposition_1_1_2 (f g : G) [t2_space α] : is_locally_moving G α → is_algebraically_disjoint f g → disjoint (support α f) (support α (g^12)) := begin --- intros locally_moving alg_disjoint, --- -- suppose to the contrary that the set U = supp(f) ∩ supp(g^12) is nonempty --- by_contra not_disjoint, --- let U := support α f ∩ support α (g^12), --- have U_nonempty : U.nonempty := Set.not_disjoint_iff_nonempty_inter.mp not_disjoint, --- -- since X is Hausdorff, we can find a nonempty open set V ⊆ U such that f(V) is disjoint from V and the sets {g^i(V): i=0..4} are pairwise disjoint --- let x := U_nonempty.some, --- have five_points : function.injective (λi : fin 5, g^(i:ℤ) • x) := moves_1234_of_moves_12 (mem_support.mp $ (Set.inter_subset_right _ _) U_nonempty.some_mem), --- rcases disjoint_nbhd_in (is_open.inter (support_open f) (support_open $ g^12)) U_nonempty.some_mem ((Set.inter_subset_left _ _) U_nonempty.some_mem) with ⟨V₀,open_V₀,x_in_V₀,V₀_in_support,disjoint_img_V₀⟩, --- rcases disjoint_nbhd_fin five_points with ⟨V₁,open_V₁,x_in_V₁,disjoint_img_V₁⟩, --- simp only at disjoint_img_V₁, --- let V := V₀ ∩ V₁, --- -- let h be a nontrivial element of rigid_stabilizer G V, and note that [f,h]≠1 since f(V) is disjoint from V --- let ristV_ne_bot := locally_moving V (is_open.inter open_V₀ open_V₁) (Set.nonempty_of_mem ⟨x_in_V₀,x_in_V₁⟩), --- rcases (or_iff_right ristV_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) with ⟨h,h_in_ristV,h_ne_one⟩, --- have comm_non_trivial : ¬commute f h := begin --- by_contra comm_trivial, --- rcases faithful_rist_moves_point h_in_ristV h_ne_one with ⟨z,z_in_V,z_moved⟩, --- let act_comm := disjoint_support_comm h f (rist_supported_in_set h_in_ristV) (Set.disjoint_of_subset (Set.inter_subset_left V₀ V₁) (smul''_subset f (Set.inter_subset_left V₀ V₁)) disjoint_img_V₀) z z_in_V, --- rw [commutator_element_eq_one_iff_commute.mpr comm_trivial.symm,one_smul] at act_comm, --- exact z_moved act_comm.symm, --- end, --- -- since g is algebraically disjoint from f, there exist f₁,f₂ ∈ C_G(g) so that the commutator h' = [f1,[f2,h]] is a nontrivial element of C_G(g) --- rcases alg_disjoint h comm_non_trivial with ⟨f₁,f₂,f₁_commutes,f₂_commutes,h'_commutes,h'_non_trivial⟩, --- let h' := ⁅f₁,⁅f₂,h⁆⁆, --- -- now observe that supp([f₂, h]) ⊆ V ∪ f₂(V), and by the same reasoning supp(h')⊆V∪f₁(V)∪f₂(V)∪f₁f₂(V) --- have support_f₂h : support α ⁅f₂,h⁆ ⊆ V ∪ (f₂ •'' V) := (support_comm α f₂ h).trans (Set.union_subset_union (rist_supported_in_set h_in_ristV) $ smul''_subset f₂ $ rist_supported_in_set h_in_ristV), --- have support_h' : support α h' ⊆ ⋃(i : fin 2 × fin 2), (f₁^i.1.val*f₂^i.2.val) •'' V := begin --- let this := (support_comm α f₁ ⁅f₂,h⁆).trans (Set.union_subset_union support_f₂h (smul''_subset f₁ support_f₂h)), --- rw [smul''_union,← one_smul'' V,← mul_smul'',← mul_smul'',← mul_smul'',mul_one,mul_one] at this, --- let rw_u := rewrite_Union (λi : fin 2 × fin 2, (f₁^i.1.val*f₂^i.2.val) •'' V), --- simp only [fin.val_eq_coe, fin.val_zero', pow_zero, mul_one, fin.val_one, pow_one, one_mul] at rw_u, --- exact rw_u.symm ▸ this, --- end, --- -- since h' is nontrivial, it has at least one point p in its support --- cases faithful_moves_point' α h'_non_trivial with p p_moves, --- -- since g commutes with h', all five of the points {gi(p):i=0..4} lie in supp(h') --- have gi_in_support : ∀i : fin 5, g^i.val • p ∈ support α h' := begin --- intro i, --- rw mem_support, --- by_contra p_fixed, --- rw [← mul_smul,(h'_commutes.pow_right i.val).eq,mul_smul,smul_left_cancel_iff] at p_fixed, --- exact p_moves p_fixed, --- end, --- -- by the pigeonhole principle, one of the four sets V, f₁(V), f₂(V), f₁f₂(V) must contain two of these points, say g^i(p),g^j(p) ∈ k(V) for some 0 ≤ i < j ≤ 4 and k ∈ {1,f₁,f₂,f₁f₂} --- let pigeonhole : fintype.card (fin 5) > fintype.card (fin 2 × fin 2) := dec_trivial, --- let choice := λi : fin 5, (Set.mem_Union.mp $ support_h' $ gi_in_support i).some, --- rcases finset.exists_ne_map_eq_of_card_lt_of_maps_to pigeonhole (λ(i : fin 5) _, finset.mem_univ (choice i)) with ⟨i,_,j,_,i_ne_j,same_choice⟩, --- clear h_1_w h_1_h_h_w pigeonhole, --- let k := f₁^(choice i).1.val*f₂^(choice i).2.val, --- have same_k : f₁^(choice j).1.val*f₂^(choice j).2.val = k := by { simp only at same_choice, --- rw ← same_choice }, --- have g_i : g^i.val • p ∈ k •'' V := (Set.mem_Union.mp $ support_h' $ gi_in_support i).some_spec, --- have g_j : g^j.val • p ∈ k •'' V := same_k ▸ (Set.mem_Union.mp $ support_h' $ gi_in_support j).some_spec, --- -- but since g^(j−i)(V) is disjoint from V and k commutes with g, we know that g^(j−i)k(V) is disjoint from k(V), a contradiction since g^i(p) and g^j(p) both lie in k(V). --- have g_disjoint : disjoint ((g^i.val)⁻¹ •'' V) ((g^j.val)⁻¹ •'' V) := begin --- let := (disjoint_smul'' (g^(-(i.val+j.val : ℤ))) (disjoint_img_V₁ i j i_ne_j)).symm, --- rw [← mul_smul'',← mul_smul'',← zpow_add,← zpow_add] at this, --- simp only [fin.val_eq_coe, neg_add_rev, coe_coe, neg_add_cancel_right, zpow_neg, zpow_coe_nat, neg_add_cancel_comm] at this, --- from Set.disjoint_of_subset (smul''_subset _ (Set.inter_subset_right V₀ V₁)) (smul''_subset _ (Set.inter_subset_right V₀ V₁)) this --- end, --- have k_commutes : commute k g := commute.mul_left (f₁_commutes.pow_left (choice i).1.val) (f₂_commutes.pow_left (choice i).2.val), --- have g_k_disjoint : disjoint ((g^i.val)⁻¹ •'' (k •'' V)) ((g^j.val)⁻¹ •'' (k •'' V)) := begin --- let this := disjoint_smul'' k g_disjoint, --- rw [← mul_smul'',← mul_smul'',← inv_pow g i.val,← inv_pow g j.val, --- ← (k_commutes.symm.inv_left.pow_left i.val).eq, --- ← (k_commutes.symm.inv_left.pow_left j.val).eq, --- mul_smul'',inv_pow g i.val,mul_smul'' (g⁻¹^j.val) k V,inv_pow g j.val] at this, --- from this --- end, --- exact Set.disjoint_left.mp g_k_disjoint (mem_inv_smul''.mpr g_i) (mem_inv_smul''.mpr g_j) --- end --- lemma remark_1_2 (f g : G) : is_algebraically_disjoint f g → commute f g := begin --- intro alg_disjoint, --- by_contra non_commute, --- rcases alg_disjoint g non_commute with ⟨_,_,_,b,_,d⟩, --- rw [commutator_element_eq_one_iff_commute.mpr b,commutator_element_one_right] at d, --- tauto --- end --- section remark_1_3 --- def G := equiv.perm (fin 2) --- def σ := equiv.swap (0 : fin 2) (1 : fin 2) --- example : is_algebraically_disjoint σ σ := begin --- intro h, --- fin_cases h, --- intro hyp1, --- exfalso, --- swap, intro hyp2, exfalso, --- -- is commute decidable? cc, --- sorry -- dec_trivial --- sorry -- second sorry needed --- end --- end remark_1_3 -end AlgebraicDisjointness - ---------------------------------------------------------------- section Rubin.RegularSupport.RegularSupport -variable [TopologicalSpace α] [Rubin.Topological.ContinuousMulAction G α] +variable [TopologicalSpace α] [Rubin.ContinuousMulAction G α] def RegularSupport.InteriorClosure (U : Set α) := interior (closure U) @@ -563,7 +122,7 @@ theorem RegularSupport.regularSupport_regular {g : G} : theorem RegularSupport.support_subset_regularSupport [T2Space α] (g : G) : Support α g ⊆ Rubin.RegularSupport.RegularSupport α g := - Rubin.RegularSupport.IsOpen.interiorClosure_subset (Rubin.Topological.support_open g) + Rubin.RegularSupport.IsOpen.interiorClosure_subset (Rubin.support_open g) #align support_in_regular_support Rubin.RegularSupport.support_subset_regularSupport theorem RegularSupport.mem_regularSupport (g : G) (U : Set α) : @@ -575,7 +134,7 @@ theorem RegularSupport.mem_regularSupport (g : G) (U : Set α) : -- FIXME: Weird naming? def RegularSupport.AlgebraicCentralizer (f : G) : Set G := - {h | ∃ g, h = g ^ 12 ∧ Rubin.is_algebraically_disjoint f g} + {h | ∃ g, h = g ^ 12 ∧ AlgebraicallyDisjoint f g} #align algebraic_centralizer Rubin.RegularSupport.AlgebraicCentralizer end Rubin.RegularSupport.RegularSupport diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean new file mode 100644 index 0000000..13cd696 --- /dev/null +++ b/Rubin/AlgebraicDisjointness.lean @@ -0,0 +1,399 @@ +import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.GroupTheory.Subgroup.Basic +import Mathlib.GroupTheory.Subgroup.Actions +import Mathlib.Topology.Basic +import Mathlib.Tactic.FinCases + +import Rubin.RigidStabilizer +import Rubin.SmulImage +import Rubin.Topological +import Rubin.FaithfulAction + +namespace Rubin + +class LocallyMoving (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] := + locally_moving: ∀ U : Set α, IsOpen U → Set.Nonempty U → RigidStabilizer G U ≠ ⊥ +#align is_locally_moving Rubin.LocallyMoving + +namespace LocallyMoving + +theorem get_nontrivial_rist_elem {G α : Type _} + [Group G] + [TopologicalSpace α] + [MulAction G α] + [h_lm : LocallyMoving G α] + {U: Set α} + (U_open : IsOpen U) + (U_nonempty : U.Nonempty) : + ∃ x : G, x ∈ RigidStabilizer G U ∧ x ≠ 1 := +by + have rist_ne_bot := h_lm.locally_moving U U_open U_nonempty + exact (or_iff_right rist_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) + +end LocallyMoving + +def AlgebraicallyDisjoint {G : Type _} [Group G] (f g : G) := + ∀ h : G, + ¬Commute f h → + ∃ f₁ f₂ : G, Commute f₁ g ∧ Commute f₂ g ∧ Commute ⁅f₁, ⁅f₂, h⁆⁆ g ∧ ⁅f₁, ⁅f₂, h⁆⁆ ≠ 1 +#align is_algebraically_disjoint Rubin.AlgebraicallyDisjoint + +@[simp] +theorem orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) : + MulAction.orbit (⊥ : Subgroup G) p = {p} := + by + ext1 + rw [MulAction.mem_orbit_iff] + constructor + · rintro ⟨⟨_, g_bot⟩, g_to_x⟩ + rw [← g_to_x, Set.mem_singleton_iff, Subgroup.mk_smul] + exact (Subgroup.mem_bot.mp g_bot).symm ▸ one_smul _ _ + exact fun h => ⟨1, Eq.trans (one_smul _ p) (Set.mem_singleton_iff.mp h).symm⟩ +#align orbit_bot Rubin.orbit_bot + +variable {G α : Type _} +variable [Group G] +variable [TopologicalSpace α] +variable [ContinuousMulAction G α] +variable [FaithfulSMul G α] + +instance dense_locally_moving [T2Space α] + (H_nip : has_no_isolated_points α) + (H_ld : LocallyDense G α) : + LocallyMoving G α +where + locally_moving := by + 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 + rw [h_rs] at some_in_orbit + simp at some_in_orbit + +lemma disjoint_nbhd [T2Space α] {g : G} {x : α} (x_moved: g • x ≠ x) : + ∃ U: Set α, IsOpen U ∧ x ∈ U ∧ Disjoint U (g •'' U) := +by + have ⟨V, W, V_open, W_open, gx_in_V, x_in_W, disjoint_V_W⟩ := T2Space.t2 (g • x) x x_moved + let U := (g⁻¹ •'' V) ∩ W + use U + constructor + { + -- NOTE: if this is common, then we should make a tactic for solving IsOpen goals + exact IsOpen.inter (img_open_open g⁻¹ V V_open) W_open + } + constructor + { + simp + rw [mem_inv_smulImage] + trivial + } + { + apply Set.disjoint_of_subset + · apply Set.inter_subset_right + · intro y hy; show y ∈ V + + rw [<-smul_inv_smul g y] + rw [<-mem_inv_smulImage] + + rw [mem_smulImage] at hy + simp at hy + + exact hy.left + · exact disjoint_V_W.symm + } + +lemma disjoint_nbhd_in [T2Space α] {g : G} {x : α} {V : Set α} + (V_open : IsOpen V) (x_in_V : x ∈ V) (x_moved : g • x ≠ x) : + ∃ U : Set α, IsOpen U ∧ x ∈ U ∧ U ⊆ V ∧ Disjoint U (g •'' U) := +by + have ⟨W, W_open, x_in_W, disjoint_W_img⟩ := disjoint_nbhd x_moved + use W ∩ V + simp + constructor + { + apply IsOpen.inter <;> assumption + } + constructor + { + constructor <;> assumption + } + show Disjoint (W ∩ V) (g •'' W ∩ V) + apply Set.disjoint_of_subset + · exact Set.inter_subset_left W V + · show g •'' W ∩ V ⊆ g •'' W + rewrite [smulImage_inter] + exact Set.inter_subset_left _ _ + · exact disjoint_W_img + +-- Kind of a boring lemma but okay +lemma rewrite_Union (f : Fin 2 × Fin 2 → Set α) : + (⋃(i : Fin 2 × Fin 2), f i) = (f (0,0) ∪ f (0,1)) ∪ (f (1,0) ∪ f (1,1)) := +by + ext x + simp only [Set.mem_iUnion, Set.mem_union] + constructor + · rewrite [forall_exists_index] + intro i + fin_cases i + <;> simp only [Fin.zero_eta, Fin.mk_one] + <;> intro h + <;> simp only [h, true_or, or_true] + · rintro ((h|h)|(h|h)) <;> exact ⟨_, h⟩ + +-- TODO: modify the proof to be less "let everything"-y, especially the first half +lemma proposition_1_1_1 [h_lm : LocallyMoving G α] [T2Space α] (f g : G) (supp_disjoint : Disjoint (Support α f) (Support α g)) : AlgebraicallyDisjoint f g := by + intros h h_not_commute + -- h is not the identity on `Support α f` + have f_h_not_disjoint := (mt (disjoint_commute (G := G) (α := α)) h_not_commute) + have ⟨x, ⟨x_in_supp_f, x_in_supp_h⟩⟩ := Set.not_disjoint_iff.mp f_h_not_disjoint + have hx_ne_x := mem_support.mp x_in_supp_h + + -- Since α is Hausdoff, there is a nonempty V ⊆ Support α f, with h •'' V disjoint from V + have ⟨V, V_open, x_in_V, V_in_support, disjoint_img_V⟩ := disjoint_nbhd_in (support_open f) x_in_supp_f hx_ne_x + + -- let f₂ be a nontrivial element of the RigidStabilizer G V + let ⟨f₂, f₂_in_rist_V, f₂_ne_one⟩ := h_lm.get_nontrivial_rist_elem V_open (Set.nonempty_of_mem x_in_V) + + -- Re-use the Hausdoff property of α again, this time yielding W ⊆ V + let ⟨y, y_moved⟩ := faithful_moves_point' α f₂_ne_one + have y_in_V := (rist_supported_in_set f₂_in_rist_V) (mem_support.mpr y_moved) + let ⟨W, W_open, y_in_W, W_in_V, disjoint_img_W⟩ := disjoint_nbhd_in V_open y_in_V y_moved + + -- Let f₁ be a nontrivial element of RigidStabilizer G W + let ⟨f₁, f₁_in_rist_W, f₁_ne_one⟩ := h_lm.get_nontrivial_rist_elem W_open (Set.nonempty_of_mem y_in_W) + + use f₁ + use f₂ + constructor <;> try constructor + · apply disjoint_commute (α := α) + apply Set.disjoint_of_subset_left _ supp_disjoint + calc + Support α f₁ ⊆ W := rist_supported_in_set f₁_in_rist_W + W ⊆ V := W_in_V + V ⊆ Support α f := V_in_support + · apply disjoint_commute (α := α) + apply Set.disjoint_of_subset_left _ supp_disjoint + calc + Support α f₂ ⊆ V := rist_supported_in_set f₂_in_rist_V + V ⊆ Support α f := V_in_support + + -- We claim that [f₁, [f₂, h]] is a nontrivial elelement of Centralizer G g + let k := ⁅f₂, h⁆ + have h₂ : ∀ z ∈ W, f₂ • z = k • z := by + intro z z_in_W + simp + symm + apply disjoint_support_comm f₂ h _ disjoint_img_V + · exact W_in_V z_in_W + · exact rist_supported_in_set f₂_in_rist_V + + constructor + · -- then `k*f₁⁻¹*k⁻¹` is supported on k W = f₂ W, + -- so [f₁,k] is supported on W ∪ f₂ W ⊆ V ⊆ support f, so commutes with g. + apply disjoint_commute (α := α) + apply Set.disjoint_of_subset_left _ supp_disjoint + have supp_f₁_subset_W := (rist_supported_in_set f₁_in_rist_W) + + show Support α ⁅f₁, ⁅f₂, h⁆⁆ ⊆ Support α f + calc + Support α ⁅f₁, k⁆ = Support α ⁅k, f₁⁆ := by rw [<-commutatorElement_inv, support_inv] + _ ⊆ Support α f₁ ∪ (k •'' Support α f₁) := support_comm α k f₁ + _ ⊆ W ∪ (k •'' Support α f₁) := Set.union_subset_union_left _ supp_f₁_subset_W + _ ⊆ W ∪ (k •'' W) := by + apply Set.union_subset_union_right + exact (smulImage_subset k supp_f₁_subset_W) + _ = W ∪ (f₂ •'' W) := by rw [<-smulImage_eq_of_smul_eq h₂] + _ ⊆ V ∪ (f₂ •'' W) := Set.union_subset_union_left _ W_in_V + _ ⊆ V ∪ V := by + apply Set.union_subset_union_right + apply smulImage_subset_in_support f₂ W V W_in_V + exact rist_supported_in_set f₂_in_rist_V + _ ⊆ V := by rw [Set.union_self] + _ ⊆ Support α f := V_in_support + + · -- finally, [f₁,k] agrees with f₁ on W, so is not the identity. + have h₄: ∀ z ∈ W, ⁅f₁, k⁆ • z = f₁ • z := by + apply disjoint_support_comm f₁ k + exact rist_supported_in_set f₁_in_rist_W + rw [<-smulImage_eq_of_smul_eq h₂] + exact disjoint_img_W + let ⟨z, z_in_W, z_moved⟩ := faithful_rigid_stabilizer_moves_point f₁_in_rist_W f₁_ne_one + + by_contra h₅ + rw [<-h₄ z z_in_W] at z_moved + have h₆ : ⁅f₁, ⁅f₂, h⁆⁆ • z = z := by rw [h₅, one_smul] + exact z_moved h₆ +#align proposition_1_1_1 Rubin.proposition_1_1_1 + +-- @[simp] lemma smul''_mul {g h : G} {U : set α} : g •'' (h •'' U) = (g*h) •'' U := +-- (mul_smul'' g h U).symm +-- lemma disjoint_nbhd_fin {ι : Type*} [fintype ι] {f : ι → G} {x : α} [t2_space α] : (λi : ι, f i • x).injective → ∃U : set α, is_open U ∧ x ∈ U ∧ (∀i j : ι, i ≠ j → disjoint (f i •'' U) (f j •'' U)) := begin +-- intro f_injective, +-- let disjoint_hyp := λi j (i_ne_j : i≠j), let x_moved : ((f j)⁻¹ * f i) • x ≠ x := begin +-- by_contra, +-- let := smul_congr (f j) h, +-- rw [mul_smul, ← mul_smul,mul_right_inv,one_smul] at this, +-- from i_ne_j (f_injective this), +-- end in disjoint_nbhd x_moved, +-- let ι2 := { p : ι×ι // p.1 ≠ p.2 }, +-- let U := ⋂(p : ι2), (disjoint_hyp p.1.1 p.1.2 p.2).some, +-- use U, +-- split, +-- exact is_open_Inter (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.1), +-- split, +-- exact Set.mem_Inter.mpr (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.2.1), +-- intros i j i_ne_j, +-- let U_inc := Set.Inter_subset (λ p : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some) ⟨⟨i,j⟩,i_ne_j⟩, +-- let := (disjoint_smul'' (f j) (Set.disjoint_of_subset U_inc (smul''_subset ((f j)⁻¹ * (f i)) U_inc) (disjoint_hyp i j i_ne_j).some_spec.2.2)).symm, +-- simp only [subtype.val_eq_coe, smul''_mul, mul_inv_cancel_left] at this, +-- from this +-- end +-- lemma moves_inj {g : G} {x : α} {n : ℕ} (period_ge_n : ∀ (k : ℤ), 1 ≤ k → k < n → g ^ k • x ≠ x) : function.injective (λ (i : fin n), g ^ (i : ℤ) • x) := begin +-- intros i j same_img, +-- by_contra i_ne_j, +-- let same_img' := congr_arg ((•) (g ^ (-(j : ℤ)))) same_img, +-- simp only [inv_smul_smul] at same_img', +-- rw [← mul_smul,← mul_smul,← zpow_add,← zpow_add,add_comm] at same_img', +-- simp only [add_left_neg, zpow_zero, one_smul] at same_img', +-- let ij := |(i:ℤ) - (j:ℤ)|, +-- rw ← sub_eq_add_neg at same_img', +-- have xfixed : g^ij • x = x := begin +-- cases abs_cases ((i:ℤ) - (j:ℤ)), +-- { rw ← h.1 at same_img', exact same_img' }, +-- { rw [smul_eq_iff_inv_smul_eq,← zpow_neg,← h.1] at same_img', exact same_img' } +-- end, +-- have ij_ge_1 : 1 ≤ ij := int.add_one_le_iff.mpr (abs_pos.mpr $ sub_ne_zero.mpr $ norm_num.nat_cast_ne i j ↑i ↑j rfl rfl (fin.vne_of_ne i_ne_j)), +-- let neg_le := int.sub_lt_sub_of_le_of_lt (nat.cast_nonneg i) (nat.cast_lt.mpr (fin.prop _)), +-- rw zero_sub at neg_le, +-- let le_pos := int.sub_lt_sub_of_lt_of_le (nat.cast_lt.mpr (fin.prop _)) (nat.cast_nonneg j), +-- rw sub_zero at le_pos, +-- have ij_lt_n : ij < n := abs_lt.mpr ⟨ neg_le, le_pos ⟩, +-- exact period_ge_n ij ij_ge_1 ij_lt_n xfixed, +-- end +-- lemma int_to_nat (k : ℤ) (k_pos : k ≥ 1) : k = k.nat_abs := begin +-- cases (int.nat_abs_eq k), +-- { exact h }, +-- { have : -(k.nat_abs : ℤ) ≤ 0 := neg_nonpos.mpr (int.nat_abs k).cast_nonneg, +-- rw ← h at this, by_contra, linarith } +-- end +-- lemma moves_inj_N {g : G} {x : α} {n : ℕ} (period_ge_n' : ∀ (k : ℕ), 1 ≤ k → k < n → g ^ k • x ≠ x) : function.injective (λ (i : fin n), g ^ (i : ℕ) • x) := begin +-- have period_ge_n : ∀ (k : ℤ), 1 ≤ k → k < n → g ^ k • x ≠ x, +-- { intros k one_le_k k_lt_n, +-- have one_le_k_nat : 1 ≤ k.nat_abs := ((int.coe_nat_le_coe_nat_iff 1 k.nat_abs).1 ((int_to_nat k one_le_k) ▸ one_le_k)), +-- have k_nat_lt_n : k.nat_abs < n := ((int.coe_nat_lt_coe_nat_iff k.nat_abs n).1 ((int_to_nat k one_le_k) ▸ k_lt_n)), +-- have := period_ge_n' k.nat_abs one_le_k_nat k_nat_lt_n, +-- rw [(zpow_coe_nat g k.nat_abs).symm, (int_to_nat k one_le_k).symm] at this, +-- exact this }, +-- have := moves_inj period_ge_n, +-- done +-- end +-- lemma moves_1234_of_moves_12 {g : G} {x : α} (xmoves : g^12 • x ≠ x) : function.injective (λi : fin 5, g^(i:ℤ) • x) := begin +-- apply moves_inj, +-- intros k k_ge_1 k_lt_5, +-- by_contra xfixed, +-- have k_div_12 : k * (12 / k) = 12 := begin +-- interval_cases using k_ge_1 k_lt_5; norm_num +-- end, +-- have veryfixed : g^12 • x = x := begin +-- let := smul_zpow_eq_of_smul_eq (12/k) xfixed, +-- rw [← zpow_mul,k_div_12] at this, +-- norm_cast at this +-- end, +-- exact xmoves veryfixed +-- end +-- lemma proposition_1_1_2 (f g : G) [t2_space α] : is_locally_moving G α → is_algebraically_disjoint f g → disjoint (support α f) (support α (g^12)) := begin +-- intros locally_moving alg_disjoint, +-- -- suppose to the contrary that the set U = supp(f) ∩ supp(g^12) is nonempty +-- by_contra not_disjoint, +-- let U := support α f ∩ support α (g^12), +-- have U_nonempty : U.nonempty := Set.not_disjoint_iff_nonempty_inter.mp not_disjoint, +-- -- since X is Hausdorff, we can find a nonempty open set V ⊆ U such that f(V) is disjoint from V and the sets {g^i(V): i=0..4} are pairwise disjoint +-- let x := U_nonempty.some, +-- have five_points : function.injective (λi : fin 5, g^(i:ℤ) • x) := moves_1234_of_moves_12 (mem_support.mp $ (Set.inter_subset_right _ _) U_nonempty.some_mem), +-- rcases disjoint_nbhd_in (is_open.inter (support_open f) (support_open $ g^12)) U_nonempty.some_mem ((Set.inter_subset_left _ _) U_nonempty.some_mem) with ⟨V₀,open_V₀,x_in_V₀,V₀_in_support,disjoint_img_V₀⟩, +-- rcases disjoint_nbhd_fin five_points with ⟨V₁,open_V₁,x_in_V₁,disjoint_img_V₁⟩, +-- simp only at disjoint_img_V₁, +-- let V := V₀ ∩ V₁, +-- -- let h be a nontrivial element of rigid_stabilizer G V, and note that [f,h]≠1 since f(V) is disjoint from V +-- let ristV_ne_bot := locally_moving V (is_open.inter open_V₀ open_V₁) (Set.nonempty_of_mem ⟨x_in_V₀,x_in_V₁⟩), +-- rcases (or_iff_right ristV_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) with ⟨h,h_in_ristV,h_ne_one⟩, +-- have comm_non_trivial : ¬commute f h := begin +-- by_contra comm_trivial, +-- rcases faithful_rist_moves_point h_in_ristV h_ne_one with ⟨z,z_in_V,z_moved⟩, +-- let act_comm := disjoint_support_comm h f (rist_supported_in_set h_in_ristV) (Set.disjoint_of_subset (Set.inter_subset_left V₀ V₁) (smul''_subset f (Set.inter_subset_left V₀ V₁)) disjoint_img_V₀) z z_in_V, +-- rw [commutator_element_eq_one_iff_commute.mpr comm_trivial.symm,one_smul] at act_comm, +-- exact z_moved act_comm.symm, +-- end, +-- -- since g is algebraically disjoint from f, there exist f₁,f₂ ∈ C_G(g) so that the commutator h' = [f1,[f2,h]] is a nontrivial element of C_G(g) +-- rcases alg_disjoint h comm_non_trivial with ⟨f₁,f₂,f₁_commutes,f₂_commutes,h'_commutes,h'_non_trivial⟩, +-- let h' := ⁅f₁,⁅f₂,h⁆⁆, +-- -- now observe that supp([f₂, h]) ⊆ V ∪ f₂(V), and by the same reasoning supp(h')⊆V∪f₁(V)∪f₂(V)∪f₁f₂(V) +-- have support_f₂h : support α ⁅f₂,h⁆ ⊆ V ∪ (f₂ •'' V) := (support_comm α f₂ h).trans (Set.union_subset_union (rist_supported_in_set h_in_ristV) $ smul''_subset f₂ $ rist_supported_in_set h_in_ristV), +-- have support_h' : support α h' ⊆ ⋃(i : fin 2 × fin 2), (f₁^i.1.val*f₂^i.2.val) •'' V := begin +-- let this := (support_comm α f₁ ⁅f₂,h⁆).trans (Set.union_subset_union support_f₂h (smul''_subset f₁ support_f₂h)), +-- rw [smul''_union,← one_smul'' V,← mul_smul'',← mul_smul'',← mul_smul'',mul_one,mul_one] at this, +-- let rw_u := rewrite_Union (λi : fin 2 × fin 2, (f₁^i.1.val*f₂^i.2.val) •'' V), +-- simp only [fin.val_eq_coe, fin.val_zero', pow_zero, mul_one, fin.val_one, pow_one, one_mul] at rw_u, +-- exact rw_u.symm ▸ this, +-- end, +-- -- since h' is nontrivial, it has at least one point p in its support +-- cases faithful_moves_point' α h'_non_trivial with p p_moves, +-- -- since g commutes with h', all five of the points {gi(p):i=0..4} lie in supp(h') +-- have gi_in_support : ∀i : fin 5, g^i.val • p ∈ support α h' := begin +-- intro i, +-- rw mem_support, +-- by_contra p_fixed, +-- rw [← mul_smul,(h'_commutes.pow_right i.val).eq,mul_smul,smul_left_cancel_iff] at p_fixed, +-- exact p_moves p_fixed, +-- end, +-- -- by the pigeonhole principle, one of the four sets V, f₁(V), f₂(V), f₁f₂(V) must contain two of these points, say g^i(p),g^j(p) ∈ k(V) for some 0 ≤ i < j ≤ 4 and k ∈ {1,f₁,f₂,f₁f₂} +-- let pigeonhole : fintype.card (fin 5) > fintype.card (fin 2 × fin 2) := dec_trivial, +-- let choice := λi : fin 5, (Set.mem_Union.mp $ support_h' $ gi_in_support i).some, +-- rcases finset.exists_ne_map_eq_of_card_lt_of_maps_to pigeonhole (λ(i : fin 5) _, finset.mem_univ (choice i)) with ⟨i,_,j,_,i_ne_j,same_choice⟩, +-- clear h_1_w h_1_h_h_w pigeonhole, +-- let k := f₁^(choice i).1.val*f₂^(choice i).2.val, +-- have same_k : f₁^(choice j).1.val*f₂^(choice j).2.val = k := by { simp only at same_choice, +-- rw ← same_choice }, +-- have g_i : g^i.val • p ∈ k •'' V := (Set.mem_Union.mp $ support_h' $ gi_in_support i).some_spec, +-- have g_j : g^j.val • p ∈ k •'' V := same_k ▸ (Set.mem_Union.mp $ support_h' $ gi_in_support j).some_spec, +-- -- but since g^(j−i)(V) is disjoint from V and k commutes with g, we know that g^(j−i)k(V) is disjoint from k(V), a contradiction since g^i(p) and g^j(p) both lie in k(V). +-- have g_disjoint : disjoint ((g^i.val)⁻¹ •'' V) ((g^j.val)⁻¹ •'' V) := begin +-- let := (disjoint_smul'' (g^(-(i.val+j.val : ℤ))) (disjoint_img_V₁ i j i_ne_j)).symm, +-- rw [← mul_smul'',← mul_smul'',← zpow_add,← zpow_add] at this, +-- simp only [fin.val_eq_coe, neg_add_rev, coe_coe, neg_add_cancel_right, zpow_neg, zpow_coe_nat, neg_add_cancel_comm] at this, +-- from Set.disjoint_of_subset (smul''_subset _ (Set.inter_subset_right V₀ V₁)) (smul''_subset _ (Set.inter_subset_right V₀ V₁)) this +-- end, +-- have k_commutes : commute k g := commute.mul_left (f₁_commutes.pow_left (choice i).1.val) (f₂_commutes.pow_left (choice i).2.val), +-- have g_k_disjoint : disjoint ((g^i.val)⁻¹ •'' (k •'' V)) ((g^j.val)⁻¹ •'' (k •'' V)) := begin +-- let this := disjoint_smul'' k g_disjoint, +-- rw [← mul_smul'',← mul_smul'',← inv_pow g i.val,← inv_pow g j.val, +-- ← (k_commutes.symm.inv_left.pow_left i.val).eq, +-- ← (k_commutes.symm.inv_left.pow_left j.val).eq, +-- mul_smul'',inv_pow g i.val,mul_smul'' (g⁻¹^j.val) k V,inv_pow g j.val] at this, +-- from this +-- end, +-- exact Set.disjoint_left.mp g_k_disjoint (mem_inv_smul''.mpr g_i) (mem_inv_smul''.mpr g_j) +-- end +-- lemma remark_1_2 (f g : G) : is_algebraically_disjoint f g → commute f g := begin +-- intro alg_disjoint, +-- by_contra non_commute, +-- rcases alg_disjoint g non_commute with ⟨_,_,_,b,_,d⟩, +-- rw [commutator_element_eq_one_iff_commute.mpr b,commutator_element_one_right] at d, +-- tauto +-- end +-- section remark_1_3 +-- def G := equiv.perm (fin 2) +-- def σ := equiv.swap (0 : fin 2) (1 : fin 2) +-- example : is_algebraically_disjoint σ σ := begin +-- intro h, +-- fin_cases h, +-- intro hyp1, +-- exfalso, +-- swap, intro hyp2, exfalso, +-- -- is commute decidable? cc, +-- sorry -- dec_trivial +-- sorry -- second sorry needed +-- end +-- end remark_1_3 + +end Rubin diff --git a/Rubin/FaithfulAction.lean b/Rubin/FaithfulAction.lean index 16110e5..3bc5782 100644 --- a/Rubin/FaithfulAction.lean +++ b/Rubin/FaithfulAction.lean @@ -25,7 +25,7 @@ theorem faithful_moves_point' {g : G} (α : Type _) [MulAction G α] [FaithfulSM #align faithful_moves_point' Rubin.faithful_moves_point' theorem faithful_rigid_stabilizer_moves_point {g : G} {U : Set α} : - g ∈ rigidStabilizer G U → g ≠ 1 → ∃ x ∈ U, g • x ≠ x := + g ∈ RigidStabilizer G U → g ≠ 1 → ∃ x ∈ U, g • x ≠ x := by intro g_rigid g_ne_one let ⟨x, xmoved⟩ := Rubin.faithful_moves_point' α g_ne_one diff --git a/Rubin/Period.lean b/Rubin/Period.lean new file mode 100644 index 0000000..6b5bc60 --- /dev/null +++ b/Rubin/Period.lean @@ -0,0 +1,131 @@ +import Mathlib.Data.Finset.Basic +import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.GroupTheory.Exponent + +import Rubin.Tactic + +namespace Rubin.Period + +variable {G a : Type _} +variable [Group G] +variable [MulAction G α] + +noncomputable def period (p : α) (g : G) : ℕ := + sInf {n : ℕ | n > 0 ∧ g ^ n • p = p} +#align period Rubin.Period.period + +theorem period_le_fix {p : α} {g : G} {m : ℕ} (m_pos : m > 0) + (gmp_eq_p : g ^ m • p = p) : 0 < Rubin.Period.period p g ∧ Rubin.Period.period p g ≤ m := + by + constructor + · by_contra h'; have period_zero : Rubin.Period.period p g = 0; linarith; + rcases Nat.sInf_eq_zero.1 period_zero with ⟨cont, h_1⟩ | h; linarith; + exact Set.eq_empty_iff_forall_not_mem.mp h ↑m ⟨m_pos, gmp_eq_p⟩ + exact Nat.sInf_le ⟨m_pos, gmp_eq_p⟩ +#align period_le_fix Rubin.Period.period_le_fix + +theorem notfix_le_period {p : α} {g : G} {n : ℕ} (n_pos : n > 0) + (period_pos : Rubin.Period.period p g > 0) (pmoves : ∀ i : ℕ, 0 < i → i < n → g ^ i • p ≠ p) : + n ≤ Rubin.Period.period p g := by + by_contra period_le + exact + (pmoves (Rubin.Period.period p g) period_pos (not_le.mp period_le)) + (Nat.sInf_mem (Nat.nonempty_of_pos_sInf period_pos)).2 +#align notfix_le_period Rubin.Period.notfix_le_period + +theorem notfix_le_period' {p : α} {g : G} {n : ℕ} (n_pos : n > 0) + (period_pos : Rubin.Period.period p g > 0) + (pmoves : ∀ i : Fin n, 0 < (i : ℕ) → g ^ (i : ℕ) • p ≠ p) : n ≤ Rubin.Period.period p g := + Rubin.Period.notfix_le_period n_pos period_pos fun (i : ℕ) (i_pos : 0 < i) (i_lt_n : i < n) => + pmoves (⟨i, i_lt_n⟩ : Fin n) i_pos +#align notfix_le_period' Rubin.Period.notfix_le_period' + +theorem period_neutral_eq_one (p : α) : Rubin.Period.period p (1 : G) = 1 := + by + have : 0 < Rubin.Period.period p (1 : G) ∧ Rubin.Period.period p (1 : G) ≤ 1 := + Rubin.Period.period_le_fix (by norm_num : 1 > 0) + (by group_action : + (1 : G) ^ 1 • p = p) + linarith +#align period_neutral_eq_one Rubin.Period.period_neutral_eq_one + +def periods (U : Set α) (H : Subgroup G) : Set ℕ := + {n : ℕ | ∃ (p : α) (g : H), p ∈ U ∧ Rubin.Period.period (p : α) (g : G) = n} +#align periods Rubin.Period.periods + +-- TODO: split into multiple lemmas +theorem periods_lemmas {U : Set α} (U_nonempty : Set.Nonempty U) {H : Subgroup G} + (exp_ne_zero : Monoid.exponent H ≠ 0) : + (Rubin.Period.periods U H).Nonempty ∧ + BddAbove (Rubin.Period.periods U H) ∧ + ∃ (m : ℕ) (m_pos : m > 0), ∀ (p : α) (g : H), g ^ m • p = p := + by + rcases Monoid.exponentExists_iff_ne_zero.2 exp_ne_zero with ⟨m, m_pos, gm_eq_one⟩ + have gmp_eq_p : ∀ (p : α) (g : H), g ^ m • p = p := by + intro p g; rw [gm_eq_one g]; + group_action + have periods_nonempty : (Rubin.Period.periods U H).Nonempty := by + use 1 + let p := Set.Nonempty.some U_nonempty; use p + use 1 + constructor + · exact Set.Nonempty.some_mem U_nonempty + · exact Rubin.Period.period_neutral_eq_one p + + have periods_bounded : BddAbove (Rubin.Period.periods U H) := by + use m; intro some_period hperiod; + rcases hperiod with ⟨p, g, hperiod⟩ + rw [← hperiod.2] + exact (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).2 + exact ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩ +#align period_lemma Rubin.Period.periods_lemmas + +theorem period_from_exponent (U : Set α) (U_nonempty : U.Nonempty) {H : Subgroup G} + (exp_ne_zero : Monoid.exponent H ≠ 0) : + ∃ (p : α) (g : H) (n : ℕ), + p ∈ U ∧ n > 0 ∧ Rubin.Period.period (p : α) (g : G) = n ∧ n = sSup (Rubin.Period.periods U H) := + by + rcases Rubin.Period.periods_lemmas U_nonempty exp_ne_zero with + ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩ + rcases Nat.sSup_mem periods_nonempty periods_bounded with ⟨p, g, hperiod⟩ + use p + use g + use sSup (Rubin.Period.periods U H) + -- TODO: cleanup? + exact ⟨ + hperiod.1, + hperiod.2 ▸ (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).1, + hperiod.2, + rfl + ⟩ +#align period_from_exponent Rubin.Period.period_from_exponent + +theorem zero_lt_period_le_Sup_periods {U : Set α} (U_nonempty : U.Nonempty) + {H : Subgroup G} (exp_ne_zero : Monoid.exponent H ≠ 0) : + ∀ (p : U) (g : H), + 0 < Rubin.Period.period (p : α) (g : G) ∧ + Rubin.Period.period (p : α) (g : G) ≤ sSup (Rubin.Period.periods U H) := + by + rcases Rubin.Period.periods_lemmas U_nonempty exp_ne_zero with + ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩ + intro p g + have period_in_periods : Rubin.Period.period (p : α) (g : G) ∈ Rubin.Period.periods U H := by + use p; use g + simp + exact + ⟨(Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).1, + le_csSup periods_bounded period_in_periods⟩ +#align zero_lt_period_le_Sup_periods Rubin.Period.zero_lt_period_le_Sup_periods + +theorem pow_period_fix (p : α) (g : G) : g ^ Rubin.Period.period p g • p = p := + by + cases eq_zero_or_neZero (Rubin.Period.period p g) with + | inl h => rw [h]; simp + | inr h => + exact + (Nat.sInf_mem + (Nat.nonempty_of_pos_sInf + (Nat.pos_of_ne_zero (@NeZero.ne _ _ (Rubin.Period.period p g) h)))).2 +#align pow_period_fix Rubin.Period.pow_period_fix + +end Rubin.Period diff --git a/Rubin/Topological.lean b/Rubin/Topological.lean index 2cc59d8..c753d12 100644 --- a/Rubin/Topological.lean +++ b/Rubin/Topological.lean @@ -3,23 +3,25 @@ import Mathlib.GroupTheory.GroupAction.Basic import Mathlib.Topology.Basic import Mathlib.Topology.Homeomorph +import Rubin.RigidStabilizer import Rubin.MulActionExt import Rubin.SmulImage import Rubin.Support -namespace Rubin.Topological +namespace Rubin +section Continuity class ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] extends MulAction G α where continuous : ∀ g : G, Continuous (fun x: α => g • x) -#align continuous_mul_action Rubin.Topological.ContinuousMulAction +#align continuous_mul_action Rubin.ContinuousMulAction -- TODO: give this a notation? structure EquivariantHomeomorph (G α β : Type _) [Group G] [TopologicalSpace α] [TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where equivariant : is_equivariant G toFun -#align equivariant_homeomorph Rubin.Topological.EquivariantHomeomorph +#align equivariant_homeomorph Rubin.EquivariantHomeomorph variable {G α β : Type _} variable [Group G] @@ -29,7 +31,7 @@ theorem equivariant_fun [MulAction G α] [MulAction G β] (h : EquivariantHomeomorph G α β) : is_equivariant G h.toFun := h.equivariant -#align equivariant_fun Rubin.Topological.equivariant_fun +#align equivariant_fun Rubin.equivariant_fun theorem equivariant_inv [MulAction G α] [MulAction G β] (h : EquivariantHomeomorph G α β) : @@ -40,19 +42,19 @@ theorem equivariant_inv [MulAction G α] [MulAction G β] let e := congr_arg h.invFun (h.equivariant g (h.invFun x)) rw [h.left_inv _, h.right_inv _] at e exact e -#align equivariant_inv Rubin.Topological.equivariant_inv +#align equivariant_inv Rubin.equivariant_inv -variable [Rubin.Topological.ContinuousMulAction G α] +variable [Rubin.ContinuousMulAction G α] theorem img_open_open (g : G) (U : Set α) (h : IsOpen U): IsOpen (g •'' U) := by rw [Rubin.smulImage_eq_inv_preimage] - exact Continuous.isOpen_preimage (Rubin.Topological.ContinuousMulAction.continuous g⁻¹) U h + exact Continuous.isOpen_preimage (Rubin.ContinuousMulAction.continuous g⁻¹) U h -#align img_open_open Rubin.Topological.img_open_open +#align img_open_open Rubin.img_open_open theorem support_open (g : G) [TopologicalSpace α] [T2Space α] - [Rubin.Topological.ContinuousMulAction G α] : IsOpen (Support α g) := + [Rubin.ContinuousMulAction G α] : IsOpen (Support α g) := by apply isOpen_iff_forall_mem_open.mpr intro x xmoved @@ -63,9 +65,45 @@ theorem support_open (g : G) [TopologicalSpace α] [T2Space α] disjoint_U_V (mem_inv_smulImage.mp (Set.mem_of_mem_inter_right yW)) (Set.mem_of_mem_inter_left yW), - IsOpen.inter open_V (Rubin.Topological.img_open_open g⁻¹ U open_U), + IsOpen.inter open_V (Rubin.img_open_open g⁻¹ U open_U), ⟨x_in_V, mem_inv_smulImage.mpr gx_in_U⟩ ⟩ -#align support_open Rubin.Topological.support_open +#align support_open Rubin.support_open -end Rubin.Topological +end Continuity + +-- TODO: come up with a name +section Other +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 + +instance has_no_isolated_points_neBot {α : Type _} [TopologicalSpace α] (h_nip: has_no_isolated_points α) (x: α): Filter.NeBot (𝓝[≠] x) where + ne' := h_nip x + +class LocallyDense (G α : Type _) [Group G] [TopologicalSpace α] extends MulAction G α := + isLocallyDense: + ∀ U : Set α, + ∀ p ∈ U, + p ∈ interior (closure (MulAction.orbit (RigidStabilizer G U) p)) +#align is_locally_dense Rubin.LocallyDense + +namespace LocallyDense + +lemma 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 + intros U H_ne + exact ⟨H_ne.some, H_ne.some_mem, LocallyDense.isLocallyDense U H_ne.some H_ne.some_mem⟩ + +end LocallyDense + + +end Other + +end Rubin