Documentation

Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

The SubMulAction of the stabilizer of a point on the complement of that point #

When a group G acts on a type α, the stabilizer of a point a : α acts naturally on the complement of that point.

Such actions (as the similar one, SubMulAction.ofFixingSubgroup, for the fixing subgroup of a set acting on the complement of that set) are useful to study the multiple transitivity of the group G, since n-transitivity of G on α is equivalent to n - 1-transitivity of MulAction.stabilizer G a on the complement of a.

We define equivariant maps that relate various of these SubMulActions and permit to manipulate them in a relatively smooth way.

SubMulAction.ofStabilizer a : the action of stabilizer G a on {a}ᶜ
SubMulAction.ENat_card_ofStabilizer_add_one_eq and SubMulAction.nat_card_ofStabilizer_eq compute the cardinality of the carrier of that action.

Consider a b : α and g : G such that hg : g • b = a.

SubMulAction.ofStabilizer.conjMap hg is the equivariant map from SubMulAction.ofStabilizer G a to SubMulAction.ofStabilizer G b.
SubMulAction.ofStabilizer.snoc : given x : Fin n ↪ ofStabilizer G a, append a to obtain y : Fin n.succ ↪ α

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

SubMulAction (↥(MulAction.stabilizer G a)) α

Action of the stabilizer of a point on the complement.

Equations

Instances For

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

SubAddAction (↥(AddAction.stabilizer G a)) α

Action of the stabilizer of a point on the complement.

Equations

Instances For

theorem SubMulAction.ofStabilizer_carrier (G : Type u_1) [Group G] {α : Type u_2} [MulAction G α] (a : α) :

(ofStabilizer G a).carrier = {a}ᶜ

theorem SubAddAction.ofStabilizer_carrier (G : Type u_1) [AddGroup G] {α : Type u_2} [AddAction G α] (a : α) :

(ofStabilizer G a).carrier = {a}ᶜ

theorem SubMulAction.mem_ofStabilizer_iff (G : Type u_1) [Group G] {α : Type u_2} [MulAction G α] (a : α) {x : α} :

x ∈ ofStabilizer G a ↔ x ≠ a

theorem SubAddAction.mem_ofStabilizer_iff (G : Type u_1) [AddGroup G] {α : Type u_2} [AddAction G α] (a : α) {x : α} :

x ∈ ofStabilizer G a ↔ x ≠ a

theorem SubMulAction.notMem_val_image (G : Type u_1) [Group G] {α : Type u_2} [MulAction G α] {a : α} (t : Set ↥(ofStabilizer G a)) :

a ∉ Subtype.val '' t

theorem SubAddAction.notMem_val_image (G : Type u_1) [AddGroup G] {α : Type u_2} [AddAction G α] {a : α} (t : Set ↥(ofStabilizer G a)) :

a ∉ Subtype.val '' t

theorem SubMulAction.neq_of_mem_ofStabilizer (G : Type u_1) [Group G] {α : Type u_2} [MulAction G α] (a : α) {x : ↥(ofStabilizer G a)} :

↑x ≠ a

theorem SubAddAction.neq_of_mem_ofStabilizer (G : Type u_1) [AddGroup G] {α : Type u_2} [AddAction G α] (a : α) {x : ↥(ofStabilizer G a)} :

↑x ≠ a

theorem SubMulAction.ENat_card_ofStabilizer_add_one_eq (G : Type u_1) [Group G] {α : Type u_2} [MulAction G α] (a : α) :

ENat.card ↥(ofStabilizer G a) + 1 = ENat.card α

theorem SubAddAction.ENat_card_ofStabilizer_add_zero_eq (G : Type u_1) [AddGroup G] {α : Type u_2} [AddAction G α] (a : α) :

ENat.card ↥(ofStabilizer G a) + 1 = ENat.card α

theorem SubMulAction.nat_card_ofStabilizer_add_one_eq (G : Type u_1) [Group G] {α : Type u_2} [MulAction G α] [Finite α] (a : α) :

Nat.card ↥(ofStabilizer G a) + 1 = Nat.card α

theorem SubAddAction.nat_card_ofStabilizer_add_zero_eq (G : Type u_1) [AddGroup G] {α : Type u_2} [AddAction G α] [Finite α] (a : α) :

Nat.card ↥(ofStabilizer G a) + 1 = Nat.card α

@[deprecated SubMulAction.nat_card_ofStabilizer_add_one_eq (since := "2025-10-03")]

theorem SubMulAction.nat_card_ofStabilizer_eq_add_one (G : Type u_1) [Group G] {α : Type u_2} [MulAction G α] [Finite α] (a : α) :

