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

• MulAction.orbit
• MulAction.fixedPoints
• MulAction.fixedBy
• MulAction.stabilizer

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 ∈ MulAction.orbit M y) : x.1 ∈ MulAction.orbit M y.1

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 ∈ AddAction.orbit M y) : x.1 ∈ AddAction.orbit M y.1

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 ∈ MulAction.orbit M y) : x.2 ∈ MulAction.orbit M y.2

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 ∈ AddAction.orbit M y) : x.2 ∈ AddAction.orbit M y.2

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

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

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

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

theorem MulAction.mem_fixedPoints_iff_card_orbit_eq_one {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} [Fintype ↑(MulAction.orbit M a)] : a ∈ MulAction.fixedPoints M α ↔ Fintype.card ↑(MulAction.orbit M a) = 1

theorem AddAction.mem_fixedPoints_iff_card_orbit_eq_one {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} [Fintype ↑(AddAction.orbit M a)] : a ∈ AddAction.fixedPoints M α ↔ Fintype.card ↑(AddAction.orbit M a) = 1

instance MulAction.instDecidablePredMemSetFixedByOfDecidableEq {M : Type u} [Monoid M] {β : Type u_1} [MulAction M β] (m : M) [DecidableEq β] : DecidablePred fun (b : β) => b ∈ MulAction.fixedBy β m

Equations

• MulAction.instDecidablePredMemSetFixedByOfDecidableEq m b = ⋯.mpr inferInstance

instance AddAction.instDecidablePredMemSetFixedByAddOfDecidableEq {M : Type u} [AddMonoid M] {β : Type u_1} [AddAction M β] (m : M) [DecidableEq β] : DecidablePred fun (b : β) => b ∈ AddAction.fixedBy β m

Equations

• AddAction.instDecidablePredMemSetFixedByAddOfDecidableEq m b = ⋯.mpr inferInstance

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

smul by a k : M over a ring 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.

@[simp]

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

@[simp]

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

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

The action of a group on an orbit is transitive.

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

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

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

theorem MulAction.pretransitive_iff_subsingleton_quotient (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] : MulAction.IsPretransitive G α ↔ Subsingleton (MulAction.orbitRel.Quotient G α)

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

theorem AddAction.pretransitive_iff_subsingleton_quotient (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] : AddAction.IsPretransitive G α ↔ Subsingleton (AddAction.orbitRel.Quotient G α)

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

theorem MulAction.pretransitive_iff_unique_quotient_of_nonempty (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] [Nonempty α] : MulAction.IsPretransitive G α ↔ Nonempty (Unique (MulAction.orbitRel.Quotient G α))

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

theorem AddAction.pretransitive_iff_unique_quotient_of_nonempty (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] [Nonempty α] : AddAction.IsPretransitive G α ↔ Nonempty (Unique (AddAction.orbitRel.Quotient G α))

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 α

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 α

theorem MulAction.orbitRel_le_fst (G : Type u_1) (α : Type u_2) (β : Type u_3) [Group G] [MulAction G α] [MulAction G β] : MulAction.orbitRel G (α × β) ≤ Setoid.comap Prod.fst (MulAction.orbitRel G α)

theorem AddAction.orbitRel_le_fst (G : Type u_1) (α : Type u_2) (β : Type u_3) [AddGroup G] [AddAction G α] [AddAction G β] : AddAction.orbitRel G (α × β) ≤ Setoid.comap Prod.fst (AddAction.orbitRel G α)

theorem MulAction.orbitRel_le_snd (G : Type u_1) (α : Type u_2) (β : Type u_3) [Group G] [MulAction G α] [MulAction G β] : MulAction.orbitRel G (α × β) ≤ Setoid.comap Prod.snd (MulAction.orbitRel G β)

theorem AddAction.orbitRel_le_snd (G : Type u_1) (α : Type u_2) (β : Type u_3) [AddGroup G] [AddAction G α] [AddAction G β] : AddAction.orbitRel G (α × β) ≤ Setoid.comap Prod.snd (AddAction.orbitRel G β)

theorem MulAction.stabilizer_smul_eq_stabilizer_map_conj {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (a : α) : MulAction.stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (MulAction.stabilizer G a)

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

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

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

Equations

• MulAction.stabilizerEquivStabilizerOfOrbitRel h = (MulEquiv.subgroupCongr ⋯).trans (MulEquiv.subgroupMap (MulAut.conj (Classical.choose h)) (MulAction.stabilizer G b)).symm

theorem AddAction.stabilizer_vadd_eq_stabilizer_map_conj {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (g : G) (a : α) : AddAction.stabilizer G (g +ᵥ a) = AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.conj g)) (AddAction.stabilizer G a)

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

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

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

Equations

• AddAction.stabilizerEquivStabilizerOfOrbitRel h = (AddEquiv.addSubgroupCongr ⋯).trans (AddEquiv.addSubgroupMap (AddAut.conj (Classical.choose h)) (AddAction.stabilizer G b)).symm

theorem Equiv.swap_mem_stabilizer {α : Type u_1} [DecidableEq α] {S : Set α} {a b : α} : Equiv.swap a b ∈ MulAction.stabilizer (Equiv.Perm α) S ↔ (a ∈ S ↔ b ∈ S)

theorem MulAction.le_stabilizer_iff_smul_le {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] (s : Set α) (H : Subgroup G) : H ≤ MulAction.stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s

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

theorem MulAction.mem_stabilizer_of_finite_iff_smul_le {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] (s : Set α) (hs : s.Finite) (g : G) : g ∈ MulAction.stabilizer G s ↔ g • s ⊆ s

To prove membership to stabilizer of a finite set, it is enough to prove one inclusion.

theorem MulAction.mem_stabilizer_of_finite_iff_le_smul {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] (s : Set α) (hs : s.Finite) (g : G) : g ∈ MulAction.stabilizer G s ↔ s ⊆ g • s

To prove membership to stabilizer of a finite set, it is enough to prove one inclusion.