Documentation

Mathlib.GroupTheory.GroupAction.Basic

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 #

def AddAction.orbit (α : Type u) {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] (b : β) :
Set β

The orbit of an element under an action.

Equations
def MulAction.orbit (α : Type u) {β : Type v} [inst : Monoid α] [inst : MulAction α β] (b : β) :
Set β

The orbit of an element under an action.

Equations
theorem AddAction.mem_orbit_iff {α : Type u} {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] {b₁ : β} {b₂ : β} :
b₂ AddAction.orbit α b₁ x, x +ᵥ b₁ = b₂
theorem MulAction.mem_orbit_iff {α : Type u} {β : Type v} [inst : Monoid α] [inst : MulAction α β] {b₁ : β} {b₂ : β} :
b₂ MulAction.orbit α b₁ x, x b₁ = b₂
@[simp]
theorem AddAction.mem_orbit {α : Type u} {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] (b : β) (x : α) :
@[simp]
theorem MulAction.mem_orbit {α : Type u} {β : Type v} [inst : Monoid α] [inst : MulAction α β] (b : β) (x : α) :
@[simp]
theorem AddAction.mem_orbit_self {α : Type u} {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] (b : β) :
@[simp]
theorem MulAction.mem_orbit_self {α : Type u} {β : Type v} [inst : Monoid α] [inst : MulAction α β] (b : β) :
theorem AddAction.orbit_nonempty {α : Type u} {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] (b : β) :
theorem MulAction.orbit_nonempty {α : Type u} {β : Type v} [inst : Monoid α] [inst : MulAction α β] (b : β) :
theorem AddAction.mapsTo_vadd_orbit {α : Type u} {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] (a : α) (b : β) :
Set.MapsTo ((fun x x_1 => x +ᵥ x_1) a) (AddAction.orbit α b) (AddAction.orbit α b)
theorem MulAction.mapsTo_smul_orbit {α : Type u} {β : Type v} [inst : Monoid α] [inst : MulAction α β] (a : α) (b : β) :
Set.MapsTo ((fun x x_1 => x x_1) a) (MulAction.orbit α b) (MulAction.orbit α b)
theorem AddAction.vadd_orbit_subset {α : Type u} {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] (a : α) (b : β) :
theorem MulAction.smul_orbit_subset {α : Type u} {β : Type v} [inst : Monoid α] [inst : MulAction α β] (a : α) (b : β) :
theorem AddAction.orbit_vadd_subset {α : Type u} {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] (a : α) (b : β) :
theorem MulAction.orbit_smul_subset {α : Type u} {β : Type v} [inst : Monoid α] [inst : MulAction α β] (a : α) (b : β) :
def AddAction.instAddActionElemOrbit.proof_2 {α : Type u_2} {β : Type u_1} [inst : AddMonoid α] [inst : AddAction α β] {b : β} (a : α) (a' : α) (b' : ↑(AddAction.orbit α b)) :
a + a' +ᵥ b' = a +ᵥ (a' +ᵥ b')
Equations
instance AddAction.instAddActionElemOrbit {α : Type u} {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] {b : β} :
Equations
def AddAction.instAddActionElemOrbit.proof_1 {α : Type u_2} {β : Type u_1} [inst : AddMonoid α] [inst : AddAction α β] {b : β} (a : ↑(AddAction.orbit α b)) :
0 +ᵥ a = a
Equations
instance MulAction.instMulActionElemOrbit {α : Type u} {β : Type v} [inst : Monoid α] [inst : MulAction α β] {b : β} :
Equations
@[simp]
theorem AddAction.orbit.coe_vadd {α : Type u} {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] {b : β} {a : α} {b' : ↑(AddAction.orbit α b)} :
↑(a +ᵥ b') = a +ᵥ b'
@[simp]
theorem MulAction.orbit.coe_smul {α : Type u} {β : Type v} [inst : Monoid α] [inst : MulAction α β] {b : β} {a : α} {b' : ↑(MulAction.orbit α b)} :
↑(a b') = a b'
def AddAction.fixedPoints (α : Type u) (β : Type v) [inst : AddMonoid α] [inst : AddAction α β] :
Set β

The set of elements fixed under the whole action.

Equations
def MulAction.fixedPoints (α : Type u) (β : Type v) [inst : Monoid α] [inst : MulAction α β] :
Set β

The set of elements fixed under the whole action.

Equations
def AddAction.fixedBy (α : Type u) (β : Type v) [inst : AddMonoid α] [inst : AddAction α β] (g : α) :
Set β

fixedBy g is the subfield of elements fixed by g.

Equations
def MulAction.fixedBy (α : Type u) (β : Type v) [inst : Monoid α] [inst : MulAction α β] (g : α) :
Set β

fixedBy g is the subfield of elements fixed by g.

Equations
theorem AddAction.fixed_eq_interᵢ_fixedBy (α : Type u) (β : Type v) [inst : AddMonoid α] [inst : AddAction α β] :
theorem MulAction.fixed_eq_interᵢ_fixedBy (α : Type u) (β : Type v) [inst : Monoid α] [inst : MulAction α β] :
@[simp]
theorem AddAction.mem_fixedPoints {α : Type u} (β : Type v) [inst : AddMonoid α] [inst : AddAction α β] {b : β} :
b AddAction.fixedPoints α β ∀ (x : α), x +ᵥ b = b
@[simp]
theorem MulAction.mem_fixedPoints {α : Type u} (β : Type v) [inst : Monoid α] [inst : MulAction α β] {b : β} :
b MulAction.fixedPoints α β ∀ (x : α), x b = b
@[simp]
theorem AddAction.mem_fixedBy {α : Type u} (β : Type v) [inst : AddMonoid α] [inst : AddAction α β] {g : α} {b : β} :
b AddAction.fixedBy α β g g +ᵥ b = b
@[simp]
theorem MulAction.mem_fixedBy {α : Type u} (β : Type v) [inst : Monoid α] [inst : MulAction α β] {g : α} {b : β} :
b MulAction.fixedBy α β g g b = b
theorem AddAction.mem_fixedPoints' {α : Type u} (β : Type v) [inst : AddMonoid α] [inst : AddAction α β] {b : β} :
b AddAction.fixedPoints α β ∀ (b' : β), b' AddAction.orbit α bb' = b
abbrev AddAction.mem_fixedPoints'.match_1 {α : Type u_1} (β : Type u_2) [inst : AddMonoid α] [inst : AddAction α β] {b : β} :
(x : β) → (motive : (x_1, x_1 +ᵥ b = x) → Prop) → ∀ (x_1 : x_1, x_1 +ᵥ b = x), (∀ (x_2 : α) (hx : x_2 +ᵥ b = x), motive (_ : x_3, x_3 +ᵥ b = x)) → motive x_1
Equations
theorem MulAction.mem_fixedPoints' {α : Type u} (β : Type v) [inst : Monoid α] [inst : MulAction α β] {b : β} :
b MulAction.fixedPoints α β ∀ (b' : β), b' MulAction.orbit α bb' = b
def AddAction.Stabilizer.addSubmonoid (α : Type u) {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] (b : β) :

The stabilizer of a point b as an additive submonoid of α.

Equations
  • One or more equations did not get rendered due to their size.
def AddAction.Stabilizer.addSubmonoid.proof_1 (α : Type u_2) {β : Type u_1} [inst : AddMonoid α] [inst : AddAction α β] (b : β) {a : α} {a' : α} (ha : a +ᵥ b = b) (hb : a' +ᵥ b = b) :
a + a' +ᵥ b = b
Equations
def MulAction.Stabilizer.submonoid (α : Type u) {β : Type v} [inst : Monoid α] [inst : MulAction α β] (b : β) :

The stabilizer of a point b as a submonoid of α.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddAction.mem_stabilizer_addSubmonoid_iff (α : Type u) {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] {b : β} {a : α} :
@[simp]
theorem MulAction.mem_stabilizer_submonoid_iff (α : Type u) {β : Type v} [inst : Monoid α] [inst : MulAction α β] {b : β} {a : α} :
theorem AddAction.orbit_eq_univ (α : Type u) {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] [inst : AddAction.IsPretransitive α β] (x : β) :
AddAction.orbit α x = Set.univ
theorem MulAction.orbit_eq_univ (α : Type u) {β : Type v} [inst : Monoid α] [inst : MulAction α β] [inst : MulAction.IsPretransitive α β] (x : β) :
MulAction.orbit α x = Set.univ
abbrev AddAction.mem_fixedPoints_iff_card_orbit_eq_zero.match_1 {α : Type u_2} {β : Type u_1} [inst : AddMonoid α] [inst : AddAction α β] {a : β} (motive : ↑(AddAction.orbit α a)Prop) :
(x : ↑(AddAction.orbit α a)) → ((b : β) → (x : α) → (hx : (fun x => x +ᵥ a) x = b) → motive { val := b, property := (_ : y, (fun x => x +ᵥ a) y = b) }) → motive x
Equations
theorem AddAction.mem_fixedPoints_iff_card_orbit_eq_zero {α : Type u} {β : Type v} [inst : AddMonoid α] [inst : AddAction α β] {a : β} [inst : Fintype ↑(AddAction.orbit α a)] :
theorem MulAction.mem_fixedPoints_iff_card_orbit_eq_one {α : Type u} {β : Type v} [inst : Monoid α] [inst : MulAction α β] {a : β} [inst : Fintype ↑(MulAction.orbit α a)] :
def AddAction.stabilizer.proof_1 (α : Type u_1) {β : Type u_2} [inst : AddGroup α] [inst : AddAction α β] (b : β) :
0 (AddAction.Stabilizer.addSubmonoid α b).toAddSubsemigroup.carrier
Equations
def AddAction.stabilizer.proof_2 (α : Type u_2) {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] (b : β) {a : α} (ha : a +ᵥ b = b) :
-a +ᵥ b = b
Equations
def AddAction.stabilizer (α : Type u) {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (b : β) :

The stabilizer of an element under an action, i.e. what sends the element to itself. An additive subgroup.

Equations
  • One or more equations did not get rendered due to their size.
def MulAction.stabilizer (α : Type u) {β : Type v} [inst : Group α] [inst : MulAction α β] (b : β) :

The stabilizer of an element under an action, i.e. what sends the element to itself. A subgroup.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddAction.mem_stabilizer_iff {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] {b : β} {a : α} :
@[simp]
theorem MulAction.mem_stabilizer_iff {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] {b : β} {a : α} :
@[simp]
theorem AddAction.vadd_orbit {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (a : α) (b : β) :
@[simp]
theorem MulAction.smul_orbit {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (a : α) (b : β) :
@[simp]
theorem AddAction.orbit_vadd {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (a : α) (b : β) :
@[simp]
theorem MulAction.orbit_smul {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (a : α) (b : β) :

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

Equations
  • One or more equations did not get rendered due to their size.
abbrev AddAction.orbit_eq_iff.match_1 {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {a : β} {b : β} (motive : a AddAction.orbit α bProp) :
(x : a AddAction.orbit α b) → ((w : α) → (hc : (fun x => x +ᵥ b) w = a) → motive (_ : y, (fun x => x +ᵥ b) y = a)) → motive x
Equations
theorem AddAction.orbit_eq_iff {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] {a : β} {b : β} :
theorem MulAction.orbit_eq_iff {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] {a : β} {b : β} :
theorem AddAction.mem_orbit_vadd (α : Type u) {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) (a : β) :
theorem MulAction.mem_orbit_smul (α : Type u) {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) (a : β) :
theorem AddAction.vadd_mem_orbit_vadd (α : Type u) {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) (h : α) (a : β) :
theorem MulAction.smul_mem_orbit_smul (α : Type u) {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) (h : α) (a : β) :
g a MulAction.orbit α (h a)
def AddAction.orbitRel.proof_1 (α : Type u_2) (β : Type u_1) [inst : AddGroup α] [inst : AddAction α β] :
Equivalence fun a b => a AddAction.orbit α b
Equations
def AddAction.orbitRel (α : Type u) (β : Type v) [inst : AddGroup α] [inst : AddAction α β] :

The relation 'in the same orbit'.

Equations
def MulAction.orbitRel (α : Type u) (β : Type v) [inst : Group α] [inst : MulAction α β] :

The relation 'in the same orbit'.

Equations
theorem AddAction.quotient_preimage_image_eq_union_add {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (U : Set β) :
Quotient.mk' ⁻¹' (Quotient.mk' '' U) = Set.unionᵢ fun a => (fun x x_1 => x +ᵥ x_1) a '' U

When you take a set U in β, push it down to the quotient, and pull back, you get the union of the orbit of U under α.

theorem MulAction.quotient_preimage_image_eq_union_mul {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (U : Set β) :
Quotient.mk' ⁻¹' (Quotient.mk' '' U) = Set.unionᵢ fun a => (fun x x_1 => x x_1) a '' U

When you take a set U in β, push it down to the quotient, and pull back, you get the union of the orbit of U under α.

theorem AddAction.disjoint_image_image_iff {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] {U : Set β} {V : Set β} :
Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ∀ (x : β), x U∀ (a : α), ¬a +ᵥ x V
theorem MulAction.disjoint_image_image_iff {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] {U : Set β} {V : Set β} :
Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ∀ (x : β), x U∀ (a : α), ¬a x V
theorem AddAction.image_inter_image_iff {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (U : Set β) (V : Set β) :
Quotient.mk' '' U Quotient.mk' '' V = ∀ (x : β), x U∀ (a : α), ¬a +ᵥ x V
theorem MulAction.image_inter_image_iff {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (U : Set β) (V : Set β) :
Quotient.mk' '' U Quotient.mk' '' V = ∀ (x : β), x U∀ (a : α), ¬a x V
def AddAction.orbitRel.Quotient (α : Type u) (β : Type v) [inst : AddGroup α] [inst : AddAction α β] :

The quotient by AddAction.orbitRel, given a name to enable dot notation.

Equations
def MulAction.orbitRel.Quotient (α : Type u) (β : Type v) [inst : Group α] [inst : MulAction α β] :

The quotient by MulAction.orbitRel, given a name to enable dot notation.

Equations
def AddAction.orbitRel.Quotient.orbit {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (x : AddAction.orbitRel.Quotient α β) :
Set β

The orbit corresponding to an element of the quotient by add_action.orbit_rel

Equations
def AddAction.orbitRel.Quotient.orbit.proof_1 {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] :
∀ (x x_1 : β), x AddAction.orbit α x_1AddAction.orbit α x = AddAction.orbit α x_1
Equations
def MulAction.orbitRel.Quotient.orbit {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (x : MulAction.orbitRel.Quotient α β) :
Set β

The orbit corresponding to an element of the quotient by MulAction.orbitRel

Equations
@[simp]
@[simp]
theorem MulAction.orbitRel.Quotient.orbit_mk {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (b : β) :
theorem AddAction.orbitRel.Quotient.orbit_eq_orbit_out {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (x : AddAction.orbitRel.Quotient α β) {φ : AddAction.orbitRel.Quotient α ββ} (hφ : Function.RightInverse φ Quotient.mk') :

Note that hφ = quotient.out_eq' is a useful choice here.

theorem MulAction.orbitRel.Quotient.orbit_eq_orbit_out {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (x : MulAction.orbitRel.Quotient α β) {φ : MulAction.orbitRel.Quotient α ββ} (hφ : Function.RightInverse φ Quotient.mk') :

Note that hφ = Quotient.out_eq' is a useful choice here.

def AddAction.selfEquivSigmaOrbits' (α : Type u) (β : Type v) [inst : AddGroup α] [inst : AddAction α β] :

Decomposition of a type X as a disjoint union of its orbits under an additive group action.

This version is expressed in terms of AddAction.orbitRel.Quotient.orbit instead of AddAction.orbit, to avoid mentioning Quotient.out'.

Equations
  • One or more equations did not get rendered due to their size.
def MulAction.selfEquivSigmaOrbits' (α : Type u) (β : Type v) [inst : Group α] [inst : MulAction α β] :

Decomposition of a type X as a disjoint union of its orbits under a group action.

This version is expressed in terms of MulAction.orbitRel.Quotient.orbit instead of MulAction.orbit, to avoid mentioning Quotient.out'.

Equations
  • One or more equations did not get rendered due to their size.
def AddAction.selfEquivSigmaOrbits (α : Type u) (β : Type v) [inst : AddGroup α] [inst : AddAction α β] :

Decomposition of a type X as a disjoint union of its orbits under an additive group action.

Equations
  • One or more equations did not get rendered due to their size.
def MulAction.selfEquivSigmaOrbits (α : Type u) (β : Type v) [inst : Group α] [inst : MulAction α β] :

Decomposition of a type X as a disjoint union of its orbits under a group action.

Equations
  • One or more equations did not get rendered due to their size.
theorem MulAction.stabilizer_smul_eq_stabilizer_map_conj {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] (g : α) (x : β) :

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

noncomputable def MulAction.stabilizerEquivStabilizerOfOrbitRel {α : Type u} {β : Type v} [inst : Group α] [inst : MulAction α β] {x : β} {y : β} (h : Setoid.Rel (MulAction.orbitRel α β) x y) :
{ x // x MulAction.stabilizer α x } ≃* { x // x MulAction.stabilizer α y }

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

Equations
  • One or more equations did not get rendered due to their size.
theorem AddAction.stabilizer_vadd_eq_stabilizer_map_conj {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] (g : α) (x : β) :

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

noncomputable def AddAction.stabilizerEquivStabilizerOfOrbitRel {α : Type u} {β : Type v} [inst : AddGroup α] [inst : AddAction α β] {x : β} {y : β} (h : Setoid.Rel (AddAction.orbitRel α β) x y) :
{ x // x AddAction.stabilizer α x } ≃+ { x // x AddAction.stabilizer α y }

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

Equations
  • One or more equations did not get rendered due to their size.
theorem smul_cancel_of_non_zero_divisor {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst : NonUnitalNonAssocRing R] [inst : DistribMulAction M R] (k : M) (h : ∀ (x : R), k x = 0x = 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.