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

def AddAction.orbit (M : Type u) [AddMonoid M] {α : Type v} [AddAction M α] (a : α) : Set α

The orbit of an element under an action.

Equations

• AddAction.orbit M a = Set.range fun (m : M) => m +ᵥ a

def MulAction.orbit (M : Type u) [Monoid M] {α : Type v} [MulAction M α] (a : α) : Set α

The orbit of an element under an action.

Equations

• MulAction.orbit M a = Set.range fun (m : M) => m • a

theorem AddAction.mem_orbit_iff {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a₁ : α} {a₂ : α} : a₂ ∈ AddAction.orbit M a₁ ↔ ∃ (x : M), x +ᵥ a₁ = a₂

theorem MulAction.mem_orbit_iff {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a₁ : α} {a₂ : α} : a₂ ∈ MulAction.orbit M a₁ ↔ ∃ (x : M), x • a₁ = a₂

@[simp]

theorem AddAction.mem_orbit {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] (a : α) (m : M) : m +ᵥ a ∈ AddAction.orbit M a

@[simp]

theorem MulAction.mem_orbit {M : Type u} [Monoid M] {α : Type v} [MulAction M α] (a : α) (m : M) : m • a ∈ MulAction.orbit M a

@[simp]

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

@[simp]

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

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

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

theorem AddAction.mapsTo_vadd_orbit {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] (m : M) (a : α) : Set.MapsTo (fun (x : α) => m +ᵥ x) (AddAction.orbit M a) (AddAction.orbit M a)

theorem MulAction.mapsTo_smul_orbit {M : Type u} [Monoid M] {α : Type v} [MulAction M α] (m : M) (a : α) : Set.MapsTo (fun (x : α) => m • x) (MulAction.orbit M a) (MulAction.orbit M a)

theorem AddAction.vadd_orbit_subset {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] (m : M) (a : α) : m +ᵥ AddAction.orbit M a ⊆ AddAction.orbit M a

theorem MulAction.smul_orbit_subset {M : Type u} [Monoid M] {α : Type v} [MulAction M α] (m : M) (a : α) : m • MulAction.orbit M a ⊆ MulAction.orbit M a

theorem AddAction.orbit_vadd_subset {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] (m : M) (a : α) : AddAction.orbit M (m +ᵥ a) ⊆ AddAction.orbit M a

theorem MulAction.orbit_smul_subset {M : Type u} [Monoid M] {α : Type v} [MulAction M α] (m : M) (a : α) : MulAction.orbit M (m • a) ⊆ MulAction.orbit M a

theorem AddAction.instElemOrbit.proof_2 {M : Type u_2} [AddMonoid M] {α : Type u_1} [AddAction M α] {a : α} (m : M) (m' : M) (a' : ↑(AddAction.orbit M a)) : m + m' +ᵥ a' = m +ᵥ (m' +ᵥ a')

theorem AddAction.instElemOrbit.proof_1 {M : Type u_2} [AddMonoid M] {α : Type u_1} [AddAction M α] {a : α} (m : ↑(AddAction.orbit M a)) : 0 +ᵥ m = m

instance AddAction.instElemOrbit {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} : AddAction M ↑(AddAction.orbit M a)

Equations

• AddAction.instElemOrbit = AddAction.mk ⋯ ⋯

instance MulAction.instElemOrbit {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} : MulAction M ↑(MulAction.orbit M a)

Equations

• MulAction.instElemOrbit = MulAction.mk ⋯ ⋯

@[simp]

theorem AddAction.orbit.coe_vadd {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} {m : M} {a' : ↑(AddAction.orbit M a)} : ↑(m +ᵥ a') = m +ᵥ ↑a'

@[simp]

theorem MulAction.orbit.coe_smul {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} {m : M} {a' : ↑(MulAction.orbit M a)} : ↑(m • a') = m • ↑a'

