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 #
@[simp]
@[simp]
@[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
@[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
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)
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)
@[simp]
theorem
AddAction.stabilizer_add_self
{G : Type u_1}
[AddGroup G]
(s : Set G)
:
↑(AddAction.stabilizer G s) + s = s
@[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 #
@[simp]
theorem
AddAction.stabilizer_addSubgroup
{G : Type u_1}
[AddGroup G]
(s : AddSubgroup G)
:
AddAction.stabilizer G ↑s = s
@[simp]
theorem
MulAction.stabilizer_subgroup
{G : Type u_1}
[Group G]
(s : Subgroup G)
:
MulAction.stabilizer G ↑s = s
@[simp]
@[simp]
theorem
MulAction.stabilizer_op_subgroup
{G : Type u_1}
[Group G]
(s : Subgroup G)
:
MulAction.stabilizer Gᵐᵒᵖ ↑s = Subgroup.op s
@[simp]
@[simp]
theorem
MulAction.stabilizer_subgroup_op
{G : Type u_1}
[Group G]
(s : Subgroup Gᵐᵒᵖ)
:
MulAction.stabilizer G ↑s = Subgroup.unop s
Stabilizer of a finset #
@[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
@[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
@[simp]
theorem
AddAction.stabilizer_finset_empty
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
[DecidableEq α]
:
@[simp]
theorem
MulAction.stabilizer_finset_empty
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
[DecidableEq α]
:
@[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
@[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
theorem
AddAction.mem_stabilizer_finset
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
{a : G}
[DecidableEq α]
{s : Finset α}
:
theorem
MulAction.mem_stabilizer_finset
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
{a : G}
[DecidableEq α]
{s : Finset α}
:
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
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
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
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
theorem
AddAction.mem_stabilizer_finset'
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
{a : G}
[DecidableEq α]
{s : Finset α}
:
theorem
MulAction.mem_stabilizer_finset'
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
{a : G}
[DecidableEq α]
{s : Finset α}
:
Stabilizer of a finite set #
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 : Set.Finite s)
:
a ∈ AddAction.stabilizer G s ↔ s ⊆ a +ᵥ s
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 : Set.Finite s)
:
a ∈ MulAction.stabilizer G s ↔ s ⊆ a • s
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 : Set.Finite s)
:
a ∈ AddAction.stabilizer G s ↔ a +ᵥ s ⊆ s
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 : Set.Finite s)
:
a ∈ MulAction.stabilizer G s ↔ a • s ⊆ s
theorem
AddAction.mem_stabilizer_set'
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
{a : G}
{s : Set α}
(hs : Set.Finite s)
:
theorem
MulAction.mem_stabilizer_set'
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
{a : G}
{s : Set α}
(hs : Set.Finite s)
:
Stabilizer in a commutative group #
@[simp]
theorem
AddAction.add_stabilizer_self
{G : Type u_1}
[AddCommGroup G]
(s : Set G)
:
s + ↑(AddAction.stabilizer G s) = s
@[simp]
theorem
MulAction.mul_stabilizer_self
{G : Type u_1}
[CommGroup G]
(s : Set G)
:
s * ↑(MulAction.stabilizer G s) = s
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) = ⊥
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) = ⊥