Documentation

Mathlib.GroupTheory.GroupAction.FixedPoints

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 #

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} [AddGroup G] [AddAction G α] (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} [Group G] [MulAction G α] (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} [AddGroup G] [AddAction G α] {a : α} {g : G} :
theorem MulAction.smul_mem_fixedBy_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] {a : α} {g : G} :
theorem AddAction.vadd_neg_mem_fixedBy_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [AddGroup G] [AddAction G α] {a : α} {g : G} :
theorem MulAction.smul_inv_mem_fixedBy_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] {a : α} {g : G} :
theorem AddAction.minimalPeriod_eq_one_iff_fixedBy {α : Type u_1} {G : Type u_2} [AddGroup G] [AddAction G α] {a : α} {g : G} :
Function.minimalPeriod (fun (x : α) => g +ᵥ x) a = 1 a AddAction.fixedBy α g
theorem MulAction.minimalPeriod_eq_one_iff_fixedBy {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] {a : α} {g : G} :
Function.minimalPeriod (fun (x : α) => g x) a = 1 a MulAction.fixedBy α g
theorem AddAction.fixedBy_subset_fixedBy_zsmul (α : Type u_1) {G : Type u_2} [AddGroup G] [AddAction G α] (g : G) (j : ) :
theorem MulAction.fixedBy_subset_fixedBy_zpow (α : Type u_1) {G : Type u_2} [Group G] [MulAction G α] (g : G) (j : ) :
@[simp]
theorem AddAction.fixedBy_zero_eq_univ (α : Type u_1) (M : Type u_3) [AddMonoid M] [AddAction M α] :
AddAction.fixedBy α 0 = Set.univ
@[simp]
theorem MulAction.fixedBy_one_eq_univ (α : Type u_1) (M : Type u_3) [Monoid M] [MulAction M α] :
MulAction.fixedBy α 1 = Set.univ
theorem AddAction.fixedBy_add (α : Type u_1) {M : Type u_3} [AddMonoid M] [AddAction M α] (m₁ : M) (m₂ : M) :
theorem MulAction.fixedBy_mul (α : Type u_1) {M : Type u_3} [Monoid M] [MulAction M α] (m₁ : M) (m₂ : M) :
theorem AddAction.vadd_fixedBy (α : Type u_1) {G : Type u_2} [AddGroup G] [AddAction G α] (g : G) (h : G) :
theorem MulAction.smul_fixedBy (α : Type u_1) {G : Type u_2} [Group G] [MulAction G α] (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} [AddGroup G] [AddAction G α] (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} [Group G] [MulAction G α] (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} [Group G] [MulAction G α] {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} [AddGroup G] [AddAction G α] {s : Set α} {g : G} (s_ss_fixedBy : s AddAction.fixedBy α g) :

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} [Group G] [MulAction G α] {s : Set α} {g : G} (s_ss_fixedBy : s MulAction.fixedBy α g) :

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} [Group G] [MulAction G α] {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} [AddGroup G] [AddAction G α] {s : Set α} {g : G} (s_subset : (AddAction.fixedBy α g) 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} [Group G] [MulAction G α] {s : Set α} {g : G} (s_subset : (MulAction.fixedBy α g) 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} [AddGroup G] [AddAction G α] {g : G} {h : G} (comm : AddCommute 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 MulAction.fixedBy_mem_fixedBy_of_commute {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] {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} [AddGroup G] [AddAction G α] {g : G} {h : G} (comm : AddCommute g h) (j : ) :

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} [Group G] [MulAction G α] {g : G} {h : G} (comm : Commute g 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} [AddGroup G] [AddAction G α] {g : G} {h : G} (comm : AddCommute 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 MulAction.movedBy_mem_fixedBy_of_commute {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] {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} [AddGroup G] [AddAction G α] {g : G} {h : G} (comm : AddCommute g h) (j : ) :

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} [Group G] [MulAction G α] {g : G} {h : G} (comm : Commute g 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} [AddMonoid M] [AddAction M α] [FaithfulVAdd M α] {m : M} :
AddAction.fixedBy α 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} [Monoid M] [MulAction M α] [FaithfulSMul M α] {m : M} :
MulAction.fixedBy α 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} [AddGroup G] [AddAction G α] [FaithfulVAdd G α] {g : G} {h : G} (ne_one : g 0) (disjoint : Disjoint (AddAction.fixedBy α g) (h +ᵥ (AddAction.fixedBy α g))) :

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} [Group G] [MulAction G α] [FaithfulSMul G α] {g : G} {h : G} (ne_one : g 1) (disjoint : Disjoint (MulAction.fixedBy α g) (h (MulAction.fixedBy α g))) :

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.