doc-next-gen

Mathlib.GroupTheory.GroupAction.Defs

Module docstring

{"# Definition of orbit, fixedPoints and stabilizer

This file defines orbits, stabilizers, and other objects defined in terms of actions.

Main definitions

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

"}

MulAction.orbit definition
(a : α)
Full source 
/-- The orbit of an element under an action. -/
@[to_additive "The orbit of an element under an action."]
def orbit (a : α) :=
  Set.range fun m : M => m • a
Orbit of an element under a monoid action
Informal description
Given a monoid \( M \) acting on a type \( \alpha \), the orbit of an element \( a \in \alpha \) under the action of \( M \) is the set of all elements of the form \( m \cdot a \) for some \( m \in M \). In other words, it is the set of all points reachable from \( a \) via the action of \( M \).
MulAction.mem_orbit_iff theorem
{a₁ a₂ : α} : a₂ ∈ orbit M a₁ ↔ ∃ x : M, x • a₁ = a₂
Full source 
@[to_additive]
theorem mem_orbit_iff {a₁ a₂ : α} : a₂ ∈ orbit M a₁a₂ ∈ orbit M a₁ ↔ ∃ x : M, x • a₁ = a₂ :=
  Iff.rfl
Characterization of Orbit Membership via Monoid Action
Informal description
For elements $a_1, a_2$ in a type $\alpha$ acted upon by a monoid $M$, the element $a_2$ belongs to the orbit of $a_1$ under $M$ if and only if there exists an element $x \in M$ such that $x \cdot a_1 = a_2$.
MulAction.mem_orbit theorem
(a : α) (m : M) : m • a ∈ orbit M a
Full source 
@[to_additive (attr := simp)]
theorem mem_orbit (a : α) (m : M) : m • a ∈ orbit M a :=
  ⟨m, rfl⟩
Action of Monoid Element Preserves Orbit Membership
Informal description
For any element $a$ in a type $\alpha$ with a monoid action of $M$ on $\alpha$, and for any element $m \in M$, the action of $m$ on $a$ (denoted $m \cdot a$) belongs to the orbit of $a$ under the action of $M$.
MulAction.mem_orbit_of_mem_orbit theorem
{a₁ a₂ : α} (m : M) (h : a₂ ∈ orbit M a₁) : m • a₂ ∈ orbit M a₁
Full source 
@[to_additive]
theorem mem_orbit_of_mem_orbit {a₁ a₂ : α} (m : M) (h : a₂ ∈ orbit M a₁) :
    m • a₂ ∈ orbit M a₁ := by
  obtain ⟨x, rfl⟩ := mem_orbit_iff.mp h
  simp [smul_smul]
Closure of Orbit under Monoid Action
Informal description
For any elements $a_1, a_2$ in a type $\alpha$ with a monoid action of $M$, if $a_2$ belongs to the orbit of $a_1$ under $M$, then for any $m \in M$, the action of $m$ on $a_2$ (denoted $m \cdot a_2$) also belongs to the orbit of $a_1$.
MulAction.mem_orbit_self theorem
(a : α) : a ∈ orbit M a
Full source 
@[to_additive (attr := simp)]
theorem mem_orbit_self (a : α) : a ∈ orbit M a :=
  ⟨1, by simp [MulAction.one_smul]⟩
Self-inclusion in Orbit under Monoid Action
Informal description
For any element $a$ in a type $\alpha$ with a monoid action of $M$, the element $a$ itself is in its own orbit under the action of $M$, i.e., $a \in \text{orbit}_M(a)$.
MulAction.orbit_nonempty theorem
(a : α) : Set.Nonempty (orbit M a)
Full source 
@[to_additive]
theorem orbit_nonempty (a : α) : Set.Nonempty (orbit M a) :=
  Set.range_nonempty _
Nonemptiness of Orbits under Monoid Action
Informal description
For any element $a$ in a type $\alpha$ acted upon by a monoid $M$, the orbit of $a$ under $M$ is nonempty. In other words, there exists at least one element in the set $\{m \cdot a \mid m \in M\}$.
MulAction.mapsTo_smul_orbit theorem
(m : M) (a : α) : Set.MapsTo (m • ·) (orbit M a) (orbit M a)
Full source 
@[to_additive]
theorem mapsTo_smul_orbit (m : M) (a : α) : Set.MapsTo (m • ·) (orbit M a) (orbit M a) :=
  Set.range_subset_iff.2 fun m' => ⟨m * m', mul_smul _ _ _⟩
Monoid Action Preserves Orbit
Informal description
For any element $m$ of a monoid $M$ acting on a type $\alpha$, and any element $a \in \alpha$, the function $x \mapsto m \cdot x$ maps the orbit of $a$ under $M$ into itself. In other words, if $x$ is in the orbit of $a$, then $m \cdot x$ is also in the orbit of $a$.
MulAction.smul_orbit_subset theorem
(m : M) (a : α) : m • orbit M a ⊆ orbit M a
Full source 
@[to_additive]
theorem smul_orbit_subset (m : M) (a : α) : m • orbit M a ⊆ orbit M a :=
  (mapsTo_smul_orbit m a).image_subset
Monoid Action Preserves Orbit under Scalar Multiplication
Informal description
For any element $m$ of a monoid $M$ acting on a type $\alpha$, and any element $a \in \alpha$, the set obtained by applying the action of $m$ to every element in the orbit of $a$ is a subset of the orbit of $a$. In other words, $m \cdot \text{orbit}_M(a) \subseteq \text{orbit}_M(a)$.
MulAction.orbit_smul_subset theorem
(m : M) (a : α) : orbit M (m • a) ⊆ orbit M a
Full source 
@[to_additive]
theorem orbit_smul_subset (m : M) (a : α) : orbitorbit M (m • a) ⊆ orbit M a :=
  Set.range_subset_iff.2 fun m' => mul_smul m' m a ▸ mem_orbit _ _
Orbit Inclusion under Monoid Action: $\text{orbit}_M(m \cdot a) \subseteq \text{orbit}_M(a)$
Informal description
For any element $m$ of a monoid $M$ acting on a type $\alpha$, and any element $a \in \alpha$, the orbit of $m \cdot a$ under the action of $M$ is a subset of the orbit of $a$. In other words, $\text{orbit}_M(m \cdot a) \subseteq \text{orbit}_M(a)$.
MulAction.instElemOrbit instance
{a : α} : MulAction M (orbit M a)
Full source 
@[to_additive]
instance {a : α} : MulAction M (orbit M a) where
  smul m := (mapsTo_smul_orbit m a).restrict _ _ _
  one_smul m := Subtype.ext (one_smul M (m : α))
  mul_smul m m' a' := Subtype.ext (mul_smul m m' (a' : α))
Natural Monoid Action on Orbits
Informal description
For any monoid $M$ acting on a type $\alpha$ and any element $a \in \alpha$, the orbit of $a$ under $M$ inherits a natural $M$-action structure.
MulAction.orbit.coe_smul theorem
{a : α} {m : M} {a' : orbit M a} : ↑(m • a') = m • (a' : α)
Full source 
@[to_additive (attr := simp)]
theorem orbit.coe_smul {a : α} {m : M} {a' : orbit M a} : ↑(m • a') = m • (a' : α) :=
  rfl
Compatibility of Monoid Action with Orbit Projection: $\overline{m \cdot a'} = m \cdot \overline{a'}$
Informal description
For any monoid $M$ acting on a type $\alpha$, any element $a \in \alpha$, any $m \in M$, and any element $a'$ in the orbit of $a$ under $M$, the projection of the action $m \cdot a'$ in $\alpha$ equals the action of $m$ on the projection of $a'$ in $\alpha$. That is, $\overline{m \cdot a'} = m \cdot \overline{a'}$, where $\overline{\cdot}$ denotes the projection from the orbit to $\alpha$.
MulAction.orbit_submonoid_subset theorem
(S : Submonoid M) (a : α) : orbit S a ⊆ orbit M a
Full source 
@[to_additive]
lemma orbit_submonoid_subset (S : Submonoid M) (a : α) : orbitorbit S a ⊆ orbit M a := by
  rintro b ⟨g, rfl⟩
  exact mem_orbit _ _
Orbit under Submonoid is Subset of Orbit under Monoid
Informal description
For any submonoid $S$ of a monoid $M$ acting on a type $\alpha$, and for any element $a \in \alpha$, the orbit of $a$ under the action of $S$ is a subset of the orbit of $a$ under the action of $M$.
MulAction.mem_orbit_of_mem_orbit_submonoid theorem
{S : Submonoid M} {a b : α} (h : a ∈ orbit S b) : a ∈ orbit M b
Full source 
@[to_additive]
lemma mem_orbit_of_mem_orbit_submonoid {S : Submonoid M} {a b : α} (h : a ∈ orbit S b) :
    a ∈ orbit M b :=
  orbit_submonoid_subset S _ h
Orbit Inclusion under Submonoid Implies Orbit Inclusion under Monoid
Informal description
For any submonoid $S$ of a monoid $M$ acting on a type $\alpha$, and for any elements $a, b \in \alpha$, if $a$ is in the orbit of $b$ under the action of $S$, then $a$ is also in the orbit of $b$ under the action of $M$.
MulAction.fixedPoints definition
: Set α
Full source 
/-- The set of elements fixed under the whole action. -/
@[to_additive "The set of elements fixed under the whole action."]
def fixedPoints : Set α :=
  { a : α | ∀ m : M, m • a = a }
Fixed points under a group action
Informal description
The set of all elements $a$ in $\alpha$ that are fixed by every element $m$ in $M$ under the group action, i.e., $m \cdot a = a$ for all $m \in M$.
MulAction.fixedBy definition
(m : M) : Set α
Full source 
/-- `fixedBy m` is the set of elements fixed by `m`. -/
@[to_additive "`fixedBy m` is the set of elements fixed by `m`."]
def fixedBy (m : M) : Set α :=
  { x | m • x = x }
Fixed points under a monoid action element
Informal description
For a monoid \( M \) acting on a set \( \alpha \), the set \(\text{fixedBy}(m)\) consists of all elements \( x \in \alpha \) that are fixed by the action of \( m \), i.e., \( m \cdot x = x \).
MulAction.fixed_eq_iInter_fixedBy theorem
: fixedPoints M α = ⋂ m : M, fixedBy α m
Full source 
@[to_additive]
theorem fixed_eq_iInter_fixedBy : fixedPoints M α = ⋂ m : M, fixedBy α m :=
  Set.ext fun _ =>
    ⟨fun hx => Set.mem_iInter.2 fun m => hx m, fun hx m => (Set.mem_iInter.1 hx m :)⟩
Fixed Points as Intersection of Fixed-by Sets
Informal description
For a monoid $M$ acting on a set $\alpha$, the set of fixed points under the action of $M$ is equal to the intersection over all $m \in M$ of the sets of points fixed by $m$. That is, \[ \text{fixedPoints}(M, \alpha) = \bigcap_{m \in M} \text{fixedBy}(\alpha, m). \]
MulAction.mem_fixedPoints theorem
{a : α} : a ∈ fixedPoints M α ↔ ∀ m : M, m • a = a
Full source 
@[to_additive (attr := simp)]
theorem mem_fixedPoints {a : α} : a ∈ fixedPoints M αa ∈ fixedPoints M α ↔ ∀ m : M, m • a = a :=
  Iff.rfl
Characterization of Fixed Points under Monoid Action
Informal description
An element $a$ of a set $\alpha$ is in the fixed points of a monoid $M$ acting on $\alpha$ if and only if for every element $m \in M$, the action of $m$ on $a$ leaves $a$ unchanged, i.e., $m \cdot a = a$.
MulAction.mem_fixedBy theorem
{m : M} {a : α} : a ∈ fixedBy α m ↔ m • a = a
Full source 
@[to_additive (attr := simp)]
theorem mem_fixedBy {m : M} {a : α} : a ∈ fixedBy α ma ∈ fixedBy α m ↔ m • a = a :=
  Iff.rfl
Characterization of Fixed Points Under Monoid Action
Informal description
For a monoid $M$ acting on a set $\alpha$, an element $a \in \alpha$ is in the set $\text{fixedBy}(m)$ if and only if the action of $m$ on $a$ fixes $a$, i.e., $m \cdot a = a$.
MulAction.mem_fixedPoints' theorem
{a : α} : a ∈ fixedPoints M α ↔ ∀ a', a' ∈ orbit M a → a' = a
Full source 
@[to_additive]
theorem mem_fixedPoints' {a : α} : a ∈ fixedPoints M αa ∈ fixedPoints M α ↔ ∀ a', a' ∈ orbit M a → a' = a :=
  ⟨fun h _ h₁ =>
    let ⟨m, hm⟩ := mem_orbit_iff.1 h₁
    hm ▸ h m,
    fun h _ => h _ (mem_orbit _ _)⟩
Characterization of Fixed Points via Orbit Triviality
Informal description
An element $a$ of a set $\alpha$ is in the fixed points of a monoid $M$ acting on $\alpha$ if and only if every element $a'$ in the orbit of $a$ under $M$ is equal to $a$. In other words, $a$ is fixed by all elements of $M$ if and only if its orbit is the singleton set $\{a\}$.
MulAction.stabilizerSubmonoid definition
(a : α) : Submonoid M
Full source 
/-- The stabilizer of a point `a` as a submonoid of `M`. -/
@[to_additive "The stabilizer of a point `a` as an additive submonoid of `M`."]
def stabilizerSubmonoid (a : α) : Submonoid M where
  carrier := { m | m • a = a }
  one_mem' := one_smul _ a
  mul_mem' {m m'} (ha : m • a = a) (hb : m' • a = a) :=
    show (m * m') • a = a by rw [← smul_smul, hb, ha]
Stabilizer submonoid of a point under monoid action
Informal description
For a monoid $M$ acting on a type $\alpha$, the stabilizer submonoid of a point $a \in \alpha$ is the submonoid of $M$ consisting of all elements $m \in M$ that fix $a$ under the action, i.e., $m \cdot a = a$.
MulAction.instDecidablePredMemSubmonoidStabilizerSubmonoidOfDecidableEq instance
[DecidableEq α] (a : α) : DecidablePred (· ∈ stabilizerSubmonoid M a)
Full source 
@[to_additive]
instance [DecidableEq α] (a : α) : DecidablePred (· ∈ stabilizerSubmonoid M a) :=
  fun _ => inferInstanceAs <| Decidable (_ = _)
Decidability of Stabilizer Submonoid Membership for Monoid Actions
Informal description
For a monoid $M$ acting on a type $\alpha$ with decidable equality, and for any point $a \in \alpha$, the predicate determining membership in the stabilizer submonoid of $a$ is decidable. That is, for any $m \in M$, it is decidable whether $m$ fixes $a$ under the action (i.e., $m \cdot a = a$).
MulAction.mem_stabilizerSubmonoid_iff theorem
{a : α} {m : M} : m ∈ stabilizerSubmonoid M a ↔ m • a = a
Full source 
@[to_additive (attr := simp)]
theorem mem_stabilizerSubmonoid_iff {a : α} {m : M} : m ∈ stabilizerSubmonoid M am ∈ stabilizerSubmonoid M a ↔ m • a = a :=
  Iff.rfl
Characterization of Stabilizer Submonoid Membership via Fixed Points
Informal description
For a monoid $M$ acting on a type $\alpha$, an element $m \in M$ belongs to the stabilizer submonoid of a point $a \in \alpha$ if and only if the action of $m$ on $a$ fixes $a$, i.e., $m \cdot a = a$.
FixedPoints.submonoid definition
: Submonoid α
Full source 
/-- The submonoid of elements fixed under the whole action. -/
def FixedPoints.submonoid : Submonoid α where
  carrier := MulAction.fixedPoints M α
  one_mem' := smul_one
  mul_mem' ha hb _ := by rw [smul_mul', ha, hb]
Submonoid of fixed points under a group action
Informal description
The submonoid of elements in $\alpha$ that are fixed under the action of $M$, i.e., the set $\{a \in \alpha \mid \forall m \in M, m \cdot a = a\}$ equipped with the submonoid structure inherited from $\alpha$.
FixedPoints.mem_submonoid theorem
(a : α) : a ∈ submonoid M α ↔ ∀ m : M, m • a = a
Full source 
@[simp]
lemma FixedPoints.mem_submonoid (a : α) : a ∈ submonoid M αa ∈ submonoid M α ↔ ∀ m : M, m • a = a :=
  Iff.rfl
Characterization of Fixed Points in a Submonoid under Monoid Action
Informal description
An element $a \in \alpha$ belongs to the submonoid of fixed points under the action of a monoid $M$ if and only if for every $m \in M$, the action of $m$ on $a$ fixes $a$, i.e., $m \cdot a = a$.
FixedPoints.subgroup definition
: Subgroup α
Full source 
/-- The subgroup of elements fixed under the whole action. -/
def subgroup : Subgroup α where
  __ := submonoid M α
  inv_mem' ha _ := by rw [smul_inv', ha]
Subgroup of fixed points under a group action
Informal description
The subgroup of elements in $\alpha$ that are fixed under the action of $M$, i.e., the set $\{a \in \alpha \mid \forall m \in M, m \cdot a = a\}$ equipped with the subgroup structure inherited from $\alpha$. This includes the additional property that the inverse of any fixed point is also a fixed point under the group action.
FixedPoints.term_^*_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- The notation for `FixedPoints.subgroup`, chosen to resemble `αᴹ`. -/
scoped notation α "^*" M:51 => FixedPoints.subgroup M α
Fixed points subgroup notation
Informal description
The notation `α^*M` represents the subgroup of fixed points of the action of a group `M` on a set `α`. An element `a ∈ α` is in `α^*M` if and only if for every `m ∈ M`, the action of `m` on `a` leaves `a` unchanged, i.e., `m • a = a`.
FixedPoints.mem_subgroup theorem
(a : α) : a ∈ α^*M ↔ ∀ m : M, m • a = a
Full source 
@[simp]
lemma mem_subgroup (a : α) : a ∈ α^*Ma ∈ α^*M ↔ ∀ m : M, m • a = a :=
  Iff.rfl
Characterization of Fixed Points in Subgroup under Group Action: $a \in \alpha^*M \leftrightarrow \forall m \in M, m \cdot a = a$
Informal description
An element $a$ of a type $\alpha$ belongs to the subgroup of fixed points under the action of a group $M$ if and only if for every element $m \in M$, the action of $m$ on $a$ leaves $a$ unchanged, i.e., $m \cdot a = a$.
FixedPoints.subgroup_toSubmonoid theorem
: (α^*M).toSubmonoid = submonoid M α
Full source 
@[simp]
lemma subgroup_toSubmonoid : (α^*M).toSubmonoid = submonoid M α :=
  rfl
Subgroup-to-Submonoid Equality for Fixed Points under Group Action
Informal description
The submonoid obtained from the subgroup of fixed points under the action of $M$ on $\alpha$ is equal to the submonoid of fixed points under the same action. In other words, $(\alpha^*M).\text{toSubmonoid} = \text{submonoid}_M \alpha$.
MulAction.orbit_smul theorem
(g : G) (a : α) : orbit G (g • a) = orbit G a
Full source 
@[to_additive (attr := simp)]
theorem orbit_smul (g : G) (a : α) : orbit G (g • a) = orbit G a :=
  (orbit_smul_subset g a).antisymm <|
    calc
      orbit G a = orbit G (g⁻¹ • g • a) := by rw [inv_smul_smul]
      _ ⊆ orbit G (g • a) := orbit_smul_subset _ _
Orbit Invariance under Group Action: $\text{orbit}_G(g \cdot a) = \text{orbit}_G(a)$
Informal description
For any element $g$ of a group $G$ acting on a type $\alpha$, and any element $a \in \alpha$, the orbit of $g \cdot a$ under the action of $G$ is equal to the orbit of $a$. In other words, $\text{orbit}_G(g \cdot a) = \text{orbit}_G(a)$.
MulAction.orbit_eq_iff theorem
{a b : α} : orbit G a = orbit G b ↔ a ∈ orbit G b
Full source 
@[to_additive]
theorem orbit_eq_iff {a b : α} : orbitorbit G a = orbit G b ↔ a ∈ orbit G b :=
  ⟨fun h => h ▸ mem_orbit_self _, fun ⟨_, hc⟩ => hc ▸ orbit_smul _ _⟩
Orbit Equality Criterion: $\text{orbit}_G(a) = \text{orbit}_G(b) \leftrightarrow a \in \text{orbit}_G(b)$
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with a group action of $G$, the orbits of $a$ and $b$ under $G$ are equal if and only if $a$ belongs to the orbit of $b$. In other words, $\text{orbit}_G(a) = \text{orbit}_G(b) \leftrightarrow a \in \text{orbit}_G(b)$.
MulAction.mem_orbit_smul theorem
(g : G) (a : α) : a ∈ orbit G (g • a)
Full source 
@[to_additive]
theorem mem_orbit_smul (g : G) (a : α) : a ∈ orbit G (g • a) := by
  simp only [orbit_smul, mem_orbit_self]
Element Belongs to Orbit of Its Group Action: $a \in \text{orbit}_G(g \cdot a)$
Informal description
For any element $g$ of a group $G$ acting on a type $\alpha$, and any element $a \in \alpha$, the element $a$ belongs to the orbit of $g \cdot a$ under the action of $G$. In other words, $a \in \text{orbit}_G(g \cdot a)$.
MulAction.smul_mem_orbit_smul theorem
(g h : G) (a : α) : g • a ∈ orbit G (h • a)
Full source 
@[to_additive]
theorem smul_mem_orbit_smul (g h : G) (a : α) : g • a ∈ orbit G (h • a) := by
  simp only [orbit_smul, mem_orbit]
Action Element in Orbit of Another Action: $g \cdot a \in \text{orbit}_G(h \cdot a)$
Informal description
For any elements $g, h$ in a group $G$ acting on a type $\alpha$, and any element $a \in \alpha$, the action of $g$ on $a$ belongs to the orbit of $h \cdot a$ under the action of $G$. In other words, $g \cdot a \in \text{orbit}_G(h \cdot a)$.
MulAction.instMulAction instance
(H : Subgroup G) : MulAction H α
Full source 
@[to_additive]
instance instMulAction (H : Subgroup G) : MulAction H α :=
  inferInstanceAs (MulAction H.toSubmonoid α)
Subgroup Action Inheritance
Informal description
For any subgroup $H$ of a group $G$ acting on a type $\alpha$, the subgroup $H$ inherits a multiplicative action on $\alpha$ from $G$.
MulAction.subgroup_smul_def theorem
{H : Subgroup G} (a : H) (b : α) : a • b = (a : G) • b
Full source 
@[to_additive]
lemma subgroup_smul_def {H : Subgroup G} (a : H) (b : α) : a • b = (a : G) • b := rfl
Subgroup Action Equals Parent Group Action
Informal description
For any subgroup $H$ of a group $G$ acting on a type $\alpha$, and for any element $a \in H$ and $b \in \alpha$, the action of $a$ on $b$ in the subgroup action equals the action of $a$ (considered as an element of $G$) on $b$ in the original group action. That is, $a \cdot b = (a : G) \cdot b$.
MulAction.orbit_subgroup_subset theorem
(H : Subgroup G) (a : α) : orbit H a ⊆ orbit G a
Full source 
@[to_additive]
lemma orbit_subgroup_subset (H : Subgroup G) (a : α) : orbitorbit H a ⊆ orbit G a :=
  orbit_submonoid_subset H.toSubmonoid a
Subgroup Orbit is Subset of Group Orbit
Informal description
For any subgroup $H$ of a group $G$ acting on a type $\alpha$, and for any element $a \in \alpha$, the orbit of $a$ under the action of $H$ is a subset of the orbit of $a$ under the action of $G$. In other words, $H \cdot a \subseteq G \cdot a$.
MulAction.mem_orbit_of_mem_orbit_subgroup theorem
{H : Subgroup G} {a b : α} (h : a ∈ orbit H b) : a ∈ orbit G b
Full source 
@[to_additive]
lemma mem_orbit_of_mem_orbit_subgroup {H : Subgroup G} {a b : α} (h : a ∈ orbit H b) :
    a ∈ orbit G b :=
  orbit_subgroup_subset H _ h
Subgroup Orbit Membership Implies Group Orbit Membership
Informal description
For any subgroup $H$ of a group $G$ acting on a type $\alpha$, and for any elements $a, b \in \alpha$, if $a$ is in the orbit of $b$ under the action of $H$, then $a$ is also in the orbit of $b$ under the action of $G$. In other words, if $a \in H \cdot b$, then $a \in G \cdot b$.
MulAction.mem_orbit_symm theorem
{a₁ a₂ : α} : a₁ ∈ orbit G a₂ ↔ a₂ ∈ orbit G a₁
Full source 
@[to_additive]
lemma mem_orbit_symm {a₁ a₂ : α} : a₁ ∈ orbit G a₂a₁ ∈ orbit G a₂ ↔ a₂ ∈ orbit G a₁ := by
  simp_rw [← orbit_eq_iff, eq_comm]
Symmetry of Group Orbits: $a_1 \in G \cdot a_2 \leftrightarrow a_2 \in G \cdot a_1$
Informal description
For any two elements $a_1$ and $a_2$ in a type $\alpha$ acted upon by a group $G$, $a_1$ is in the orbit of $a_2$ under $G$ if and only if $a_2$ is in the orbit of $a_1$ under $G$. In other words, $a_1 \in \text{orbit}(G, a_2) \leftrightarrow a_2 \in \text{orbit}(G, a_1)$.
MulAction.mem_subgroup_orbit_iff theorem
{H : Subgroup G} {x : α} {a b : orbit G x} : a ∈ MulAction.orbit H b ↔ (a : α) ∈ MulAction.orbit H (b : α)
Full source 
@[to_additive]
lemma mem_subgroup_orbit_iff {H : Subgroup G} {x : α} {a b : orbit G x} :
    a ∈ MulAction.orbit H ba ∈ MulAction.orbit H b ↔ (a : α) ∈ MulAction.orbit H (b : α) := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rcases h with ⟨g, rfl⟩
    exact MulAction.mem_orbit _ g
  · rcases h with ⟨g, h⟩
    dsimp at h
    rw [subgroup_smul_def, ← orbit.coe_smul, ← Subtype.ext_iff] at h
    subst h
    exact MulAction.mem_orbit _ g
Subgroup Orbit Membership Equivalence: $a \in H \cdot b \leftrightarrow \overline{a} \in H \cdot \overline{b}$
Informal description
For any subgroup $H$ of a group $G$ acting on a type $\alpha$, and for any two elements $a$ and $b$ in the orbit of $x \in \alpha$ under $G$, the element $a$ is in the orbit of $b$ under the action of $H$ if and only if the underlying elements of $\alpha$ satisfy the same condition. That is, $a \in \text{orbit}(H, b) \leftrightarrow \overline{a} \in \text{orbit}(H, \overline{b})$, where $\overline{a}$ and $\overline{b}$ denote the projections of $a$ and $b$ in $\alpha$.
MulAction.orbitRel definition
: Setoid α
Full source 
/-- The relation 'in the same orbit'. -/
@[to_additive "The relation 'in the same orbit'."]
def orbitRel : Setoid α where
  r a b := a ∈ orbit G b
  iseqv :=
    ⟨mem_orbit_self, fun {a b} => by simp [orbit_eq_iff.symm, eq_comm], fun {a b} => by
      simp +contextual [orbit_eq_iff.symm, eq_comm]⟩
Orbit equivalence relation
Informal description
The equivalence relation on a type $\alpha$ induced by the action of a monoid $G$, where two elements $a$ and $b$ are related if and only if they are in the same orbit under the action of $G$. In other words, $a$ and $b$ are related if there exists some $g \in G$ such that $g \cdot a = b$.
MulAction.orbitRel_apply theorem
{a b : α} : orbitRel G α a b ↔ a ∈ orbit G b
Full source 
@[to_additive]
theorem orbitRel_apply {a b : α} : orbitRelorbitRel G α a b ↔ a ∈ orbit G b :=
  Iff.rfl
Characterization of Orbit Relation: $a \sim b$ iff $a \in G \cdot b$
Informal description
For any two elements $a$ and $b$ in a type $\alpha$ with a monoid action by $G$, the relation $\text{orbitRel}\,G\,\alpha\,a\,b$ holds if and only if $a$ belongs to the orbit of $b$ under the action of $G$. In other words, $a$ is related to $b$ under the orbit equivalence relation if and only if there exists some $g \in G$ such that $g \cdot b = a$.
MulAction.quotient_preimage_image_eq_union_mul theorem
(U : Set α) : letI := orbitRel G α Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ g : G, (g • ·) '' U
Full source 
/-- 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`. -/
@[to_additive
      "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 quotient_preimage_image_eq_union_mul (U : Set α) :
    letI := orbitRel G α
    Quotient.mk'Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ g : G, (g • ·) '' U := by
  letI := orbitRel G α
  set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'
  ext a
  constructor
  · rintro ⟨b, hb, hab⟩
    obtain ⟨g, rfl⟩ := Quotient.exact hab
    rw [Set.mem_iUnion]
    exact ⟨g⁻¹, g • a, hb, inv_smul_smul g a⟩
  · intro hx
    rw [Set.mem_iUnion] at hx
    obtain ⟨g, u, hu₁, hu₂⟩ := hx
    rw [Set.mem_preimage, Set.mem_image]
    refine ⟨g⁻¹ • a, ?_, by simp [f, orbitRel, Quotient.eq']⟩
    rw [← hu₂]
    convert hu₁
    simp only [inv_smul_smul]
Preimage of Quotient Image Equals Union of Group Translates
Informal description
Let $G$ be a group acting on a set $\alpha$, and let $U \subseteq \alpha$. The preimage of the image of $U$ under the quotient map $\alpha \to \alpha/G$ is equal to the union of all translates of $U$ by elements of $G$, i.e., \[ \pi^{-1}(\pi(U)) = \bigcup_{g \in G} g \cdot U, \] where $\pi: \alpha \to \alpha/G$ is the quotient map and $g \cdot U = \{g \cdot x \mid x \in U\}$.
MulAction.disjoint_image_image_iff theorem
{U V : Set α} : letI := orbitRel G α Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ g : G, g • x ∉ V
Full source 
@[to_additive]
theorem disjoint_image_image_iff {U V : Set α} :
    letI := orbitRel G α
    DisjointDisjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ g : G, g • x ∉ V := by
  letI := orbitRel G α
  set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'
  refine
    ⟨fun h a a_in_U g g_in_V =>
      h.le_bot ⟨⟨a, a_in_U, Quotient.sound ⟨g⁻¹, ?_⟩⟩, ⟨g • a, g_in_V, rfl⟩⟩, ?_⟩
  · simp
  · intro h
    rw [Set.disjoint_left]
    rintro _ ⟨b, hb₁, hb₂⟩ ⟨c, hc₁, hc₂⟩
    obtain ⟨g, rfl⟩ := Quotient.exact (hc₂.trans hb₂.symm)
    exact h b hb₁ g hc₁
Disjointness of Quotient Images under Group Action
Informal description
Let $G$ be a group acting on a set $\alpha$, and let $U, V \subseteq \alpha$. The images of $U$ and $V$ under the quotient map $\alpha \to \alpha / G$ are disjoint if and only if for every $x \in U$ and every $g \in G$, the action of $g$ on $x$ does not lie in $V$. In other words, the sets $\{g \cdot x \mid g \in G, x \in U\}$ and $V$ are disjoint.
MulAction.image_inter_image_iff theorem
(U V : Set α) : letI := orbitRel G α Quotient.mk' '' U ∩ Quotient.mk' '' V = ∅ ↔ ∀ x ∈ U, ∀ g : G, g • x ∉ V
Full source 
@[to_additive]
theorem image_inter_image_iff (U V : Set α) :
    letI := orbitRel G α
    Quotient.mk'Quotient.mk' '' UQuotient.mk' '' U ∩ Quotient.mk' '' VQuotient.mk' '' U ∩ Quotient.mk' '' V = ∅ ↔ ∀ x ∈ U, ∀ g : G, g • x ∉ V :=
  Set.disjoint_iff_inter_eq_empty.symm.trans disjoint_image_image_iff
Disjointness of Quotient Images under Group Action
Informal description
Let $G$ be a group acting on a set $\alpha$, and let $U, V \subseteq \alpha$. The images of $U$ and $V$ under the quotient map $\alpha \to \alpha/G$ are disjoint if and only if for every $x \in U$ and every $g \in G$, the action of $g$ on $x$ does not lie in $V$. In other words, the intersection $\pi(U) \cap \pi(V) = \emptyset$ if and only if for all $x \in U$ and $g \in G$, we have $g \cdot x \notin V$, where $\pi: \alpha \to \alpha/G$ is the quotient map.
MulAction.orbitRel.Quotient abbrev
: Type _
Full source 
/-- The quotient by `MulAction.orbitRel`, given a name to enable dot notation. -/
@[to_additive
    "The quotient by `AddAction.orbitRel`, given a name to enable dot notation."]
abbrev orbitRel.Quotient : Type _ :=
  _root_.Quotient <| orbitRel G α
Quotient by Group Action Orbit Relation
Informal description
The quotient type $\alpha/G$ obtained by taking the quotient of $\alpha$ by the orbit equivalence relation induced by the action of a monoid $G$ on $\alpha$. Here, two elements $a, b \in \alpha$ are equivalent if they lie in the same $G$-orbit, i.e., there exists $g \in G$ such that $g \cdot a = b$.
MulAction.orbitRel.Quotient.orbit definition
(x : orbitRel.Quotient G α) : Set α
Full source 
/-- The orbit corresponding to an element of the quotient by `MulAction.orbitRel` -/
@[to_additive "The orbit corresponding to an element of the quotient by `AddAction.orbitRel`"]
nonrec def orbitRel.Quotient.orbit (x : orbitRel.Quotient G α) : Set α :=
  Quotient.liftOn' x (orbit G) fun _ _ => MulAction.orbit_eq_iff.2
Orbit of a quotient element under group action
Informal description
Given a quotient element \( x \) of \( \alpha \) under the orbit equivalence relation induced by the action of a monoid \( G \), the function returns the orbit of \( x \), which is the set of all elements in \( \alpha \) that are equivalent to \( x \) under this relation. In other words, it is the set of all elements reachable from any representative of \( x \) via the action of \( G \).
MulAction.orbitRel.Quotient.orbit_mk theorem
(a : α) : orbitRel.Quotient.orbit (Quotient.mk'' a : orbitRel.Quotient G α) = MulAction.orbit G a
Full source 
@[to_additive (attr := simp)]
theorem orbitRel.Quotient.orbit_mk (a : α) :
    orbitRel.Quotient.orbit (Quotient.mk'' a : orbitRel.Quotient G α) = MulAction.orbit G a :=
  rfl
Orbit of Quotient Class Equals Orbit of Element
Informal description
For any element $a$ in a type $\alpha$ acted upon by a monoid $G$, the orbit of the equivalence class of $a$ in the quotient $\alpha/G$ (under the orbit equivalence relation) is equal to the orbit of $a$ under the action of $G$. In other words, \[ \text{orbit}(\overline{a}) = G \cdot a \] where $\overline{a}$ denotes the equivalence class of $a$ in $\alpha/G$.
MulAction.orbitRel.Quotient.mem_orbit theorem
{a : α} {x : orbitRel.Quotient G α} : a ∈ x.orbit ↔ Quotient.mk'' a = x
Full source 
@[to_additive]
theorem orbitRel.Quotient.mem_orbit {a : α} {x : orbitRel.Quotient G α} :
    a ∈ x.orbita ∈ x.orbit ↔ Quotient.mk'' a = x := by
  induction x using Quotient.inductionOn'
  rw [Quotient.eq'']
  rfl
Characterization of Membership in Quotient Orbit
Informal description
For an element $a$ in a type $\alpha$ acted upon by a monoid $G$, and for an element $x$ in the quotient $\alpha/G$ under the orbit equivalence relation, $a$ belongs to the orbit of $x$ if and only if the equivalence class of $a$ in $\alpha/G$ equals $x$. In other words, \[ a \in x.\text{orbit} \leftrightarrow \overline{a} = x \] where $\overline{a}$ denotes the equivalence class of $a$ in $\alpha/G$.
MulAction.orbitRel.Quotient.orbit_eq_orbit_out theorem
(x : orbitRel.Quotient G α) {φ : orbitRel.Quotient G α → α} (hφ : letI := orbitRel G α; RightInverse φ Quotient.mk') : orbitRel.Quotient.orbit x = MulAction.orbit G (φ x)
Full source 
/-- Note that `hφ = Quotient.out_eq'` is a useful choice here. -/
@[to_additive "Note that `hφ = Quotient.out_eq'` is a useful choice here."]
theorem orbitRel.Quotient.orbit_eq_orbit_out (x : orbitRel.Quotient G α)
    {φ : orbitRel.Quotient G α → α} (hφ : letI := orbitRel G α; RightInverse φ Quotient.mk') :
    orbitRel.Quotient.orbit x = MulAction.orbit G (φ x) := by
  conv_lhs => rw [← hφ x]
  rfl
Orbit of Quotient Element Equals Orbit of Representative
Informal description
Let $G$ be a monoid acting on a type $\alpha$, and let $\alpha/G$ be the quotient of $\alpha$ by the orbit equivalence relation. For any element $x \in \alpha/G$ and any right inverse $\varphi \colon \alpha/G \to \alpha$ of the quotient map $\text{Quotient.mk}' \colon \alpha \to \alpha/G$, the orbit of $x$ in $\alpha/G$ is equal to the orbit of $\varphi(x)$ in $\alpha$ under the action of $G$. That is, \[ \text{orbitRel.Quotient.orbit}(x) = \text{MulAction.orbit}(G, \varphi(x)). \]
MulAction.orbitRel.Quotient.orbit_injective theorem
: Injective (orbitRel.Quotient.orbit : orbitRel.Quotient G α → Set α)
Full source 
@[to_additive]
lemma orbitRel.Quotient.orbit_injective :
    Injective (orbitRel.Quotient.orbit : orbitRel.Quotient G α → Set α) := by
  intro x y h
  simp_rw [orbitRel.Quotient.orbit_eq_orbit_out _ Quotient.out_eq', orbit_eq_iff,
    ← orbitRel_apply] at h
  simpa [← Quotient.eq''] using h
Injectivity of the Orbit Map on the Quotient Space $\alpha/G$
Informal description
The function that maps each element $x$ in the quotient $\alpha/G$ of a type $\alpha$ by the orbit equivalence relation induced by a monoid action of $G$ to its orbit $x.\text{orbit}$ is injective. In other words, if two elements $x, y \in \alpha/G$ have the same orbit, then $x = y$.
MulAction.orbitRel.Quotient.orbit_inj theorem
{x y : orbitRel.Quotient G α} : x.orbit = y.orbit ↔ x = y
Full source 
@[to_additive (attr := simp)]
lemma orbitRel.Quotient.orbit_inj {x y : orbitRel.Quotient G α} : x.orbit = y.orbit ↔ x = y :=
  orbitRel.Quotient.orbit_injective.eq_iff
Injectivity of Orbit Map in Quotient Space: $x.\text{orbit} = y.\text{orbit} \leftrightarrow x = y$
Informal description
For any two elements $x$ and $y$ in the quotient space $\alpha/G$ under the orbit equivalence relation induced by a monoid action of $G$ on $\alpha$, the orbits of $x$ and $y$ are equal if and only if $x = y$. In other words, the map sending each element of $\alpha/G$ to its orbit is injective.
MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq theorem
{H : Subgroup G} {a b : α} (h : (⟦a⟧ : orbitRel.Quotient H α) = ⟦b⟧) : (⟦a⟧ : orbitRel.Quotient G α) = ⟦b⟧
Full source 
@[to_additive]
lemma orbitRel.quotient_eq_of_quotient_subgroup_eq {H : Subgroup G} {a b : α}
    (h : (⟦a⟧ : orbitRel.Quotient H α) = ⟦b⟧) : (⟦a⟧ : orbitRel.Quotient G α) = ⟦b⟧ := by
  rw [@Quotient.eq] at h ⊢
  exact mem_orbit_of_mem_orbit_subgroup h
Subgroup Orbit Equality Implies Group Orbit Equality
Informal description
Let $H$ be a subgroup of a group $G$ acting on a type $\alpha$, and let $a, b \in \alpha$. If the equivalence classes of $a$ and $b$ under the orbit relation of $H$ are equal, then their equivalence classes under the orbit relation of $G$ are also equal. In other words, if $a$ and $b$ are in the same $H$-orbit, then they are in the same $G$-orbit.
MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq' theorem
{H : Subgroup G} {a b : α} (h : (Quotient.mk'' a : orbitRel.Quotient H α) = Quotient.mk'' b) : (Quotient.mk'' a : orbitRel.Quotient G α) = Quotient.mk'' b
Full source 
@[to_additive]
lemma orbitRel.quotient_eq_of_quotient_subgroup_eq' {H : Subgroup G} {a b : α}
    (h : (Quotient.mk'' a : orbitRel.Quotient H α) = Quotient.mk'' b) :
    (Quotient.mk'' a : orbitRel.Quotient G α) = Quotient.mk'' b :=
  orbitRel.quotient_eq_of_quotient_subgroup_eq h
Subgroup Orbit Equality Implies Group Orbit Equality
Informal description
Let $H$ be a subgroup of a group $G$ acting on a set $\alpha$, and let $a, b \in \alpha$. If the equivalence classes of $a$ and $b$ under the orbit relation of $H$ are equal, then their equivalence classes under the orbit relation of $G$ are also equal. In other words, if $a$ and $b$ are in the same $H$-orbit, then they are in the same $G$-orbit.
MulAction.orbitRel.Quotient.orbit_nonempty theorem
(x : orbitRel.Quotient G α) : Set.Nonempty x.orbit
Full source 
@[to_additive]
nonrec lemma orbitRel.Quotient.orbit_nonempty (x : orbitRel.Quotient G α) :
    Set.Nonempty x.orbit := by
  rw [orbitRel.Quotient.orbit_eq_orbit_out x Quotient.out_eq']
  exact orbit_nonempty _
Nonemptiness of Orbits in Quotient Space under Monoid Action
Informal description
For any element $x$ in the quotient space $\alpha/G$ under the orbit equivalence relation induced by a monoid action of $G$ on $\alpha$, the orbit of $x$ is nonempty. That is, the set $\{g \cdot a \mid g \in G\}$ is nonempty for any representative $a$ of $x$.
MulAction.orbitRel.Quotient.mapsTo_smul_orbit theorem
(g : G) (x : orbitRel.Quotient G α) : Set.MapsTo (g • ·) x.orbit x.orbit
Full source 
@[to_additive]
nonrec lemma orbitRel.Quotient.mapsTo_smul_orbit (g : G) (x : orbitRel.Quotient G α) :
    Set.MapsTo (g • ·) x.orbit x.orbit := by
  rw [orbitRel.Quotient.orbit_eq_orbit_out x Quotient.out_eq']
  exact mapsTo_smul_orbit g x.out
Monoid Action Preserves Quotient Orbit
Informal description
For any element $g$ of a monoid $G$ acting on a type $\alpha$, and any element $x$ in the quotient $\alpha/G$ by the orbit equivalence relation, the function $y \mapsto g \cdot y$ maps the orbit of $x$ into itself. In other words, if $y$ is in the orbit of $x$, then $g \cdot y$ is also in the orbit of $x$.
MulAction.instElemOrbit_1 instance
(x : orbitRel.Quotient G α) : MulAction G x.orbit
Full source 
@[to_additive]
instance (x : orbitRel.Quotient G α) : MulAction G x.orbit where
  smul g := (orbitRel.Quotient.mapsTo_smul_orbit g x).restrict _ _ _
  one_smul a := Subtype.ext (one_smul G (a : α))
  mul_smul g g' a' := Subtype.ext (mul_smul g g' (a' : α))
Group Action on Orbits in Quotient Space
Informal description
For any quotient element $x$ of $\alpha$ under the orbit equivalence relation induced by a monoid action of $G$ on $\alpha$, the orbit of $x$ carries a natural $G$-action. Specifically, for any $g \in G$ and $a$ in the orbit of $x$, the action $g \cdot a$ is well-defined and preserves the orbit.
MulAction.orbitRel.Quotient.orbit.coe_smul theorem
{g : G} {x : orbitRel.Quotient G α} {a : x.orbit} : ↑(g • a) = g • (a : α)
Full source 
@[to_additive (attr := simp)]
lemma orbitRel.Quotient.orbit.coe_smul {g : G} {x : orbitRel.Quotient G α} {a : x.orbit} :
    ↑(g • a) = g • (a : α) :=
  rfl
Compatibility of Group Action with Orbit Quotient Projection
Informal description
For any element $g$ in a group $G$ acting on a type $\alpha$, any element $x$ in the quotient $\alpha/G$ by the orbit equivalence relation, and any element $a$ in the orbit of $x$, the image of $g \cdot a$ under the canonical projection to $\alpha$ equals the action of $g$ on the image of $a$ in $\alpha$. In other words, the following diagram commutes: $$(g \cdot a) \mapsto g \cdot (a : \alpha)$$
MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff theorem
{H : Subgroup G} {x : orbitRel.Quotient G α} {a b : x.orbit} : (a : α) ∈ MulAction.orbit H (b : α) ↔ a ∈ MulAction.orbit H b
Full source 
@[to_additive (attr := norm_cast, simp)]
lemma orbitRel.Quotient.mem_subgroup_orbit_iff {H : Subgroup G} {x : orbitRel.Quotient G α}
    {a b : x.orbit} : (a : α) ∈ MulAction.orbit H (b : α)(a : α) ∈ MulAction.orbit H (b : α) ↔ a ∈ MulAction.orbit H b := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rcases h with ⟨g, h⟩
    dsimp at h
    rw [subgroup_smul_def, ← orbit.coe_smul, ← Subtype.ext_iff] at h
    subst h
    exact MulAction.mem_orbit _ g
  · rcases h with ⟨g, rfl⟩
    exact MulAction.mem_orbit _ g
Equivalence of Subgroup Orbit Membership in Quotient and Original Space
Informal description
Let $G$ be a group acting on a type $\alpha$, and let $H$ be a subgroup of $G$. For any two elements $a$ and $b$ in the same orbit of $x \in \alpha/G$, the element $a$ (considered as an element of $\alpha$) lies in the $H$-orbit of $b$ (considered as an element of $\alpha$) if and only if $a$ lies in the $H$-orbit of $b$ (considered as elements of the orbit of $x$).
MulAction.orbitRel.Quotient.subgroup_quotient_eq_iff theorem
{H : Subgroup G} {x : orbitRel.Quotient G α} {a b : x.orbit} : (⟦a⟧ : orbitRel.Quotient H x.orbit) = ⟦b⟧ ↔ (⟦↑a⟧ : orbitRel.Quotient H α) = ⟦↑b⟧
Full source 
@[to_additive]
lemma orbitRel.Quotient.subgroup_quotient_eq_iff {H : Subgroup G} {x : orbitRel.Quotient G α}
    {a b : x.orbit} : (⟦a⟧ : orbitRel.Quotient H x.orbit) = ⟦b⟧ ↔
      (⟦↑a⟧ : orbitRel.Quotient H α) = ⟦↑b⟧ := by
  simp_rw [← @Quotient.mk''_eq_mk, Quotient.eq'']
  exact orbitRel.Quotient.mem_subgroup_orbit_iff.symm
Equivalence of Subgroup Quotient Relations in Orbit and Original Space
Informal description
Let $G$ be a group acting on a type $\alpha$, and let $H$ be a subgroup of $G$. For any two elements $a$ and $b$ in the same orbit $x \in \alpha/G$, the equivalence classes of $a$ and $b$ in the quotient of the orbit of $x$ by the action of $H$ are equal if and only if their equivalence classes in the quotient of $\alpha$ by the action of $H$ are equal. In other words, the following equivalence holds: $$ [a]_{H} = [b]_{H} \text{ in } x.orbit/H \leftrightarrow [a]_{H} = [b]_{H} \text{ in } \alpha/H $$
MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff' theorem
{H : Subgroup G} {x : orbitRel.Quotient G α} {a b : x.orbit} {c : α} (h : (⟦a⟧ : orbitRel.Quotient H x.orbit) = ⟦b⟧) : (a : α) ∈ MulAction.orbit H c ↔ (b : α) ∈ MulAction.orbit H c
Full source 
@[to_additive]
lemma orbitRel.Quotient.mem_subgroup_orbit_iff' {H : Subgroup G} {x : orbitRel.Quotient G α}
    {a b : x.orbit} {c : α} (h : (⟦a⟧ : orbitRel.Quotient H x.orbit) = ⟦b⟧) :
    (a : α) ∈ MulAction.orbit H c(a : α) ∈ MulAction.orbit H c ↔ (b : α) ∈ MulAction.orbit H c := by
  simp_rw [mem_orbit_symm (a₂ := c)]
  convert Iff.rfl using 2
  rw [orbit_eq_iff]
  suffices hb : ↑b ∈ orbitRel.Quotient.orbit (⟦a⟧ : orbitRel.Quotient H x.orbit) by
    rw [orbitRel.Quotient.orbit_eq_orbit_out (⟦a⟧ : orbitRel.Quotient H x.orbit) Quotient.out_eq']
       at hb
    rw [orbitRel.Quotient.mem_subgroup_orbit_iff]
    convert hb using 1
    rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]
  rw [orbitRel.Quotient.mem_orbit, h, @Quotient.mk''_eq_mk]
Equivalence of Subgroup Orbit Membership for Equivalent Elements in Quotient Space
Informal description
Let $G$ be a group acting on a type $\alpha$, and let $H$ be a subgroup of $G$. For any two elements $a$ and $b$ in the same orbit $x \in \alpha/G$, if $a$ and $b$ are equivalent in the quotient of the orbit of $x$ by the action of $H$ (i.e., $[a]_H = [b]_H$ in $x.orbit/H$), then for any element $c \in \alpha$, $a$ lies in the $H$-orbit of $c$ if and only if $b$ lies in the $H$-orbit of $c$. In other words, $$ a \in H \cdot c \leftrightarrow b \in H \cdot c. $$
MulAction.selfEquivSigmaOrbits' definition
: α ≃ Σ ω : Ω, ω.orbit
Full source 
/-- 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`. -/
@[to_additive
      "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`. "]
def selfEquivSigmaOrbits' : α ≃ Σω : Ω, ω.orbit :=
  letI := orbitRel G α
  calc
    α ≃ Σω : Ω, { a // Quotient.mk' a = ω } := (Equiv.sigmaFiberEquiv Quotient.mk').symm
    _ ≃ Σω : Ω, ω.orbit :=
      Equiv.sigmaCongrRight fun _ =>
        Equiv.subtypeEquivRight fun _ => orbitRel.Quotient.mem_orbit.symm
Equivalence between a type and the disjoint union of its orbits under a group action
Informal description
Given a type $\alpha$ with an action by a group $G$, there is a natural equivalence between $\alpha$ and the disjoint union of all orbits under this action. Specifically, $\alpha$ is equivalent to the sigma type $\Sigma \omega \in \Omega, \omega.\text{orbit}$, where $\Omega$ is the quotient of $\alpha$ by the orbit equivalence relation and $\omega.\text{orbit}$ is the orbit corresponding to the equivalence class $\omega$.
MulAction.selfEquivSigmaOrbits definition
: α ≃ Σ ω : Ω, orbit G ω.out
Full source 
/-- Decomposition of a type `X` as a disjoint union of its orbits under a group action. -/
@[to_additive
      "Decomposition of a type `X` as a disjoint union of its orbits under an additive group
      action."]
def selfEquivSigmaOrbits : α ≃ Σω : Ω, orbit G ω.out :=
  (selfEquivSigmaOrbits' G α).trans <|
    Equiv.sigmaCongrRight fun _ =>
      Equiv.setCongr <| orbitRel.Quotient.orbit_eq_orbit_out _ Quotient.out_eq'
Equivalence between a type and the disjoint union of its orbits under a group action
Informal description
Given a type $\alpha$ with an action by a group $G$, there is a natural equivalence between $\alpha$ and the disjoint union of all orbits under this action. Specifically, $\alpha$ is equivalent to the sigma type $\Sigma \omega \in \Omega, \text{orbit}(G, \omega.\text{out})$, where $\Omega$ is the quotient of $\alpha$ by the orbit equivalence relation and $\omega.\text{out}$ is a representative of the equivalence class $\omega$.
MulAction.univ_eq_iUnion_orbit theorem
: Set.univ (α := α) = ⋃ x : Ω, x.orbit
Full source 
/-- Decomposition of a type `X` as a disjoint union of its orbits under a group action.
Phrased as a set union. See `MulAction.selfEquivSigmaOrbits` for the type isomorphism. -/
@[to_additive "Decomposition of a type `X` as a disjoint union of its orbits under an additive group
action. Phrased as a set union. See `AddAction.selfEquivSigmaOrbits` for the type isomorphism."]
lemma univ_eq_iUnion_orbit :
    Set.univ (α := α) = ⋃ x : Ω, x.orbit := by
  ext x
  simp only [Set.mem_univ, Set.mem_iUnion, true_iff]
  exact ⟨Quotient.mk'' x, by simp⟩
Decomposition of a Type into Orbits under Group Action
Informal description
For a type $\alpha$ acted upon by a group $G$, the universal set of $\alpha$ is equal to the union of all orbits under the action of $G$. That is, $\alpha = \bigcup_{x \in \Omega} \text{orbit}(x)$, where $\Omega$ is the quotient of $\alpha$ by the orbit equivalence relation.
MulAction.stabilizer definition
(a : α) : Subgroup G
Full source 
/-- The stabilizer of an element under an action, i.e. what sends the element to itself.
A subgroup. -/
@[to_additive
      "The stabilizer of an element under an action, i.e. what sends the element to itself.
      An additive subgroup."]
def stabilizer (a : α) : Subgroup G :=
  { stabilizerSubmonoid G a with
    inv_mem' := fun {m} (ha : m • a = a) => show m⁻¹ • a = a by rw [inv_smul_eq_iff, ha] }
Stabilizer subgroup of a point under group action
Informal description
For a group $G$ acting on a type $\alpha$, the stabilizer subgroup of a point $a \in \alpha$ is the subgroup of $G$ consisting of all elements $g \in G$ that fix $a$ under the action, i.e., $g \cdot a = a$.
MulAction.instDecidablePredMemSubgroupStabilizerOfDecidableEq instance
[DecidableEq α] (a : α) : DecidablePred (· ∈ stabilizer G a)
Full source 
@[to_additive]
instance [DecidableEq α] (a : α) : DecidablePred (· ∈ stabilizer G a) :=
  fun _ => inferInstanceAs <| Decidable (_ = _)
Decidability of Stabilizer Subgroup Membership for Group Actions
Informal description
For a group $G$ acting on a type $\alpha$ with decidable equality, and for any point $a \in \alpha$, the membership predicate in the stabilizer subgroup $\text{Stab}_G(a)$ is decidable. That is, given $g \in G$, we can algorithmically determine whether $g$ fixes $a$ under the group action (i.e., whether $g \cdot a = a$).
MulAction.mem_stabilizer_iff theorem
{a : α} {g : G} : g ∈ stabilizer G a ↔ g • a = a
Full source 
@[to_additive (attr := simp)]
theorem mem_stabilizer_iff {a : α} {g : G} : g ∈ stabilizer G ag ∈ stabilizer G a ↔ g • a = a :=
  Iff.rfl
Characterization of Stabilizer Subgroup Membership: $g \in \text{Stab}_G(a) \leftrightarrow g \cdot a = a$
Informal description
For a group $G$ acting on a type $\alpha$, an element $g \in G$ belongs to the stabilizer subgroup of a point $a \in \alpha$ if and only if the action of $g$ fixes $a$, i.e., $g \cdot a = a$.
MulAction.le_stabilizer_smul_left theorem
[SMul α β] [IsScalarTower G α β] (a : α) (b : β) : stabilizer G a ≤ stabilizer G (a • b)
Full source 
@[to_additive]
lemma le_stabilizer_smul_left [SMul α β] [IsScalarTower G α β] (a : α) (b : β) :
    stabilizer G a ≤ stabilizer G (a • b) := by
  simp_rw [SetLike.le_def, mem_stabilizer_iff, ← smul_assoc]; rintro a h; rw [h]
Stabilizer containment under scalar multiplication in a scalar tower
Informal description
Let $G$ be a group acting on types $\alpha$ and $\beta$, with $\alpha$ having a scalar multiplication operation on $\beta$ that forms a scalar tower with the $G$-actions. For any $a \in \alpha$ and $b \in \beta$, the stabilizer subgroup of $a$ under the $G$-action is contained in the stabilizer subgroup of $a \cdot b$ under the $G$-action. In other words, if $g \in G$ fixes $a$, then it also fixes $a \cdot b$.
MulAction.le_stabilizer_smul_right theorem
{G'} [Group G'] [SMul α β] [MulAction G' β] [SMulCommClass G' α β] (a : α) (b : β) : stabilizer G' b ≤ stabilizer G' (a • b)
Full source 
@[to_additive]
lemma le_stabilizer_smul_right {G'} [Group G'] [SMul α β] [MulAction G' β]
    [SMulCommClass G' α β] (a : α) (b : β) :
    stabilizer G' b ≤ stabilizer G' (a • b) := by
  simp_rw [SetLike.le_def, mem_stabilizer_iff, smul_comm]; rintro a h; rw [h]
Stabilizer containment under commuting scalar multiplication
Informal description
Let $G'$ be a group acting on a type $\beta$, and let $\alpha$ be another type with a scalar multiplication operation on $\beta$ such that the actions of $G'$ and $\alpha$ on $\beta$ commute. For any $a \in \alpha$ and $b \in \beta$, the stabilizer subgroup of $b$ under the action of $G'$ is contained in the stabilizer subgroup of $a \cdot b$ under the action of $G'$. In other words, if $g \in G'$ fixes $b$, then it also fixes $a \cdot b$.
MulAction.stabilizer_smul_eq_left theorem
[SMul α β] [IsScalarTower G α β] (a : α) (b : β) (h : Injective (· • b : α → β)) : stabilizer G (a • b) = stabilizer G a
Full source 
@[to_additive (attr := simp)]
lemma stabilizer_smul_eq_left [SMul α β] [IsScalarTower G α β] (a : α) (b : β)
    (h : Injective (· • b : α → β)) : stabilizer G (a • b) = stabilizer G a := by
  refine (le_stabilizer_smul_left _ _).antisymm' fun a ha ↦ ?_
  simpa only [mem_stabilizer_iff, ← smul_assoc, h.eq_iff] using ha
Stabilizer Equality under Scalar Multiplication with Injective Condition: $G_{a \cdot b} = G_a$
Informal description
Let $G$ be a group acting on types $\alpha$ and $\beta$, with $\alpha$ having a scalar multiplication operation on $\beta$ that forms a scalar tower with the $G$-actions. For any $a \in \alpha$ and $b \in \beta$, if the map $x \mapsto x \cdot b$ from $\alpha$ to $\beta$ is injective, then the stabilizer subgroup of $a \cdot b$ under the $G$-action is equal to the stabilizer subgroup of $a$ under the $G$-action. In other words, $G_{a \cdot b} = G_a$ where $G_x$ denotes the stabilizer of $x$.
MulAction.stabilizer_smul_eq_right theorem
{α} [Group α] [MulAction α β] [SMulCommClass G α β] (a : α) (b : β) : stabilizer G (a • b) = stabilizer G b
Full source 
@[to_additive (attr := simp)]
lemma stabilizer_smul_eq_right {α} [Group α] [MulAction α β] [SMulCommClass G α β] (a : α) (b : β) :
    stabilizer G (a • b) = stabilizer G b :=
  (le_stabilizer_smul_right _ _).antisymm' <| (le_stabilizer_smul_right a⁻¹ _).trans_eq <| by
    rw [inv_smul_smul]
Stabilizer Equality under Commuting Scalar Multiplication: $G_{a \cdot b} = G_b$
Informal description
Let $G$ be a group acting on a type $\beta$, and let $\alpha$ be another group acting on $\beta$ such that the actions of $G$ and $\alpha$ on $\beta$ commute. For any $a \in \alpha$ and $b \in \beta$, the stabilizer subgroup of $a \cdot b$ under the action of $G$ is equal to the stabilizer subgroup of $b$ under the action of $G$, i.e., $G_{a \cdot b} = G_b$.
MulAction.stabilizer_mul_eq_left theorem
[Group α] [IsScalarTower G α α] (a b : α) : stabilizer G (a * b) = stabilizer G a
Full source 
@[to_additive (attr := simp)]
lemma stabilizer_mul_eq_left [Group α] [IsScalarTower G α α] (a b : α)  :
    stabilizer G (a * b) = stabilizer G a := stabilizer_smul_eq_left a _ <| mul_left_injective _
Stabilizer Equality under Left Multiplication: $\text{stabilizer}_G(a \cdot b) = \text{stabilizer}_G(a)$
Informal description
Let $G$ be a group acting on a group $\alpha$ such that the action of $G$ on $\alpha$ forms a scalar tower with the multiplication in $\alpha$. For any elements $a, b \in \alpha$, the stabilizer subgroup of $a \cdot b$ under the action of $G$ is equal to the stabilizer subgroup of $a$ under the action of $G$, i.e., $\text{stabilizer}_G(a \cdot b) = \text{stabilizer}_G(a)$.
MulAction.stabilizer_mul_eq_right theorem
[Group α] [SMulCommClass G α α] (a b : α) : stabilizer G (a * b) = stabilizer G b
Full source 
@[to_additive (attr := simp)]
lemma stabilizer_mul_eq_right [Group α] [SMulCommClass G α α] (a b : α) :
    stabilizer G (a * b) = stabilizer G b := stabilizer_smul_eq_right a _
Stabilizer Equality under Right Multiplication: $G_{a \cdot b} = G_b$
Informal description
Let $G$ be a group acting on a group $\alpha$ such that the actions of $G$ and $\alpha$ on $\alpha$ commute. For any elements $a, b \in \alpha$, the stabilizer subgroup of $a \cdot b$ under the action of $G$ is equal to the stabilizer subgroup of $b$ under the action of $G$, i.e., $G_{a \cdot b} = G_b$.