# 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.

@[simp]
theorem AddAction.fixedBy_neg (α : Type u_1) {G : Type u_2} [] [] (g : G) :
=

In an additive group action, the points fixed by g are also fixed by g⁻¹

@[simp]
theorem MulAction.fixedBy_inv (α : Type u_1) {G : Type u_2} [] [] (g : G) :

In a multiplicative group action, the points fixed by g are also fixed by g⁻¹

theorem AddAction.vadd_mem_fixedBy_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [] [] {a : α} {g : G} :
g +ᵥ a a
theorem MulAction.smul_mem_fixedBy_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [] [] {a : α} {g : G} :
g a a
theorem AddAction.vadd_neg_mem_fixedBy_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [] [] {a : α} {g : G} :
-g +ᵥ a a
theorem MulAction.smul_inv_mem_fixedBy_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [] [] {a : α} {g : G} :
theorem AddAction.minimalPeriod_eq_one_iff_fixedBy {α : Type u_1} {G : Type u_2} [] [] {a : α} {g : G} :
Function.minimalPeriod (fun (x : α) => g +ᵥ x) a = 1 a
theorem MulAction.minimalPeriod_eq_one_iff_fixedBy {α : Type u_1} {G : Type u_2} [] [] {a : α} {g : G} :
Function.minimalPeriod (fun (x : α) => g x) a = 1 a
theorem AddAction.fixedBy_subset_fixedBy_zsmul (α : Type u_1) {G : Type u_2} [] [] (g : G) (j : ) :
theorem MulAction.fixedBy_subset_fixedBy_zpow (α : Type u_1) {G : Type u_2} [] [] (g : G) (j : ) :
@[simp]
theorem AddAction.fixedBy_zero_eq_univ (α : Type u_1) (M : Type u_3) [] [] :
= Set.univ
@[simp]
theorem MulAction.fixedBy_one_eq_univ (α : Type u_1) (M : Type u_3) [] [] :
= Set.univ
abbrev AddAction.fixedBy_add.match_1 (α : Type u_1) {M : Type u_2} [] [] (m₁ : M) (m₂ : M) ⦃a : α (motive : a Prop) :
∀ (h : a ), (∀ (h₁ : a ) (h₂ : a ), motive )motive h
Equations
• =
Instances For
theorem AddAction.fixedBy_add (α : Type u_1) {M : Type u_3} [] [] (m₁ : M) (m₂ : M) :
theorem MulAction.fixedBy_mul (α : Type u_1) {M : Type u_3} [] [] (m₁ : M) (m₂ : M) :
MulAction.fixedBy α (m₁ * m₂)
theorem AddAction.vadd_fixedBy (α : Type u_1) {G : Type u_2} [] [] (g : G) (h : G) :
h +ᵥ = AddAction.fixedBy α (h + g + -h)
theorem MulAction.smul_fixedBy (α : Type u_1) {G : Type u_2} [] [] (g : G) (h : G) :

### fixedBy sets of the pointwise group action #

The theorems below need the Pointwise scoped to be opened (using open Pointwise) to be used effectively.

theorem AddAction.set_mem_fixedBy_iff {α : Type u_1} {G : Type u_2} [] [] (s : Set α) (g : G) :
s AddAction.fixedBy (Set α) g ∀ (x : α), g +ᵥ x s x s

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 MulAction.set_mem_fixedBy_iff {α : Type u_1} {G : Type u_2} [] [] (s : Set α) (g : G) :
s MulAction.fixedBy (Set α) g ∀ (x : α), g x s x s

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 MulAction.smul_mem_of_set_mem_fixedBy {α : Type u_1} {G : Type u_2} [] [] {s : Set α} {g : G} (s_in_fixedBy : s MulAction.fixedBy (Set α) g) {x : α} :
g x s x s
theorem AddAction.set_mem_fixedBy_of_subset_fixedBy {α : Type u_1} {G : Type u_2} [] [] {s : Set α} {g : G} (s_ss_fixedBy : s ) :

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 MulAction.set_mem_fixedBy_of_subset_fixedBy {α : Type u_1} {G : Type u_2} [] [] {s : Set α} {g : G} (s_ss_fixedBy : s ) :

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 MulAction.smul_subset_of_set_mem_fixedBy {α : Type u_1} {G : Type u_2} [] [] {s : Set α} {t : Set α} {g : G} (t_ss_s : t s) (s_in_fixedBy : s MulAction.fixedBy (Set α) g) :
g t s

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.

