Mathlib.GroupTheory.GroupAction.Basic

MulAction.fst_mem_orbit_of_mem_orbit theorem

{x y : α × β} (h : x ∈ MulAction.orbit M y) : x.1 ∈ MulAction.orbit M y.1

Full source

@[to_additive]
lemma fst_mem_orbit_of_mem_orbit {x y : α × β} (h : x ∈ MulAction.orbit M y) :
    x.1 ∈ MulAction.orbit M y.1 := by
  rcases h with ⟨g, rfl⟩
  exact mem_orbit _ _

First Component Preserves Orbit Membership under Monoid Action

Informal description

For any elements $x, y$ in the product type $\alpha \times \beta$, if $x$ is in the orbit of $y$ under the action of a monoid $M$, then the first component of $x$ is in the orbit of the first component of $y$ under the same action.

MulAction.snd_mem_orbit_of_mem_orbit theorem

{x y : α × β} (h : x ∈ MulAction.orbit M y) : x.2 ∈ MulAction.orbit M y.2

Full source

@[to_additive]
lemma snd_mem_orbit_of_mem_orbit {x y : α × β} (h : x ∈ MulAction.orbit M y) :
    x.2 ∈ MulAction.orbit M y.2 := by
  rcases h with ⟨g, rfl⟩
  exact mem_orbit _ _

Second Component Preserves Orbit Membership under Monoid Action

Informal description

For any elements $x, y$ in the product type $\alpha \times \beta$, if $x$ is in the orbit of $y$ under the action of a monoid $M$, then the second component of $x$ is in the orbit of the second component of $y$ under the same action.

Finite.finite_mulAction_orbit theorem

[Finite M] (a : α) : Set.Finite (orbit M a)

Full source

@[to_additive]
lemma _root_.Finite.finite_mulAction_orbit [Finite M] (a : α) : Set.Finite (orbit M a) :=
  Set.finite_range _

Finiteness of Orbits under Finite Monoid Action

Informal description

For a finite monoid $M$ acting on a type $\alpha$, the orbit of any element $a \in \alpha$ under the action of $M$ is a finite set.

MulAction.orbit_eq_univ theorem

[IsPretransitive M α] (a : α) : orbit M a = Set.univ

Full source

@[to_additive]
theorem orbit_eq_univ [IsPretransitive M α] (a : α) : orbit M a = Set.univ :=
  (surjective_smul M a).range_eq

Orbit Covers Entire Type under Transitive Action

Informal description

For a monoid $M$ acting transitively on a type $\alpha$, the orbit of any element $a \in \alpha$ under the action of $M$ is equal to the entire set $\alpha$. That is, $\text{orbit}_M(a) = \alpha$.

MulAction.subsingleton_orbit_iff_mem_fixedPoints theorem

{a : α} : (orbit M a).Subsingleton ↔ a ∈ fixedPoints M α

Full source

@[to_additive (attr := simp)]
theorem subsingleton_orbit_iff_mem_fixedPoints {a : α} :
    (orbit M a).Subsingleton ↔ a ∈ fixedPoints M α := by
  rw [mem_fixedPoints]
  constructor
  · exact fun h m ↦ h (mem_orbit a m) (mem_orbit_self a)
  · rintro h _ ⟨m, rfl⟩ y ⟨p, rfl⟩
    simp only [h]

Orbit is Subsingleton if and only if Element is Fixed Point

Informal description

For an element $a$ in a type $\alpha$ with a monoid action by $M$, the orbit of $a$ is a subsingleton (i.e., has at most one element) if and only if $a$ is a fixed point under the action of $M$, meaning $m \cdot a = a$ for all $m \in M$.

MulAction.mem_fixedPoints_iff_card_orbit_eq_one theorem

{a : α} [Fintype (orbit M a)] : a ∈ fixedPoints M α ↔ Fintype.card (orbit M a) = 1

Full source

