From 253c33035d0bf017d413cbb493b51fed4460756f Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Mon, 1 Jan 2024 17:00:19 +0100 Subject: [PATCH] :tada: Finished the proof of rubin's theorem --- Rubin.lean | 86 ++++++---- Rubin/HomeoGroup.lean | 257 ------------------------------ Rubin/LocallyDense.lean | 18 ++- Rubin/MulActionExt.lean | 6 - Rubin/RegularSupportBasis.lean | 1 - Rubin/RigidStabilizerBasis.lean | 268 -------------------------------- Rubin/Topology.lean | 94 ++++++++--- 7 files changed, 144 insertions(+), 586 deletions(-) delete mode 100644 Rubin/HomeoGroup.lean delete mode 100644 Rubin/RigidStabilizerBasis.lean diff --git a/Rubin.lean b/Rubin.lean index 2d95869..4f7c01f 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -24,12 +24,10 @@ import Rubin.SmulImage import Rubin.Support import Rubin.Topology import Rubin.RigidStabilizer --- import Rubin.RigidStabilizerBasis import Rubin.Period import Rubin.AlgebraicDisjointness import Rubin.RegularSupport import Rubin.RegularSupportBasis -import Rubin.HomeoGroup import Rubin.Filter #align_import rubin @@ -37,33 +35,54 @@ import Rubin.Filter namespace Rubin open Rubin.Tactic --- TODO: find a home -theorem equiv_congr_ne {ι ι' : Type _} (e : ι ≃ ι') {x y : ι} : x ≠ y → e x ≠ e y := - by - intro x_ne_y - by_contra h - apply x_ne_y - convert congr_arg e.symm h <;> simp only [Equiv.symm_apply_apply] -#align equiv.congr_ne Rubin.equiv_congr_ne - ---------------------------------------------------------------- section Rubin ---------------------------------------------------------------- section RubinActions -structure RubinAction (G α : Type _) extends - Group G, - TopologicalSpace α, - MulAction G α, - FaithfulSMul G α -where +-- TODO: debate whether having this structure is relevant or not, +-- since the instance inference engine doesn't play well with it. +-- One alternative would be to lay out all of the properties as-is (without their class wrappers), +-- then provide ways to reconstruct them in instances. +structure RubinAction (G α : Type _) where + group : Group G + action : MulAction G α + topology : TopologicalSpace α + faithful : FaithfulSMul G α locally_compact : LocallyCompactSpace α hausdorff : T2Space α no_isolated_points : HasNoIsolatedPoints α - locallyDense : LocallyDense G α + locally_dense : LocallyDense G α #align rubin_action Rubin.RubinAction +/-- +Constructs a RubinAction from ambient instances. +If needed, missing instances can be passed as named parameters. +--/ +def RubinAction.mk' (G α : Type _) + [group : Group G] [topology : TopologicalSpace α] [hausdorff : T2Space α] [action : MulAction G α] + [faithful : FaithfulSMul G α] [locally_compact : LocallyCompactSpace α] + [no_isolated_points : HasNoIsolatedPoints α] [locally_dense : LocallyDense G α] : + RubinAction G α := ⟨ + group, + action, + topology, + faithful, + locally_compact, + hausdorff, + no_isolated_points, + locally_dense + ⟩ + +variable {G α : Type _} + +instance RubinAction.instGroup (act : RubinAction G α) : Group G := act.group + +instance RubinAction.instFaithful (act : RubinAction G α) : @FaithfulSMul G α (@MulAction.toSMul G α act.group.toMonoid act.action) := act.faithful + +instance RubinAction.topologicalSpace (act : RubinAction G α) : TopologicalSpace α := act.topology + end RubinActions section AlgebraicDisjointness @@ -2317,6 +2336,7 @@ theorem RubinFilter.mul_smul (g h : G) (F : RubinFilter G) : (F.smul g).smul h = rw [Filter.map_map, <-MulAut.coe_mul] rw [Filter.InBasis.map_basis_toOrderIsoSet _ F.filter.in_basis] +-- Note: awfully slow to compile (since it isn't noncomputable, it gets compiled down to IR) 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 @@ -2344,9 +2364,9 @@ instance : MulAction G (RubinSpace G) where theorem RubinSpace.smul_def (g : G) (Q : RubinSpace G) : g • Q = Q.smul g := rfl -noncomputable def rubin' : EquivariantHomeomorph G (RubinSpace G) α where +noncomputable def RubinSpace.equivariantHomeomorph : EquivariantHomeomorph G (RubinSpace G) α where toHomeomorph := RubinSpace.homeomorph (G := G) α - equivariant := by + toFun_equivariant' := by intro g Q simp [RubinSpace.homeomorph] rw [RubinSpace.smul_def] @@ -2356,20 +2376,18 @@ noncomputable def rubin' : EquivariantHomeomorph G (RubinSpace G) α where end Equivariant --- theorem rubin' (hα : RubinAction G α) : EquivariantHomeomorph G α (RubinSpace G) where --- toFun := fun x => ⟦⟧ --- invFun := fun S => sorry - - - -/- -variable {β : Type _} -variable [TopologicalSpace β] [MulAction G β] [ContinuousConstSMul G β] - -theorem rubin (hα : RubinAction G α) (hβ : RubinAction G β) : EquivariantHomeomorph G α β := by - -- by composing rubin' hα - sorry --/ +variable (G : Type _) +variable [Group G] [Nontrivial G] +variable (α : Type _) [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] [HasNoIsolatedPoints α] +variable [MulAction G α] [FaithfulSMul G α] [ContinuousConstSMul G α] [LocallyDense G α] +variable (β : Type _) [TopologicalSpace β] [T2Space β] [LocallyCompactSpace β] [HasNoIsolatedPoints β] +variable [MulAction G β] [FaithfulSMul G β] [ContinuousConstSMul G β] [LocallyDense G β] + +noncomputable def rubin : EquivariantHomeomorph G α β := + let α_nonempty : Nonempty α := by rwa [LocallyMoving.nonempty_iff_nontrivial G] + let β_nonempty : Nonempty β := by rwa [LocallyMoving.nonempty_iff_nontrivial G] + (RubinSpace.equivariantHomeomorph (G := G) (α := α)).inv.trans + (RubinSpace.equivariantHomeomorph (G := G) (α := β)) end Rubin diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean deleted file mode 100644 index 6d16930..0000000 --- a/Rubin/HomeoGroup.lean +++ /dev/null @@ -1,257 +0,0 @@ -import Mathlib.Logic.Equiv.Defs -import Mathlib.Topology.Basic -import Mathlib.Topology.Homeomorph -import Mathlib.Topology.Algebra.ConstMulAction - -import Rubin.LocallyDense -import Rubin.Topology -import Rubin.Support -import Rubin.RegularSupport - -structure HomeoGroup (α : Type _) [TopologicalSpace α] extends Homeomorph α α - -variable {α : Type _} -variable [TopologicalSpace α] - -def HomeoGroup.coe : HomeoGroup α -> Homeomorph α α := HomeoGroup.toHomeomorph - -def HomeoGroup.from : Homeomorph α α -> HomeoGroup α := HomeoGroup.mk - -instance homeoGroup_coe : Coe (HomeoGroup α) (Homeomorph α α) where - coe := HomeoGroup.coe - -instance homeoGroup_coe₂ : Coe (Homeomorph α α) (HomeoGroup α) where - coe := HomeoGroup.from - -def HomeoGroup.toPerm : HomeoGroup α → Equiv.Perm α := fun g => g.coe.toEquiv - -instance homeoGroup_coe_perm : Coe (HomeoGroup α) (Equiv.Perm α) where - coe := HomeoGroup.toPerm - -@[simp] -theorem HomeoGroup.toPerm_def (g : HomeoGroup α) : g.coe.toEquiv = (g : Equiv.Perm α) := rfl - -@[simp] -theorem HomeoGroup.mk_coe (g : HomeoGroup α) : HomeoGroup.mk (g.coe) = g := rfl - -@[simp] -theorem HomeoGroup.eq_iff_coe_eq {f g : HomeoGroup α} : f.coe = g.coe ↔ f = g := by - constructor - { - intro f_eq_g - rw [<-HomeoGroup.mk_coe f] - rw [f_eq_g] - simp - } - { - intro f_eq_g - unfold HomeoGroup.coe - rw [f_eq_g] - } - -@[simp] -theorem HomeoGroup.from_toHomeomorph (m : Homeomorph α α) : (HomeoGroup.from m).toHomeomorph = m := rfl - -instance homeoGroup_one : One (HomeoGroup α) where - one := HomeoGroup.from (Homeomorph.refl α) - -theorem HomeoGroup.one_def : (1 : HomeoGroup α) = (Homeomorph.refl α : HomeoGroup α) := rfl - -instance homeoGroup_inv : Inv (HomeoGroup α) where - inv := fun g => HomeoGroup.from (g.coe.symm) - -@[simp] -theorem HomeoGroup.inv_def (g : HomeoGroup α) : (Homeomorph.symm g.coe : HomeoGroup α) = g⁻¹ := rfl - -theorem HomeoGroup.coe_inv {g : HomeoGroup α} : HomeoGroup.coe (g⁻¹) = (HomeoGroup.coe g).symm := rfl - -instance homeoGroup_mul : Mul (HomeoGroup α) where - mul := fun a b => ⟨b.toHomeomorph.trans a.toHomeomorph⟩ - -theorem HomeoGroup.coe_mul {f g : HomeoGroup α} : HomeoGroup.coe (f * g) = (HomeoGroup.coe g).trans (HomeoGroup.coe f) := rfl - -@[simp] -theorem HomeoGroup.mul_def (f g : HomeoGroup α) : HomeoGroup.from ((HomeoGroup.coe g).trans (HomeoGroup.coe f)) = f * g := rfl - -instance homeoGroup_group : Group (HomeoGroup α) where - mul_assoc := by - intro a b c - rw [<-HomeoGroup.eq_iff_coe_eq] - repeat rw [HomeoGroup_coe_mul] - rfl - mul_one := by - intro a - rw [<-HomeoGroup.eq_iff_coe_eq] - rw [HomeoGroup.coe_mul] - rfl - one_mul := by - intro a - rw [<-HomeoGroup.eq_iff_coe_eq] - rw [HomeoGroup.coe_mul] - rfl - mul_left_inv := by - intro a - rw [<-HomeoGroup.eq_iff_coe_eq] - rw [HomeoGroup.coe_mul] - rw [HomeoGroup.coe_inv] - simp - rfl - -/-- -The HomeoGroup trivially has a continuous and faithful `MulAction` on the underlying topology `α`. ---/ -instance homeoGroup_smul₁ : SMul (HomeoGroup α) α where - smul := fun g x => g.toFun x - -@[simp] -theorem HomeoGroup.smul₁_def (f : HomeoGroup α) (x : α) : f.toFun x = f • x := rfl - -@[simp] -theorem HomeoGroup.smul₁_def' (f : HomeoGroup α) (x : α) : f.toHomeomorph x = f • x := rfl - -@[simp] -theorem HomeoGroup.coe_toFun_eq_smul₁ (f : HomeoGroup α) (x : α) : FunLike.coe (HomeoGroup.coe f) x = f • x := rfl - -instance homeoGroup_mulAction₁ : MulAction (HomeoGroup α) α where - one_smul := by - intro x - rfl - mul_smul := by - intro f g x - rfl - -instance homeoGroup_mulAction₁_continuous : ContinuousConstSMul (HomeoGroup α) α where - continuous_const_smul := by - intro h - constructor - intro S S_open - conv => { - congr; ext - congr; ext - rw [<-HomeoGroup.smul₁_def'] - } - simp only [Homeomorph.isOpen_preimage] - exact S_open - -instance homeoGroup_mulAction₁_faithful : FaithfulSMul (HomeoGroup α) α where - eq_of_smul_eq_smul := by - intro f g hyp - rw [<-HomeoGroup.eq_iff_coe_eq] - ext x - simp - exact hyp x - -theorem HomeoGroup.smulImage_eq_image (g : HomeoGroup α) (S : Set α) : - g •'' S = ⇑g.toHomeomorph '' S := rfl - -section FromContinuousConstSMul - -variable {G : Type _} [Group G] -variable [MulAction G α] [ContinuousConstSMul G α] - -/-- -`fromContinuous` is a structure-preserving transformation from a continuous `MulAction` to a `HomeoGroup` ---/ -def HomeoGroup.fromContinuous (α : Type _) [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] - (g : G) : HomeoGroup α := - HomeoGroup.from (Homeomorph.smul g) - -@[simp] -theorem HomeoGroup.fromContinuous_def (g : G) : - HomeoGroup.from (Homeomorph.smul g) = HomeoGroup.fromContinuous α g := rfl - -@[simp] -theorem HomeoGroup.fromContinuous_smul (g : G) : - ∀ x : α, (HomeoGroup.fromContinuous α g) • x = g • x := -by - intro x - unfold fromContinuous - rw [<-HomeoGroup.smul₁_def', HomeoGroup.from_toHomeomorph] - unfold Homeomorph.smul - simp - -theorem HomeoGroup.fromContinuous_one : - HomeoGroup.fromContinuous α (1 : G) = (1 : HomeoGroup α) := -by - apply FaithfulSMul.eq_of_smul_eq_smul (α := α) - simp - -theorem HomeoGroup.fromContinuous_mul (g h : G): - (HomeoGroup.fromContinuous α g) * (HomeoGroup.fromContinuous α h) = (HomeoGroup.fromContinuous α (g * h)) := -by - apply FaithfulSMul.eq_of_smul_eq_smul (α := α) - intro x - rw [mul_smul] - simp - rw [mul_smul] - -theorem HomeoGroup.fromContinuous_inv (g : G): - HomeoGroup.fromContinuous α g⁻¹ = (HomeoGroup.fromContinuous α g)⁻¹ := -by - apply FaithfulSMul.eq_of_smul_eq_smul (α := α) - intro x - group_action - rw [mul_smul] - simp - -theorem HomeoGroup.fromContinuous_eq_iff [FaithfulSMul G α] (g h : G): - (HomeoGroup.fromContinuous α g) = (HomeoGroup.fromContinuous α h) ↔ g = h := -by - constructor - · intro cont_eq - apply FaithfulSMul.eq_of_smul_eq_smul (α := α) - intro x - rw [<-HomeoGroup.fromContinuous_smul g] - rw [cont_eq] - simp - · tauto - -@[simp] -theorem HomeoGroup.fromContinuous_support (g : G) : - Rubin.Support α (HomeoGroup.fromContinuous α g) = Rubin.Support α g := -by - ext x - repeat rw [Rubin.mem_support] - rw [<-HomeoGroup.smul₁_def, <-HomeoGroup.fromContinuous_def] - rw [HomeoGroup.from_toHomeomorph] - rw [Homeomorph.smul] - simp only [Equiv.toFun_as_coe, MulAction.toPerm_apply] - -@[simp] -theorem HomeoGroup.fromContinuous_regularSupport (g : G) : - Rubin.RegularSupport α (HomeoGroup.fromContinuous α g) = Rubin.RegularSupport α g := -by - unfold Rubin.RegularSupport - rw [HomeoGroup.fromContinuous_support] - -@[simp] -theorem HomeoGroup.fromContinuous_smulImage (g : G) (V : Set α) : - (HomeoGroup.fromContinuous α g) •'' V = g •'' V := -by - repeat rw [Rubin.smulImage_def] - simp - -def HomeoGroup.fromContinuous_embedding (α : Type _) [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α]: G ↪ (HomeoGroup α) where - toFun := fun (g : G) => HomeoGroup.fromContinuous α g - inj' := by - intro g h fromCont_eq - simp at fromCont_eq - apply FaithfulSMul.eq_of_smul_eq_smul (α := α) - intro x - rw [<-fromContinuous_smul, fromCont_eq, fromContinuous_smul] - -@[simp] -theorem HomeoGroup.fromContinuous_embedding_toFun [FaithfulSMul G α] (g : G): - HomeoGroup.fromContinuous_embedding α g = HomeoGroup.fromContinuous α g := rfl - -def HomeoGroup.fromContinuous_monoidHom (α : Type _) [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α]: G →* (HomeoGroup α) where - toFun := fun (g : G) => HomeoGroup.fromContinuous α g - map_one' := by - simp - rw [fromContinuous_one] - map_mul' := by - simp - intros - rw [fromContinuous_mul] - -end FromContinuousConstSMul diff --git a/Rubin/LocallyDense.lean b/Rubin/LocallyDense.lean index be947e5..4f0eeb1 100644 --- a/Rubin/LocallyDense.lean +++ b/Rubin/LocallyDense.lean @@ -126,13 +126,29 @@ by let ⟨g, _, g_ne_one⟩ := (get_nontrivial_rist_elem (G := G) (α := α) isOpen_univ Set.univ_nonempty) use g -theorem LocallyMoving.nontrivial {G α : Type _} [Group G] [TopologicalSpace α] +theorem LocallyMoving.nontrivial (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] [LocallyMoving G α] [Nonempty α] : Nontrivial G where exists_pair_ne := by use 1 simp only [ne_comm] exact nontrivial_elem G α +theorem LocallyMoving.nonempty_iff_nontrivial (G α : Type _) [Group G] [TopologicalSpace α] + [MulAction G α] [FaithfulSMul G α] [LocallyMoving G α] : Nonempty α ↔ Nontrivial G := +by + constructor + · intro; exact LocallyMoving.nontrivial G α + · intro nontrivial + by_contra α_empty + rw [not_nonempty_iff] at α_empty + let ⟨g, h, g_ne_h⟩ := nontrivial.exists_pair_ne + apply g_ne_h + apply FaithfulSMul.eq_of_smul_eq_smul (α := α) + intro a + exfalso + exact α_empty.false a + + variable {G α : Type _} variable [Group G] variable [TopologicalSpace α] diff --git a/Rubin/MulActionExt.lean b/Rubin/MulActionExt.lean index 86be76b..3cf04d6 100644 --- a/Rubin/MulActionExt.lean +++ b/Rubin/MulActionExt.lean @@ -37,12 +37,6 @@ theorem smul_zpow_eq_of_smul_eq {x : α} {g : G} (n : ℤ) : exact res #align smul_zpow_eq_of_smul_eq Rubin.smul_zpow_eq_of_smul_eq --- TODO: turn this into a structure? -def is_equivariant (G : Type _) {β : Type _} [Group G] [MulAction G α] - [MulAction G β] (f : α → β) := - ∀ g : G, ∀ x : α, f (g • x) = g • f x -#align is_equivariant Rubin.is_equivariant - lemma disjoint_not_mem {α : Type _} {U V : Set α} (disj: Disjoint U V) : ∀ {x : α}, x ∈ U → x ∉ V := by diff --git a/Rubin/RegularSupportBasis.lean b/Rubin/RegularSupportBasis.lean index d9fd0aa..34d1031 100644 --- a/Rubin/RegularSupportBasis.lean +++ b/Rubin/RegularSupportBasis.lean @@ -11,7 +11,6 @@ import Rubin.LocallyDense import Rubin.Topology import Rubin.Support import Rubin.RegularSupport -import Rubin.HomeoGroup namespace Rubin diff --git a/Rubin/RigidStabilizerBasis.lean b/Rubin/RigidStabilizerBasis.lean deleted file mode 100644 index 6b41dea..0000000 --- a/Rubin/RigidStabilizerBasis.lean +++ /dev/null @@ -1,268 +0,0 @@ -/- -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 [ContinuousConstSMul 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 α] - [ContinuousConstSMul 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 diff --git a/Rubin/Topology.lean b/Rubin/Topology.lean index ee1990f..fd94dfc 100644 --- a/Rubin/Topology.lean +++ b/Rubin/Topology.lean @@ -1,5 +1,6 @@ import Mathlib.GroupTheory.Subgroup.Basic import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.GroupTheory.GroupAction.Hom import Mathlib.Topology.Basic import Mathlib.Topology.Homeomorph import Mathlib.Topology.Algebra.ConstMulAction @@ -9,33 +10,88 @@ import Rubin.MulActionExt namespace Rubin --- TODO: give this a notation? --- TODO: coe to / extend MulActionHom +section Equivariant + +-- TODO: rename or remove? +def IsEquivariant (G : Type _) {β : Type _} [Group G] [MulAction G α] + [MulAction G β] (f : α → β) := + ∀ g : G, ∀ x : α, f (g • x) = g • f x + +-- TODO: rename to MulActionHomeomorph structure EquivariantHomeomorph (G α β : Type _) [Group G] [TopologicalSpace α] [TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where - equivariant : is_equivariant G toFun -#align equivariant_homeomorph Rubin.EquivariantHomeomorph + toFun_equivariant' : IsEquivariant G toFun -variable {G α β : Type _} +variable {G α β γ: Type*} variable [Group G] -variable [TopologicalSpace α] [TopologicalSpace β] - -theorem equivariant_fun [MulAction G α] [MulAction G β] - (h : EquivariantHomeomorph G α β) : - is_equivariant G h.toFun := - h.equivariant -#align equivariant_fun Rubin.equivariant_fun - -theorem equivariant_inv [MulAction G α] [MulAction G β] - (h : EquivariantHomeomorph G α β) : - is_equivariant G h.invFun := - by +variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] +variable [MulAction G α] [MulAction G β] [MulAction G γ] + +theorem EquivariantHomeomorph.toFun_equivariant (f : EquivariantHomeomorph G α β) : + IsEquivariant G f.toHomeomorph := +by + show IsEquivariant G f.toFun + exact f.toFun_equivariant' + +instance EquivariantHomeomorph.smulHomClass : SMulHomClass (EquivariantHomeomorph G α β) G α β where + coe := fun f => f.toFun + coe_injective' := by + show Function.Injective (fun f => f.toHomeomorph) + refine Function.Injective.comp FunLike.coe_injective ?mk_inj + intro f g + rw [mk.injEq] + tauto + map_smul := fun f => f.toFun_equivariant + +theorem EquivariantHomeomorph.invFun_equivariant + (h : EquivariantHomeomorph G α β) : + IsEquivariant G h.invFun := +by intro g x symm - let e := congr_arg h.invFun (h.equivariant g (h.invFun x)) + let e := congr_arg h.invFun (h.toFun_equivariant' g (h.invFun x)) rw [h.left_inv _, h.right_inv _] at e exact e -#align equivariant_inv Rubin.equivariant_inv + +def EquivariantHomeomorph.trans (f₁ : EquivariantHomeomorph G α β) (f₂ : EquivariantHomeomorph G β γ) : + EquivariantHomeomorph G α γ +where + toHomeomorph := Homeomorph.trans f₁.toHomeomorph f₂.toHomeomorph + toFun_equivariant' := by + intro g x + simp + rw [f₁.toFun_equivariant] + rw [f₂.toFun_equivariant] + +@[simp] +theorem EquivariantHomeomorph.trans_toFun (f₁ : EquivariantHomeomorph G α β) (f₂ : EquivariantHomeomorph G β γ) : + (f₁.trans f₂).toFun = f₂.toFun ∘ f₁.toFun := +by + simp [trans] + rfl + +@[simp] +theorem EquivariantHomeomorph.trans_invFun (f₁ : EquivariantHomeomorph G α β) (f₂ : EquivariantHomeomorph G β γ) : + (f₁.trans f₂).invFun = f₁.invFun ∘ f₂.invFun := +by + simp [trans] + rfl + +def EquivariantHomeomorph.inv (f : EquivariantHomeomorph G α β) : + EquivariantHomeomorph G β α +where + toHomeomorph := f.symm + toFun_equivariant' := f.invFun_equivariant + +@[simp] +theorem EquivariantHomeomorph.inv_toFun (f : EquivariantHomeomorph G α β) : + f.inv.toFun = f.invFun := rfl + +@[simp] +theorem EquivariantHomeomorph.inv_invFun (f : EquivariantHomeomorph G α β) : + f.inv.invFun = f.toFun := rfl + +end Equivariant open Topology