theorem AddAction.set_mem_fixedBy_of_movedBy_subset {α : Type u_1} {G : Type u_2} [] [] {s : Set α} {g : G} (s_subset : () s) :

If (fixedBy α g)ᶜ ⊆ s, then g cannot move a point of s outside of s.

theorem MulAction.set_mem_fixedBy_of_movedBy_subset {α : Type u_1} {G : Type u_2} [] [] {s : Set α} {g : G} (s_subset : () s) :

If (fixedBy α g)ᶜ ⊆ s, then g cannot move a point of s outside of s.

## 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.

theorem AddAction.fixedBy_mem_fixedBy_of_addCommute {α : Type u_1} {G : Type u_2} [] [] {g : G} {h : G} (comm : ) :

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 MulAction.fixedBy_mem_fixedBy_of_commute {α : Type u_1} {G : Type u_2} [] [] {g : G} {h : G} (comm : Commute g 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.

theorem AddAction.vadd_zsmul_fixedBy_eq_of_addCommute {α : Type u_1} {G : Type u_2} [] [] {g : G} {h : G} (comm : ) (j : ) :
j h +ᵥ =

If g and h commute, then g fixes (j • h) +ᵥ x iff g fixes x.

theorem MulAction.smul_zpow_fixedBy_eq_of_commute {α : Type u_1} {G : Type u_2} [] [] {g : G} {h : G} (comm : Commute g h) (j : ) :
h ^ j =

If g and h commute, then g fixes (h ^ j) • x iff g fixes x.

theorem AddAction.movedBy_mem_fixedBy_of_addCommute {α : Type u_1} {G : Type u_2} [] [] {g : G} {h : G} (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.

theorem MulAction.movedBy_mem_fixedBy_of_commute {α : Type u_1} {G : Type u_2} [] [] {g : G} {h : G} (comm : Commute g h) :

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 AddAction.vadd_zsmul_movedBy_eq_of_addCommute {α : Type u_1} {G : Type u_2} [] [] {g : G} {h : G} (comm : ) (j : ) :
j h +ᵥ () = ()

If g and h commute, then g moves (j • h) +ᵥ x iff g moves x.

theorem MulAction.smul_zpow_movedBy_eq_of_commute {α : Type u_1} {G : Type u_2} [] [] {g : G} {h : G} (comm : Commute g h) (j : ) :
h ^ j () = ()

If g and h commute, then g moves h ^ j • x iff g moves x.

theorem AddAction.fixedBy_eq_univ_iff_eq_zero {α : Type u_1} {M : Type u_3} [] [] [] {m : M} :
= Set.univ m = 0

If the additive action of M on α is faithful, then fixedBy α m = Set.univ implies that m = 1.

theorem MulAction.fixedBy_eq_univ_iff_eq_one {α : Type u_1} {M : Type u_3} [] [] [] {m : M} :
= Set.univ m = 1

If the multiplicative action of M on α is faithful, then fixedBy α m = Set.univ implies that m = 1.

theorem AddAction.not_addCommute_of_disjoint_movedBy_preimage {α : Type u_1} {G : Type u_2} [] [] [] {g : G} {h : G} (ne_one : g 0) (disjoint : Disjoint () (h +ᵥ ())) :

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 MulAction.not_commute_of_disjoint_movedBy_preimage {α : Type u_1} {G : Type u_2} [] [] [] {g : G} {h : G} (ne_one : g 1) (disjoint : Disjoint () (h ())) :

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.