@[to_additive mem_fixedPoints_iff_card_orbit_eq_one]
theorem mem_fixedPoints_iff_card_orbit_eq_one {a : α} [Fintype (orbit M a)] :
    a ∈ fixedPoints M αa ∈ fixedPoints M α ↔ Fintype.card (orbit M a) = 1 := by
  simp only [← subsingleton_orbit_iff_mem_fixedPoints, le_antisymm_iff,
    Fintype.card_le_one_iff_subsingleton, Nat.add_one_le_iff, Fintype.card_pos_iff,
    Set.subsingleton_coe, iff_self_and, Set.nonempty_coe_sort, orbit_nonempty, implies_true]

Fixed Point Characterization via Orbit Cardinality: $a \in \text{fixedPoints}(M, \alpha) \leftrightarrow |\text{orbit}(M, a)| = 1$

Informal description

For an element $a$ in a type $\alpha$ with a monoid action by $M$, and assuming the orbit of $a$ is finite, $a$ is a fixed point under the action of $M$ if and only if the cardinality of its orbit is 1. In other words, $a$ is fixed by all elements of $M$ if and only if its orbit $\{m \cdot a \mid m \in M\}$ is a singleton set.

MulAction.instDecidablePredMemSetFixedByOfDecidableEq instance

(m : M) [DecidableEq β] : DecidablePred fun b : β => b ∈ MulAction.fixedBy β m

Full source

@[to_additive instDecidablePredMemSetFixedByAddOfDecidableEq]
instance (m : M) [DecidableEq β] :
    DecidablePred fun b : β => b ∈ MulAction.fixedBy β m := fun b ↦ by
  simp only [MulAction.mem_fixedBy, Equiv.Perm.smul_def]
  infer_instance

Decidability of Fixed Points under Monoid Action

Informal description

For a monoid $M$ acting on a set $\beta$ with decidable equality, and for any element $m \in M$, the predicate "$b \in \text{fixedBy}(m)$" (i.e., $m \cdot b = b$) is decidable for any $b \in \beta$.

