Documentation

Mathlib.Algebra.Pointwise.Stabilizer

Stabilizer of a set under a pointwise action #

This file characterises the stabilizer of a set/finset under the pointwise action of a group.

Stabilizer of a set #

source
@[simp]
theorem AddAction.stabilizer_empty {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] :
AddAction.stabilizer G ∅ = ⊤
source
@[simp]
theorem MulAction.stabilizer_empty {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] :
MulAction.stabilizer G ∅ = ⊤
source
@[simp]
theorem AddAction.stabilizer_univ {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] :
AddAction.stabilizer G Set.univ = ⊤
source
@[simp]
theorem MulAction.stabilizer_univ {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] :
MulAction.stabilizer G Set.univ = ⊤
source
@[simp]
theorem AddAction.stabilizer_singleton {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] (b : α) :
AddAction.stabilizer G {b} = AddAction.stabilizer G b
source
@[simp]
theorem MulAction.stabilizer_singleton {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] (b : α) :
MulAction.stabilizer G {b} = MulAction.stabilizer G b
source
theorem AddAction.mem_stabilizer_set {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {a : G} {s : Set α} :
a ∈ AddAction.stabilizer G s ↔ ∀ (b : α), a +ᵥ b ∈ s ↔ b ∈ s
source
theorem MulAction.mem_stabilizer_set {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {a : G} {s : Set α} :
a ∈ MulAction.stabilizer G s ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
source
theorem AddAction.map_stabilizer_le {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) (s : Set G) :
AddSubgroup.map f (AddAction.stabilizer G s) ≤ AddAction.stabilizer H (⇑f '' s)
source
theorem MulAction.map_stabilizer_le {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (s : Set G) :
Subgroup.map f (MulAction.stabilizer G s) ≤ MulAction.stabilizer H (⇑f '' s)
source
@[simp]
theorem AddAction.stabilizer_add_self {G : Type u_1} [AddGroup G] (s : Set G) :
↑(AddAction.stabilizer G s) + s = s
source
@[simp]
theorem MulAction.stabilizer_mul_self {G : Type u_1} [Group G] (s : Set G) :
↑(MulAction.stabilizer G s) * s = s

Stabilizer of a subgroup #

source
@[simp]
theorem AddAction.stabilizer_addSubgroup {G : Type u_1} [AddGroup G] (s : AddSubgroup G) :
AddAction.stabilizer G ↑s = s
source
@[simp]
theorem MulAction.stabilizer_subgroup {G : Type u_1} [Group G] (s : Subgroup G) :
MulAction.stabilizer G ↑s = s
source
@[simp]
theorem AddAction.stabilizer_op_addSubgroup {G : Type u_1} [AddGroup G] (s : AddSubgroup G) :
AddAction.stabilizer Gᵃᵒᵖ ↑s = s.op
source
@[simp]
theorem MulAction.stabilizer_op_subgroup {G : Type u_1} [Group G] (s : Subgroup G) :
MulAction.stabilizer Gᵐᵒᵖ ↑s = s.op
source
@[simp]
theorem AddAction.stabilizer_addSubgroup_op {G : Type u_1} [AddGroup G] (s : AddSubgroup Gᵃᵒᵖ) :
AddAction.stabilizer G ↑s = s.unop
source
@[simp]
theorem MulAction.stabilizer_subgroup_op {G : Type u_1} [Group G] (s : Subgroup Gᵐᵒᵖ) :
MulAction.stabilizer G ↑s = s.unop

Stabilizer of a finset #

source
@[simp]
theorem AddAction.stabilizer_coe_finset {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [DecidableEq α] (s : Finset α) :
AddAction.stabilizer G ↑s = AddAction.stabilizer G s
source
@[simp]
theorem MulAction.stabilizer_coe_finset {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [DecidableEq α] (s : Finset α) :
MulAction.stabilizer G ↑s = MulAction.stabilizer G s
source
@[simp]
theorem AddAction.stabilizer_finset_empty {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [DecidableEq α] :
AddAction.stabilizer G ∅ = ⊤
source
@[simp]
theorem MulAction.stabilizer_finset_empty {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [DecidableEq α] :
MulAction.stabilizer G ∅ = ⊤
source
@[simp]
theorem AddAction.stabilizer_finset_univ {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [DecidableEq α] [Fintype α] :
AddAction.stabilizer G Finset.univ = ⊤
source
@[simp]
theorem MulAction.stabilizer_finset_univ {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [DecidableEq α] [Fintype α] :
MulAction.stabilizer G Finset.univ = ⊤
source
@[simp]
theorem AddAction.stabilizer_finset_singleton {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [DecidableEq α] (b : α) :
AddAction.stabilizer G {b} = AddAction.stabilizer G b
source
@[simp]
theorem MulAction.stabilizer_finset_singleton {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [DecidableEq α] (b : α) :
MulAction.stabilizer G {b} = MulAction.stabilizer G b
source
theorem AddAction.mem_stabilizer_finset {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {a : G} [DecidableEq α] {s : Finset α} :
a ∈ AddAction.stabilizer G s ↔ ∀ (b : α), a +ᵥ b ∈ s ↔ b ∈ s
source
theorem MulAction.mem_stabilizer_finset {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {a : G} [DecidableEq α] {s : Finset α} :
a ∈ MulAction.stabilizer G s ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
source
theorem AddAction.mem_stabilizer_finset_iff_subset_vadd_finset {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {a : G} [DecidableEq α] {s : Finset α} :
a ∈ AddAction.stabilizer G s ↔ s ⊆ a +ᵥ s
source
theorem MulAction.mem_stabilizer_finset_iff_subset_smul_finset {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {a : G} [DecidableEq α] {s : Finset α} :
a ∈ MulAction.stabilizer G s ↔ s ⊆ a • s
source
theorem AddAction.mem_stabilizer_finset_iff_vadd_finset_subset {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {a : G} [DecidableEq α] {s : Finset α} :
a ∈ AddAction.stabilizer G s ↔ a +ᵥ s ⊆ s
source
theorem MulAction.mem_stabilizer_finset_iff_smul_finset_subset {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {a : G} [DecidableEq α] {s : Finset α} :
a ∈ MulAction.stabilizer G s ↔ a • s ⊆ s
source
theorem AddAction.mem_stabilizer_finset' {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {a : G} [DecidableEq α] {s : Finset α} :
a ∈ AddAction.stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a +ᵥ b ∈ s
source
theorem MulAction.mem_stabilizer_finset' {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {a : G} [DecidableEq α] {s : Finset α} :
a ∈ MulAction.stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s

Stabilizer of a finite set #

source
theorem AddAction.mem_stabilizer_set_iff_subset_vadd_set {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {a : G} {s : Set α} (hs : s.Finite) :
a ∈ AddAction.stabilizer G s ↔ s ⊆ a +ᵥ s
source
theorem MulAction.mem_stabilizer_set_iff_subset_smul_set {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {a : G} {s : Set α} (hs : s.Finite) :
a ∈ MulAction.stabilizer G s ↔ s ⊆ a • s
source
theorem AddAction.mem_stabilizer_set_iff_vadd_set_subset {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {a : G} {s : Set α} (hs : s.Finite) :
a ∈ AddAction.stabilizer G s ↔ a +ᵥ s ⊆ s
source
theorem MulAction.mem_stabilizer_set_iff_smul_set_subset {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {a : G} {s : Set α} (hs : s.Finite) :
a ∈ MulAction.stabilizer G s ↔ a • s ⊆ s
source
theorem AddAction.mem_stabilizer_set' {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {a : G} {s : Set α} (hs : s.Finite) :
a ∈ AddAction.stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a +ᵥ b ∈ s
source
theorem MulAction.mem_stabilizer_set' {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {a : G} {s : Set α} (hs : s.Finite) :
a ∈ MulAction.stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s

Stabilizer in a commutative group #

source
@[simp]
theorem AddAction.add_stabilizer_self {G : Type u_1} [AddCommGroup G] (s : Set G) :
s + ↑(AddAction.stabilizer G s) = s
source
@[simp]
theorem MulAction.mul_stabilizer_self {G : Type u_1} [CommGroup G] (s : Set G) :
s * ↑(MulAction.stabilizer G s) = s
source
theorem AddAction.stabilizer_image_coe_quotient {G : Type u_1} [AddCommGroup G] (s : Set G) :
AddAction.stabilizer (G ⧸ AddAction.stabilizer G s) (QuotientAddGroup.mk '' s) = ⊥
source
theorem MulAction.stabilizer_image_coe_quotient {G : Type u_1} [CommGroup G] (s : Set G) :
MulAction.stabilizer (G ⧸ MulAction.stabilizer G s) (QuotientGroup.mk '' s) = ⊥