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 #
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 α]
[IsPretransitive M α]
(a : α)
:
theorem
AddAction.orbit_eq_univ
(M : Type u)
[AddMonoid M]
{α : Type v}
[AddAction M α]
[IsPretransitive M α]
(a : α)
:
@[simp]
theorem
MulAction.subsingleton_orbit_iff_mem_fixedPoints
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
{a : α}
:
@[simp]
theorem
AddAction.subsingleton_orbit_iff_mem_fixedPoints
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
{a : α}
:
instance
MulAction.instDecidablePredMemSetFixedByOfDecidableEq
{M : Type u}
[Monoid M]
{β : Type u_1}
[MulAction M β]
(m : M)
[DecidableEq β]
:
DecidablePred fun (b : β) => b ∈ fixedBy β m
Equations
instance
AddAction.instDecidablePredMemSetFixedByAddOfDecidableEq
{M : Type u}
[AddMonoid M]
{β : Type u_1}
[AddAction M β]
(m : M)
[DecidableEq β]
:
DecidablePred fun (b : β) => b ∈ fixedBy β m
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)
:
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.
theorem
MulAction.fixedPoints_of_subsingleton
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
[Subsingleton α]
:
theorem
AddAction.fixedPoints_of_subsingleton
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
[Subsingleton α]
:
theorem
MulAction.nontrivial_of_fixedPoints_ne_univ
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(h : fixedPoints G α ≠ Set.univ)
:
If a group acts nontrivially, then the type is nontrivial
theorem
AddAction.nontrivial_of_fixedPoints_ne_univ
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(h : fixedPoints G α ≠ Set.univ)
:
If a subgroup acts nontrivially, then the type is nontrivial.
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.
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.
theorem
AddAction.orbitRel_addSubgroup_le
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(H : AddSubgroup G)
:
theorem
AddAction.orbitRel_addSubgroupOf
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(H K : AddSubgroup G)
:
theorem
MulAction.pretransitive_iff_subsingleton_quotient
(G : Type u_1)
(α : Type u_2)
[Group G]
[MulAction 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 α]
:
An additive action is pretransitive if and only if the quotient by
AddAction.orbitRel is a subsingleton.
instance
MulAction.instIsPretransitiveElemOrbit_1
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(x : orbitRel.Quotient G α)
:
IsPretransitive G ↑x.orbit
instance
AddAction.instIsPretransitiveElemOrbit_1
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(x : orbitRel.Quotient G α)
:
IsPretransitive G ↑x.orbit
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.stabilizer_smul_eq_stabilizer_map_conj
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(g : G)
(a : α)
:
If the stabilizer of a is S, then the stabilizer of g • a is gSg⁻¹.
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))
:
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))
:
theorem
MulAction.stabilizerEquivStabilizer_one
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{a : α}
:
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).
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))
:
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))
:
theorem
AddAction.stabilizerEquivStabilizer_zero
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{a : α}
:
theorem
AddAction.le_stabilizer_iff_vadd_le
{G : Type u_1}
[AddGroup G]
{α : Type u_2}
[AddAction G α]
(s : Set α)
(H : AddSubgroup G)
:
To prove inclusion of a subgroup in a stabilizer, it is enough to prove inclusions.
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)
: