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
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.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.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
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
Finite.finite_addAction_orbit
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
[Finite M]
(a : α)
:
(AddAction.orbit M a).Finite
theorem
Finite.finite_mulAction_orbit
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
[Finite M]
(a : α)
:
(MulAction.orbit M a).Finite
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.orbit_eq_univ
(M : Type u)
[Monoid M]
{α : Type v}
[MulAction M α]
[MulAction.IsPretransitive M α]
(a : α)
:
MulAction.orbit M a = Set.univ
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
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
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 : R}
{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
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
@[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
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
- ⋯ = ⋯
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
- ⋯ = ⋯
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_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_addSubgroupOf
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(H : AddSubgroup G)
(K : AddSubgroup G)
:
AddAction.orbitRel (↥(H.addSubgroupOf K)) α = AddAction.orbitRel (↥(H ⊓ K)) α
theorem
MulAction.orbitRel_subgroupOf
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(H : Subgroup G)
(K : Subgroup G)
:
MulAction.orbitRel (↥(H.subgroupOf K)) α = MulAction.orbitRel (↥(H ⊓ K)) α
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.
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.
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
- ⋯ = ⋯
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
- ⋯ = ⋯
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
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
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_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_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.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
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
Instances For
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
Instances For
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)