doc-next-gen

Mathlib.GroupTheory.GroupAction.FixedPoints

Module docstring

{"# 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. ","### 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 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. ","## 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. "}

MulAction.fixedBy_inv theorem
(g : G) : fixedBy α g⁻¹ = fixedBy α g
Full source 
/-- 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]
Fixed Points of Group Element and Its Inverse Coincide
Informal description
For any group element $g$ in a multiplicative group action on a set $\alpha$, the set of points fixed by $g^{-1}$ is equal to the set of points fixed by $g$, i.e., $$\{x \in \alpha \mid g^{-1} \cdot x = x\} = \{x \in \alpha \mid g \cdot x = x\}.$$
MulAction.smul_mem_fixedBy_iff_mem_fixedBy theorem
{a : α} {g : G} : g • a ∈ fixedBy α g ↔ a ∈ fixedBy α g
Full source 
@[to_additive]
theorem smul_mem_fixedBy_iff_mem_fixedBy {a : α} {g : G} :
    g • a ∈ fixedBy α gg • a ∈ fixedBy α g ↔ a ∈ fixedBy α g := by
  rw [mem_fixedBy, smul_left_cancel_iff]
  rfl
Fixed Point Characterization under Group Action
Informal description
For any element $a$ in a set $\alpha$ acted upon by a group $G$, and for any group element $g \in G$, the action of $g$ on $a$ lies in the fixed points of $g$ if and only if $a$ itself lies in the fixed points of $g$. In other words, $$g \cdot a \in \{x \in \alpha \mid g \cdot x = x\} \leftrightarrow a \in \{x \in \alpha \mid g \cdot x = x\}.$$
MulAction.smul_inv_mem_fixedBy_iff_mem_fixedBy theorem
{a : α} {g : G} : g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g
Full source 
@[to_additive]
theorem smul_inv_mem_fixedBy_iff_mem_fixedBy {a : α} {g : G} :
    g⁻¹g⁻¹ • a ∈ fixedBy α gg⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g := by
  rw [← fixedBy_inv, smul_mem_fixedBy_iff_mem_fixedBy, fixedBy_inv]
Fixed Point Characterization under Inverse Group Action
Informal description
For any element $a$ in a set $\alpha$ acted upon by a group $G$, and for any group element $g \in G$, the action of $g^{-1}$ on $a$ lies in the fixed points of $g$ if and only if $a$ itself lies in the fixed points of $g$. In other words, $$g^{-1} \cdot a \in \{x \in \alpha \mid g \cdot x = x\} \leftrightarrow a \in \{x \in \alpha \mid g \cdot x = x\}.$$
MulAction.minimalPeriod_eq_one_iff_fixedBy theorem
{a : α} {g : G} : Function.minimalPeriod (fun x => g • x) a = 1 ↔ a ∈ fixedBy α g
Full source 
@[to_additive minimalPeriod_eq_one_iff_fixedBy]
theorem minimalPeriod_eq_one_iff_fixedBy {a : α} {g : G} :
    Function.minimalPeriodFunction.minimalPeriod (fun x => g • x) a = 1 ↔ a ∈ fixedBy α g :=
  Function.minimalPeriod_eq_one_iff_isFixedPt
Minimal Period One Characterizes Fixed Points in Group Actions
Informal description
For an element $a$ in a set $\alpha$ acted upon by a group $G$, and for an element $g \in G$, the minimal period of $a$ under the action of $g$ is equal to 1 if and only if $a$ is fixed by $g$, i.e., $g \cdot a = a$.
MulAction.fixedBy_subset_fixedBy_zpow theorem
(g : G) (j : ℤ) : fixedBy α g ⊆ fixedBy α (g ^ j)
Full source 
@[to_additive]
theorem fixedBy_subset_fixedBy_zpow (g : G) (j : ℤ) :
    fixedByfixedBy α 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, Int.natCast_one]
  exact one_dvd j
Fixed Points are Preserved under Integer Powers
Informal description
For any group element $g \in G$ acting on a set $\alpha$ and any integer $j \in \mathbb{Z}$, the set of points fixed by $g$ is contained in the set of points fixed by $g^j$. In other words, if $x \in \alpha$ is fixed by $g$ (i.e., $g \cdot x = x$), then $x$ is also fixed by any integer power $g^j$ of $g$.
MulAction.fixedBy_one_eq_univ theorem
: fixedBy α (1 : M) = Set.univ
Full source 
@[to_additive (attr := simp)]
theorem fixedBy_one_eq_univ : fixedBy α (1 : M) = Set.univ :=
  Set.eq_univ_iff_forall.mpr <| one_smul M
Fixed Points of Identity Element is Universal Set
Informal description
The set of fixed points of the identity element $1$ in a monoid $M$ acting on a type $\alpha$ is equal to the universal set $\alpha$, i.e., $\text{fixedBy}_\alpha(1) = \alpha$.
MulAction.fixedBy_mul theorem
(m₁ m₂ : M) : fixedBy α m₁ ∩ fixedBy α m₂ ⊆ fixedBy α (m₁ * m₂)
Full source 
@[to_additive]
theorem fixedBy_mul (m₁ m₂ : M) : fixedByfixedBy α m₁ ∩ fixedBy α m₂fixedBy α m₁ ∩ fixedBy α m₂ ⊆ fixedBy α (m₁ * m₂) := by
  intro a ⟨h₁, h₂⟩
  rw [mem_fixedBy, mul_smul, h₂, h₁]
