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 MulAction.stabilizer_empty {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] :
stabilizer G ∅ = ⊤
source
@[simp]
theorem AddAction.stabilizer_empty {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] :
stabilizer G ∅ = ⊤
source
@[simp]
theorem MulAction.stabilizer_univ {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] :
stabilizer G Set.univ = ⊤
source
@[simp]
theorem AddAction.stabilizer_univ {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] :
stabilizer G Set.univ = ⊤
source
@[simp]
theorem MulAction.stabilizer_singleton {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] (b : α) :
stabilizer G {b} = stabilizer G b
source
@[simp]
theorem AddAction.stabilizer_singleton {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] (b : α) :
stabilizer G {b} = stabilizer G b
source
theorem MulAction.mem_stabilizer_set {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {a : G} {s : Set α} :
a ∈ stabilizer G s ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
source
theorem AddAction.mem_stabilizer_set {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {a : G} {s : Set α} :
a ∈ stabilizer G s ↔ ∀ (b : α), a +ᵥ b ∈ s ↔ b ∈ 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 (stabilizer G s) ≤ stabilizer H (⇑f '' 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 (stabilizer G s) ≤ stabilizer H (⇑f '' s)
source
@[simp]
theorem MulAction.stabilizer_mul_self {G : Type u_1} [Group G] (s : Set G) :
↑(stabilizer G s) * s = s
source
@[simp]
theorem AddAction.stabilizer_add_self {G : Type u_1} [AddGroup G] (s : Set G) :
↑(stabilizer G s) + s = s
source
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)) :
stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (f s t)
source
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)) :
stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (f s t)
source
theorem MulAction.stabilizer_inf_stabilizer_le_stabilizer_union {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s t : Set α} :
stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (s ∪ t)
source
theorem AddAction.stabilizer_inf_stabilizer_le_stabilizer_union {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s t : Set α} :
stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (s ∪ t)
source
theorem MulAction.stabilizer_inf_stabilizer_le_stabilizer_inter {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s t : Set α} :
stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (s ∩ t)
source
theorem AddAction.stabilizer_inf_stabilizer_le_stabilizer_inter {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s t : Set α} :
stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (s ∩ t)
source
theorem MulAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s t : Set α} :
stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (s \ t)
source
theorem AddAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s t : Set α} :
stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (s \ t)
source
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 : stabilizer G s ≤ stabilizer G t) (hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t) :
stabilizer G (s ∪ t) = stabilizer G s
source
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 : stabilizer G s ≤ stabilizer G t) (hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t) :
stabilizer G (s ∪ t) = stabilizer G s
source
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 : stabilizer G t ≤ stabilizer G s) (hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G s) :
stabilizer G (s ∪ t) = stabilizer G t
source
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 : stabilizer G t ≤ stabilizer G s) (hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G s) :
stabilizer G (s ∪ t) = stabilizer G t
source
theorem MulAction.op_smul_set_stabilizer_subset {G : Type u_1} [Group G] {a : G} {s : Set G} (ha : a ∈ s) :
MulOpposite.op a • ↑(stabilizer G s) ⊆ s
source
theorem AddAction.op_vadd_set_stabilizer_subset {G : Type u_1} [AddGroup G] {a : G} {s : Set G} (ha : a ∈ s) :
AddOpposite.op a +ᵥ ↑(stabilizer G s) ⊆ s
source
theorem MulAction.stabilizer_subset_div_right {G : Type u_1} [Group G] {a : G} {s : Set G} (ha : a ∈ s) :
↑(stabilizer G s) ⊆ s / {a}
source
theorem AddAction.stabilizer_subset_sub_right {G : Type u_1} [AddGroup G] {a : G} {s : Set G} (ha : a ∈ s) :
↑(stabilizer G s) ⊆ s - {a}
source
theorem MulAction.stabilizer_finite {G : Type u_1} [Group G] {s : Set G} (hs₀ : s.Nonempty) (hs : s.Finite) :
(↑(stabilizer G s)).Finite
source
theorem AddAction.stabilizer_finite {G : Type u_1} [AddGroup G] {s : Set G} (hs₀ : s.Nonempty) (hs : s.Finite) :
(↑(stabilizer G s)).Finite
source
theorem MulAction.smul_set_stabilizer_subset {G : Type u_1} [CommGroup G] {s : Set G} {a : G} (ha : a ∈ s) :
a • ↑(stabilizer G s) ⊆ s
source
theorem AddAction.vadd_set_stabilizer_subset {G : Type u_1} [AddCommGroup G] {s : Set G} {a : G} (ha : a ∈ s) :
a +ᵥ ↑(stabilizer G s) ⊆ s

Stabilizer of a subgroup #

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

Stabilizer of a finset #

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

Stabilizer of a finite set #

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 ∈ stabilizer G s ↔ s ⊆ a • s
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 ∈ stabilizer G s ↔ s ⊆ a +ᵥ 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 ∈ stabilizer G s ↔ a • s ⊆ 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 ∈ stabilizer G s ↔ a +ᵥ s ⊆ s
source
@[deprecated MulAction.mem_stabilizer_set_iff_subset_smul_set (since := "2024-11-25")]
theorem MulAction.mem_stabilizer_of_finite_iff_smul_le {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {a : G} {s : Set α} (hs : s.Finite) :
a ∈ stabilizer G s ↔ s ⊆ a • s

Alias of MulAction.mem_stabilizer_set_iff_subset_smul_set.

source
@[deprecated MulAction.mem_stabilizer_set_iff_smul_set_subset (since := "2024-11-25")]
theorem MulAction.mem_stabilizer_of_finite_iff_le_smul {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {a : G} {s : Set α} (hs : s.Finite) :
a ∈ stabilizer G s ↔ a • s ⊆ s

Alias of MulAction.mem_stabilizer_set_iff_smul_set_subset.

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 ∈ stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ 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 ∈ stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a +ᵥ b ∈ s

Stabilizer in a commutative group #

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