From cd9ad02e1d58fde7e68bb9a532a8e8b60c81680e Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Fri, 24 Nov 2023 15:58:12 +0100 Subject: [PATCH] :sparkles: Prove disjoint_nbhd_fin --- Rubin/AlgebraicDisjointness.lean | 103 ++++++++++++++++++++++++------- Rubin/SmulImage.lean | 42 +++++++++++++ 2 files changed, 122 insertions(+), 23 deletions(-) diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean index 13cd696..09e4d1e 100644 --- a/Rubin/AlgebraicDisjointness.lean +++ b/Rubin/AlgebraicDisjointness.lean @@ -225,29 +225,86 @@ 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 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 +@[simp] lemma smulImage_mul {g h : G} {U : Set α} : g •'' (h •'' U) = (g*h) •'' U := + (mul_smulImage g h U) + +#check isOpen_iInter_of_finite + +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)) : + ((f j)⁻¹ * f i) • x ≠ x := by + by_contra h + apply i_ne_j + apply f_smul_inj + group_action + group_action at h + exact h + +def smul_inj_nbhd {ι : Type*} [Fintype ι] [T2Space α] + {f : ι → G} {x : α} {i j : ι} (i_ne_j : i ≠ j) + (f_smul_inj : Function.Injective (fun i : ι => (f i) • x)) : + Set α := + (disjoint_nbhd (smul_inj_moves i_ne_j f_smul_inj)).choose + +lemma smul_inj_nbhd_open {ι : Type*} [Fintype ι] [T2Space α] + {f : ι → G} {x : α} {i j : ι} (i_ne_j : i ≠ j) + (f_smul_inj : Function.Injective (fun i : ι => (f i) • x)) : + IsOpen (smul_inj_nbhd i_ne_j f_smul_inj) := +by + exact (disjoint_nbhd (smul_inj_moves i_ne_j f_smul_inj)).choose_spec.1 + +lemma smul_inj_nbhd_mem {ι : Type*} [Fintype ι] [T2Space α] + {f : ι → G} {x : α} {i j : ι} (i_ne_j : i ≠ j) + (f_smul_inj : Function.Injective (fun i : ι => (f i) • x)) : + x ∈ (smul_inj_nbhd i_ne_j f_smul_inj) := +by + exact (disjoint_nbhd (smul_inj_moves i_ne_j f_smul_inj)).choose_spec.2.1 + +lemma smul_inj_nbhd_disjoint {ι : Type*} [Fintype ι] [T2Space α] + {f : ι → G} {x : α} {i j : ι} (i_ne_j : i ≠ j) + (f_smul_inj : Function.Injective (fun i : ι => (f i) • x)) : + Disjoint + (smul_inj_nbhd i_ne_j f_smul_inj) + ((f j)⁻¹ * f i •'' (smul_inj_nbhd i_ne_j f_smul_inj)) := +by + exact (disjoint_nbhd (smul_inj_moves i_ne_j f_smul_inj)).choose_spec.2.2 + + +lemma disjoint_nbhd_fin {ι : Type*} [Fintype ι] [T2Space α] + {f : ι → G} {x : α} (f_smul_inj : Function.Injective (fun i : ι => (f i) • x)): + ∃ U : Set α, + IsOpen U ∧ x ∈ U ∧ (∀ (i j : ι), i ≠ j → Disjoint (f i •'' U) (f j •'' U)) := +by + let ι₂ := { p : ι × ι | p.1 ≠ p.2 } + let U := ⋂(p : ι₂), smul_inj_nbhd p.prop f_smul_inj + use U + + -- The notations provided afterwards tend to be quite ugly because we used `Exists.choose`, + -- but the idea is that this all boils down to applying `Exists.choose_spec`, except in the disjointness case, + -- where we transform `Disjoint (f i •'' U) (f j •'' U)` into `Disjoint U ((f i)⁻¹ * f j •'' U)` + -- and transform both instances of `U` into `N`, the neighborhood of the chosen `(i, j) ∈ ι₂` + repeat' constructor + · apply isOpen_iInter_of_finite + intro ⟨⟨i, j⟩, i_ne_j⟩ + apply smul_inj_nbhd_open + · apply Set.mem_iInter.mpr + intro ⟨⟨i, j⟩, i_ne_j⟩ + apply smul_inj_nbhd_mem + · intro i j i_ne_j + let N := smul_inj_nbhd i_ne_j f_smul_inj + have U_subset_N : U ⊆ N := Set.iInter_subset + (fun (⟨⟨i, j⟩, i_ne_j⟩ : ι₂) => (smul_inj_nbhd i_ne_j f_smul_inj)) + ⟨⟨i, j⟩, i_ne_j⟩ + + rw [disjoint_comm, smulImage_disjoint_mul] + + apply Set.disjoint_of_subset U_subset_N + · apply smulImage_subset + exact U_subset_N + · exact smul_inj_nbhd_disjoint i_ne_j f_smul_inj + + -- 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, diff --git a/Rubin/SmulImage.lean b/Rubin/SmulImage.lean index ef38992..2d09422 100644 --- a/Rubin/SmulImage.lean +++ b/Rubin/SmulImage.lean @@ -61,6 +61,7 @@ theorem mem_inv_smulImage {x : α} {g : G} {U : Set α} : x ∈ g⁻¹ •'' U exact msi #align mem_inv_smul'' Rubin.mem_inv_smulImage +-- TODO: rename to smulImage_mul @[simp] theorem mul_smulImage (g h : G) (U : Set α) : g •'' (h •'' U) = (g * h) •'' U := by @@ -135,4 +136,45 @@ theorem smulImage_eq_of_smul_eq {g h : G} {U : Set α} : simp only [smul_inv_smul, inv_smul_smul] at a ; exact Set.mem_of_eq_of_mem a.symm k #align smul''_eq_of_smul_eq Rubin.smulImage_eq_of_smul_eq + +theorem smulImage_subset_inv {G α : Type _} [Group G] [MulAction G α] + (f : G) (U V : Set α) : + f •'' U ⊆ V ↔ U ⊆ f⁻¹ •'' V := +by + constructor + · intro h + apply smulImage_subset f⁻¹ at h + rw [mul_smulImage] 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 [mul_right_inv, one_smulImage] at h + exact h + +theorem smulImage_subset_inv' {G α : Type _} [Group G] [MulAction G α] + (f : G) (U V : Set α) : + f⁻¹ •'' U ⊆ V ↔ U ⊆ f •'' V := +by + nth_rewrite 2 [<-inv_inv f] + exact smulImage_subset_inv f⁻¹ U V + +theorem smulImage_disjoint_mul {G α : Type _} [Group G] [MulAction G α] + (f g : G) (U : Set α) : + Disjoint (f •'' U) (g •'' U) ↔ Disjoint U ((f⁻¹ * g) •'' U) := by + constructor + · intro h + apply disjoint_smulImage f⁻¹ at h + repeat rw [mul_smulImage] 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 + rw [<-mul_assoc] at h + rw [mul_right_inv, one_mul] at h + exact h + end Rubin