Intersection of Fixed Point Sets is Contained in Fixed Points of Product
Informal description
For any two elements $m_1$ and $m_2$ in a monoid $M$ acting on a type $\alpha$, the intersection of the fixed point sets $\text{fixedBy}(\alpha, m_1)$ and $\text{fixedBy}(\alpha, m_2)$ is contained in the fixed point set of their product $\text{fixedBy}(\alpha, m_1 * m_2)$. In other words, if an element $x \in \alpha$ is fixed by both $m_1$ and $m_2$, then it is also fixed by $m_1 * m_2$.
MulAction.smul_fixedBy theorem
(g h : G) : h • fixedBy α g = fixedBy α (h * g * h⁻¹)
Full source 
@[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]
Conjugation of Fixed Points under Group Action
Informal description
For any group elements $g$ and $h$ in a group $G$ acting on a set $\alpha$, the image of the fixed points of $g$ under the action of $h$ is equal to the fixed points of the conjugate $hgh^{-1}$. That is, $$ h \cdot \text{fixedBy}(\alpha, g) = \text{fixedBy}(\alpha, hgh^{-1}). $$
MulAction.set_mem_fixedBy_iff theorem
(s : Set α) (g : G) : s ∈ fixedBy (Set α) g ↔ ∀ x, g • x ∈ s ↔ x ∈ s
Full source 
/--
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 α) gs ∈ 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]
Characterization of Fixed Sets under Group Action: $s \in \text{fixedBy} (\text{Set } \alpha) g \leftrightarrow \forall x, g \cdot x \in s \leftrightarrow x \in s$
Informal description
For a set $s$ in a type $\alpha$ with a group action by $G$, and an element $g \in G$, the set $s$ is fixed by $g$ (i.e., $s \in \text{fixedBy} (\text{Set } \alpha) g$) if and only if for every $x \in \alpha$, the action of $g$ on $x$ satisfies $g \cdot x \in s \leftrightarrow x \in s$.
MulAction.smul_mem_of_set_mem_fixedBy theorem
{s : Set α} {g : G} (s_in_fixedBy : s ∈ fixedBy (Set α) g) {x : α} : g • x ∈ s ↔ x ∈ s
Full source 
@[to_additive]
theorem smul_mem_of_set_mem_fixedBy {s : Set α} {g : G} (s_in_fixedBy : s ∈ fixedBy (Set α) g)
    {x : α} : g • x ∈ sg • x ∈ s ↔ x ∈ s := (set_mem_fixedBy_iff s g).mp s_in_fixedBy x