Nat.card ↥(ofStabilizer G a) + 1 = Nat.card α

Alias of SubMulAction.nat_card_ofStabilizer_add_one_eq.

theorem SubMulAction.nat_card_ofStabilizer_eq (G : Type u_1) [Group G] {α : Type u_2} [MulAction G α] [Finite α] (a : α) :

Nat.card ↥(ofStabilizer G a) = Nat.card α - 1

theorem SubAddAction.nat_card_ofStabilizer_eq (G : Type u_1) [AddGroup G] {α : Type u_2} [AddAction G α] [Finite α] (a : α) :

Nat.card ↥(ofStabilizer G a) = Nat.card α - 1

def SubAddAction.ofStabilizer.conjMap {G : Type u_3} [AddGroup G] {α : Type u_4} [AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a) :

↥(ofStabilizer G a) →ₑ[⇑(AddAction.stabilizerEquivStabilizer hg)] ↥(ofStabilizer G b)

Conjugation induces an equivariant map between the SubAddAction of the stabilizer of a point and that of its translate.

Equations

Instances For

def SubMulAction.ofStabilizer.conjMap {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {g : G} {a b : α} (hg : b = g • a) :

↥(ofStabilizer G a) →ₑ[⇑(MulAction.stabilizerEquivStabilizer hg)] ↥(ofStabilizer G b)

Conjugation induces an equivariant map between the SubMulAction of the stabilizer of a point and that of its translate.

Equations

Instances For

theorem SubMulAction.ofStabilizer.conjMap_apply {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {g : G} {a b : α} (hg : b = g • a) (x : ↥(ofStabilizer G a)) :

↑((conjMap hg) x) = g • ↑x

theorem SubAddAction.ofStabilizer.conjMap_apply {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a) (x : ↥(ofStabilizer G a)) :

↑((conjMap hg) x) = g +ᵥ ↑x

theorem AddAction.stabilizerEquivStabilizer_compTriple {G : Type u_3} [AddGroup G] {α : Type u_4} [AddAction G α] {g h k : G} {a b c : α} {hg : b = g +ᵥ a} {hh : c = h +ᵥ b} {hk : c = k +ᵥ a} (H : k = h + g) :

CompTriple ⇑(stabilizerEquivStabilizer hg) ⇑(stabilizerEquivStabilizer hh) ⇑(stabilizerEquivStabilizer hk)

theorem MulAction.stabilizerEquivStabilizer_compTriple {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {g h k : G} {a b c : α} {hg : b = g • a} {hh : c = h • b} {hk : c = k • a} (H : k = h * g) :

CompTriple ⇑(stabilizerEquivStabilizer hg) ⇑(stabilizerEquivStabilizer hh) ⇑(stabilizerEquivStabilizer hk)

theorem SubMulAction.ofStabilizer.conjMap_comp_apply {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {g h k : G} {a b c : α} {hg : b = g • a} {hh : c = h • b} {hk : c = k • a} (H : k = h * g) (x : ↥(ofStabilizer G a)) :

(conjMap hh) ((conjMap hg) x) = (conjMap hk) x

theorem SubAddAction.ofStabilizer.conjMap_comp_apply {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {g h k : G} {a b c : α} {hg : b = g +ᵥ a} {hh : c = h +ᵥ b} {hk : c = k +ᵥ a} (H : k = h + g) (x : ↥(ofStabilizer G a)) :

(conjMap hh) ((conjMap hg) x) = (conjMap hk) x

theorem SubMulAction.ofStabilizer.conjMap_comp_inv_apply {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {g : G} {a b : α} (hg : b = g • a) (x : ↥(ofStabilizer G a)) :

(conjMap ⋯) ((conjMap hg) x) = x

theorem SubAddAction.ofStabilizer.conjMap_comp_neg_apply {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a) (x : ↥(ofStabilizer G a)) :

(conjMap ⋯) ((conjMap hg) x) = x

theorem SubMulAction.ofStabilizer.inv_conjMap_comp_apply {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {g : G} {a b : α} (hg : b = g • a) (x : ↥(ofStabilizer G b)) :

(conjMap hg) ((conjMap ⋯) x) = x

theorem SubAddAction.ofStabilizer.neg_conjMap_comp_apply {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a) (x : ↥(ofStabilizer G b)) :

(conjMap hg) ((conjMap ⋯) x) = x

theorem SubMulAction.ofStabilizer.conjMap_comp {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {g h k : G} {a b c : α} (hg : b = g • a) (hh : c = h • b) (hk : c = k • a) (H : k = h * g) :

(conjMap hh).comp (conjMap hg) = conjMap hk

theorem SubAddAction.ofStabilizer.conjMap_comp {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {g h k : G} {a b c : α} (hg : b = g +ᵥ a) (hh : c = h +ᵥ b) (hk : c = k +ᵥ a) (H : k = h + g) :

(conjMap hh).comp (conjMap hg) = conjMap hk

theorem SubMulAction.ofStabilizer.conjMap_bijective {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {g : G} {a b : α} (hg : b = g • a) :

Function.Bijective ⇑(conjMap hg)

theorem SubAddAction.ofStabilizer.conjMap_bijective {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a) :

Function.Bijective ⇑(conjMap hg)

def SubMulAction.ofStabilizer.snoc {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {a : α} {n : ℕ} (x : Fin n ↪ ↥(ofStabilizer G a)) :

Fin n.succ ↪ α

Append a to x : Fin n ↪ ofStabilizer G a to get an element of Fin n.succ ↪ α.

Equations

Instances For

def SubAddAction.ofStabilizer.snoc {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {a : α} {n : ℕ} (x : Fin n ↪ ↥(ofStabilizer G a)) :

Fin n.succ ↪ α

Append a to x : Fin n ↪ ofStabilizer G a to get an element of Fin n.succ ↪ α.

Equations

Instances For

theorem SubMulAction.ofStabilizer.snoc_castSucc {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {a : α} {n : ℕ} (x : Fin n ↪ ↥(ofStabilizer G a)) (i : Fin n) :

(snoc x) i.castSucc = ↑(x i)

theorem SubAddAction.ofStabilizer.snoc_castSucc {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {a : α} {n : ℕ} (x : Fin n ↪ ↥(ofStabilizer G a)) (i : Fin n) :

(snoc x) i.castSucc = ↑(x i)

theorem SubMulAction.ofStabilizer.snoc_last {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {a : α} {n : ℕ} (x : Fin n ↪ ↥(ofStabilizer G a)) :

(snoc x) (Fin.last n) = a

theorem SubAddAction.ofStabilizer.snoc_last {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {a : α} {n : ℕ} (x : Fin n ↪ ↥(ofStabilizer G a)) :

(snoc x) (Fin.last n) = a

theorem SubMulAction.exists_smul_of_last_eq (G : Type u_1) [Group G] {α : Type u_2} [MulAction G α] [MulAction.IsPretransitive G α] {n : ℕ} (a : α) (x : Fin n.succ ↪ α) :

∃ (g : G) (y : Fin n ↪ ↥(ofStabilizer G a)), g • x = ofStabilizer.snoc y

theorem SubAddAction.exists_vadd_of_last_eq (G : Type u_1) [AddGroup G] {α : Type u_2} [AddAction G α] [AddAction.IsPretransitive G α] {n : ℕ} (a : α) (x : Fin n.succ ↪ α) :

∃ (g : G) (y : Fin n ↪ ↥(ofStabilizer G a)), g +ᵥ x = ofStabilizer.snoc y

instance SMul.ofStabilizer (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] (s : Set α) :

SMul ↥(MulAction.stabilizer G s) ↑s

The stabilizer of a set acts on that set.

Equations

instance VAdd.ofStabilizer (G : Type u_1) [AddGroup G] (α : Type u_2) [AddAction G α] (s : Set α) :

VAdd ↥(AddAction.stabilizer G s) ↑s

The stabilizer of a set acts on that set.

Equations

@[simp]

theorem SMul.smul_stabilizer_def (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] (s : Set α) (g : ↥(MulAction.stabilizer G s)) (x : ↑s) :

↑(g • x) = ↑g • ↑x

instance instMulActionSubtypeMemSubgroupStabilizerSetElem (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] (s : Set α) :

MulAction ↥(MulAction.stabilizer G s) ↑s

The stabilizer of a set acts on that set

Equations

instance instAddActionSubtypeMemAddSubgroupStabilizerSetElem (G : Type u_1) [AddGroup G] (α : Type u_2) [AddAction G α] (s : Set α) :

AddAction ↥(AddAction.stabilizer G s) ↑s

The stabilizer of a set acts on that set.

Equations

theorem stabilizer_empty_eq_top (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] :

MulAction.stabilizer G ∅ = ⊤

theorem stabilizer_univ_eq_top (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] :

MulAction.stabilizer G Set.univ = ⊤

@[simp]

theorem stabilizer_compl (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] {s : Set α} :

MulAction.stabilizer G sᶜ = MulAction.stabilizer G s

The stabilizer of the complement is the stabilizer of the set.