From 6b2f21fec8411f47177ea7b02d7dd0d8e792d853 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Fri, 29 Dec 2023 23:28:20 +0100 Subject: [PATCH] :sparkles: Fix all sorries --- Rubin.lean | 160 ++++++++++++++++++++++--------- Rubin/AlgebraicDisjointness.lean | 153 ++++++++++++++++++++++++++++- 2 files changed, 263 insertions(+), 50 deletions(-) diff --git a/Rubin.lean b/Rubin.lean index b1efb1a..39bf500 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -736,22 +736,18 @@ by · simp theorem AlgebraicCentralizerBasis.exists_rigidStabilizer_inv (H : Set G) [Nonempty α]: - ∃ S ∈ RegularSupportBasis G α, H ∈ AlgebraicCentralizerBasis G → H = G•[S] := + ∃ S, + (H ∈ AlgebraicCentralizerBasis G → S ∈ RegularSupportBasis G α ∧ H = G•[S]) + ∧ (H ∉ AlgebraicCentralizerBasis G → S = ∅) := by by_cases H_in_basis?: H ∈ AlgebraicCentralizerBasis G swap { - use Set.univ + use ∅ constructor - rw [RegularSupportBasis.mem_iff] - constructor - · exact Set.univ_nonempty - · use ∅ - unfold RegularSupport.FiniteInter - simp - · intro H_in_basis - exfalso - exact H_in_basis? H_in_basis + tauto + intro _ + rfl } have ⟨H_ne_one, ⟨seed, H_eq⟩⟩ := (AlgebraicCentralizerBasis.mem_iff H).mp H_in_basis? @@ -760,15 +756,15 @@ by use RegularSupport.FiniteInter α seed constructor - · rw [RegularSupportBasis.mem_iff] - constructor + · intro _ + rw [RegularSupportBasis.mem_iff] + repeat' apply And.intro · rw [<-regularSupportInter_nonEmpty_iff_neBot] exact H_ne_one · use seed - · intro _ - - rw [rigidStabilizer_inter_eq_algebraicCentralizerInter] - exact H_eq + · rw [rigidStabilizer_inter_eq_algebraicCentralizerInter] + exact H_eq + · tauto theorem AlgebraicCentralizerBasis.mem_of_regularSupportBasis {S : Set α} (S_in_basis : S ∈ RegularSupportBasis G α) : @@ -806,8 +802,9 @@ by apply mem_of_regularSupportBasis S_in_basis · intro H_in_basis simp - let ⟨S, S_in_rsupp, H_eq⟩ := AlgebraicCentralizerBasis.exists_rigidStabilizer_inv (α := α) H - specialize H_eq H_in_basis + + let ⟨S, ⟨S_props, _⟩⟩ := AlgebraicCentralizerBasis.exists_rigidStabilizer_inv (α := α) H + let ⟨S_in_basis, H_eq⟩ := S_props H_in_basis symm at H_eq use S @@ -818,13 +815,20 @@ theorem rigidStabilizer_inv_eq [Nonempty α] {H : Set G} (H_in_basis : H ∈ Alg H = G•[rigidStabilizer_inv (α := α) H] := by have spec := (AlgebraicCentralizerBasis.exists_rigidStabilizer_inv (α := α) H).choose_spec - exact spec.right H_in_basis + exact (spec.left H_in_basis).right -theorem rigidStabilizer_in_basis [Nonempty α] (H : Set G) : - rigidStabilizer_inv (α := α) H ∈ RegularSupportBasis G α := +theorem rigidStabilizer_inv_in_basis [Nonempty α] (H : Set G) : + H ∈ AlgebraicCentralizerBasis G ↔ rigidStabilizer_inv (α := α) H ∈ RegularSupportBasis G α := by have spec := (AlgebraicCentralizerBasis.exists_rigidStabilizer_inv (α := α) H).choose_spec - exact spec.left + constructor + · intro H_in_basis + exact (spec.left H_in_basis).left + · intro iH_in_basis + by_contra H_notin_basis + unfold rigidStabilizer_inv at iH_in_basis + rw [(spec.right H_notin_basis)] at iH_in_basis + exact RegularSupportBasis.empty_not_mem G α iH_in_basis theorem rigidStabilizer_inv_eq' [Nonempty α] {S : Set α} (S_in_basis : S ∈ RegularSupportBasis G α) : rigidStabilizer_inv (α := α) (G := G) G•[S] = S := @@ -836,7 +840,7 @@ by rw [SetLike.coe_set_eq, rigidStabilizer_eq_iff] at eq · exact eq.symm · exact RegularSupportBasis.regular S_in_basis - · exact RegularSupportBasis.regular (rigidStabilizer_in_basis _) + · exact RegularSupportBasis.regular ((rigidStabilizer_inv_in_basis _).mp GS_in_basis) variable [Nonempty α] [HasNoIsolatedPoints α] [LocallyDense G α] @@ -929,16 +933,57 @@ by simp at res exact res U_in_basis -theorem AlgebraicCentralizerBasis.mem_of_regularSupportBasis_inv {S : Set G} - (S_in_basis : rigidStabilizer_inv (α := α) S ∈ RegularSupportBasis G α) : - S ∈ AlgebraicCentralizerBasis G := + +theorem rigidStabilizer_subset_iff_subset_inv [Nonempty α] {S : Set α} (S_in_basis : S ∈ RegularSupportBasis G α) {T : Set G} (T_in_basis : T ∈ AlgebraicCentralizerBasis G): + (G•[S] : Set G) ⊆ T ↔ S ⊆ rigidStabilizer_inv T := by - let ⟨T, T_in_basis, T_eq⟩ := (RegularSupportBasis.eq_inv_rist_image (G := G) (α := α)).symm ▸ S_in_basis - simp only at T_eq + nth_rw 1 [<-RigidStabilizer_rightInv (α := α) T_in_basis] + rw [SetLike.coe_subset_coe] + rw [rigidStabilizer_subset_iff (G := G)] + · exact RegularSupportBasis.regular S_in_basis + · apply RegularSupportBasis.regular (G := G) + rw [<-rigidStabilizer_inv_in_basis T] + assumption - -- Note: currently not provable, we need to add another requirement to rigidStabilizer_inv +theorem subset_rigidStabilizer_iff_inv_subset [Nonempty α] {S : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G) {T : Set α} (T_in_basis : T ∈ RegularSupportBasis G α): + S ⊆ (G•[T] : Set G) ↔ rigidStabilizer_inv S ⊆ T := +by + nth_rw 1 [<-RigidStabilizer_rightInv (α := α) S_in_basis] + rw [SetLike.coe_subset_coe] + rw [rigidStabilizer_subset_iff (G := G)] + · apply RegularSupportBasis.regular (G := G) + rw [<-rigidStabilizer_inv_in_basis S] + assumption + · exact RegularSupportBasis.regular T_in_basis - sorry +theorem rigidStabilizer_inv_smulImage [Nonempty α] {S : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G) (h : G) : + h •'' rigidStabilizer_inv S = rigidStabilizer_inv (α := α) ((fun g => h * g * h⁻¹) '' S) := +by + rw [smulImage_inv] + rw [<-rigidStabilizer_eq_iff (G := G)] + swap + { + apply RegularSupportBasis.regular (G := G) + rw [<-rigidStabilizer_inv_in_basis S] + exact S_in_basis + } + swap + { + rw [<-smulImage_regular] + apply RegularSupportBasis.regular (G := G) + rw [<-rigidStabilizer_inv_in_basis] + apply AlgebraicCentralizerBasis.conj_mem + assumption + } + rw [<-SetLike.coe_set_eq] + rw [<-rigidStabilizer_conj_image_eq] + repeat rw [RigidStabilizer_rightInv] + · rw [Set.image_image] + group + simp + · apply AlgebraicCentralizerBasis.conj_mem + assumption + · assumption end RegularSupport @@ -1919,9 +1964,10 @@ by simp rw [<-filter_of.mem_inv U_in_basis] exact U_in_filter - exact rigidStabilizer_in_basis U - · intro ⟨iU_in_filter, iU_in_basis⟩ - have U_in_basis := AlgebraicCentralizerBasis.mem_of_regularSupportBasis_inv iU_in_basis + rw [<-rigidStabilizer_inv_in_basis] + assumption + · intro ⟨iU_in_filter, U_in_basis⟩ + rw [<-rigidStabilizer_inv_in_basis] at U_in_basis constructor · simp rw [filter_of.mem_inv U_in_basis] @@ -1931,22 +1977,21 @@ by theorem IsRubinFilterOf.subsets_ss_orbit {A : UltrafilterInBasis (RegularSupportBasis G α)} {B : UltrafilterInBasis (AlgebraicCentralizerBasis G)} (filter_of : IsRubinFilterOf A B) - {V : Set α} (V_in_basis : V ∈ RegularSupportBasis G α) + {V : Set α} -- (V_in_basis : V ∈ RegularSupportBasis G α) {W : Set α} (W_in_basis : W ∈ RegularSupportBasis G α) : RSuppSubsets G W ⊆ RSuppOrbit A G•[V] ↔ AlgebraicSubsets (G•[W]) ⊆ AlgebraicOrbit B.filter G•[V] := by + have dec_eq : DecidableEq G := Classical.typeDecidableEq _ + constructor · intro rsupp_ss unfold AlgebraicSubsets AlgebraicOrbit intro U ⟨U_in_basis, U_ss_GW⟩ let U' := rigidStabilizer_inv (α := α) U - have U'_in_basis : U' ∈ RegularSupportBasis G α := rigidStabilizer_in_basis U + have U'_in_basis : U' ∈ RegularSupportBasis G α := (rigidStabilizer_inv_in_basis U).mp U_in_basis have U'_ss_W : U' ⊆ W := by - rw [rigidStabilizer_subset_iff (G := G) (RegularSupportBasis.regular U'_in_basis) (RegularSupportBasis.regular W_in_basis)] - unfold_let - rw [<-SetLike.coe_subset_coe] - rw [RigidStabilizer_rightInv (G := G) (α := α) U_in_basis] - assumption + rw [subset_rigidStabilizer_iff_inv_subset U_in_basis W_in_basis] at U_ss_GW + exact U_ss_GW let ⟨g, g_in_GV, ⟨W, W_in_A, gW_eq_U⟩⟩ := rsupp_ss ⟨U'_in_basis, U'_ss_W⟩ use g constructor @@ -1955,8 +2000,6 @@ by exact g_in_GV } - have dec_eq : DecidableEq G := Classical.typeDecidableEq _ - have W_in_basis : W ∈ RegularSupportBasis G α := by rw [smulImage_inv] at gW_eq_U rw [gW_eq_U] @@ -1970,7 +2013,33 @@ by rw [rigidStabilizer_conj_image_eq, gW_eq_U] unfold_let exact RigidStabilizer_rightInv U_in_basis - sorry + · intro algsupp_ss + unfold RSuppSubsets RSuppOrbit + simp + intro U U_in_basis U_ss_W + let U' := (G•[U] : Set G) + have U'_in_basis : U' ∈ AlgebraicCentralizerBasis G := + AlgebraicCentralizerBasis.mem_of_regularSupportBasis U_in_basis + have U'_ss_GW : U' ⊆ G•[W] := by + rw [SetLike.coe_subset_coe] + rw [<-rigidStabilizer_subset_iff] + · assumption + · exact RegularSupportBasis.regular U_in_basis + · exact RegularSupportBasis.regular W_in_basis + + let ⟨g, g_in_GV, ⟨X, X_in_inter, X_eq⟩⟩ := algsupp_ss ⟨U'_in_basis, U'_ss_GW⟩ + have X_in_basis := X_in_inter.right + rw [filter_of.mem_inter_inv] at X_in_inter + + simp at g_in_GV + use g + refine ⟨g_in_GV, ⟨rigidStabilizer_inv X, X_in_inter.left, ?giX_eq_U⟩⟩ + + apply (And.right) at X_in_inter + rw [rigidStabilizer_inv_smulImage X_in_basis, X_eq] + unfold_let + rw [RigidStabilizer_leftInv U_in_basis] + def RubinFilter.from (F : UltrafilterInBasis (RegularSupportBasis G α)) (F_converges : ∃ p : α, F ≤ nhds p) : RubinFilter G where filter := (F.map_basis @@ -1999,7 +2068,8 @@ def RubinFilter.from (F : UltrafilterInBasis (RegularSupportBasis G α)) (F_conv } rw [<-Subgroup.coe_top, <-rigidStabilizer_univ (α := α) (G := G)] - rw [<-(RubinFilter.from_isRubinFilterOf' F).subsets_ss_orbit (RegularSupportBasis.univ_mem G α) W_in_basis] + -- (RegularSupportBasis.univ_mem G α) + rw [<-(RubinFilter.from_isRubinFilterOf' F).subsets_ss_orbit W_in_basis] assumption diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean index 58f8afb..875d531 100644 --- a/Rubin/AlgebraicDisjointness.lean +++ b/Rubin/AlgebraicDisjointness.lean @@ -17,7 +17,38 @@ import Rubin.LocallyDense namespace Rubin -structure AlgebraicallyDisjointElem {G : Type _} [Group G] (f g h : G) := +variable {G : Type _} [Group G] + +theorem Commute.conj (f g h : G) : Commute (f * g * f⁻¹) h ↔ Commute g (f⁻¹ * h * f) := by + suffices ∀ (f g h : G), Commute (f * g * f⁻¹) h → Commute g (f⁻¹ * h * f) by + constructor + · apply this + · intro cg + symm + nth_rw 1 [<-inv_inv f] + apply this + symm + rw [inv_inv] + exact cg + + intro f g h fgf_h_comm + unfold Commute SemiconjBy at * + rw [<-mul_assoc, <-mul_assoc] + rw [<-mul_assoc, <-mul_assoc] at fgf_h_comm + have gfh_eq : g * f⁻¹ * h = f⁻¹ * h * f * g * f⁻¹ := by + repeat rw [mul_assoc f⁻¹] + rw [<-fgf_h_comm] + group + rw [gfh_eq] + group + +theorem Commute.conj' (f g h : G) : Commute (f⁻¹ * g * f) h ↔ Commute g (f * h * f⁻¹) := by + nth_rw 2 [<-inv_inv f] + nth_rw 3 [<-inv_inv f] + apply Commute.conj + + +structure AlgebraicallyDisjointElem (f g h : G) := non_commute: ¬Commute f h fst : G snd : G @@ -28,16 +59,47 @@ structure AlgebraicallyDisjointElem {G : Type _} [Group G] (f g h : G) := namespace AlgebraicallyDisjointElem -def comm_elem {G : Type _} [Group G] {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) : G := +def comm_elem {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) : G := ⁅disj_elem.fst, ⁅disj_elem.snd, h⁆⁆ @[simp] -theorem comm_elem_eq {G : Type _} [Group G] {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) : +theorem comm_elem_eq {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) : disj_elem.comm_elem = ⁅disj_elem.fst, ⁅disj_elem.snd, h⁆⁆ := by unfold comm_elem simp +lemma comm_elem_conj (f g h i : G) : + ⁅i * f * i⁻¹, ⁅i * g * i⁻¹, i * h * i⁻¹⁆⁆ = i * ⁅f, ⁅g, h⁆⁆ * i⁻¹ := by group + +theorem conj {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) (i : G): AlgebraicallyDisjointElem (i * f * i⁻¹) (i * g * i⁻¹) (i * h * i⁻¹) where + non_commute := by + rw [Commute.conj] + group + exact disj_elem.non_commute + fst := i * disj_elem.fst * i⁻¹ + snd := i * disj_elem.snd * i⁻¹ + fst_commute := by + rw [Commute.conj] + group + exact disj_elem.fst_commute + snd_commute := by + rw [Commute.conj] + group + exact disj_elem.snd_commute + comm_elem_nontrivial := by + intro eq_one + apply disj_elem.comm_elem_nontrivial + rw [comm_elem_conj, <-mul_right_inv i] at eq_one + apply mul_right_cancel at eq_one + nth_rw 2 [<-mul_one i] at eq_one + apply mul_left_cancel at eq_one + exact eq_one + comm_elem_commute := by + rw [comm_elem_conj, Commute.conj] + rw [(by group : i⁻¹ * (i * g * i⁻¹) * i = g)] + exact disj_elem.comm_elem_commute + end AlgebraicallyDisjointElem -- Also known as `η_G(f)`. @@ -117,6 +179,16 @@ noncomputable instance coeFnAlgebraicallyDisjoint : CoeFun instance coeAlgebraicallyDisjoint : Coe (AlgebraicallyDisjoint f g) (IsAlgebraicallyDisjoint f g) where coe := mk +theorem conj (is_alg_disj : IsAlgebraicallyDisjoint f g) (h : G) : + IsAlgebraicallyDisjoint (h * f * h⁻¹) (h * g * h⁻¹) := +by + apply elim at is_alg_disj + apply mk + intro i nc + rw [Commute.conj] at nc + rw [(by group : i = h * (h⁻¹ * i * h) * h⁻¹)] + exact (is_alg_disj (h⁻¹ * i * h) nc).conj h + end IsAlgebraicallyDisjoint -- TODO: find a better home for these lemmas @@ -357,8 +429,24 @@ by simp simp only [gxg12_eq] ext x - sorry - -- unfold IsAlgebraicallyDisjoint + simp + constructor + · intro ⟨y, y_disj, x_eq⟩ + use g * y * g⁻¹ + rw [<-gxg12_eq] + refine ⟨?disj, x_eq⟩ + exact y_disj.conj g + · intro ⟨y, y_disj, x_eq⟩ + use g⁻¹ * y * g + constructor + · rw [(by group : f = g⁻¹ * (g * f * g⁻¹) * g⁻¹⁻¹)] + nth_rw 6 [<-inv_inv g] + exact y_disj.conj g⁻¹ + · nth_rw 3 [<-inv_inv g] + simp only [conj_pow] + group + group at x_eq + exact x_eq @[simp] @@ -424,6 +512,61 @@ theorem AlgebraicCentralizerBasis.empty_not_mem : ∅ ∉ AlgebraicCentralizerBa rw [<-Set.nonempty_iff_ne_empty] exact Subgroup.coe_nonempty _ +theorem AlgebraicCentralizerBasis.to_subgroup {S : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G): + ∃ S' : Subgroup G, S = S' := +by + rw [mem_iff] at S_in_basis + let ⟨_, ⟨seed, S_eq⟩⟩ := S_in_basis + use AlgebraicCentralizerInter seed + +theorem Set.image_equiv_eq {α β : Type _} (S : Set α) (T : Set β) (f : α ≃ β) : + f '' S = T ↔ S = f.symm '' T := +by + constructor + · intro fS_eq_T + ext x + rw [<-fS_eq_T] + simp + · intro S_eq_fT + ext x + rw [S_eq_fT] + simp + +theorem AlgebraicCentralizerBasis.conj_mem {S : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G) + (h : G) : (fun g => h * g * h⁻¹) '' S ∈ AlgebraicCentralizerBasis G := +by + let ⟨S', S_eq⟩ := to_subgroup S_in_basis + rw [S_eq] + rw [S_eq, subgroup_mem_iff] at S_in_basis + rw [mem_iff] + + have conj_eq : (fun g => h * g * h⁻¹) = (MulAut.conj h).toEquiv := by + ext x + simp + + constructor + · rw [conj_eq] + rw [ne_eq, Set.image_equiv_eq] + simp + rw [<-Subgroup.coe_bot, SetLike.coe_set_eq] + exact S_in_basis.left + · let ⟨seed, S'_eq⟩ := S_in_basis.right + have dec_eq : DecidableEq G := Classical.typeDecidableEq _ + use Finset.image (fun g => h * g * h⁻¹) seed + rw [S'_eq] + unfold AlgebraicCentralizerInter + ext g + rw [conj_eq] + rw [Set.mem_image_equiv] + simp + conv => { + rhs + intro + intro + rw [<-SetLike.mem_coe, <-AlgebraicCentralizer.conj, conj_eq, Set.mem_image_equiv] + } + + end AlgebraicCentralizer end Rubin