theorem AddAction.orbit_addSubmonoid_subset {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] (S : AddSubmonoid M) (a : α) : AddAction.orbit { x : M // x ∈ S } a ⊆ AddAction.orbit M a

theorem MulAction.orbit_submonoid_subset {M : Type u} [Monoid M] {α : Type v} [MulAction M α] (S : Submonoid M) (a : α) : MulAction.orbit { x : M // x ∈ S } a ⊆ MulAction.orbit M a

theorem AddAction.mem_orbit_of_mem_orbit_addSubmonoid {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {S : AddSubmonoid M} {a : α} {b : α} (h : a ∈ AddAction.orbit { x : M // x ∈ S } b) : a ∈ AddAction.orbit M b

theorem MulAction.mem_orbit_of_mem_orbit_submonoid {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {S : Submonoid M} {a : α} {b : α} (h : a ∈ MulAction.orbit { x : M // x ∈ S } b) : a ∈ MulAction.orbit M b

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 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

def AddAction.fixedPoints (M : Type u) [AddMonoid M] (α : Type v) [AddAction M α] : Set α

The set of elements fixed under the whole action.

Equations

• AddAction.fixedPoints M α = {a : α | ∀ (m : M), m +ᵥ a = a}

def MulAction.fixedPoints (M : Type u) [Monoid M] (α : Type v) [MulAction M α] : Set α

The set of elements fixed under the whole action.

Equations

• MulAction.fixedPoints M α = {a : α | ∀ (m : M), m • a = a}

def AddAction.fixedBy {M : Type u} [AddMonoid M] (α : Type v) [AddAction M α] (m : M) : Set α

fixedBy m is the set of elements fixed by m.

Equations

• AddAction.fixedBy α m = {x : α | m +ᵥ x = x}

def MulAction.fixedBy {M : Type u} [Monoid M] (α : Type v) [MulAction M α] (m : M) : Set α

fixedBy m is the set of elements fixed by m.

Equations

• MulAction.fixedBy α m = {x : α | m • x = x}

theorem AddAction.fixed_eq_iInter_fixedBy (M : Type u) [AddMonoid M] (α : Type v) [AddAction M α] : AddAction.fixedPoints M α = ⋂ (m : M), AddAction.fixedBy α m

theorem MulAction.fixed_eq_iInter_fixedBy (M : Type u) [Monoid M] (α : Type v) [MulAction M α] : MulAction.fixedPoints M α = ⋂ (m : M), MulAction.fixedBy α m

@[simp]

theorem AddAction.mem_fixedPoints {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} : a ∈ AddAction.fixedPoints M α ↔ ∀ (m : M), m +ᵥ a = a

@[simp]

theorem MulAction.mem_fixedPoints {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} : a ∈ MulAction.fixedPoints M α ↔ ∀ (m : M), m • a = a

@[simp]

theorem AddAction.mem_fixedBy {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {m : M} {a : α} : a ∈ AddAction.fixedBy α m ↔ m +ᵥ a = a

@[simp]

theorem MulAction.mem_fixedBy {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {m : M} {a : α} : a ∈ MulAction.fixedBy α m ↔ m • a = a

theorem AddAction.mem_fixedPoints' {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} : a ∈ AddAction.fixedPoints M α ↔ ∀ a' ∈ AddAction.orbit M a, a' = a

theorem MulAction.mem_fixedPoints' {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} : a ∈ MulAction.fixedPoints M α ↔ ∀ a' ∈ MulAction.orbit M a, a' = a

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

def AddAction.stabilizerAddSubmonoid (M : Type u) [AddMonoid M] {α : Type v} [AddAction M α] (a : α) : AddSubmonoid M

The stabilizer of a point a as an additive submonoid of M.

Equations

• AddAction.stabilizerAddSubmonoid M a = { carrier := {m : M | m +ᵥ a = a}, add_mem' := ⋯, zero_mem' := ⋯ }

theorem AddAction.stabilizerAddSubmonoid.proof_1 (M : Type u_2) [AddMonoid M] {α : Type u_1} [AddAction M α] (a : α) {m : M} {m' : M} (ha : m +ᵥ a = a) (hb : m' +ᵥ a = a) : m + m' +ᵥ a = a

def MulAction.stabilizerSubmonoid (M : Type u) [Monoid M] {α : Type v} [MulAction M α] (a : α) : Submonoid M

The stabilizer of a point a as a submonoid of M.

Equations

• MulAction.stabilizerSubmonoid M a = { carrier := {m : M | m • a = a}, mul_mem' := ⋯, one_mem' := ⋯ }

instance AddAction.instDecidablePredMemAddSubmonoidStabilizerAddSubmonoidOfDecidableEq {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] [DecidableEq α] (a : α) : DecidablePred fun (x : M) => x ∈ AddAction.stabilizerAddSubmonoid M a

Equations

• AddAction.instDecidablePredMemAddSubmonoidStabilizerAddSubmonoidOfDecidableEq a x = inferInstanceAs (Decidable (x +ᵥ a = a))

instance MulAction.instDecidablePredMemSubmonoidStabilizerSubmonoidOfDecidableEq {M : Type u} [Monoid M] {α : Type v} [MulAction M α] [DecidableEq α] (a : α) : DecidablePred fun (x : M) => x ∈ MulAction.stabilizerSubmonoid M a

Equations

• MulAction.instDecidablePredMemSubmonoidStabilizerSubmonoidOfDecidableEq a x = inferInstanceAs (Decidable (x • a = a))

@[simp]

theorem AddAction.mem_stabilizerAddSubmonoid_iff {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {a : α} {m : M} : m ∈ AddAction.stabilizerAddSubmonoid M a ↔ m +ᵥ a = a

@[simp]

theorem MulAction.mem_stabilizerSubmonoid_iff {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {a : α} {m : M} : m ∈ MulAction.stabilizerSubmonoid M a ↔ m • a = a

def FixedPoints.submonoid (M : Type u) (α : Type v) [Monoid M] [Monoid α] [MulDistribMulAction M α] : Submonoid α

The submonoid of elements fixed under the whole action.

Equations

• FixedPoints.submonoid M α = { carrier := MulAction.fixedPoints M α, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem FixedPoints.mem_submonoid (M : Type u) (α : Type v) [Monoid M] [Monoid α] [MulDistribMulAction M α] (a : α) : a ∈ FixedPoints.submonoid M α ↔ ∀ (m : M), m • a = a

def FixedPoints.subgroup (M : Type u) (α : Type v) [Monoid M] [Group α] [MulDistribMulAction M α] : Subgroup α

The subgroup of elements fixed under the whole action.

Equations

• FixedPoints.subgroup M α = { toSubmonoid := FixedPoints.submonoid M α, inv_mem' := ⋯ }

def FixedPoints.«term_^*_» : Lean.TrailingParserDescr

The notation for FixedPoints.subgroup, chosen to resemble αᴹ.

Equations

• FixedPoints.«term_^*_» = Lean.ParserDescr.trailingNode `FixedPoints.term_^*_ 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^*") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem FixedPoints.mem_subgroup (M : Type u) (α : Type v) [Monoid M] [Group α] [MulDistribMulAction M α] (a : α) : a ∈ FixedPoints.subgroup M α ↔ ∀ (m : M), m • a = a

@[simp]

theorem FixedPoints.subgroup_toSubmonoid (M : Type u) (α : Type v) [Monoid M] [Group α] [MulDistribMulAction M α] : (FixedPoints.subgroup M α).toSubmonoid = FixedPoints.submonoid M α

def FixedPoints.addSubmonoid (M : Type u) (α : Type v) [Monoid M] [AddMonoid α] [DistribMulAction M α] : AddSubmonoid α

The additive submonoid of elements fixed under the whole action.

Equations

• FixedPoints.addSubmonoid M α = { carrier := MulAction.fixedPoints M α, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem FixedPoints.mem_addSubmonoid (M : Type u) (α : Type v) [Monoid M] [AddMonoid α] [DistribMulAction M α] (a : α) : a ∈ FixedPoints.addSubmonoid M α ↔ ∀ (m : M), m • a = a

def FixedPoints.addSubgroup (M : Type u) (α : Type v) [Monoid M] [AddGroup α] [DistribMulAction M α] : AddSubgroup α

The additive subgroup of elements fixed under the whole action.

Equations

• α^+M = { toAddSubmonoid := FixedPoints.addSubmonoid M α, neg_mem' := ⋯ }

def «term_^+_» : Lean.TrailingParserDescr

The notation for FixedPoints.addSubgroup, chosen to resemble αᴹ.

Equations

• «term_^+_» = Lean.ParserDescr.trailingNode `term_^+_ 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^+") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem FixedPoints.mem_addSubgroup (M : Type u) (α : Type v) [Monoid M] [AddGroup α] [DistribMulAction M α] (a : α) : a ∈ α^+M ↔ ∀ (m : M), m • a = a

@[simp]

theorem FixedPoints.addSubgroup_toAddSubmonoid (M : Type u) (α : Type v) [Monoid M] [AddGroup α] [DistribMulAction M α] : (α^+M).toAddSubmonoid = FixedPoints.addSubmonoid M α

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

@[simp]

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

@[simp]

theorem MulAction.orbit_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (a : α) : MulAction.orbit G (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.orbit_eq_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} {b : α} : AddAction.orbit G a = AddAction.orbit G b ↔ a ∈ AddAction.orbit G b

theorem MulAction.orbit_eq_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} {b : α} : MulAction.orbit G a = MulAction.orbit G b ↔ a ∈ MulAction.orbit G b

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

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

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

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

instance AddAction.instAddAction {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (H : AddSubgroup G) : AddAction { x : G // x ∈ H } α

Equations

• AddAction.instAddAction H = inferInstanceAs (AddAction { x : G // x ∈ H.toAddSubmonoid } α)

instance MulAction.instMulAction {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (H : Subgroup G) : MulAction { x : G // x ∈ H } α

Equations

• MulAction.instMulAction H = inferInstanceAs (MulAction { x : G // x ∈ H.toSubmonoid } α)

theorem AddAction.orbit_addSubgroup_subset {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (H : AddSubgroup G) (a : α) : AddAction.orbit { x : G // x ∈ H } a ⊆ AddAction.orbit G a

theorem MulAction.orbit_subgroup_subset {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (H : Subgroup G) (a : α) : MulAction.orbit { x : G // x ∈ H } a ⊆ MulAction.orbit G a

theorem AddAction.mem_orbit_of_mem_orbit_addSubgroup {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {a : α} {b : α} (h : a ∈ AddAction.orbit { x : G // x ∈ H } b) : a ∈ AddAction.orbit G b

theorem MulAction.mem_orbit_of_mem_orbit_subgroup {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {a : α} {b : α} (h : a ∈ MulAction.orbit { x : G // x ∈ H } b) : a ∈ MulAction.orbit G b

theorem AddAction.mem_orbit_symm {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a₁ : α} {a₂ : α} : a₁ ∈ AddAction.orbit G a₂ ↔ a₂ ∈ AddAction.orbit G a₁

theorem MulAction.mem_orbit_symm {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a₁ : α} {a₂ : α} : a₁ ∈ MulAction.orbit G a₂ ↔ a₂ ∈ MulAction.orbit G a₁

theorem AddAction.mem_addSubgroup_orbit_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {x : α} {a : ↑(AddAction.orbit G x)} {b : ↑(AddAction.orbit G x)} : a ∈ AddAction.orbit { x : G // x ∈ H } b ↔ ↑a ∈ AddAction.orbit { x : G // x ∈ H } ↑b

theorem MulAction.mem_subgroup_orbit_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {x : α} {a : ↑(MulAction.orbit G x)} {b : ↑(MulAction.orbit G x)} : a ∈ MulAction.orbit { x : G // x ∈ H } b ↔ ↑a ∈ MulAction.orbit { x : G // x ∈ H } ↑b

theorem AddAction.orbitRel.proof_1 (G : Type u_2) (α : Type u_1) [AddGroup G] [AddAction G α] : Equivalence fun (a b : α) => a ∈ AddAction.orbit G b

def AddAction.orbitRel (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] : Setoid α

The relation 'in the same orbit'.

Equations

• AddAction.orbitRel G α = { r := fun (a b : α) => a ∈ AddAction.orbit G b, iseqv := ⋯ }

def MulAction.orbitRel (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] : Setoid α

The relation 'in the same orbit'.

Equations

• MulAction.orbitRel G α = { r := fun (a b : α) => a ∈ MulAction.orbit G b, iseqv := ⋯ }

theorem AddAction.orbitRel_apply {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} {b : α} : (AddAction.orbitRel G α).Rel a b ↔ a ∈ AddAction.orbit G b

theorem MulAction.orbitRel_apply {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} {b : α} : (MulAction.orbitRel G α).Rel a b ↔ a ∈ MulAction.orbit G b

theorem AddAction.orbitRel_r_apply {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} {b : α} : Setoid.r a b ↔ a ∈ AddAction.orbit G b

theorem MulAction.orbitRel_r_apply {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} {b : α} : Setoid.r a b ↔ a ∈ MulAction.orbit G b

theorem AddAction.orbitRel_addSubgroup_le {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (H : AddSubgroup G) : AddAction.orbitRel { x : G // x ∈ 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 { x : G // x ∈ 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 { x : { x : G // x ∈ K } // x ∈ H.addSubgroupOf K } α = AddAction.orbitRel { x : G // x ∈ 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 { x : { x : G // x ∈ K } // x ∈ H.subgroupOf K } α = MulAction.orbitRel { x : G // x ∈ H ⊓ K } α

theorem AddAction.quotient_preimage_image_eq_union_add {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (U : Set α) : Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (g : G), (fun (x : α) => g +ᵥ x) '' 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 G.

theorem MulAction.quotient_preimage_image_eq_union_mul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (U : Set α) : Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (g : G), (fun (x : α) => g • x) '' 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 G.

theorem AddAction.disjoint_image_image_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {U : Set α} {V : Set α} : Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ (g : G), g +ᵥ x ∉ V

theorem MulAction.disjoint_image_image_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {U : Set α} {V : Set α} : Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V

theorem AddAction.image_inter_image_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (U : Set α) (V : Set α) : Quotient.mk' '' U ∩ Quotient.mk' '' V = ∅ ↔ ∀ x ∈ U, ∀ (g : G), g +ᵥ x ∉ V

theorem MulAction.image_inter_image_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (U : Set α) (V : Set α) : Quotient.mk' '' U ∩ Quotient.mk' '' V = ∅ ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V

@[reducible, inline]

abbrev AddAction.orbitRel.Quotient (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] : Type u_2

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

Equations

• AddAction.orbitRel.Quotient G α = Quotient (AddAction.orbitRel G α)

@[reducible, inline]

abbrev MulAction.orbitRel.Quotient (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] : Type u_2

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

Equations

• MulAction.orbitRel.Quotient G α = Quotient (MulAction.orbitRel G α)

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_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_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.

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.orbitRel.Quotient.orbit.proof_1 {G : Type u_2} {α : Type u_1} [AddGroup G] [AddAction G α] : ∀ (x x_1 : α), x ∈ AddAction.orbit G x_1 → AddAction.orbit G x = AddAction.orbit G x_1

def AddAction.orbitRel.Quotient.orbit {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (x : AddAction.orbitRel.Quotient G α) : Set α

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

Equations

• x.orbit = Quotient.liftOn' x (AddAction.orbit G) ⋯

def MulAction.orbitRel.Quotient.orbit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (x : MulAction.orbitRel.Quotient G α) : Set α

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

Equations

• x.orbit = Quotient.liftOn' x (MulAction.orbit G) ⋯

@[simp]

theorem AddAction.orbitRel.Quotient.orbit_mk {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (a : α) : AddAction.orbitRel.Quotient.orbit (Quotient.mk'' a) = AddAction.orbit G a

@[simp]

theorem MulAction.orbitRel.Quotient.orbit_mk {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (a : α) : MulAction.orbitRel.Quotient.orbit (Quotient.mk'' a) = MulAction.orbit G a

theorem AddAction.orbitRel.Quotient.mem_orbit {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} {x : AddAction.orbitRel.Quotient G α} : a ∈ x.orbit ↔ Quotient.mk'' a = x

theorem MulAction.orbitRel.Quotient.mem_orbit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} {x : MulAction.orbitRel.Quotient G α} : a ∈ x.orbit ↔ Quotient.mk'' a = x

theorem AddAction.orbitRel.Quotient.orbit_eq_orbit_out {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (x : AddAction.orbitRel.Quotient G α) {φ : AddAction.orbitRel.Quotient G α → α} (hφ : Function.RightInverse φ Quotient.mk') : x.orbit = AddAction.orbit G (φ x)

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

theorem MulAction.orbitRel.Quotient.orbit_eq_orbit_out {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (x : MulAction.orbitRel.Quotient G α) {φ : MulAction.orbitRel.Quotient G α → α} (hφ : Function.RightInverse φ Quotient.mk') : x.orbit = MulAction.orbit G (φ x)

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

theorem AddAction.orbitRel.Quotient.orbit_injective {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] : Function.Injective AddAction.orbitRel.Quotient.orbit

theorem MulAction.orbitRel.Quotient.orbit_injective {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] : Function.Injective MulAction.orbitRel.Quotient.orbit

@[simp]

theorem AddAction.orbitRel.Quotient.orbit_inj {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {x : AddAction.orbitRel.Quotient G α} {y : AddAction.orbitRel.Quotient G α} : x.orbit = y.orbit ↔ x = y

@[simp]

theorem MulAction.orbitRel.Quotient.orbit_inj {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {x : MulAction.orbitRel.Quotient G α} {y : MulAction.orbitRel.Quotient G α} : x.orbit = y.orbit ↔ x = y

theorem AddAction.orbitRel.quotient_eq_of_quotient_addSubgroup_eq {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {a : α} {b : α} (h : ⟦a⟧ = ⟦b⟧) : ⟦a⟧ = ⟦b⟧

theorem MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {a : α} {b : α} (h : ⟦a⟧ = ⟦b⟧) : ⟦a⟧ = ⟦b⟧

theorem AddAction.orbitRel.quotient_eq_of_quotient_addSubgroup_eq' {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {a : α} {b : α} (h : Quotient.mk'' a = Quotient.mk'' b) : Quotient.mk'' a = Quotient.mk'' b

theorem MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq' {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {a : α} {b : α} (h : Quotient.mk'' a = Quotient.mk'' b) : Quotient.mk'' a = Quotient.mk'' b

theorem AddAction.orbitRel.Quotient.orbit_nonempty {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (x : AddAction.orbitRel.Quotient G α) : x.orbit.Nonempty

theorem MulAction.orbitRel.Quotient.orbit_nonempty {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (x : MulAction.orbitRel.Quotient G α) : x.orbit.Nonempty

theorem AddAction.orbitRel.Quotient.mapsTo_vadd_orbit {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (g : G) (x : AddAction.orbitRel.Quotient G α) : Set.MapsTo (fun (x : α) => g +ᵥ x) x.orbit x.orbit

theorem MulAction.orbitRel.Quotient.mapsTo_smul_orbit {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (x : MulAction.orbitRel.Quotient G α) : Set.MapsTo (fun (x : α) => g • x) x.orbit x.orbit

theorem AddAction.instElemOrbit_1.proof_1 {G : Type u_2} {α : Type u_1} [AddGroup G] [AddAction G α] (x : AddAction.orbitRel.Quotient G α) (a : ↑x.orbit) : 0 +ᵥ a = a

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

Equations

• AddAction.instElemOrbit_1 x = AddAction.mk ⋯ ⋯

theorem AddAction.instElemOrbit_1.proof_2 {G : Type u_2} {α : Type u_1} [AddGroup G] [AddAction G α] (x : AddAction.orbitRel.Quotient G α) (g : G) (g' : G) (a' : ↑x.orbit) : g + g' +ᵥ a' = g +ᵥ (g' +ᵥ a')

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

Equations

• MulAction.instElemOrbit_1 x = MulAction.mk ⋯ ⋯

@[simp]

theorem AddAction.orbitRel.Quotient.orbit.coe_vadd {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {g : G} {x : AddAction.orbitRel.Quotient G α} {a : ↑x.orbit} : ↑(g +ᵥ a) = g +ᵥ ↑a

@[simp]

theorem MulAction.orbitRel.Quotient.orbit.coe_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {g : G} {x : MulAction.orbitRel.Quotient G α} {a : ↑x.orbit} : ↑(g • a) = g • ↑a

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

• ⋯ = ⋯

@[simp]

theorem AddAction.orbitRel.Quotient.mem_addSubgroup_orbit_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {x : AddAction.orbitRel.Quotient G α} {a : ↑x.orbit} {b : ↑x.orbit} : ↑a ∈ AddAction.orbit { x : G // x ∈ H } ↑b ↔ a ∈ AddAction.orbit { x : G // x ∈ H } b

@[simp]

theorem MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {x : MulAction.orbitRel.Quotient G α} {a : ↑x.orbit} {b : ↑x.orbit} : ↑a ∈ MulAction.orbit { x : G // x ∈ H } ↑b ↔ a ∈ MulAction.orbit { x : G // x ∈ H } b

theorem AddAction.orbitRel.Quotient.addSubgroup_quotient_eq_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {x : AddAction.orbitRel.Quotient G α} {a : ↑x.orbit} {b : ↑x.orbit} : ⟦a⟧ = ⟦b⟧ ↔ ⟦↑a⟧ = ⟦↑b⟧

theorem MulAction.orbitRel.Quotient.subgroup_quotient_eq_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {x : MulAction.orbitRel.Quotient G α} {a : ↑x.orbit} {b : ↑x.orbit} : ⟦a⟧ = ⟦b⟧ ↔ ⟦↑a⟧ = ⟦↑b⟧

theorem AddAction.orbitRel.Quotient.mem_addSubgroup_orbit_iff' {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : AddSubgroup G} {x : AddAction.orbitRel.Quotient G α} {a : ↑x.orbit} {b : ↑x.orbit} {c : α} (h : ⟦a⟧ = ⟦b⟧) : ↑a ∈ AddAction.orbit { x : G // x ∈ H } c ↔ ↑b ∈ AddAction.orbit { x : G // x ∈ H } c

theorem MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff' {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Subgroup G} {x : MulAction.orbitRel.Quotient G α} {a : ↑x.orbit} {b : ↑x.orbit} {c : α} (h : ⟦a⟧ = ⟦b⟧) : ↑a ∈ MulAction.orbit { x : G // x ∈ H } c ↔ ↑b ∈ MulAction.orbit { x : G // x ∈ H } c

def AddAction.selfEquivSigmaOrbits' (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] : α ≃ (ω : AddAction.orbitRel.Quotient G α) × ↑ω.orbit

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

• AddAction.selfEquivSigmaOrbits' G α = Trans.trans (Equiv.sigmaFiberEquiv Quotient.mk').symm (Equiv.sigmaCongrRight fun (x : AddAction.orbitRel.Quotient G α) => Equiv.subtypeEquivRight ⋯)

theorem AddAction.selfEquivSigmaOrbits'.proof_1 (G : Type u_2) (α : Type u_1) [AddGroup G] [AddAction G α] : ∀ (x : AddAction.orbitRel.Quotient G α) (x_1 : α), Quotient.mk'' x_1 = x ↔ x_1 ∈ x.orbit

def MulAction.selfEquivSigmaOrbits' (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] : α ≃ (ω : MulAction.orbitRel.Quotient G α) × ↑ω.orbit

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

• MulAction.selfEquivSigmaOrbits' G α = Trans.trans (Equiv.sigmaFiberEquiv Quotient.mk').symm (Equiv.sigmaCongrRight fun (x : MulAction.orbitRel.Quotient G α) => Equiv.subtypeEquivRight ⋯)

theorem AddAction.selfEquivSigmaOrbits.proof_1 (G : Type u_2) (α : Type u_1) [AddGroup G] [AddAction G α] : ∀ (x : AddAction.orbitRel.Quotient G α), x.orbit = AddAction.orbit G (Quotient.out' x)

def AddAction.selfEquivSigmaOrbits (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] : α ≃ (ω : AddAction.orbitRel.Quotient G α) × ↑(AddAction.orbit G (Quotient.out' ω))

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

Equations

• AddAction.selfEquivSigmaOrbits G α = (AddAction.selfEquivSigmaOrbits' G α).trans (Equiv.sigmaCongrRight fun (x : AddAction.orbitRel.Quotient G α) => Equiv.Set.ofEq ⋯)

def MulAction.selfEquivSigmaOrbits (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] : α ≃ (ω : MulAction.orbitRel.Quotient G α) × ↑(MulAction.orbit G (Quotient.out' ω))

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

Equations

• MulAction.selfEquivSigmaOrbits G α = (MulAction.selfEquivSigmaOrbits' G α).trans (Equiv.sigmaCongrRight fun (x : MulAction.orbitRel.Quotient G α) => Equiv.Set.ofEq ⋯)

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 AddAction.stabilizer.proof_1 (G : Type u_2) {α : Type u_1} [AddGroup G] [AddAction G α] (a : α) {m : G} (ha : m +ᵥ a = a) : -m +ᵥ a = a

def AddAction.stabilizer (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] (a : α) : AddSubgroup G

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

Equations

• AddAction.stabilizer G a = { toAddSubmonoid := AddAction.stabilizerAddSubmonoid G a, neg_mem' := ⋯ }

def MulAction.stabilizer (G : Type u_1) {α : Type u_2} [Group G] [MulAction G α] (a : α) : Subgroup G

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

Equations

• MulAction.stabilizer G a = { toSubmonoid := MulAction.stabilizerSubmonoid G a, inv_mem' := ⋯ }

instance AddAction.instDecidablePredMemAddSubgroupStabilizerOfDecidableEq {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] [DecidableEq α] (a : α) : DecidablePred fun (x : G) => x ∈ AddAction.stabilizer G a

Equations

• AddAction.instDecidablePredMemAddSubgroupStabilizerOfDecidableEq a x = inferInstanceAs (Decidable (x +ᵥ a = a))

instance MulAction.instDecidablePredMemSubgroupStabilizerOfDecidableEq {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] (a : α) : DecidablePred fun (x : G) => x ∈ MulAction.stabilizer G a

Equations

• MulAction.instDecidablePredMemSubgroupStabilizerOfDecidableEq a x = inferInstanceAs (Decidable (x • a = a))

@[simp]

theorem AddAction.mem_stabilizer_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a : α} {g : G} : g ∈ AddAction.stabilizer G a ↔ g +ᵥ a = a

@[simp]

theorem MulAction.mem_stabilizer_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a : α} {g : G} : g ∈ MulAction.stabilizer G a ↔ g • a = a

theorem AddAction.le_stabilizer_vadd_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup G] [AddAction G α] [AddAction G β] [VAdd α β] [VAddAssocClass G α β] (a : α) (b : β) : AddAction.stabilizer G a ≤ AddAction.stabilizer G (a +ᵥ b)

theorem MulAction.le_stabilizer_smul_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [MulAction G α] [MulAction G β] [SMul α β] [IsScalarTower G α β] (a : α) (b : β) : MulAction.stabilizer G a ≤ MulAction.stabilizer G (a • b)

theorem AddAction.le_stabilizer_vadd_right {α : Type u_2} {β : Type u_3} {G' : Type u_4} [AddGroup G'] [VAdd α β] [AddAction G' β] [VAddCommClass G' α β] (a : α) (b : β) : AddAction.stabilizer G' b ≤ AddAction.stabilizer G' (a +ᵥ b)

theorem MulAction.le_stabilizer_smul_right {α : Type u_2} {β : Type u_3} {G' : Type u_4} [Group G'] [SMul α β] [MulAction G' β] [SMulCommClass G' α β] (a : α) (b : β) : MulAction.stabilizer G' b ≤ MulAction.stabilizer G' (a • b)

@[simp]

theorem AddAction.stabilizer_vadd_eq_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup G] [AddAction G α] [AddAction G β] [VAdd α β] [VAddAssocClass G α β] (a : α) (b : β) (h : Function.Injective fun (x : α) => x +ᵥ b) : AddAction.stabilizer G (a +ᵥ b) = AddAction.stabilizer G a

@[simp]

theorem MulAction.stabilizer_smul_eq_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [MulAction G α] [MulAction G β] [SMul α β] [IsScalarTower G α β] (a : α) (b : β) (h : Function.Injective fun (x : α) => x • b) : MulAction.stabilizer G (a • b) = MulAction.stabilizer G a

@[simp]

theorem AddAction.stabilizer_vadd_eq_right {G : Type u_1} {β : Type u_3} [AddGroup G] [AddAction G β] {α : Type u_4} [AddGroup α] [AddAction α β] [VAddCommClass G α β] (a : α) (b : β) : AddAction.stabilizer G (a +ᵥ b) = AddAction.stabilizer G b

@[simp]

theorem MulAction.stabilizer_smul_eq_right {G : Type u_1} {β : Type u_3} [Group G] [MulAction G β] {α : Type u_4} [Group α] [MulAction α β] [SMulCommClass G α β] (a : α) (b : β) : MulAction.stabilizer G (a • b) = MulAction.stabilizer G b

@[simp]

theorem AddAction.stabilizer_add_eq_left {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] [AddGroup α] [VAddAssocClass G α α] (a : α) (b : α) : AddAction.stabilizer G (a + b) = AddAction.stabilizer G a

@[simp]

theorem MulAction.stabilizer_mul_eq_left {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [Group α] [IsScalarTower G α α] (a : α) (b : α) : MulAction.stabilizer G (a * b) = MulAction.stabilizer G a

@[simp]

theorem AddAction.stabilizer_add_eq_right {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] [AddGroup α] [VAddCommClass G α α] (a : α) (b : α) : AddAction.stabilizer G (a + b) = AddAction.stabilizer G b

@[simp]

theorem MulAction.stabilizer_mul_eq_right {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [Group α] [SMulCommClass G α α] (a : α) (b : α) : MulAction.stabilizer G (a * b) = MulAction.stabilizer G b

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 α).Rel a b) : { x : G // x ∈ MulAction.stabilizer G a } ≃* { x : G // x ∈ 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 α).Rel a b) : { x : G // x ∈ AddAction.stabilizer G a } ≃+ { x : G // x ∈ 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.