From 55d674e96a4ceebddc16559b86799c561f441c63 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Sat, 9 Dec 2023 00:51:54 +0100 Subject: [PATCH] :sparkles: Implement RigidStabilizerBasis and AlgebraicCentralizerBasis --- Rubin.lean | 110 +++++++++---- Rubin/AlgebraicDisjointness.lean | 63 ++++++++ Rubin/HomeoGroup.lean | 24 +++ Rubin/RigidStabilizer.lean | 9 ++ Rubin/RigidStabilizerBasis.lean | 269 +++++++++++++++++++++++++++++++ 5 files changed, 443 insertions(+), 32 deletions(-) create mode 100644 Rubin/RigidStabilizerBasis.lean diff --git a/Rubin.lean b/Rubin.lean index d49d1e7..37b6d98 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -23,6 +23,7 @@ import Rubin.SmulImage import Rubin.Support import Rubin.Topology import Rubin.RigidStabilizer +import Rubin.RigidStabilizerBasis import Rubin.Period import Rubin.AlgebraicDisjointness import Rubin.RegularSupport @@ -487,13 +488,6 @@ by rw [<-period_hg_eq_n] apply Period.pow_period_fix --- This is referred to as `ξ_G^12(f)` --- TODO: put in a different file and introduce some QoL theorems -def AlgebraicSubgroup {G : Type _} [Group G] (f : G) : Set G := - (fun g : G => g^12) '' { g : G | IsAlgebraicallyDisjoint f g } - -def AlgebraicCentralizer {G: Type _} [Group G] (f : G) : Subgroup G := - Subgroup.centralizer (AlgebraicSubgroup f) -- Given the statement `¬Support α h ⊆ RegularSupport α f`, -- we construct an open subset within `Support α h \ RegularSupport α f`, @@ -679,6 +673,10 @@ by exact h_in_rist } +variable {G α : Type _} +variable [Group G] +variable [TopologicalSpace α] [T2Space α] +variable [MulAction G α] [ContinuousMulAction G α] [FaithfulSMul G α] [LocallyMoving G α] /-- This demonstrates that the disjointness of the supports of two elements `f` and `g` @@ -689,8 +687,7 @@ We could prove that the intersection of the algebraic centralizers of `f` and `g purely within group theory, and then apply this theorem to know that their support in `α` will be disjoint. --/ -lemma remark_2_3 {G α : Type _} [Group G] [TopologicalSpace α] [T2Space α] [MulAction G α] - [ContinuousMulAction G α] [FaithfulSMul G α] [LocallyMoving G α] {f g : G} : +lemma remark_2_3 {f g : G} : (AlgebraicCentralizer f) ⊓ (AlgebraicCentralizer g) = ⊥ → Disjoint (Support α f) (Support α g) := by intro alg_disj @@ -702,37 +699,86 @@ by repeat rw [<-proposition_2_1] exact alg_disj +lemma rigidStabilizerInter_eq_algebraicCentralizerInter {S : Finset G} : + RigidStabilizerInter₀ α S = AlgebraicCentralizerInter₀ S := +by + unfold RigidStabilizerInter₀ + unfold AlgebraicCentralizerInter₀ + conv => { + lhs + congr; intro; congr; intro + rw [<-proposition_2_1] + } + +theorem rigidStabilizerBasis_eq_algebraicCentralizerBasis : + AlgebraicCentralizerBasis G = RigidStabilizerBasis G α := +by + apply le_antisymm <;> intro B B_mem + any_goals rw [RigidStabilizerBasis.mem_iff] + any_goals rw [AlgebraicCentralizerBasis.mem_iff] + any_goals rw [RigidStabilizerBasis.mem_iff] at B_mem + any_goals rw [AlgebraicCentralizerBasis.mem_iff] at B_mem + + all_goals let ⟨⟨seed, B_ne_bot⟩, B_eq⟩ := B_mem + + any_goals rw [RigidStabilizerBasis₀.val_def] at B_eq + any_goals rw [AlgebraicCentralizerBasis₀.val_def] at B_eq + all_goals simp at B_eq + all_goals rw [<-B_eq] + + rw [<-rigidStabilizerInter_eq_algebraicCentralizerInter (α := α)] at B_ne_bot + swap + rw [rigidStabilizerInter_eq_algebraicCentralizerInter (α := α)] at B_ne_bot + + all_goals use ⟨seed, B_ne_bot⟩ + + symm + all_goals apply rigidStabilizerInter_eq_algebraicCentralizerInter + end RegularSupport section HomeoGroup open Topology +variable {G α : Type _} [Group G] [TopologicalSpace α] [T2Space α] +variable [MulAction G α] [ContinuousMulAction G α] [FaithfulSMul G α] [LocallyMoving G α] + +#check RegularSupportBasis.asSet +#check RigidStabilizerBasis + +-- TODO: implement Smul of G on RigidStabilizerBasis? + +-- theorem regularSupportBasis_eq_ridigStabilizerBasis : +-- RegularSupportBasis.asSet α = RigidStabilizerBasis (HomeoGroup α) α := +-- by +-- sorry + -- TODO: implement Membership on RegularSupportBasis -- TODO: wrap these things in some neat structures -theorem proposition_3_5 {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] - [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α] - [hc : ContinuousMulAction G α] - (U : RegularSupportBasis α) (F: Filter α): - (∃ p ∈ U.val, F.HasBasis (fun S: Set α => S ∈ RegularSupportBasis.asSet α ∧ p ∈ S) id) - ↔ ∃ V : RegularSupportBasis α, V ≤ U ∧ {W : RegularSupportBasis α | W ≤ V} ⊆ { g •'' W | (g ∈ RigidStabilizer G U.val) (W ∈ F) (_: W ∈ RegularSupportBasis.asSet α) } - := -by - constructor - { - simp - intro p p_in_U filter_basis - have assoc_poset_basis := RegularSupportBasis.isBasis G α - have F_eq_nhds : F = 𝓝 p := by - have nhds_basis := assoc_poset_basis.nhds_hasBasis (a := p) - rw [<-filter_basis.filter_eq] - rw [<-nhds_basis.filter_eq] - have p_in_int_cl := h_ld.isLocallyDense U U.regular.isOpen p p_in_U - -- TODO: show that ∃ V ⊆ closure (orbit (rist G U) p) - - sorry - } - sorry +-- theorem proposition_3_5 {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] +-- [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α] +-- [hc : ContinuousMulAction G α] +-- (U : RegularSupportBasis α) (F: Filter α): +-- (∃ p ∈ U.val, F.HasBasis (fun S: Set α => S ∈ RegularSupportBasis.asSet α ∧ p ∈ S) id) +-- ↔ ∃ V : RegularSupportBasis α, V ≤ U ∧ {W : RegularSupportBasis α | W ≤ V} ⊆ { g •'' W | (g ∈ RigidStabilizer G U.val) (W ∈ F) (_: W ∈ RegularSupportBasis.asSet α) } +-- := +-- by +-- constructor +-- { +-- simp +-- intro p p_in_U filter_basis +-- have assoc_poset_basis := RegularSupportBasis.isBasis G α +-- have F_eq_nhds : F = 𝓝 p := by +-- have nhds_basis := assoc_poset_basis.nhds_hasBasis (a := p) +-- rw [<-filter_basis.filter_eq] +-- rw [<-nhds_basis.filter_eq] +-- have p_in_int_cl := h_ld.isLocallyDense U U.regular.isOpen p p_in_U +-- -- TODO: show that ∃ V ⊆ closure (orbit (rist G U) p) + +-- sorry +-- } +-- sorry end HomeoGroup diff --git a/Rubin/AlgebraicDisjointness.lean b/Rubin/AlgebraicDisjointness.lean index b5450ef..d99a500 100644 --- a/Rubin/AlgebraicDisjointness.lean +++ b/Rubin/AlgebraicDisjointness.lean @@ -328,4 +328,67 @@ by exact k_lt_n #align moves_inj_period Rubin.smul_injective_within_period + +/- +The algebraic centralizer (and its associated basis) allow for a purely group-theoretic construction of the +`RegularSupport` sets. +They are defined as the centralizers of the subgroups `{g^12 | g ∈ G ∧ AlgebraicallyDisjoint f g}` +-/ +section AlgebraicCentralizer + +variable {G : Type _} +variable [Group G] + +-- TODO: prove this is a subgroup? +-- This is referred to as `ξ_G^12(f)` +def AlgebraicSubgroup (f : G) : Set G := + (fun g : G => g^12) '' { g : G | IsAlgebraicallyDisjoint f g } + +def AlgebraicCentralizer (f : G) : Subgroup G := + Subgroup.centralizer (AlgebraicSubgroup f) + +/-- +Finite intersections of [`AlgebraicCentralizer`]. +--/ +def AlgebraicCentralizerInter₀ (S : Finset G) : Subgroup G := + ⨅ (g ∈ S), AlgebraicCentralizer g + +structure AlgebraicCentralizerBasis₀ (G: Type _) [Group G] where + seed : Finset G + val_ne_bot : AlgebraicCentralizerInter₀ seed ≠ ⊥ + +def AlgebraicCentralizerBasis₀.val (B : AlgebraicCentralizerBasis₀ G) : Subgroup G := + AlgebraicCentralizerInter₀ B.seed + +theorem AlgebraicCentralizerBasis₀.val_def (B : AlgebraicCentralizerBasis₀ G) : + B.val = AlgebraicCentralizerInter₀ B.seed := rfl + +def AlgebraicCentralizerBasis (G : Type _) [Group G] : Set (Subgroup G) := + { H.val | H : AlgebraicCentralizerBasis₀ G } + +theorem AlgebraicCentralizerBasis.mem_iff (H : Subgroup G) : + H ∈ AlgebraicCentralizerBasis G ↔ ∃ B : AlgebraicCentralizerBasis₀ G, B.val = H := by rfl + +theorem AlgebraicCentralizerBasis.mem_iff' (H : Subgroup G) + (H_ne_bot : H ≠ ⊥) : + H ∈ AlgebraicCentralizerBasis G ↔ ∃ seed : Finset G, AlgebraicCentralizerInter₀ seed = H := +by + rw [mem_iff] + constructor + · intro ⟨B, B_eq⟩ + use B.seed + rw [AlgebraicCentralizerBasis₀.val_def] at B_eq + exact B_eq + · intro ⟨seed, seed_eq⟩ + let B := AlgebraicCentralizerInter₀ seed + have val_ne_bot : B ≠ ⊥ := by + unfold_let + rw [seed_eq] + exact H_ne_bot + use ⟨seed, val_ne_bot⟩ + rw [<-seed_eq] + rfl + +end AlgebraicCentralizer + end Rubin diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean index ee725cd..2f70ca7 100644 --- a/Rubin/HomeoGroup.lean +++ b/Rubin/HomeoGroup.lean @@ -207,6 +207,30 @@ by exact f_notin_ristV (rist_ss f_in_ristU) +theorem homeoGroup_rigidStabilizer_eq_iff {α : Type _} [TopologicalSpace α] + [LocallyMoving (HomeoGroup α) α] + {U V : Set α} (U_reg : Regular U) (V_reg : Regular V): + RigidStabilizer (HomeoGroup α) U = RigidStabilizer (HomeoGroup α) V ↔ U = V := +by + constructor + · intro rist_eq + apply le_antisymm <;> simp only [Set.le_eq_subset] + all_goals { + rw [homeoGroup_rigidStabilizer_subset_iff] <;> try assumption + rewrite [rist_eq] + rfl + } + · intro H_eq + rw [H_eq] + +theorem homeoGroup_rigidStabilizer_injective {α : Type _} [TopologicalSpace α] [LocallyMoving (HomeoGroup α) α] + : Function.Injective (fun U : { S : Set α // Regular S } => RigidStabilizer (HomeoGroup α) U.val) := +by + intro ⟨U, U_reg⟩ + intro ⟨V, V_reg⟩ + simp + exact (homeoGroup_rigidStabilizer_eq_iff U_reg V_reg).mp + end Other end Rubin diff --git a/Rubin/RigidStabilizer.lean b/Rubin/RigidStabilizer.lean index d443c4a..891aca3 100644 --- a/Rubin/RigidStabilizer.lean +++ b/Rubin/RigidStabilizer.lean @@ -172,4 +172,13 @@ by rw [Subgroup.mem_iInf] at x_in_rist exact x_in_rist T_in_S +theorem rigidStabilizer_smulImage (f g : G) (S : Set α) : + g ∈ RigidStabilizer G (f •'' S) ↔ f⁻¹ * g * f ∈ RigidStabilizer G S := +by + repeat rw [rigidStabilizer_support] + nth_rw 3 [<-inv_inv f] + rw [support_conjugate] + rw [smulImage_subset_inv] + simp + end Rubin diff --git a/Rubin/RigidStabilizerBasis.lean b/Rubin/RigidStabilizerBasis.lean new file mode 100644 index 0000000..9c4de6f --- /dev/null +++ b/Rubin/RigidStabilizerBasis.lean @@ -0,0 +1,269 @@ +/- +This file describes [`RigidStabilizerBasis`], which are all non-trivial subgroups of `G` constructed +by finite intersections of `RigidStabilizer G (RegularSupport α g)`. +-/ + +import Mathlib.Topology.Basic +import Mathlib.Topology.Homeomorph + +import Rubin.RegularSupport +import Rubin.RigidStabilizer + +namespace Rubin + +variable {G α : Type _} +variable [Group G] +variable [MulAction G α] +variable [TopologicalSpace α] + +/-- +Finite intersections of rigid stabilizers of regular supports +(which are equivalent to the rigid stabilizers of finite intersections of regular supports). +-/ +def RigidStabilizerInter₀ {G: Type _} (α : Type _) [Group G] [MulAction G α] [TopologicalSpace α] + (S : Finset G) : Subgroup G := + ⨅ (g ∈ S), RigidStabilizer G (RegularSupport α g) + +theorem RigidStabilizerInter₀.eq_sInter (S : Finset G) : + RigidStabilizerInter₀ α S = RigidStabilizer G (⋂ g ∈ S, (RegularSupport α g)) := +by + have img_eq : ⋂ g ∈ S, RegularSupport α g = ⋂₀ ((fun g : G => RegularSupport α g) '' S) := + by simp only [Set.sInter_image, Finset.mem_coe] + + rw [img_eq] + rw [rigidStabilizer_sInter] + unfold RigidStabilizerInter₀ + + ext x + repeat rw [Subgroup.mem_iInf] + constructor + · intro H T + rw [Subgroup.mem_iInf] + intro T_in_img + simp at T_in_img + let ⟨g, ⟨g_in_S, T_eq⟩⟩ := T_in_img + specialize H g + rw [Subgroup.mem_iInf] at H + rw [<-T_eq] + apply H; assumption + · intro H g + rw [Subgroup.mem_iInf] + intro g_in_S + specialize H (RegularSupport α g) + rw [Subgroup.mem_iInf] at H + simp at H + apply H g <;> tauto + +/-- +A predecessor structure to [`RigidStabilizerBasis`], where equality is defined on the choice of +group elements who regular support's rigid stabilizer get intersected upon. +--/ +structure RigidStabilizerBasis₀ (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α] where + seed : Finset G + val_ne_bot : RigidStabilizerInter₀ α seed ≠ ⊥ + +def RigidStabilizerBasis₀.val (B : RigidStabilizerBasis₀ G α) : Subgroup G := + RigidStabilizerInter₀ α B.seed + +theorem RigidStabilizerBasis₀.val_def (B : RigidStabilizerBasis₀ G α) : B.val = RigidStabilizerInter₀ α B.seed := rfl + +/-- +The set of all non-trivial subgroups of `G` constructed +by finite intersections of `RigidStabilizer G (RegularSupport α g)`. +--/ +def RigidStabilizerBasis (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α] : Set (Subgroup G) := + { H.val | H : RigidStabilizerBasis₀ G α } + +theorem RigidStabilizerBasis.mem_iff (H : Subgroup G) : + H ∈ RigidStabilizerBasis G α ↔ ∃ B : RigidStabilizerBasis₀ G α, B.val = H := by rfl + +theorem RigidStabilizerBasis.mem_iff' (H : Subgroup G) + (H_ne_bot : H ≠ ⊥) : + H ∈ RigidStabilizerBasis G α ↔ ∃ seed : Finset G, RigidStabilizerInter₀ α seed = H := +by + rw [mem_iff] + constructor + · intro ⟨B, B_eq⟩ + use B.seed + rw [RigidStabilizerBasis₀.val_def] at B_eq + exact B_eq + · intro ⟨seed, seed_eq⟩ + let B := RigidStabilizerInter₀ α seed + have val_ne_bot : B ≠ ⊥ := by + unfold_let + rw [seed_eq] + exact H_ne_bot + use ⟨seed, val_ne_bot⟩ + rw [<-seed_eq] + rfl + +def RigidStabilizerBasis.asSets (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α] : Set (Set G) := + { (H.val : Set G) | H : RigidStabilizerBasis₀ G α } + +theorem RigidStabilizerBasis.mem_asSets_iff (S : Set G) : + S ∈ RigidStabilizerBasis.asSets G α ↔ ∃ H ∈ RigidStabilizerBasis G α, H.carrier = S := +by + unfold asSets RigidStabilizerBasis + simp + rfl + +theorem RigidStabilizerBasis.mem_iff_asSets (H : Subgroup G) : + H ∈ RigidStabilizerBasis G α ↔ (H : Set G) ∈ RigidStabilizerBasis.asSets G α := +by + unfold asSets RigidStabilizerBasis + simp + +variable [ContinuousMulAction G α] + +lemma RigidStabilizerBasis.smulImage_mem₀ {H : Subgroup G} (H_in_ristBasis : H ∈ RigidStabilizerBasis G α) + (f : G) : ((fun g => f * g * f⁻¹) '' H.carrier) ∈ RigidStabilizerBasis.asSets G α := +by + have G_decidable : DecidableEq G := Classical.decEq _ + rw [mem_iff] at H_in_ristBasis + let ⟨seed, H_eq⟩ := H_in_ristBasis + rw [mem_asSets_iff] + + let new_seed := Finset.image (fun g => f * g * f⁻¹) seed.seed + have new_seed_ne_bot : RigidStabilizerInter₀ α new_seed ≠ ⊥ := by + rw [RigidStabilizerInter₀.eq_sInter] + unfold_let + simp [<-regularSupport_smulImage] + rw [<-ne_eq] + rw [<-smulImage_iInter_fin] + + have val_ne_bot := seed.val_ne_bot + rw [Subgroup.ne_bot_iff_exists_ne_one] at val_ne_bot + let ⟨⟨g, g_in_ristInter⟩, g_ne_one⟩ := val_ne_bot + simp at g_ne_one + + have fgf_in_ristInter₂ : f * g * f⁻¹ ∈ RigidStabilizer G (f •'' ⋂ x ∈ seed.seed, RegularSupport α x) := by + rw [rigidStabilizer_smulImage] + group + rw [RigidStabilizerInter₀.eq_sInter] at g_in_ristInter + exact g_in_ristInter + + have fgf_ne_one : f * g * f⁻¹ ≠ 1 := by + intro h₁ + have h₂ := congr_arg (fun x => x * f) h₁ + group at h₂ + have h₃ := congr_arg (fun x => f⁻¹ * x) h₂ + group at h₃ + exact g_ne_one h₃ + + + rw [Subgroup.ne_bot_iff_exists_ne_one] + use ⟨f * g * f⁻¹, fgf_in_ristInter₂⟩ + simp + rw [<-ne_eq] + exact fgf_ne_one + + use RigidStabilizerInter₀ α new_seed + apply And.intro + exact ⟨⟨new_seed, new_seed_ne_bot⟩, rfl⟩ + rw [RigidStabilizerInter₀.eq_sInter] + unfold_let + simp [<-regularSupport_smulImage] + rw [<-smulImage_iInter_fin] + + ext x + simp only [Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup, + Subgroup.mem_toSubmonoid, Set.mem_image] + rw [rigidStabilizer_smulImage] + rw [<-H_eq, RigidStabilizerBasis₀.val_def, RigidStabilizerInter₀.eq_sInter] + + constructor + · intro fxf_mem + use f⁻¹ * x * f + constructor + · exact fxf_mem + · group + · intro ⟨y, ⟨y_in_H, y_conj⟩⟩ + rw [<-y_conj] + group + exact y_in_H + +def RigidStabilizerBasisMul (G α : Type _) [Group G] [MulAction G α] [TopologicalSpace α] + [ContinuousMulAction G α] (f : G) (H : Subgroup G) + : Subgroup G +where + carrier := (fun g => f * g * f⁻¹) '' H.carrier + mul_mem' := by + intro a b a_mem b_mem + simp at a_mem + simp at b_mem + let ⟨a', a'_in_H, a'_eq⟩ := a_mem + let ⟨b', b'_in_H, b'_eq⟩ := b_mem + use a' * b' + constructor + · apply Subsemigroup.mul_mem' <;> simp <;> assumption + · simp + rw [<-a'_eq, <-b'_eq] + group + one_mem' := by + simp + use 1 + constructor + exact Subgroup.one_mem H + group + inv_mem' := by + simp + intro g g_in_H + use g⁻¹ + constructor + exact Subgroup.inv_mem H g_in_H + rw [mul_assoc] + +theorem RigidStabilizerBasisMul_mem (f : G) {H : Subgroup G} (H_in_basis : H ∈ RigidStabilizerBasis G α) + : RigidStabilizerBasisMul G α f H ∈ RigidStabilizerBasis G α := +by + rw [RigidStabilizerBasis.mem_iff_asSets] + unfold RigidStabilizerBasisMul + simp + + apply RigidStabilizerBasis.smulImage_mem₀ + assumption + +instance rigidStabilizerBasis_smul : SMul G (RigidStabilizerBasis G α) where + smul := fun g H => ⟨ + RigidStabilizerBasisMul G α g H.val, + RigidStabilizerBasisMul_mem g H.prop + ⟩ + +theorem RigidStabilizerBasis.smul_eq (g : G) {H: Subgroup G} (H_in_basis : H ∈ RigidStabilizerBasis G α) : + g • (⟨H, H_in_basis⟩ : RigidStabilizerBasis G α) = ⟨ + RigidStabilizerBasisMul G α g H, + RigidStabilizerBasisMul_mem g H_in_basis + ⟩ := rfl + +theorem RigidStabilizerBasis.mem_smul (f g : G) {H: Subgroup G} (H_in_basis : H ∈ RigidStabilizerBasis G α): + f ∈ (g • (⟨H, H_in_basis⟩ : RigidStabilizerBasis G α)).val ↔ g⁻¹ * f * g ∈ H := +by + rw [RigidStabilizerBasis.smul_eq] + simp + rw [<-Subgroup.mem_carrier] + unfold RigidStabilizerBasisMul + simp + constructor + · intro ⟨x, x_in_H, f_eq⟩ + rw [<-f_eq] + group + exact x_in_H + · intro gfg_in_H + use g⁻¹ * f * g + constructor + assumption + group + +instance rigidStabilizerBasis_mulAction : MulAction G (RigidStabilizerBasis G α) where + one_smul := by + intro ⟨H, H_in_ristBasis⟩ + ext x + rw [RigidStabilizerBasis.mem_smul] + group + mul_smul := by + intro f g ⟨B, B_in_ristBasis⟩ + ext x + repeat rw [RigidStabilizerBasis.mem_smul] + group + +end Rubin