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

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 MulAction.fixedBy_inv (α : Type u_1) {G : Type u_2} [Group G] [MulAction G α] (g : G) : fixedBy α g⁻¹ = fixedBy α g

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

@[simp]

theorem AddAction.fixedBy_neg (α : Type u_1) {G : Type u_2} [AddGroup G] [AddAction G α] (g : G) : fixedBy α (-g) = fixedBy α g

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

theorem MulAction.smul_mem_fixedBy_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] {a : α} {g : G} : g • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

theorem AddAction.vadd_mem_fixedBy_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [AddGroup G] [AddAction G α] {a : α} {g : G} : g +ᵥ a ∈ fixedBy α g ↔ a ∈ fixedBy α g

theorem MulAction.smul_inv_mem_fixedBy_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] {a : α} {g : G} : g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

theorem AddAction.vadd_neg_mem_fixedBy_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [AddGroup G] [AddAction G α] {a : α} {g : G} : -g +ᵥ a ∈ fixedBy α g ↔ a ∈ 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 ∈ fixedBy α 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 ∈ fixedBy α g

theorem MulAction.mem_fixedBy_zpow {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] {g : G} {a : α} (h : a ∈ fixedBy α g) (j : ℤ) : a ∈ fixedBy α (g ^ j)

theorem AddAction.mem_fixedBy_zsmul {α : Type u_1} {G : Type u_2} [AddGroup G] [AddAction G α] {g : G} {a : α} (h : a ∈ fixedBy α g) (j : ℤ) : a ∈ fixedBy α (j • g)

theorem MulAction.mem_fixedBy_zpowers_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] {g : G} {a : α} : (∀ (j : ℤ), a ∈ fixedBy α (g ^ j)) ↔ a ∈ fixedBy α g

theorem AddAction.mem_fixedBy_zmultiples_iff_mem_fixedBy {α : Type u_1} {G : Type u_2} [AddGroup G] [AddAction G α] {g : G} {a : α} : (∀ (j : ℤ), a ∈ fixedBy α (j • g)) ↔ a ∈ fixedBy α g

theorem MulAction.fixedBy_subset_fixedBy_zpow (α : Type u_1) {G : Type u_2} [Group G] [MulAction G α] (g : G) (j : ℤ) : fixedBy α g ⊆ fixedBy α (g ^ j)

theorem AddAction.fixedBy_subset_fixedBy_zsmul (α : Type u_1) {G : Type u_2} [AddGroup G] [AddAction G α] (g : G) (j : ℤ) : fixedBy α g ⊆ fixedBy α (j • g)

@[simp]

theorem MulAction.fixedBy_one_eq_univ (α : Type u_1) (M : Type u_3) [Monoid M] [MulAction M α] : fixedBy α 1 = Set.univ

@[simp]

theorem AddAction.fixedBy_zero_eq_univ (α : Type u_1) (M : Type u_3) [AddMonoid M] [AddAction M α] : fixedBy α 0 = Set.univ

theorem MulAction.fixedBy_mul (α : Type u_1) {M : Type u_3} [Monoid M] [MulAction M α] (m₁ m₂ : M) : fixedBy α m₁ ∩ fixedBy α m₂ ⊆ fixedBy α (m₁ * m₂)

theorem AddAction.fixedBy_add (α : Type u_1) {M : Type u_3} [AddMonoid M] [AddAction M α] (m₁ m₂ : M) : fixedBy α m₁ ∩ fixedBy α m₂ ⊆ fixedBy α (m₁ + m₂)

theorem MulAction.smul_fixedBy (α : Type u_1) {G : Type u_2} [Group G] [MulAction G α] (g h : G) : h • fixedBy α g = fixedBy α (h * g * h⁻¹)

theorem AddAction.vadd_fixedBy (α : Type u_1) {G : Type u_2} [AddGroup G] [AddAction G α] (g h : G) : h +ᵥ fixedBy α g = fixedBy α (h + g + -h)

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 MulAction.set_mem_fixedBy_iff {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] (s : Set α) (g : G) : s ∈ 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 AddAction.set_mem_fixedBy_iff {α : Type u_1} {G : Type u_2} [AddGroup G] [AddAction G α] (s : Set α) (g : G) : s ∈ 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 ∈ fixedBy (Set α) g) {x : α} : g • x ∈ s ↔ x ∈ s

theorem AddAction.vadd_mem_of_set_mem_fixedBy {α : Type u_1} {G : Type u_2} [AddGroup G] [AddAction G α] {s : Set α} {g : G} (s_in_fixedBy : s ∈ fixedBy (Set α) g) {x : α} : g +ᵥ x ∈ s ↔ 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 ⊆ fixedBy α g) : s ∈ fixedBy (Set α) 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 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 ⊆ fixedBy α g) : s ∈ fixedBy (Set α) 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 t : Set α} {g : G} (t_ss_s : t ⊆ s) (s_in_fixedBy : s ∈ 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 MulAction.set_mem_fixedBy_of_movedBy_subset {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] {s : Set α} {g : G} (s_subset : (fixedBy α g)ᶜ ⊆ s) : s ∈ fixedBy (Set α) g

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

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 : (fixedBy α g)ᶜ ⊆ s) : s ∈ fixedBy (Set α) g

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

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

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

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

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

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

theorem MulAction.movedBy_mem_fixedBy_of_commute {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] {g h : G} (comm : Commute g h) : (fixedBy α g)ᶜ ∈ fixedBy (Set α) 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.movedBy_mem_fixedBy_of_addCommute {α : Type u_1} {G : Type u_2} [AddGroup G] [AddAction G α] {g h : G} (comm : AddCommute g h) : (fixedBy α g)ᶜ ∈ fixedBy (Set α) 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.smul_zpow_movedBy_eq_of_commute {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] {g h : G} (comm : Commute g h) (j : ℤ) : h ^ j • (fixedBy α g)ᶜ = (fixedBy α g)ᶜ

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

theorem AddAction.vadd_zsmul_movedBy_eq_of_addCommute {α : Type u_1} {G : Type u_2} [AddGroup G] [AddAction G α] {g h : G} (comm : AddCommute g h) (j : ℤ) : j • h +ᵥ (fixedBy α g)ᶜ = (fixedBy α g)ᶜ

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

theorem MulAction.fixedBy_eq_univ_iff_eq_one {α : Type u_1} {M : Type u_3} [Monoid M] [MulAction M α] [FaithfulSMul M α] {m : M} : 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.fixedBy_eq_univ_iff_eq_zero {α : Type u_1} {M : Type u_3} [AddMonoid M] [AddAction M α] [FaithfulVAdd M α] {m : M} : 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.not_commute_of_disjoint_movedBy_preimage {α : Type u_1} {G : Type u_2} [Group G] [MulAction G α] [FaithfulSMul G α] {g h : G} (ne_one : g ≠ 1) (disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)) : ¬Commute g 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 AddAction.not_addCommute_of_disjoint_movedBy_preimage {α : Type u_1} {G : Type u_2} [AddGroup G] [AddAction G α] [FaithfulVAdd G α] {g h : G} (ne_zero : g ≠ 0) (disjoint : Disjoint (fixedBy α g)ᶜ (h +ᵥ (fixedBy α g)ᶜ)) : ¬AddCommute g 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.