Characterization of Fixed Set Membership under Group Action: $g \cdot x \in s \leftrightarrow x \in s$
Informal description
For a set $s \subseteq \alpha$ fixed by a group element $g \in G$ (i.e., $s \in \text{fixedBy} (\text{Set } \alpha) g$), and for any element $x \in \alpha$, the action of $g$ on $x$ satisfies $g \cdot x \in s$ if and only if $x \in s$.
MulAction.set_mem_fixedBy_of_subset_fixedBy theorem
{s : Set α} {g : G} (s_ss_fixedBy : s ⊆ fixedBy α g) : s ∈ fixedBy (Set α) g
Full source 
/--
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
Subset of Fixed Points is Fixed Under Pointwise Action
Informal description
For a set $s$ in a type $\alpha$ with a group action by $G$, and an element $g \in G$, if every element of $s$ is fixed by $g$ (i.e., $s \subseteq \{x \in \alpha \mid g \cdot x = x\}$), then $s$ is fixed by $g$ under the pointwise action (i.e., $g \cdot s = s$).
MulAction.smul_subset_of_set_mem_fixedBy theorem
{s t : Set α} {g : G} (t_ss_s : t ⊆ s) (s_in_fixedBy : s ∈ fixedBy (Set α) g) : g • t ⊆ s
Full source 
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.smul_set_subset_smul_set_iff.mpr t_ss_s).trans s_in_fixedBy.subset
Image of Subset under Group Action Preserves Fixed Superset
Informal description
Let $G$ be a group acting on a set $\alpha$, and let $g \in G$. For any subsets $s, t \subseteq \alpha$ such that $t \subseteq s$ and $s$ is fixed by $g$ under the pointwise action (i.e., $g \cdot s = s$), the image of $t$ under the action of $g$ is contained in $s$, i.e., $g \cdot t \subseteq s$.
MulAction.set_mem_fixedBy_of_movedBy_subset theorem
{s : Set α} {g : G} (s_subset : (fixedBy α g)ᶜ ⊆ s) : s ∈ fixedBy (Set α) g
Full source 
/-- 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)ᶜ(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]
Superset of Non-Fixed Points is Fixed Under Group Action
Informal description
Let $G$ be a group acting on a set $\alpha$, and let $g \in G$. For any subset $s \subseteq \alpha$ containing the complement of the fixed points of $g$ (i.e., $(fixedBy\ \alpha\ g)^c \subseteq s$), the set $s$ is fixed by $g$ under the pointwise action, meaning $g \cdot s = s$.
MulAction.fixedBy_mem_fixedBy_of_commute theorem
{g h : G} (comm : Commute g h) : (fixedBy α g) ∈ fixedBy (Set α) h
Full source 
/--
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]
Fixed Points of Commuting Group Elements are Invariant Under Each Other's Action
Informal description
Let $G$ be a group acting on a set $\alpha$, and let $g, h \in G$ be commuting elements. Then the set of fixed points of $g$ (denoted $\text{fixedBy}(\alpha, g) = \{x \in \alpha \mid g \cdot x = x\}$) is fixed by the action of $h$, i.e., $h \cdot \text{fixedBy}(\alpha, g) = \text{fixedBy}(\alpha, g)$.
MulAction.smul_zpow_fixedBy_eq_of_commute theorem
{g h : G} (comm : Commute g h) (j : ℤ) : h ^ j • fixedBy α g = fixedBy α g
Full source 
/--
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)
Invariance of Fixed Points under Commuting Integer Powers
Informal description
Let $G$ be a group acting on a set $\alpha$, and let $g, h \in G$ be commuting elements. Then for any integer $j \in \mathbb{Z}$, the action of $h^j$ on the set of fixed points of $g$ (i.e., $\{x \in \alpha \mid g \cdot x = x\}$) leaves it invariant: $h^j \cdot \text{fixedBy}(\alpha, g) = \text{fixedBy}(\alpha, g)$.
MulAction.movedBy_mem_fixedBy_of_commute theorem
{g h : G} (comm : Commute g h) : (fixedBy α g)ᶜ ∈ fixedBy (Set α) h
Full source 
/--
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 α g)ᶜ ∈ fixedBy (Set α) h := by
  rw [mem_fixedBy, Set.smul_set_compl, fixedBy_mem_fixedBy_of_commute comm]
Invariance of Moved Points under Commuting Group Action
Informal description
Let $G$ be a group acting on a set $\alpha$, and let $g, h \in G$ be commuting elements. Then the complement of the fixed points of $g$ (denoted $(\text{fixedBy}(\alpha, g))^c = \{x \in \alpha \mid g \cdot x \neq x\}$) is fixed by the action of $h$, i.e., $h \cdot (\text{fixedBy}(\alpha, g))^c = (\text{fixedBy}(\alpha, g))^c$.
MulAction.smul_zpow_movedBy_eq_of_commute theorem
{g h : G} (comm : Commute g h) (j : ℤ) : h ^ j • (fixedBy α g)ᶜ = (fixedBy α g)ᶜ
Full source 
/--
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)
Invariance of Moved Points under Commuting Integer Powers
Informal description
Let $G$ be a group acting on a set $\alpha$, and let $g, h \in G$ be commuting elements. Then for any integer $j \in \mathbb{Z}$, the action of $h^j$ on the complement of the fixed points of $g$ (i.e., $\{x \in \alpha \mid g \cdot x \neq x\}$) leaves it invariant: $h^j \cdot (\text{fixedBy}(\alpha, g))^c = (\text{fixedBy}(\alpha, g))^c$.
MulAction.fixedBy_eq_univ_iff_eq_one theorem
{m : M} : fixedBy α m = Set.univ ↔ m = 1
Full source 
/-- 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} : fixedByfixedBy α m = Set.univ ↔ m = 1 := by
  rw [← (smul_left_injective' (M := M) (α := α)).eq_iff, Set.eq_univ_iff_forall]
  simp_rw [funext_iff, one_smul, mem_fixedBy]
Fixed Points Cover Entire Set if and only if Acting Element is Identity
Informal description
For a faithful multiplicative action of a group $M$ on a set $\alpha$, the set of fixed points of $m \in M$ is equal to the entire set $\alpha$ if and only if $m$ is the identity element of $M$. In other words, $\text{fixedBy}(\alpha, m) = \alpha \leftrightarrow m = 1$.
MulAction.not_commute_of_disjoint_movedBy_preimage theorem
{g h : G} (ne_one : g ≠ 1) (disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)) : ¬Commute g h
Full source 
/--
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
Non-commutativity from Disjoint Moved Sets
Informal description
Let $G$ be a group acting on a set $\alpha$, and let $g, h \in G$ with $g \neq 1$. If the set of points moved by $g$ (i.e., the complement of $\text{fixedBy}(\alpha, g)$) is disjoint from its image under the action of $h$, then $g$ and $h$ do not commute. In other words, if $\{x \in \alpha \mid g \cdot x \neq x\} \cap h \cdot \{x \in \alpha \mid g \cdot x \neq x\} = \emptyset$, then $\neg \text{Commute}(g, h)$.