From 8a5da17db79146db00328f4beadbd15941fd9d3a Mon Sep 17 00:00:00 2001 From: Shad Amethyst Date: Mon, 12 Feb 2024 10:30:27 +0000 Subject: [PATCH] feat(GroupTheory/GroupAction): new `FixedPoints` module with a few basic properties of `fixedBy` (#9477) Introduces a new module, `Mathlib.GroupTheory.GroupAction.FixedPoints`, which contains some properties of `MulAction.fixedBy` that wouldn't quite belong to `Mathlib.GroupTheory.GroupAction.Basic`. --- Mathlib.lean | 1 + Mathlib/Data/Set/Pointwise/SMul.lean | 4 + .../GroupTheory/GroupAction/FixedPoints.lean | 255 ++++++++++++++++++ .../GroupAction/FixingSubgroup.lean | 20 ++ 4 files changed, 280 insertions(+) create mode 100644 Mathlib/GroupTheory/GroupAction/FixedPoints.lean diff --git a/Mathlib.lean b/Mathlib.lean index 39bb623071ff8..94ff7999676b7 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2261,6 +2261,7 @@ import Mathlib.GroupTheory.GroupAction.Defs import Mathlib.GroupTheory.GroupAction.DomAct.ActionHom import Mathlib.GroupTheory.GroupAction.DomAct.Basic import Mathlib.GroupTheory.GroupAction.Embedding +import Mathlib.GroupTheory.GroupAction.FixedPoints import Mathlib.GroupTheory.GroupAction.FixingSubgroup import Mathlib.GroupTheory.GroupAction.Group import Mathlib.GroupTheory.GroupAction.Hom diff --git a/Mathlib/Data/Set/Pointwise/SMul.lean b/Mathlib/Data/Set/Pointwise/SMul.lean index e1132f9845abc..cd71a5d311198 100644 --- a/Mathlib/Data/Set/Pointwise/SMul.lean +++ b/Mathlib/Data/Set/Pointwise/SMul.lean @@ -972,6 +972,10 @@ theorem smul_univ {s : Set α} (hs : s.Nonempty) : s • (univ : Set β) = univ #align set.smul_univ Set.smul_univ #align set.vadd_univ Set.vadd_univ +@[to_additive] +theorem smul_set_compl : a • sᶜ = (a • s)ᶜ := by + simp_rw [Set.compl_eq_univ_diff, smul_set_sdiff, smul_set_univ] + @[to_additive] theorem smul_inter_ne_empty_iff {s t : Set α} {x : α} : x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x := by diff --git a/Mathlib/GroupTheory/GroupAction/FixedPoints.lean b/Mathlib/GroupTheory/GroupAction/FixedPoints.lean new file mode 100644 index 0000000000000..de7379856e034 --- /dev/null +++ b/Mathlib/GroupTheory/GroupAction/FixedPoints.lean @@ -0,0 +1,255 @@ +/- +Copyright (c) 2024 Emilie Burgun. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Emilie Burgun +-/ +import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.Dynamics.PeriodicPts +import Mathlib.Data.Set.Pointwise.SMul + +/-! +# Properties of `fixedPoints` and `fixedBy` + +This module contains some useful properties of `MulAction.fixedPoints` and `MulAction.fixedBy` +that don't directly belong to `Mathlib.GroupTheory.GroupAction.Basic`. + +## Main theorems + +* `MulAction.fixedBy_mul`: `fixedBy α (g * h) ⊆ fixedBy α g ∪ fixedBy α h` +* `MulAction.fixedBy_conj` and `MulAction.smul_fixedBy`: the pointwise group action of `h` on + `fixedBy α g` is equal to the `fixedBy` set of the conjugation of `h` with `g` + (`fixedBy α (h * g * h⁻¹)`). +* `MulAction.set_mem_fixedBy_of_movedBy_subset` shows that if a set `s` is a superset of + `(fixedBy α g)ᶜ`, then the group action of `g` cannot send elements of `s` outside of `s`. + This is expressed as `s ∈ fixedBy (Set α) g`, and `MulAction.set_mem_fixedBy_iff` allows one + to convert the relationship back to `g • x ∈ s ↔ x ∈ s`. +* `MulAction.not_commute_of_disjoint_smul_movedBy` allows one to prove that `g` and `h` + do not commute from the disjointness of the `(fixedBy α g)ᶜ` set and `h • (fixedBy α g)ᶜ`, + which is a property used in the proof of Rubin's theorem. + +The theorems above are also available for `AddAction`. + +## Pointwise group action and `fixedBy (Set α) g` + +Since `fixedBy α g = { x | g • x = x }` by definition, properties about the pointwise action of +a set `s : Set α` can be expressed using `fixedBy (Set α) g`. +To properly use theorems using `fixedBy (Set α) g`, you should `open Pointwise` in your file. + +`s ∈ fixedBy (Set α) g` means that `g • s = s`, which is equivalent to say that +`∀ x, g • x ∈ s ↔ x ∈ s` (the translation can be done using `MulAction.set_mem_fixedBy_iff`). + +`s ∈ fixedBy (Set α) g` is a weaker statement than `s ⊆ fixedBy α g`: the latter requires that +all points in `s` are fixed by `g`, whereas the former only requires that `g • x ∈ s`. +-/ + +namespace MulAction +open Pointwise + +variable {α : Type*} +variable {G : Type*} [Group G] [MulAction G α] +variable {M : Type*} [Monoid M] [MulAction M α] + + +section FixedPoints + +variable (α) in +/-- In a multiplicative group action, the points fixed by `g` are also fixed by `g⁻¹` -/ +@[to_additive (attr := simp) + "In an additive group action, the points fixed by `g` are also fixed by `g⁻¹`"] +theorem fixedBy_inv (g : G) : fixedBy α g⁻¹ = fixedBy α g := by + ext + rw [mem_fixedBy, mem_fixedBy, inv_smul_eq_iff, eq_comm] + +@[to_additive] +theorem smul_mem_fixedBy_iff_mem_fixedBy {a : α} {g : G} : + g • a ∈ fixedBy α g ↔ a ∈ fixedBy α g := by + rw [mem_fixedBy, smul_left_cancel_iff] + rfl + +@[to_additive] +theorem smul_inv_mem_fixedBy_iff_mem_fixedBy {a : α} {g : G} : + g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g := by + rw [← fixedBy_inv, smul_mem_fixedBy_iff_mem_fixedBy, fixedBy_inv] + +@[to_additive minimalPeriod_eq_one_iff_fixedBy] +theorem minimalPeriod_eq_one_iff_fixedBy {a : α} {g : G} : + Function.minimalPeriod (fun x => g • x) a = 1 ↔ a ∈ fixedBy α g := + Function.minimalPeriod_eq_one_iff_isFixedPt + +variable (α) in +@[to_additive] +theorem fixedBy_subset_fixedBy_zpow (g : G) (j : ℤ) : + fixedBy α g ⊆ fixedBy α (g ^ j) := by + intro a a_in_fixedBy + rw [mem_fixedBy, zpow_smul_eq_iff_minimalPeriod_dvd, + minimalPeriod_eq_one_iff_fixedBy.mpr a_in_fixedBy, Nat.cast_one] + exact one_dvd j + +variable (M α) in +@[to_additive (attr := simp)] +theorem fixedBy_one_eq_univ : fixedBy α (1 : M) = Set.univ := + Set.eq_univ_iff_forall.mpr <| one_smul M + +variable (α) in +@[to_additive] +theorem fixedBy_mul (m₁ m₂ : M) : fixedBy α m₁ ∩ fixedBy α m₂ ⊆ fixedBy α (m₁ * m₂) := by + intro a ⟨h₁, h₂⟩ + rw [mem_fixedBy, mul_smul, h₂, h₁] + +variable (α) in +@[to_additive] +theorem smul_fixedBy (g h: G) : + h • fixedBy α g = fixedBy α (h * g * h⁻¹) := by + ext a + simp_rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, mul_smul, smul_eq_iff_eq_inv_smul h] + +end FixedPoints + +section Pointwise + +/-! +### `fixedBy` sets of the pointwise group action + +The theorems below need the `Pointwise` scoped to be opened (using `open Pointwise`) +to be used effectively. +-/ + +/-- +If a set `s : Set α` is in `fixedBy (Set α) g`, then all points of `s` will stay in `s` after being +moved by `g`. +-/ +@[to_additive "If a set `s : Set α` is in `fixedBy (Set α) g`, then all points of `s` will stay in +`s` after being moved by `g`."] +theorem set_mem_fixedBy_iff (s : Set α) (g : G) : + s ∈ fixedBy (Set α) g ↔ ∀ x, g • x ∈ s ↔ x ∈ s := by + simp_rw [mem_fixedBy, ← eq_inv_smul_iff, Set.ext_iff, Set.mem_inv_smul_set_iff, Iff.comm] + +theorem smul_mem_of_set_mem_fixedBy {s : Set α} {g : G} (s_in_fixedBy : s ∈ fixedBy (Set α) g) + {x : α} : g • x ∈ s ↔ x ∈ s := (set_mem_fixedBy_iff s g).mp s_in_fixedBy x + +/-- +If `s ⊆ fixedBy α g`, then `g • s = s`, which means that `s ∈ fixedBy (Set α) g`. + +Note that the reverse implication is in general not true, as `s ∈ fixedBy (Set α) g` is a +weaker statement (it allows for points `x ∈ s` for which `g • x ≠ x` and `g • x ∈ s`). +-/ +@[to_additive "If `s ⊆ fixedBy α g`, then `g +ᵥ s = s`, which means that `s ∈ fixedBy (Set α) g`. + +Note that the reverse implication is in general not true, as `s ∈ fixedBy (Set α) g` is a +weaker statement (it allows for points `x ∈ s` for which `g +ᵥ x ≠ x` and `g +ᵥ x ∈ s`)."] +theorem set_mem_fixedBy_of_subset_fixedBy {s : Set α} {g : G} (s_ss_fixedBy : s ⊆ fixedBy α g) : + s ∈ fixedBy (Set α) g := by + rw [← fixedBy_inv] + ext x + rw [Set.mem_inv_smul_set_iff] + refine ⟨fun gxs => ?xs, fun xs => (s_ss_fixedBy xs).symm ▸ xs⟩ + rw [← fixedBy_inv] at s_ss_fixedBy + rwa [← s_ss_fixedBy gxs, inv_smul_smul] at gxs + +theorem smul_subset_of_set_mem_fixedBy {s t : Set α} {g : G} (t_ss_s : t ⊆ s) + (s_in_fixedBy : s ∈ fixedBy (Set α) g) : g • t ⊆ s := + (Set.set_smul_subset_set_smul_iff.mpr t_ss_s).trans s_in_fixedBy.subset + +/-! +If a set `s : Set α` is a superset of `(MulAction.fixedBy α g)ᶜ` (resp. `(AddAction.fixedBy α g)ᶜ`), +then no point or subset of `s` can be moved outside of `s` by the group action of `g`. +-/ + +/-- If `(fixedBy α g)ᶜ ⊆ s`, then `g` cannot move a point of `s` outside of `s`. -/ +@[to_additive "If `(fixedBy α g)ᶜ ⊆ s`, then `g` cannot move a point of `s` outside of `s`."] +theorem set_mem_fixedBy_of_movedBy_subset {s : Set α} {g : G} (s_subset : (fixedBy α g)ᶜ ⊆ s) : + s ∈ fixedBy (Set α) g := by + rw [← fixedBy_inv] + ext a + rw [Set.mem_inv_smul_set_iff] + by_cases a ∈ fixedBy α g + case pos a_fixed => + rw [a_fixed] + case neg a_moved => + constructor <;> (intro; apply s_subset) + · exact a_moved + · rwa [Set.mem_compl_iff, smul_mem_fixedBy_iff_mem_fixedBy] + +end Pointwise + +section Commute + +/-! +## Pointwise image of the `fixedBy` set by a commuting group element + +If two group elements `g` and `h` commute, then `g` fixes `h • x` (resp. `h +ᵥ x`) +if and only if `g` fixes `x`. + +This is equivalent to say that if `Commute g h`, then `fixedBy α g ∈ fixedBy (Set α) h` and +`(fixedBy α g)ᶜ ∈ fixedBy (Set α) h`. +-/ + +/-- +If `g` and `h` commute, then `g` fixes `h • x` iff `g` fixes `x`. +This is equivalent to say that the set `fixedBy α g` is fixed by `h`. +-/ +@[to_additive "If `g` and `h` commute, then `g` fixes `h +ᵥ x` iff `g` fixes `x`. +This is equivalent to say that the set `fixedBy α g` is fixed by `h`. +"] +theorem fixedBy_mem_fixedBy_of_commute {g h : G} (comm: Commute g h) : + (fixedBy α g) ∈ fixedBy (Set α) h := by + ext x + rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul, + smul_left_cancel_iff, mem_fixedBy] + +/-- +If `g` and `h` commute, then `g` fixes `(h ^ j) • x` iff `g` fixes `x`. +-/ +@[to_additive "If `g` and `h` commute, then `g` fixes `(j • h) +ᵥ x` iff `g` fixes `x`."] +theorem smul_zpow_fixedBy_eq_of_commute {g h : G} (comm : Commute g h) (j : ℤ) : + h ^ j • fixedBy α g = fixedBy α g := + fixedBy_subset_fixedBy_zpow (Set α) h j (fixedBy_mem_fixedBy_of_commute comm) + +/-- +If `g` and `h` commute, then `g` moves `h • x` iff `g` moves `x`. +This is equivalent to say that the set `(fixedBy α g)ᶜ` is fixed by `h`. +-/ +@[to_additive "If `g` and `h` commute, then `g` moves `h +ᵥ x` iff `g` moves `x`. +This is equivalent to say that the set `(fixedBy α g)ᶜ` is fixed by `h`."] +theorem movedBy_mem_fixedBy_of_commute {g h : G} (comm: Commute g h) : + (fixedBy α g)ᶜ ∈ fixedBy (Set α) h := by + rw [mem_fixedBy, Set.smul_set_compl, fixedBy_mem_fixedBy_of_commute comm] + +/-- +If `g` and `h` commute, then `g` moves `h ^ j • x` iff `g` moves `x`. +-/ +@[to_additive "If `g` and `h` commute, then `g` moves `(j • h) +ᵥ x` iff `g` moves `x`."] +theorem smul_zpow_movedBy_eq_of_commute {g h : G} (comm : Commute g h) (j : ℤ) : + h ^ j • (fixedBy α g)ᶜ = (fixedBy α g)ᶜ := + fixedBy_subset_fixedBy_zpow (Set α) h j (movedBy_mem_fixedBy_of_commute comm) + +end Commute + +section Faithful + +variable [FaithfulSMul G α] +variable [FaithfulSMul M α] + +/-- If the multiplicative action of `M` on `α` is faithful, +then `fixedBy α m = Set.univ` implies that `m = 1`. -/ +@[to_additive "If the additive action of `M` on `α` is faithful, +then `fixedBy α m = Set.univ` implies that `m = 1`."] +theorem fixedBy_eq_univ_iff_eq_one {m : M} : fixedBy α m = Set.univ ↔ m = 1 := by + rw [← (smul_left_injective' (M := M) (α := α)).eq_iff, Set.eq_univ_iff_forall] + simp_rw [Function.funext_iff, one_smul, mem_fixedBy] + +/-- +If the image of the `(fixedBy α g)ᶜ` set by the pointwise action of `h: G` +is disjoint from `(fixedBy α g)ᶜ`, then `g` and `h` cannot commute. +-/ +@[to_additive "If the image of the `(fixedBy α g)ᶜ` set by the pointwise action of `h: G` +is disjoint from `(fixedBy α g)ᶜ`, then `g` and `h` cannot commute."] +theorem not_commute_of_disjoint_movedBy_preimage {g h : G} (ne_one : g ≠ 1) + (disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)) : ¬Commute g h := by + contrapose! ne_one with comm + rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ, + compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint + +end Faithful + +end MulAction diff --git a/Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean b/Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean index e89f809e43ac2..90e29f5f68235 100644 --- a/Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean +++ b/Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean @@ -5,6 +5,7 @@ Authors: Antoine Chambert-Loir -/ import Mathlib.GroupTheory.Subgroup.Actions import Mathlib.GroupTheory.GroupAction.Basic +import Mathlib.GroupTheory.GroupAction.FixedPoints #align_import group_theory.group_action.fixing_subgroup from "leanprover-community/mathlib"@"f93c11933efbc3c2f0299e47b8ff83e9b539cbf6" @@ -36,6 +37,8 @@ TODO : * Treat semigroups ? +* add `to_additive` for the various lemmas + -/ @@ -120,6 +123,14 @@ theorem mem_fixingSubgroup_iff {s : Set α} {m : M} : m ∈ fixingSubgroup M s ⟨fun hg y hy => hg ⟨y, hy⟩, fun h ⟨y, hy⟩ => h y hy⟩ #align mem_fixing_subgroup_iff mem_fixingSubgroup_iff +theorem mem_fixingSubgroup_iff_subset_fixedBy {s : Set α} {m : M} : + m ∈ fixingSubgroup M s ↔ s ⊆ fixedBy α m := by + simp_rw [mem_fixingSubgroup_iff, Set.subset_def, mem_fixedBy] + +theorem mem_fixingSubgroup_compl_iff_movedBy_subset {s : Set α} {m : M} : + m ∈ fixingSubgroup M sᶜ ↔ (fixedBy α m)ᶜ ⊆ s := by + rw [mem_fixingSubgroup_iff_subset_fixedBy, Set.compl_subset_comm] + variable (α) /-- The Galois connection between fixing subgroups and fixed points of a group action -/ @@ -161,4 +172,13 @@ theorem fixedPoints_subgroup_iSup {ι : Sort*} {P : ι → Subgroup M} : (fixingSubgroup_fixedPoints_gc M α).u_iInf #align fixed_points_subgroup_supr fixedPoints_subgroup_iSup +/-- The orbit of the fixing subgroup of `sᶜ` (ie. the moving subgroup of `s`) is a subset of `s` -/ +theorem orbit_fixingSubgroup_compl_subset {s : Set α} {a : α} (a_in_s : a ∈ s) : + MulAction.orbit (fixingSubgroup M sᶜ) a ⊆ s := by + intro b b_in_orbit + let ⟨⟨g, g_fixing⟩, g_eq⟩ := MulAction.mem_orbit_iff.mp b_in_orbit + rw [Submonoid.mk_smul] at g_eq + rw [mem_fixingSubgroup_compl_iff_movedBy_subset] at g_fixing + rwa [← g_eq, smul_mem_of_set_mem_fixedBy (set_mem_fixedBy_of_movedBy_subset g_fixing)] + end Group