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
MulAction.stabilizer_univ
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
:
MulAction.stabilizer G Set.univ = ⊤
@[simp]
theorem
AddAction.stabilizer_univ
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
:
AddAction.stabilizer G Set.univ = ⊤
@[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
@[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
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)
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)
@[simp]
theorem
MulAction.stabilizer_mul_self
{G : Type u_1}
[Group G]
(s : Set G)
:
↑(MulAction.stabilizer G s) * s = s
@[simp]
theorem
AddAction.stabilizer_add_self
{G : Type u_1}
[AddGroup G]
(s : Set G)
:
↑(AddAction.stabilizer G s) + s = s
theorem
MulAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
{s t : Set α}
{f : Set α → Set α → Set α}
(hf : ∀ (a : G), a • f s t = f (a • s) (a • t))
:
MulAction.stabilizer G s ⊓ MulAction.stabilizer G t ≤ MulAction.stabilizer G (f s t)
theorem
AddAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
{s t : Set α}
{f : Set α → Set α → Set α}
(hf : ∀ (a : G), a +ᵥ f s t = f (a +ᵥ s) (a +ᵥ t))
:
AddAction.stabilizer G s ⊓ AddAction.stabilizer G t ≤ AddAction.stabilizer G (f s t)
theorem
MulAction.stabilizer_inf_stabilizer_le_stabilizer_union
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
{s t : Set α}
:
MulAction.stabilizer G s ⊓ MulAction.stabilizer G t ≤ MulAction.stabilizer G (s ∪ t)
theorem
AddAction.stabilizer_inf_stabilizer_le_stabilizer_union
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
{s t : Set α}
:
AddAction.stabilizer G s ⊓ AddAction.stabilizer G t ≤ AddAction.stabilizer G (s ∪ t)
theorem
MulAction.stabilizer_inf_stabilizer_le_stabilizer_inter
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
{s t : Set α}
:
MulAction.stabilizer G s ⊓ MulAction.stabilizer G t ≤ MulAction.stabilizer G (s ∩ t)
theorem
AddAction.stabilizer_inf_stabilizer_le_stabilizer_inter
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
{s t : Set α}
:
AddAction.stabilizer G s ⊓ AddAction.stabilizer G t ≤ AddAction.stabilizer G (s ∩ t)
theorem
MulAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
{s t : Set α}
:
MulAction.stabilizer G s ⊓ MulAction.stabilizer G t ≤ MulAction.stabilizer G (s \ t)
theorem
AddAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
{s t : Set α}
:
AddAction.stabilizer G s ⊓ AddAction.stabilizer G t ≤ AddAction.stabilizer G (s \ t)
theorem
MulAction.stabilizer_union_eq_left
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
{s t : Set α}
(hdisj : Disjoint s t)
(hstab : MulAction.stabilizer G s ≤ MulAction.stabilizer G t)
(hstab_union : MulAction.stabilizer G (s ∪ t) ≤ MulAction.stabilizer G t)
:
MulAction.stabilizer G (s ∪ t) = MulAction.stabilizer G s
theorem
AddAction.stabilizer_union_eq_left
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
{s t : Set α}
(hdisj : Disjoint s t)
(hstab : AddAction.stabilizer G s ≤ AddAction.stabilizer G t)
(hstab_union : AddAction.stabilizer G (s ∪ t) ≤ AddAction.stabilizer G t)
:
AddAction.stabilizer G (s ∪ t) = AddAction.stabilizer G s
theorem
MulAction.stabilizer_union_eq_right
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
{s t : Set α}
(hdisj : Disjoint s t)
(hstab : MulAction.stabilizer G t ≤ MulAction.stabilizer G s)
(hstab_union : MulAction.stabilizer G (s ∪ t) ≤ MulAction.stabilizer G s)
:
MulAction.stabilizer G (s ∪ t) = MulAction.stabilizer G t
theorem
AddAction.stabilizer_union_eq_right
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
{s t : Set α}
(hdisj : Disjoint s t)
(hstab : AddAction.stabilizer G t ≤ AddAction.stabilizer G s)
(hstab_union : AddAction.stabilizer G (s ∪ t) ≤ AddAction.stabilizer G s)
:
AddAction.stabilizer G (s ∪ t) = AddAction.stabilizer G t
theorem
MulAction.op_smul_set_stabilizer_subset
{G : Type u_1}
[Group G]
{a : G}
{s : Set G}
(ha : a ∈ s)
:
MulOpposite.op a • ↑(MulAction.stabilizer G s) ⊆ s
theorem
AddAction.op_vadd_set_stabilizer_subset
{G : Type u_1}
[AddGroup G]
{a : G}
{s : Set G}
(ha : a ∈ s)
:
AddOpposite.op a +ᵥ ↑(AddAction.stabilizer G s) ⊆ s
theorem
MulAction.stabilizer_subset_div_right
{G : Type u_1}
[Group G]
{a : G}
{s : Set G}
(ha : a ∈ s)
:
↑(MulAction.stabilizer G s) ⊆ s / {a}
theorem
AddAction.stabilizer_subset_sub_right
{G : Type u_1}
[AddGroup G]
{a : G}
{s : Set G}
(ha : a ∈ s)
:
↑(AddAction.stabilizer G s) ⊆ s - {a}
theorem
MulAction.stabilizer_finite
{G : Type u_1}
[Group G]
{s : Set G}
(hs₀ : s.Nonempty)
(hs : s.Finite)
:
(↑(MulAction.stabilizer G s)).Finite
theorem
AddAction.stabilizer_finite
{G : Type u_1}
[AddGroup G]
{s : Set G}
(hs₀ : s.Nonempty)
(hs : s.Finite)
:
(↑(AddAction.stabilizer G s)).Finite
theorem
MulAction.smul_set_stabilizer_subset
{G : Type u_1}
[CommGroup G]
{s : Set G}
{a : G}
(ha : a ∈ s)
:
a • ↑(MulAction.stabilizer G s) ⊆ s
theorem
AddAction.vadd_set_stabilizer_subset
{G : Type u_1}
[AddCommGroup G]
{s : Set G}
{a : G}
(ha : a ∈ s)
:
a +ᵥ ↑(AddAction.stabilizer G s) ⊆ s
Stabilizer of a subgroup #
@[simp]
theorem
MulAction.stabilizer_subgroup
{G : Type u_1}
[Group G]
(s : Subgroup G)
:
MulAction.stabilizer G ↑s = s
@[simp]
theorem
AddAction.stabilizer_addSubgroup
{G : Type u_1}
[AddGroup G]
(s : AddSubgroup G)
:
AddAction.stabilizer G ↑s = s
@[simp]
theorem
MulAction.stabilizer_op_subgroup
{G : Type u_1}
[Group G]
(s : Subgroup G)
:
MulAction.stabilizer Gᵐᵒᵖ ↑s = s.op
@[simp]
theorem
AddAction.stabilizer_op_addSubgroup
{G : Type u_1}
[AddGroup G]
(s : AddSubgroup G)
:
AddAction.stabilizer Gᵃᵒᵖ ↑s = s.op
@[simp]
theorem
MulAction.stabilizer_subgroup_op
{G : Type u_1}
[Group G]
(s : Subgroup Gᵐᵒᵖ)
:
MulAction.stabilizer G ↑s = s.unop
@[simp]
theorem
AddAction.stabilizer_addSubgroup_op
{G : Type u_1}
[AddGroup G]
(s : AddSubgroup Gᵃᵒᵖ)
:
AddAction.stabilizer G ↑s = s.unop
Stabilizer of a finset #
@[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_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_finset_empty
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
[DecidableEq α]
:
@[simp]
theorem
AddAction.stabilizer_finset_empty
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
[DecidableEq α]
:
@[simp]
theorem
MulAction.stabilizer_finset_univ
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
[DecidableEq α]
[Fintype α]
:
MulAction.stabilizer G Finset.univ = ⊤
@[simp]
theorem
AddAction.stabilizer_finset_univ
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
[DecidableEq α]
[Fintype α]
:
AddAction.stabilizer G Finset.univ = ⊤
@[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
@[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
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
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
{a : G}
[DecidableEq α]
{s : Finset α}
:
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_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_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_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'
{G : Type u_1}
{α : Type u_3}
[Group G]
[MulAction G α]
{a : G}
[DecidableEq α]
{s : Finset α}
:
theorem
AddAction.mem_stabilizer_finset'
{G : Type u_1}
{α : Type u_3}
[AddGroup G]
[AddAction G α]
{a : G}
[DecidableEq α]
{s : Finset α}
:
Stabilizer of a finite set #
Stabilizer in a commutative group #
@[simp]
theorem
MulAction.mul_stabilizer_self
{G : Type u_1}
[CommGroup G]
(s : Set G)
:
s * ↑(MulAction.stabilizer G s) = s
@[simp]
theorem
AddAction.add_stabilizer_self
{G : Type u_1}
[AddCommGroup G]
(s : Set G)
:
s + ↑(AddAction.stabilizer G s) = 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) = ⊥
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) = ⊥