diff --git a/Rubin.lean b/Rubin.lean index 16d7573..2d95869 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -1637,6 +1637,9 @@ instance RubinFilterSetoid (G : Type _) [Group G] : Setoid (RubinFilter G) where specialize h₂₃ U U_rigid exact Iff.trans h₁₂ h₂₃ +theorem RubinFilter.eqv_def (F₁ F₂ : RubinFilter G): + F₁ ≈ F₂ ↔ ∀ U ∈ AlgebraicCentralizerBasis G, AlgebraicConvergent F₁.filter U ↔ AlgebraicConvergent F₂.filter U := by rfl + lemma RubinFilter.lim_mem_iff_of_eqv {F₁ F₂ : RubinFilter G} (F_equiv : F₁ ≈ F₂) {S : Set α} (S_in_basis : S ∈ RegularSupportBasis G α) : F₁.lim α ∈ S ↔ F₂.lim α ∈ S @@ -1772,6 +1775,86 @@ by convert p_in_S exact (le_nhds_eq_lim α F p F_le_nhds).symm +lemma RubinFilter.rigidStabilizer_mem_of_lim_in_set (F : RubinFilter G) {S : Set α} (S_in_basis : S ∈ RegularSupportBasis G α) + (lim_in_set : F.lim α ∈ S) : + (G•[S] : Set G) ∈ F.filter := +by + have S_in_F : S ∈ F.map α := by + apply RubinFilter.le_nhds_lim + refine (IsOpen.mem_nhds_iff ?isOpen).mpr lim_in_set + exact (RegularSupportBasis.regular S_in_basis).isOpen + rwa [F.map_isRubinFilterOf S S_in_basis] at S_in_F + +theorem AlgebraicSubsets.conj (S T: Set G) (g : G) : + S ∈ AlgebraicSubsets T → (MulAut.conj g) '' S ∈ AlgebraicSubsets ((MulAut.conj g) '' T) := +by + unfold AlgebraicSubsets + simp + intro S_in_subsets S_ss_T + refine ⟨AlgebraicCentralizerBasis.conj_mem S_in_subsets g, ?S_ss_T⟩ + rwa [Set.preimage_image_eq _ conj_injective] + +theorem AlgebraicConvergent.conj {F : Filter G} {S : Set G} + (convergent : AlgebraicConvergent F S) + (g : G) : + AlgebraicConvergent (F.map (MulAut.conj g)) ((MulAut.conj g) '' S) := +by + unfold AlgebraicConvergent at * + let ⟨V, V_in_basis, V_ss_S, V_subsets_ss_orbit⟩ := convergent + refine ⟨ + (MulAut.conj g) '' V, + AlgebraicCentralizerBasis.conj_mem V_in_basis g, + Set.image_subset _ V_ss_S, + ?subsets_ss_orbit + ⟩ + unfold AlgebraicOrbit + + intro U U_in_subsets + have gU_in_subsets : ⇑(MulAut.conj g⁻¹) '' U ∈ AlgebraicSubsets V := by + convert AlgebraicSubsets.conj U ((MulAut.conj g) '' V) g⁻¹ U_in_subsets + rw [Set.image_image] + simp only [map_inv, MulAut.conj_apply, map_mul, MulAut.conj_inv_apply, mul_left_inv, one_mul] + group + rw [Set.image_id'] + + have ⟨h, h_in_S, W, ⟨W_in_F, W_in_basis⟩, W_eq⟩ := V_subsets_ss_orbit gU_in_subsets + + refine ⟨g * h * g⁻¹, (by simp; assumption), ?rest⟩ + + refine ⟨(MulAut.conj g) '' W, + ⟨ + Filter.image_mem_map W_in_F, + by simp [MulAut.conj]; apply AlgebraicCentralizerBasis.conj_mem W_in_basis⟩, + ?W_eq + ⟩ + rw [Set.image_image] + simp only [MulAut.conj_apply, conj_mul, mul_inv_rev, inv_inv] + group + simp only [zpow_neg, zpow_one] + + have conj₁ : (fun i => g * h * i * h⁻¹ * g⁻¹) = (MulAut.conj (g * h)).toEquiv := by + ext i + simp + group + + rw [conj₁, Set.image_equiv_eq_preimage_symm] + + rw [ + (by rfl : (MulAut.conj g⁻¹) '' U = (MulAut.conj g⁻¹).toEquiv '' U), + (by rfl : (fun i => h * i * h⁻¹) '' W = (MulAut.conj h).toEquiv '' W), + Equiv.eq_image_iff_symm_image_eq, + <-Set.preimage_equiv_eq_image_symm, + Set.image_equiv_eq_preimage_symm, + Set.preimage_preimage + ] at W_eq + + convert W_eq using 2 + ext i + rw [MulEquiv.toEquiv_eq_coe, MulEquiv.coe_toEquiv_symm, MulAut.conj_symm_apply] + simp + group + + def RubinFilterBasis (G : Type _) [Group G] : Set (Set (RubinFilter G)) := (fun S : Set G => { F : RubinFilter G | AlgebraicConvergent F.filter S }) '' AlgebraicCentralizerBasis G @@ -1978,7 +2061,7 @@ theorem RubinSpace.basis : TopologicalSpace.IsTopologicalBasis ( end Basis -section Equivariant +section Homeomorph variable {G : Type _} [Group G] variable (α : Type _) [TopologicalSpace α] [T2Space α] [HasNoIsolatedPoints α] [LocallyCompactSpace α] [Nonempty α] @@ -2060,7 +2143,216 @@ noncomputable def RubinSpace.homeomorph : Homeomorph (RubinSpace G) α where continuous_toFun := RubinSpace.lim_continuous α continuous_invFun := RubinSpace.fromPoint_continuous α -instance : MulAction G (RubinSpace G) := sorry +end Homeomorph + +section Equivariant + +variable {G : Type _} [Group G] +variable {α : Type _} [TopologicalSpace α] [T2Space α] [HasNoIsolatedPoints α] [LocallyCompactSpace α] [Nonempty α] +variable [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyDense G α] + +-- TODO: move elsewhere +@[simp] +theorem Group.range_conj_eq_univ {G : Type*} [Group G] (g : G) : + Set.range (fun i => g * i * g⁻¹) = Set.univ := +by + ext h + simp + use g⁻¹ * h * g + group + +@[simp] +theorem Group.range_conj'_eq_univ {G : Type*} [Group G] (g : G) : + Set.range (fun i => g⁻¹ * i * g) = Set.univ := +by + nth_rw 2 [<-inv_inv g] + exact Group.range_conj_eq_univ g⁻¹ + +def RubinFilter.smul (F : RubinFilter G) (g : G) : RubinFilter G where + filter := (F.filter.map_basis + (AlgebraicCentralizerBasis.empty_not_mem (G := G)) + ((MulAut.conj_order_iso g).orderIsoOn (AlgebraicCentralizerBasis G)) + (by + rw [OrderIso.orderIsoOn_image] + rw [AlgebraicCentralizerBasis.eq_conj_self g] + apply AlgebraicCentralizerBasis.empty_not_mem + ) + ).cast (AlgebraicCentralizerBasis.eq_conj_self g) + + converges := by + simp [MulAut.conj_order_iso] + rw [Filter.InBasis.map_basis_toOrderIsoSet _ F.filter.in_basis] + convert AlgebraicConvergent.conj F.converges g + simp + +theorem RubinFilter.smul_lim (F : RubinFilter G) (g : G) : + (F.smul g).lim α = g • F.lim α := +by + symm + apply le_nhds_eq_lim + + intro U gU_in_nhds + rw [<-smulFilter_nhds, mem_smulFilter_iff] at gU_in_nhds + rw [RubinFilter.map] + simp [smul] + + -- Please look away + let m₁ := (MulAut.conj_order_iso g).orderIsoOn (AlgebraicCentralizerBasis G) + let m₂: OrderIsoOn (Set G) (Set α) (m₁.toFun '' (AlgebraicCentralizerBasis G)) := + (RigidStabilizer.inv_order_iso_on G α).mk_of_subset (by + nth_rw 3 [<-AlgebraicCentralizerBasis.eq_conj_self g] + unfold_let + rfl + ) + have eq := Filter.InBasis.map_basis_comp (α := G) (β := G) (γ := α) m₁ m₂ F.filter.in_basis + simp at eq + rw [AlgebraicCentralizerBasis.eq_conj_self g] at eq + + rw [eq] + clear eq m₁ m₂ + + rw [Filter.InBasis.mem_map_basis _ _ F.filter.in_basis] + swap + { + intro S S_in_basis T T_in_basis S_ss_T + -- simp [MulAut.conj_order_iso] + apply RigidStabilizer_inv_doubleMonotone.monotoneOn + any_goals apply AlgebraicCentralizerBasis.conj_mem' + any_goals assumption + apply OrderIso.monotone + assumption + } + + simp [MulAut.conj_order_iso] + rw [(RegularSupportBasis.isBasis G α).mem_nhds_iff] at gU_in_nhds + let ⟨T, T_in_basis, lim_in_T, T_ss_gU⟩ := gU_in_nhds + refine ⟨G•[T], ?T_in_filter, ?T_in_basis, ?inv_T_ss_U⟩ + · exact rigidStabilizer_mem_of_lim_in_set F T_in_basis lim_in_T + · exact AlgebraicCentralizerBasis.mem_of_regularSupportBasis T_in_basis + · rw [Equiv.toOrderIsoSet_apply] + simp + rw [rigidStabilizer_conj_image_eq, RigidStabilizer_leftInv] + rwa [smulImage_subset_inv] + have dec_eq : DecidableEq G := Classical.typeDecidableEq _ + apply RegularSupportBasis.smulImage_in_basis + assumption + +theorem RubinFilter.smul_eqv_of_eqv (g : G) {F₁ F₂ : RubinFilter G} + (F_eqv : F₁ ≈ F₂) : (F₁.smul g ≈ F₂.smul g) := +by + rw [RubinFilter.eqv_def] + intro U U_in_basis + simp [smul, MulAut.conj_order_iso] + repeat rw [Filter.InBasis.map_basis_toOrderIsoSet] + any_goals exact F₁.filter.in_basis + any_goals exact F₂.filter.in_basis + + rw [RubinFilter.eqv_def] at F_eqv + specialize F_eqv ((MulAut.conj g⁻¹) '' U) ?gU_in_basis + { + exact AlgebraicCentralizerBasis.conj_mem' U_in_basis g⁻¹ + } + rw [map_inv] at F_eqv + + constructor + · intro F₁_conv + have F₁_conv' := AlgebraicConvergent.conj F₁_conv g⁻¹ + rw [Filter.map_map, <-MulAut.coe_mul, map_inv, mul_left_inv, MulAut.coe_one, Filter.map_id] at F₁_conv' + rw [F_eqv] at F₁_conv' + convert AlgebraicConvergent.conj F₁_conv' g using 1 + simp [Set.image_image] + group + simp + · intro F₂_conv + have F₂_conv' := AlgebraicConvergent.conj F₂_conv g⁻¹ + rw [Filter.map_map, <-MulAut.coe_mul, map_inv, mul_left_inv, MulAut.coe_one, Filter.map_id] at F₂_conv' + rw [<-F_eqv] at F₂_conv' + convert AlgebraicConvergent.conj F₂_conv' g using 1 + simp [Set.image_image] + group + simp + +theorem RubinFilter.smul_one (F : RubinFilter G) : RubinFilter.smul F 1 = F := +by + rw [smul, mk.injEq] + rw [UltrafilterInBasis.mk.injEq] + simp [MulAut.conj_order_iso] + rw [Filter.InBasis.map_basis_toOrderIsoSet _ F.filter.in_basis] + rw [MulAut.coe_one, Filter.map_id] + +theorem RubinFilter.mul_smul (g h : G) (F : RubinFilter G) : (F.smul g).smul h = F.smul (h * g) := by + unfold smul + rw [mk.injEq, UltrafilterInBasis.mk.injEq] + unfold MulAut.conj_order_iso + simp + + rw [Filter.InBasis.map_basis_toOrderIsoSet _ F.filter.in_basis] + rw [Filter.InBasis.map_basis_toOrderIsoSet] + swap + { + -- TODO: lemmatize + intro S S_in_mF + rw [Filter.mem_map] at S_in_mF + have ⟨T, T_in_F, T_in_basis, T_ss_gS⟩ := F.filter.in_basis _ S_in_mF + use (MulAut.conj g⁻¹) ⁻¹' T + constructor + · rw [Filter.mem_map, Set.preimage_preimage] + simp + group + simp + exact T_in_F + constructor + · show (MulAut.conj g⁻¹).toEquiv ⁻¹' T ∈ AlgebraicCentralizerBasis G + rw [Set.preimage_equiv_eq_image_symm] + show (MulEquiv.symm (MulAut.conj g⁻¹)) '' T ∈ AlgebraicCentralizerBasis G + rw [<-MulAut.inv_def, map_inv, inv_inv] + exact AlgebraicCentralizerBasis.conj_mem T_in_basis g + · show (MulAut.conj g⁻¹).toEquiv ⁻¹' T ⊆ S + rw [Set.preimage_equiv_eq_image_symm, Equiv.subset_image] + have T_ss_gS : T ⊆ (MulAut.conj g).toEquiv ⁻¹' S := T_ss_gS + rw [Set.preimage_equiv_eq_image_symm] at T_ss_gS + rw [map_inv, MulAut.inv_def] + exact T_ss_gS + } + rw [Filter.map_map, <-MulAut.coe_mul] + rw [Filter.InBasis.map_basis_toOrderIsoSet _ F.filter.in_basis] + +def RubinSpace.smul (Q : RubinSpace G) (g : G) : RubinSpace G := + Quotient.map (fun F => F.smul g) (fun _ _ F_eqv => RubinFilter.smul_eqv_of_eqv g F_eqv) Q + +theorem RubinSpace.smul_mk (F : RubinFilter G) (g : G) : + RubinSpace.smul (⟦F⟧ : RubinSpace G) g = ⟦F.smul g⟧ := by simp [RubinSpace.smul] + +instance : MulAction G (RubinSpace G) where + smul := fun g Q => Q.smul g + + one_smul := by + intro Q + let ⟨F, F_eq⟩ := Q.exists_rep + rw [<-F_eq] + show RubinSpace.smul ⟦F⟧ 1 = ⟦F⟧ + rw [RubinSpace.smul_mk] + rw [RubinFilter.smul_one] + + mul_smul := by + intro g h Q + let ⟨F, F_eq⟩ := Q.exists_rep + rw [<-F_eq] + show RubinSpace.smul ⟦F⟧ (g * h) = RubinSpace.smul (RubinSpace.smul ⟦F⟧ h) g + repeat rw [RubinSpace.smul_mk] + rw [RubinFilter.mul_smul] + +theorem RubinSpace.smul_def (g : G) (Q : RubinSpace G) : g • Q = Q.smul g := rfl + +noncomputable def rubin' : EquivariantHomeomorph G (RubinSpace G) α where + toHomeomorph := RubinSpace.homeomorph (G := G) α + equivariant := by + intro g Q + simp [RubinSpace.homeomorph] + rw [RubinSpace.smul_def] + let ⟨F, F_eq⟩ := Q.exists_rep + rw [<-F_eq, RubinSpace.smul_mk, RubinSpace.lim_mk, RubinSpace.lim_mk] + rw [RubinFilter.smul_lim] end Equivariant @@ -2070,7 +2362,6 @@ end Equivariant - /- variable {β : Type _} variable [TopologicalSpace β] [MulAction G β] [ContinuousConstSMul G β] diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean index 91099af..8dd51e9 100644 --- a/Rubin/AlgebraicDisjointness.lean +++ b/Rubin/AlgebraicDisjointness.lean @@ -596,6 +596,37 @@ by rw [S'_eq, T'_eq] rfl + +def MulAut.conj_order_iso (g : G) : Set G ≃o Set G := (MulAut.conj g).toEquiv.toOrderIsoSet + +theorem AlgebraicCentralizerBasis.eq_conj_self (g : G) : + (MulAut.conj_order_iso g) '' AlgebraicCentralizerBasis G = AlgebraicCentralizerBasis G := +by + ext S + simp [MulAut.conj_order_iso] + conv => { + lhs + congr; intro x + rw [Equiv.toOrderIsoSet_apply] + } + simp + constructor + · intro ⟨T, T_in_basis, T_eq⟩ + rw [<-T_eq] + exact conj_mem T_in_basis g + · intro S_in_basis + use (fun h => g⁻¹ * h * g⁻¹⁻¹) '' S + refine ⟨conj_mem S_in_basis g⁻¹, ?S_eq⟩ + rw [Set.image_image] + group + rw [Set.image_id'] + +theorem AlgebraicCentralizerBasis.conj_mem' {S : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G) (g : G) : + (MulAut.conj_order_iso g) S ∈ AlgebraicCentralizerBasis G := +by + show (fun i => g * i * g⁻¹) '' S ∈ AlgebraicCentralizerBasis G + exact conj_mem S_in_basis g + end AlgebraicCentralizer end Rubin diff --git a/Rubin/Filter.lean b/Rubin/Filter.lean index 8022226..200765d 100644 --- a/Rubin/Filter.lean +++ b/Rubin/Filter.lean @@ -1,4 +1,6 @@ import Mathlib.Order.Filter.Basic +import Mathlib.Order.Hom.CompleteLattice + import Mathlib.Topology.Basic import Mathlib.Topology.Bases import Mathlib.Topology.Separation @@ -244,8 +246,19 @@ def OrderIso.orderIsoOn (F : α ≃o β) (S : Set α) : OrderIsoOn α β S where intro a _ b _ exact Iff.symm (RelIso.map_rel_iff F) -instance : Coe (α ≃o β) (OrderIsoOn α β S) where - coe := fun f => OrderIso.orderIsoOn f S +-- instance : Coe (α ≃o β) (OrderIsoOn α β S) where +-- coe := fun f => OrderIso.orderIsoOn f S + +@[simp] +theorem OrderIso.orderIsoOn_toFun (F : α ≃o β) (S : Set α) : + (OrderIso.orderIsoOn F S).toFun = F.toFun := rfl + +@[simp] +theorem OrderIso.orderIsoOn_invFun (F : α ≃o β) (S : Set α) : + (OrderIso.orderIsoOn F S).invFun = F.invFun := rfl + +theorem OrderIso.orderIsoOn_image (F : α ≃o β) (S T : Set α) : + (OrderIso.orderIsoOn F S).toFun '' T = F '' T := rfl def OrderIsoOn.identity (α : Type _) [Preorder α] (S : Set α) : OrderIsoOn α α S where toFun := id @@ -723,6 +736,32 @@ by rw [Filter.InBasis.map_basis_le_inv _ G_basis F_basis] simp +@[simp] +theorem Filter.InBasis.map_basis_toOrderIsoSet {M : Type*} (map : M) [EquivLike M α β] + {F : Filter α} (F_basis : F.InBasis B) : + Filter.InBasis.map_basis F B (EquivLike.toEquiv map).toOrderIsoSet = + F.map map := +by + simp + ext S + rw [mem_map_basis _ _ F_basis, Filter.mem_map, F_basis.basis_hasBasis.mem_iff, basis] + swap + { + apply Monotone.monotoneOn + exact OrderHomClass.mono _ + } + simp + rw [(by rfl : map ⁻¹' S = (EquivLike.toEquiv map) ⁻¹' S)] + rw [Set.preimage_equiv_eq_image_symm] + conv => { + lhs; congr; intro y + rw [Equiv.toOrderIsoSet_apply] + } + conv => { + rhs; congr; intro y + rw [<-Equiv.subset_image, and_assoc] + } + instance Filter.InBasis.order_bot : OrderBot { F : Filter α // F.InBasis B ∨ F = ⊥ } where bot := ⟨⊥, by right; rfl ⟩ bot_le := by