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 for the fixator of a set acting on the complement of that set, defined in Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup) are useful to study the multiple transitivity of the group G, since n-transitivity of G on α is equivalent to n - 1-transitivity of stabilizer G a on the complement of a.

We define equivariant maps that relate various of these sub_mul_actions 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_eq_add_one, 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.conjMap hg is the equivariant map from SubMulAction.ofStabilizer G a to SubMulAction.ofStabilizer G b.

• SubMulAction.ofStabilizer.isPretransitive_iff_conj hg shows that this actions are equivalently pretransitive or

• SubMulAction.ofStabilizer.isMultiplyPretransitive_iff_conj hg shows that this actions are equivalently n-pretransitive for all n : ℕ.

• SubMulAction.ofStabilizer.append : given x : Fin n ↪ ofStabilizer G a, append a to obtain y : Fin n.succ ↪ α

• SubMulAction.ofStabilizer.isMultiplyPretransitive_iff : is the action of G on α is pretransitive, then it is n.succ pretransitive if and only if the action of stabilizer G a on ofStabilizer G a is n-pretransitive.

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

• SubMulAction.ofStabilizer G a = { carrier := {a}ᶜ, smul_mem' := ⋯ }

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

• SubAddAction.ofStabilizer G a = { carrier := {a}ᶜ, vadd_mem' := ⋯ }

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.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_eq_add_one (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_eq_add_zero (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_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

• SubAddAction.ofStabilizer.conjMap hg = { toFun := fun (x : ↥(SubAddAction.ofStabilizer G a)) => ⟨g +ᵥ ↑x, ⋯⟩, map_vadd' := ⋯ }

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

• SubMulAction.ofStabilizer.conjMap hg = { toFun := fun (x : ↥(SubMulAction.ofStabilizer G a)) => ⟨g • ↑x, ⋯⟩, map_smul' := ⋯ }

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

• SubMulAction.ofStabilizer.snoc x = Fin.Embedding.snoc (x.trans (Function.Embedding.subtype fun (x : α) => x ∈ SubMulAction.ofStabilizer G a)) ⋯

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

• SubAddAction.ofStabilizer.snoc x = Fin.Embedding.snoc (x.trans (Function.Embedding.subtype fun (x : α) => x ∈ SubAddAction.ofStabilizer G a)) ⋯

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