Basic properties of group actions #

This file primarily concerns itself with orbits, stabilizers, and other objects defined in terms of actions. Despite this file being called basic, low-level helper lemmas for algebraic manipulation of • belong elsewhere.

Main definitions #

source

theorem MulAction.fst_mem_orbit_of_mem_orbit {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {β : Type u_1} [MulAction M β] {x y : α × β} (h : x ∈ orbit M y) :

x.1 ∈ orbit M y.1

source

theorem AddAction.fst_mem_orbit_of_mem_orbit {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {β : Type u_1} [AddAction M β] {x y : α × β} (h : x ∈ orbit M y) :

x.1 ∈ orbit M y.1

source

theorem MulAction.snd_mem_orbit_of_mem_orbit {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {β : Type u_1} [MulAction M β] {x y : α × β} (h : x ∈ orbit M y) :

x.2 ∈ orbit M y.2

source

theorem AddAction.snd_mem_orbit_of_mem_orbit {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {β : Type u_1} [AddAction M β] {x y : α × β} (h : x ∈ orbit M y) :

x.2 ∈ orbit M y.2

source

theorem Finite.finite_mulAction_orbit {M : Type u} [Monoid M] {α : Type v} [MulAction M α] [Finite M] (a : α) :

(MulAction.orbit M a).Finite

source

theorem Finite.finite_addAction_orbit {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] [Finite M] (a : α) :

(AddAction.orbit M a).Finite

source

theorem MulAction.orbit_eq_univ (M : Type u) [Monoid M] {α : Type v} [MulAction M α] [IsPretransitive M α] (a : α) :

orbit M a = Set.univ

source

theorem AddAction.orbit_eq_univ (M : Type u) [AddMonoid M] {α : Type v} [AddAction M α] [IsPretransitive M α] (a : α) :

orbit M a = Set.univ

source

@[simp]

theorem MulAction.subsingleton_orbit_iff_mem_fixedPoints {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} :

(orbit M a).Subsingleton ↔ a ∈ fixedPoints M α

source

@[simp]

theorem AddAction.subsingleton_orbit_iff_mem_fixedPoints {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} :

(orbit M a).Subsingleton ↔ a ∈ fixedPoints M α

source

theorem MulAction.mem_fixedPoints_iff_card_orbit_eq_one {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} [Fintype ↑(orbit M a)] :

a ∈ fixedPoints M α ↔ Fintype.card ↑(orbit M a) = 1

source

theorem AddAction.mem_fixedPoints_iff_card_orbit_eq_one {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} [Fintype ↑(orbit M a)] :

a ∈ fixedPoints M α ↔ Fintype.card ↑(orbit M a) = 1

source

instance MulAction.instDecidablePredMemSetFixedByOfDecidableEq {M : Type u} [Monoid M] {β : Type u_1} [MulAction M β] (m : M) [DecidableEq β] :

DecidablePred fun (b : β) => b ∈ fixedBy β m

Equations

source

instance AddAction.instDecidablePredMemSetFixedByAddOfDecidableEq {M : Type u} [AddMonoid M] {β : Type u_1} [AddAction M β] (m : M) [DecidableEq β] :

DecidablePred fun (b : β) => b ∈ fixedBy β m

Equations

source

theorem smul_cancel_of_non_zero_divisor {M : Type u_1} {G : Type u_2} [Monoid M] [AddGroup G] [DistribMulAction M G] (k : M) (h : ∀ (x : G), k • x = 0 → x = 0) {a b : G} (h' : k • a = k • b) :

a = b

smul by a k : M over a group is injective, if k is not a zero divisor. The general theory of such k is elaborated by IsSMulRegular. The typeclass that restricts all terms of M to have this property is NoZeroSMulDivisors.

source

theorem MulAction.fixedPoints_of_subsingleton {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [Subsingleton α] :

fixedPoints G α = Set.univ

source

theorem AddAction.fixedPoints_of_subsingleton {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] [Subsingleton α] :

fixedPoints G α = Set.univ

source

theorem MulAction.nontrivial_of_fixedPoints_ne_univ {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (h : fixedPoints G α ≠ Set.univ) :

Nontrivial α

If a group acts nontrivially, then the type is nontrivial

source

theorem AddAction.nontrivial_of_fixedPoints_ne_univ {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (h : fixedPoints G α ≠ Set.univ) :

Nontrivial α

If a subgroup acts nontrivially, then the type is nontrivial.

source

@[simp]

theorem MulAction.smul_orbit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (a : α) :

g • orbit G a = orbit G a

source

@[simp]

theorem AddAction.vadd_orbit {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (g : G) (a : α) :

g +ᵥ orbit G a = orbit G a

source

instance MulAction.instIsPretransitiveElemOrbit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (a : α) :

IsPretransitive G ↑(orbit G a)

The action of a group on an orbit is transitive.

source

instance AddAction.instIsPretransitiveElemOrbit {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (a : α) :

IsPretransitive G ↑(orbit G a)

The action of an additive group on an orbit is transitive.

source

theorem MulAction.orbitRel_subgroup_le {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (H : Subgroup G) :

orbitRel (↥H) α ≤ orbitRel G α

source

theorem AddAction.orbitRel_addSubgroup_le {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (H : AddSubgroup G) :

orbitRel (↥H) α ≤ orbitRel G α

source

theorem MulAction.orbitRel_subgroupOf {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (H K : Subgroup G) :

orbitRel (↥(H.subgroupOf K)) α = orbitRel (↥(H ⊓ K)) α

source

theorem AddAction.orbitRel_addSubgroupOf {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (H K : AddSubgroup G) :

orbitRel (↥(H.addSubgroupOf K)) α = orbitRel (↥(H ⊓ K)) α

source

theorem MulAction.pretransitive_iff_subsingleton_quotient (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] :

IsPretransitive G α ↔ Subsingleton (orbitRel.Quotient G α)

An action is pretransitive if and only if the quotient by MulAction.orbitRel is a subsingleton.

source

theorem AddAction.pretransitive_iff_subsingleton_quotient (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] :

IsPretransitive G α ↔ Subsingleton (orbitRel.Quotient G α)

An additive action is pretransitive if and only if the quotient by AddAction.orbitRel is a subsingleton.

source

theorem MulAction.pretransitive_iff_unique_quotient_of_nonempty (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] [Nonempty α] :

IsPretransitive G α ↔ Nonempty (Unique (orbitRel.Quotient G α))

If α is non-empty, an action is pretransitive if and only if the quotient has exactly one element.

source

theorem AddAction.pretransitive_iff_unique_quotient_of_nonempty (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] [Nonempty α] :

IsPretransitive G α ↔ Nonempty (Unique (orbitRel.Quotient G α))

If α is non-empty, an additive action is pretransitive if and only if the quotient has exactly one element.

source

instance MulAction.instIsPretransitiveElemOrbit_1 {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (x : orbitRel.Quotient G α) :

IsPretransitive G ↑x.orbit

source

instance AddAction.instIsPretransitiveElemOrbit_1 {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (x : orbitRel.Quotient G α) :

IsPretransitive G ↑x.orbit

source

theorem Finite.of_finite_mulAction_orbitRel_quotient (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] [Finite G] [Finite (MulAction.orbitRel.Quotient G α)] :

Finite α

source

theorem Finite.of_finite_addAction_orbitRel_quotient (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] [Finite G] [Finite (AddAction.orbitRel.Quotient G α)] :

Finite α

source

theorem MulAction.orbitRel_le_fst (G : Type u_1) (α : Type u_2) (β : Type u_3) [Group G] [MulAction G α] [MulAction G β] :

orbitRel G (α × β) ≤ Setoid.comap Prod.fst (orbitRel G α)

source

theorem AddAction.orbitRel_le_fst (G : Type u_1) (α : Type u_2) (β : Type u_3) [AddGroup G] [AddAction G α] [AddAction G β] :

orbitRel G (α × β) ≤ Setoid.comap Prod.fst (orbitRel G α)

source

theorem MulAction.orbitRel_le_snd (G : Type u_1) (α : Type u_2) (β : Type u_3) [Group G] [MulAction G α] [MulAction G β] :

orbitRel G (α × β) ≤ Setoid.comap Prod.snd (orbitRel G β)

source

theorem AddAction.orbitRel_le_snd (G : Type u_1) (α : Type u_2) (β : Type u_3) [AddGroup G] [AddAction G α] [AddAction G β] :

orbitRel G (α × β) ≤ Setoid.comap Prod.snd (orbitRel G β)

source

theorem MulAction.stabilizer_smul_eq_stabilizer_map_conj {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (a : α) :

stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)

If the stabilizer of a is S, then the stabilizer of g • a is gSg⁻¹.

source

def MulAction.stabilizerEquivStabilizer {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {g : G} {a b : α} (hg : b = g • a) :

↥(stabilizer G a) ≃* ↥(stabilizer G b)

The natural group equivalence between the stabilizers of two elements in the same orbit.

Equations

Instances For

source

theorem MulAction.stabilizerEquivStabilizer_apply {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {g : G} {a b : α} (hg : b = g • a) (x : ↥(stabilizer G a)) :

↑((stabilizerEquivStabilizer hg) x) = (MulAut.conj g) ↑x

source

theorem MulAction.stabilizerEquivStabilizer_symm_apply {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {g : G} {a b : α} (hg : b = g • a) (x : ↥(stabilizer G b)) :

↑((stabilizerEquivStabilizer hg).symm x) = (MulAut.conj g⁻¹) ↑x

source

theorem MulAction.stabilizerEquivStabilizer_trans {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {g h k : G} {a b c : α} (hg : b = g • a) (hh : c = h • b) (hk : c = k • a) (H : k = h * g) :

(stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) = stabilizerEquivStabilizer hk

source

theorem MulAction.stabilizerEquivStabilizer_one {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} :

stabilizerEquivStabilizer ⋯ = MulEquiv.refl ↥(stabilizer G a)

source

theorem MulAction.stabilizerEquivStabilizer_symm {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {g : G} {a b : α} (hg : b = g • a) :

(stabilizerEquivStabilizer hg).symm = stabilizerEquivStabilizer ⋯

source

theorem MulAction.stabilizerEquivStabilizer_inv {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {g : G} {a b : α} (hg : b = g⁻¹ • a) :

stabilizerEquivStabilizer hg = (stabilizerEquivStabilizer ⋯).symm

source

noncomputable def MulAction.stabilizerEquivStabilizerOfOrbitRel {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a b : α} (h : (orbitRel G α) a b) :

↥(stabilizer G a) ≃* ↥(stabilizer G b)

A bijection between the stabilizers of two elements in the same orbit.

Equations

Instances For

source

theorem AddAction.stabilizer_vadd_eq_stabilizer_map_conj {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (g : G) (a : α) :

stabilizer G (g +ᵥ a) = AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) (stabilizer G a)

If the stabilizer of x is S, then the stabilizer of g +ᵥ x is g + S + (-g).

source

def AddAction.stabilizerEquivStabilizer {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a) :

↥(stabilizer G a) ≃+ ↥(stabilizer G b)

The natural group equivalence between the stabilizers of two elements in the same orbit.

Equations

Instances For

source

theorem AddAction.stabilizerEquivStabilizer_apply {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a) (x : ↥(stabilizer G a)) :

↑((stabilizerEquivStabilizer hg) x) = (Additive.toMul (AddAut.conj g)) ↑x

source

theorem AddAction.stabilizerEquivStabilizer_symm_apply {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {g : G} {b : α} (hg : b = g +ᵥ b) (x : ↥(stabilizer G b)) :

↑((stabilizerEquivStabilizer hg).symm x) = (Additive.toMul (AddAut.conj (-g))) ↑x

source

theorem AddAction.stabilizerEquivStabilizer_trans {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {g h k : G} {a b c : α} (hg : b = g +ᵥ a) (hh : c = h +ᵥ b) (hk : c = k +ᵥ a) (H : k = h + g) :

(stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) = stabilizerEquivStabilizer hk

source

theorem AddAction.stabilizerEquivStabilizer_zero {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} :

stabilizerEquivStabilizer ⋯ = AddEquiv.refl ↥(stabilizer G a)

source

theorem AddAction.stabilizerEquivStabilizer_symm {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a) :

(stabilizerEquivStabilizer hg).symm = stabilizerEquivStabilizer ⋯

source

theorem AddAction.stabilizerEquivStabilizer_neg {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {g : G} {a b : α} (hg : b = -g +ᵥ a) :

stabilizerEquivStabilizer hg = (stabilizerEquivStabilizer ⋯).symm

source

noncomputable def AddAction.stabilizerEquivStabilizerOfOrbitRel {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a b : α} (h : (orbitRel G α) a b) :

↥(stabilizer G a) ≃+ ↥(stabilizer G b)

A bijection between the stabilizers of two elements in the same orbit.

Equations

Instances For

source

theorem Equiv.swap_mem_stabilizer {α : Type u_1} [DecidableEq α] {S : Set α} {a b : α} :

swap a b ∈ MulAction.stabilizer (Perm α) S ↔ (a ∈ S ↔ b ∈ S)

source

theorem MulAction.le_stabilizer_iff_smul_le {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] (s : Set α) (H : Subgroup G) :

H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s

To prove inclusion of a subgroup in a stabilizer, it is enough to prove inclusions.

source

theorem AddAction.le_stabilizer_iff_vadd_le {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] (s : Set α) (H : AddSubgroup G) :

H ≤ stabilizer G s ↔ ∀ g ∈ H, g +ᵥ s ⊆ s

To prove inclusion of a subgroup in a stabilizer, it is enough to prove inclusions.

source

theorem Module.stabilizer_units_eq_bot_of_ne_zero (R : Type u_1) {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : M} (hx : x ≠ 0) :

MulAction.stabilizer Rˣ x = ⊥

Documentation

Mathlib.GroupTheory.GroupAction.Basic

Basic properties of group actions #

Main definitions #