smul_cancel_of_non_zero_divisor theorem

 {M G : Type*} [Monoid M] [AddGroup G] [DistribMulAction M G] (k : M) (h : ∀ x : G, k • x = 0 → x = 0) {a b : G}
  (h' : k • a = k • b) : a = b

Full source

/-- `smul` by a `k : M` over a group is injective, if `k` is not a zero divisor.
The general theory of such `k` is elaborated by `IsSMulRegular`.
The typeclass that restricts all terms of `M` to have this property is `NoZeroSMulDivisors`. -/
theorem smul_cancel_of_non_zero_divisor {M G : Type*} [Monoid M] [AddGroup G]
    [DistribMulAction M G] (k : M) (h : ∀ x : G, k • x = 0 → x = 0) {a b : G} (h' : k • a = k • b) :
    a = b := by
  rw [← sub_eq_zero]
  refine h _ ?_
  rw [smul_sub, h', sub_self]

Cancellation Property of Non-Zero Divisors in Distributive Group Actions

Informal description

Let $M$ be a monoid acting distributively on an additive group $G$, and let $k \in M$ be a non-zero divisor (i.e., for all $x \in G$, if $k \cdot x = 0$ then $x = 0$). If $k \cdot a = k \cdot b$ for some $a, b \in G$, then $a = b$.

MulAction.fixedPoints_of_subsingleton theorem

[Subsingleton α] : fixedPoints G α = .univ

Full source

@[to_additive] theorem fixedPoints_of_subsingleton [Subsingleton α] :
    fixedPoints G α = .univ := by
  apply Set.eq_univ_of_forall
  simp only [mem_fixedPoints]
  intro x hx
  apply Subsingleton.elim ..

Fixed Points of Group Action on Subsingleton is Universal Set

Informal description

If the type $\alpha$ is a subsingleton (i.e., has at most one element), then the set of fixed points under the action of a group $G$ on $\alpha$ is equal to the universal set (the set of all elements of $\alpha$).

MulAction.nontrivial_of_fixedPoints_ne_univ theorem

(h : fixedPoints G α ≠ .univ) : Nontrivial α

Full source

/-- If a group acts nontrivially, then the type is nontrivial -/
@[to_additive "If a subgroup acts nontrivially, then the type is nontrivial."]
theorem nontrivial_of_fixedPoints_ne_univ (h : fixedPointsfixedPoints G α ≠ .univ) :
    Nontrivial α :=
  (subsingleton_or_nontrivial α).resolve_left fun _ ↦ h fixedPoints_of_subsingleton

Nontriviality of Type under Nontrivial Group Action

Informal description

If the set of fixed points of a group action of $G$ on $\alpha$ is not equal to the universal set (i.e., not all elements of $\alpha$ are fixed by every element of $G$), then the type $\alpha$ is nontrivial (i.e., contains at least two distinct elements).

MulAction.smul_orbit theorem

(g : G) (a : α) : g • orbit G a = orbit G a

Full source

@[to_additive (attr := simp)]
theorem smul_orbit (g : G) (a : α) : g • orbit G a = orbit G a :=
  (smul_orbit_subset g a).antisymm <|
    calc
      orbit G a = g • g⁻¹ • orbit G a := (smul_inv_smul _ _).symm
      _ ⊆ g • orbit G a := Set.image_subset _ (smul_orbit_subset _ _)

Group Action Preserves Orbit Equality

Informal description

For any element $g$ of a group $G$ acting on a type $\alpha$, and any element $a \in \alpha$, the action of $g$ on the orbit of $a$ under $G$ equals the orbit itself, i.e., $g \cdot \text{orbit}_G(a) = \text{orbit}_G(a)$.

MulAction.instIsPretransitiveElemOrbit instance

(a : α) : IsPretransitive G (orbit G a)

Full source

/-- The action of a group on an orbit is transitive. -/
@[to_additive "The action of an additive group on an orbit is transitive."]
instance (a : α) : IsPretransitive G (orbit G a) :=
  ⟨by
    rintro ⟨_, g, rfl⟩ ⟨_, h, rfl⟩
    use h * g⁻¹
    ext1
    simp [mul_smul]⟩

Transitivity of Group Action on Orbits

Informal description

For any monoid $G$ acting on a type $\alpha$ and any element $a \in \alpha$, the action of $G$ on the orbit of $a$ is transitive. That is, for any two elements $x, y$ in the orbit of $a$, there exists an element $g \in G$ such that $g \cdot x = y$.

MulAction.orbitRel_subgroup_le theorem

(H : Subgroup G) : orbitRel H α ≤ orbitRel G α

Full source

@[to_additive]
lemma orbitRel_subgroup_le (H : Subgroup G) : orbitRel H α ≤ orbitRel G α :=
  Setoid.le_def.2 mem_orbit_of_mem_orbit_subgroup

Subgroup Orbit Relation Refinement: $\text{orbitRel}_H \leq \text{orbitRel}_G$

Informal description

For any subgroup $H$ of a group $G$ acting on a type $\alpha$, the orbit equivalence relation induced by $H$ is finer than the orbit equivalence relation induced by $G$. That is, if two elements $a$ and $b$ in $\alpha$ are related under the action of $H$ (i.e., $a \in H \cdot b$), then they are also related under the action of $G$ (i.e., $a \in G \cdot b$).

MulAction.orbitRel_subgroupOf theorem

(H K : Subgroup G) : orbitRel (H.subgroupOf K) α = orbitRel (H ⊓ K : Subgroup G) α

Full source

@[to_additive]
lemma orbitRel_subgroupOf (H K : Subgroup G) :
    orbitRel (H.subgroupOf K) α = orbitRel (H ⊓ K : Subgroup G) α := by
  rw [← Subgroup.subgroupOf_map_subtype]
  ext x
  simp_rw [orbitRel_apply]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rcases h with ⟨⟨gv, gp⟩, rfl⟩
    simp only [Submonoid.mk_smul]
    refine mem_orbit _ (⟨gv, ?_⟩ : Subgroup.map K.subtype (H.subgroupOf K))
    simpa using gp
  · rcases h with ⟨⟨gv, gp⟩, rfl⟩
    simp only [Submonoid.mk_smul]
    simp only [Subgroup.subgroupOf_map_subtype, Subgroup.mem_inf] at gp
    refine mem_orbit _ (⟨⟨gv, ?_⟩, ?_⟩ : H.subgroupOf K)
    · exact gp.2
    · simp only [Subgroup.mem_subgroupOf]
      exact gp.1

Orbit Equivalence Relation for Intersection of Subgroups

Informal description

For any subgroups $H$ and $K$ of a group $G$ acting on a type $\alpha$, the orbit equivalence relation induced by the subgroup $H \cap K$ is equal to the orbit equivalence relation induced by the subgroup $H$ when restricted to $K$.

MulAction.pretransitive_iff_subsingleton_quotient theorem

: IsPretransitive G α ↔ Subsingleton (orbitRel.Quotient G α)

Full source

/-- An action is pretransitive if and only if the quotient by `MulAction.orbitRel` is a
subsingleton. -/
@[to_additive "An additive action is pretransitive if and only if the quotient by
`AddAction.orbitRel` is a subsingleton."]
theorem pretransitive_iff_subsingleton_quotient :
    IsPretransitiveIsPretransitive G α ↔ Subsingleton (orbitRel.Quotient G α) := by
  refine ⟨fun _ ↦ ⟨fun a b ↦ ?_⟩, fun _ ↦ ⟨fun a b ↦ ?_⟩⟩
  · refine Quot.inductionOn a (fun x ↦ ?_)
    exact Quot.inductionOn b (fun y ↦ Quot.sound <| exists_smul_eq G y x)
  · have h : Quotient.mk (orbitRel G α) b = ⟦a⟧ := Subsingleton.elim _ _
    exact Quotient.eq''.mp h

Pretransitive Action Characterization via Quotient Subsingleton

Informal description

A group action of $G$ on $\alpha$ is pretransitive if and only if the quotient space $\alpha/G$ (formed by the orbit equivalence relation) is a subsingleton (i.e., has at most one element).

MulAction.pretransitive_iff_unique_quotient_of_nonempty theorem

[Nonempty α] : IsPretransitive G α ↔ Nonempty (Unique <| orbitRel.Quotient G α)

Full source

/-- If `α` is non-empty, an action is pretransitive if and only if the quotient has exactly one
element. -/
@[to_additive "If `α` is non-empty, an additive action is pretransitive if and only if the
quotient has exactly one element."]
theorem pretransitive_iff_unique_quotient_of_nonempty [Nonempty α] :
    IsPretransitiveIsPretransitive G α ↔ Nonempty (Unique <| orbitRel.Quotient G α) := by
  rw [unique_iff_subsingleton_and_nonempty, pretransitive_iff_subsingleton_quotient, iff_self_and]
  exact fun _ ↦ (nonempty_quotient_iff _).mpr inferInstance

Pretransitive Action Characterization via Unique Quotient for Non-Empty Sets

Informal description

For a non-empty type $\alpha$ acted upon by a group $G$, the action is pretransitive (i.e., there is exactly one orbit) if and only if the quotient $\alpha/G$ by the orbit equivalence relation has exactly one element (i.e., it is a unique quotient).

MulAction.instIsPretransitiveElemOrbit_1 instance

(x : orbitRel.Quotient G α) : IsPretransitive G x.orbit

Full source

@[to_additive]
instance (x : orbitRel.Quotient G α) : IsPretransitive G x.orbit where
  exists_smul_eq := by
    induction x using Quotient.inductionOn'
    rintro ⟨y, yh⟩ ⟨z, zh⟩
    rw [orbitRel.Quotient.mem_orbit, Quotient.eq''] at yh zh
    rcases yh with ⟨g, rfl⟩
    rcases zh with ⟨h, rfl⟩
    refine ⟨h * g⁻¹, ?_⟩
    ext
    simp [mul_smul]

Pretransitivity of Group Action on Orbits in Quotient Space

Informal description

For any quotient element $x$ of $\alpha$ under the orbit equivalence relation induced by the action of a group $G$ on $\alpha$, the action of $G$ on the orbit of $x$ is pretransitive. That is, for any two elements $a, b$ in the orbit of $x$, there exists some $g \in G$ such that $g \cdot a = b$.

Finite.of_finite_mulAction_orbitRel_quotient theorem

[Finite G] [Finite Ω] : Finite α

Full source

@[to_additive]
lemma _root_.Finite.of_finite_mulAction_orbitRel_quotient [Finite G] [Finite Ω] : Finite α := by
  rw [(selfEquivSigmaOrbits' G _).finite_iff]
  have : ∀ g : Ω, Finite g.orbit := by
    intro g
    induction g using Quotient.inductionOn'
    simpa [Set.finite_coe_iff] using Finite.finite_mulAction_orbit _
  exact Finite.instSigma

Finiteness of Type under Finite Group Action and Finite Quotient

Informal description

If a group $G$ and the quotient $\Omega = \alpha/G$ by the orbit equivalence relation are both finite, then the original type $\alpha$ is also finite.

MulAction.orbitRel_le_fst theorem

: orbitRel G (α × β) ≤ (orbitRel G α).comap Prod.fst

Full source

@[to_additive]
lemma orbitRel_le_fst :
    orbitRel G (α × β) ≤ (orbitRel G α).comap Prod.fst :=
  Setoid.le_def.2 fst_mem_orbit_of_mem_orbit

Orbit Relation Refinement under First Projection

Informal description

For a monoid $G$ acting on the product type $\alpha \times \beta$, the orbit equivalence relation on $\alpha \times \beta$ is finer than the pullback of the orbit equivalence relation on $\alpha$ via the first projection. In other words, if two pairs $(x_1, y_1)$ and $(x_2, y_2)$ are in the same orbit under the action of $G$, then their first components $x_1$ and $x_2$ must also be in the same orbit under the action of $G$.

MulAction.orbitRel_le_snd theorem

: orbitRel G (α × β) ≤ (orbitRel G β).comap Prod.snd

Full source

@[to_additive]
lemma orbitRel_le_snd :
    orbitRel G (α × β) ≤ (orbitRel G β).comap Prod.snd :=
  Setoid.le_def.2 snd_mem_orbit_of_mem_orbit

Orbit Relation Refinement under Second Projection

Informal description

For a monoid $G$ acting on the product type $\alpha \times \beta$, the orbit equivalence relation on $\alpha \times \beta$ is finer than the pullback of the orbit equivalence relation on $\beta$ via the second projection. In other words, if two pairs $(x_1, y_1)$ and $(x_2, y_2)$ are in the same orbit under the action of $G$, then their second components $y_1$ and $y_2$ must also be in the same orbit under the action of $G$.

MulAction.stabilizer_smul_eq_stabilizer_map_conj theorem

(g : G) (a : α) : stabilizer G (g • a) = (stabilizer G a).map (MulAut.conj g).toMonoidHom

Full source

/-- If the stabilizer of `a` is `S`, then the stabilizer of `g • a` is `gSg⁻¹`. -/
theorem stabilizer_smul_eq_stabilizer_map_conj (g : G) (a : α) :
    stabilizer G (g • a) = (stabilizer G a).map (MulAut.conj g).toMonoidHom := by
  ext h
  rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]

Conjugation of Stabilizer Subgroup under Group Action: $\text{Stab}_G(g \cdot a) = g \text{Stab}_G(a) g^{-1}$

Informal description

Let $G$ be a group acting on a set $\alpha$. For any $g \in G$ and $a \in \alpha$, the stabilizer subgroup of $g \cdot a$ is equal to the image of the stabilizer subgroup of $a$ under conjugation by $g$, i.e., \[ \text{Stab}_G(g \cdot a) = g (\text{Stab}_G(a)) g^{-1}. \]

MulAction.stabilizerEquivStabilizerOfOrbitRel definition

{a b : α} (h : orbitRel G α a b) : stabilizer G a ≃* stabilizer G b

Full source

/-- A bijection between the stabilizers of two elements in the same orbit. -/
noncomputable def stabilizerEquivStabilizerOfOrbitRel {a b : α} (h : orbitRel G α a b) :
    stabilizerstabilizer G a ≃* stabilizer G b :=
  let g : G := Classical.choose h
  have hg : g • b = a := Classical.choose_spec h
  have this : stabilizer G a = (stabilizer G b).map (MulAut.conj g).toMonoidHom := by
    rw [← hg, stabilizer_smul_eq_stabilizer_map_conj]
  (MulEquiv.subgroupCongr this).trans ((MulAut.conj g).subgroupMap <| stabilizer G b).symm

Stabilizer isomorphism for elements in the same orbit under group action

Informal description

Given a group action of $G$ on $\alpha$ and two elements $a, b \in \alpha$ that are in the same orbit (i.e., there exists $g \in G$ such that $g \cdot b = a$), there is a group isomorphism between the stabilizer subgroups $\text{Stab}_G(a)$ and $\text{Stab}_G(b)$.

AddAction.stabilizer_vadd_eq_stabilizer_map_conj theorem

(g : G) (a : α) : stabilizer G (g +ᵥ a) = (stabilizer G a).map (AddAut.conj g).toMul.toAddMonoidHom

Full source

/-- If the stabilizer of `x` is `S`, then the stabilizer of `g +ᵥ x` is `g + S + (-g)`. -/
theorem stabilizer_vadd_eq_stabilizer_map_conj (g : G) (a : α) :
    stabilizer G (g +ᵥ a) = (stabilizer G a).map (AddAut.conj g).toMul.toAddMonoidHom := by
  ext h
  rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd,
    neg_add_cancel, zero_vadd, ← mem_stabilizer_iff, AddSubgroup.mem_map_equiv,
    AddAut.conj_symm_apply]

Stabilizer Transformation under Additive Group Action via Conjugation

Informal description

Let $G$ be an additive group acting on a set $\alpha$. For any $g \in G$ and $a \in \alpha$, the stabilizer subgroup of $g +ᵥ a$ is equal to the image of the stabilizer subgroup of $a$ under the conjugation map $\text{AddAut.conj}(g)$ composed with the monoid homomorphism from multiplicative to additive structure. That is, \[ \text{stabilizer}_G(g +ᵥ a) = (\text{stabilizer}_G(a)).\text{map}\big((\text{AddAut.conj}(g)).\text{toMul}.\text{toAddMonoidHom}\big). \]

AddAction.stabilizerEquivStabilizerOfOrbitRel definition

{a b : α} (h : orbitRel G α a b) : stabilizer G a ≃+ stabilizer G b

Full source

/-- A bijection between the stabilizers of two elements in the same orbit. -/
noncomputable def stabilizerEquivStabilizerOfOrbitRel {a b : α} (h : orbitRel G α a b) :
    stabilizerstabilizer G a ≃+ stabilizer G b :=
  let g : G := Classical.choose h
  have hg : g +ᵥ b = a := Classical.choose_spec h
  have this : stabilizer G a = (stabilizer G b).map (AddAut.conj g).toMul.toAddMonoidHom := by
    rw [← hg, stabilizer_vadd_eq_stabilizer_map_conj]
  (AddEquiv.addSubgroupCongr this).trans ((AddAut.conj g).addSubgroupMap <| stabilizer G b).symm

Stabilizer isomorphism for elements in the same orbit under an additive group action

Informal description

Given an additive group action of $G$ on $\alpha$ and two elements $a, b \in \alpha$ that are in the same orbit (i.e., there exists $g \in G$ such that $g + b = a$), there is a group isomorphism between the stabilizer subgroups $\text{stabilizer}_G(a)$ and $\text{stabilizer}_G(b)$. This isomorphism is constructed via conjugation by the group element $g$ that maps $b$ to $a$.

Equiv.swap_mem_stabilizer theorem

 {α : Type*} [DecidableEq α] {S : Set α} {a b : α} :
  Equiv.swap a b ∈ MulAction.stabilizer (Equiv.Perm α) S ↔ (a ∈ S ↔ b ∈ S)

Full source

theorem Equiv.swap_mem_stabilizer {α : Type*} [DecidableEq α] {S : Set α} {a b : α} :
    Equiv.swapEquiv.swap a b ∈ MulAction.stabilizer (Equiv.Perm α) SEquiv.swap a b ∈ MulAction.stabilizer (Equiv.Perm α) S ↔ (a ∈ S ↔ b ∈ S) := by
  rw [MulAction.mem_stabilizer_iff, Set.ext_iff, ← swap_inv]
  simp_rw [Set.mem_inv_smul_set_iff, Perm.smul_def, swap_apply_def]
  exact ⟨fun h ↦ by simpa [Iff.comm] using h a, by intros; split_ifs <;> simp [*]⟩

Stabilizer Membership Criterion for Transpositions: $\text{swap}(a, b) \in \text{Stab}(S) \leftrightarrow (a \in S \leftrightarrow b \in S)$

Informal description

For a set $S$ in a type $\alpha$ with decidable equality, and elements $a, b \in \alpha$, the transposition (swap) of $a$ and $b$ belongs to the stabilizer subgroup of $S$ under the action of the permutation group if and only if $a \in S$ is equivalent to $b \in S$. That is, \[ \text{swap}(a, b) \in \text{Stab}_{\text{Perm}(\alpha)}(S) \leftrightarrow (a \in S \leftrightarrow b \in S). \]

MulAction.le_stabilizer_iff_smul_le theorem

(s : Set α) (H : Subgroup G) : H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s

Full source

/-- To prove inclusion of a *subgroup* in a stabilizer, it is enough to prove inclusions. -/
@[to_additive
  "To prove inclusion of a *subgroup* in a stabilizer, it is enough to prove inclusions."]
theorem le_stabilizer_iff_smul_le (s : Set α) (H : Subgroup G) :
    H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s := by
  constructor
  · intro hyp g hg
    apply Eq.subset
    rw [← mem_stabilizer_iff]
    exact hyp hg
  · intro hyp g hg
    rw [mem_stabilizer_iff]
    apply subset_antisymm (hyp g hg)
    intro x hx
    use g⁻¹ • x
    constructor
    · apply hyp g⁻¹ (inv_mem hg)
      simp only [Set.smul_mem_smul_set_iff, hx]
    · simp only [smul_inv_smul]

Subgroup Containment in Stabilizer iff Action Preserves Subset

Informal description

For a group $G$ acting on a type $\alpha$, a subgroup $H \leq G$, and a subset $s \subseteq \alpha$, the subgroup $H$ is contained in the stabilizer of $s$ if and only if for every $g \in H$, the action of $g$ preserves $s$, i.e., $g \cdot s \subseteq s$.

Module.stabilizer_units_eq_bot_of_ne_zero theorem

{x : M} (hx : x ≠ 0) : MulAction.stabilizer Rˣ x = ⊥

Full source

lemma Module.stabilizer_units_eq_bot_of_ne_zero {x : M} (hx : x ≠ 0) :
    MulAction.stabilizer Rˣ x = ⊥ := by
  rw [eq_bot_iff]
  intro g (hg : g.val • x = x)
  ext
  rw [← sub_eq_zero, ← smul_eq_zero_iff_left hx, Units.val_one, sub_smul, hg, one_smul, sub_self]

Trivial Stabilizer for Nonzero Module Elements under Units Action

Informal description

For any nonzero element $x$ in a module $M$ over a ring $R$, the stabilizer subgroup of $x$ under the action of the units of $R$ is trivial (i.e., equal to the bottom subgroup $\bot$).

Main definitions