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]

theorem MulAction.stabilizer_empty {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] : stabilizer G ∅ = ⊤

@[simp]

theorem AddAction.stabilizer_empty {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] : stabilizer G ∅ = ⊤

@[simp]

theorem MulAction.stabilizer_univ {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] : stabilizer G Set.univ = ⊤

@[simp]

theorem AddAction.stabilizer_univ {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] : stabilizer G Set.univ = ⊤

@[simp]

theorem MulAction.stabilizer_singleton {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] (b : α) : stabilizer G {b} = stabilizer G b

@[simp]

theorem AddAction.stabilizer_singleton {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] (b : α) : stabilizer G {b} = stabilizer G b

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

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

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)

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)

@[simp]

theorem MulAction.stabilizer_mul_self {G : Type u_1} [Group G] (s : Set G) : ↑(stabilizer G s) * s = s

@[simp]

theorem AddAction.stabilizer_add_self {G : Type u_1} [AddGroup G] (s : Set G) : ↑(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)) : stabilizer G s ⊓ stabilizer G t ≤ 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)) : stabilizer G s ⊓ stabilizer G t ≤ 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 α} : stabilizer G s ⊓ stabilizer G t ≤ 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 α} : stabilizer G s ⊓ stabilizer G t ≤ 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 α} : stabilizer G s ⊓ stabilizer G t ≤ 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 α} : stabilizer G s ⊓ stabilizer G t ≤ 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 α} : stabilizer G s ⊓ stabilizer G t ≤ 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 α} : stabilizer G s ⊓ stabilizer G t ≤ 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 : stabilizer G s ≤ stabilizer G t) (hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t) : stabilizer G (s ∪ t) = 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 : stabilizer G s ≤ stabilizer G t) (hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t) : stabilizer G (s ∪ t) = 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 : stabilizer G t ≤ stabilizer G s) (hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G s) : stabilizer G (s ∪ t) = 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 : stabilizer G t ≤ stabilizer G s) (hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G s) : stabilizer G (s ∪ t) = 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 • ↑(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 +ᵥ ↑(stabilizer G s) ⊆ s

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}

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}

theorem MulAction.stabilizer_finite {G : Type u_1} [Group G] {s : Set G} (hs₀ : s.Nonempty) (hs : s.Finite) : (↑(stabilizer G s)).Finite

theorem AddAction.stabilizer_finite {G : Type u_1} [AddGroup G] {s : Set G} (hs₀ : s.Nonempty) (hs : s.Finite) : (↑(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 • ↑(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 +ᵥ ↑(stabilizer G s) ⊆ s

Stabilizer of a subgroup

@[simp]

theorem MulAction.stabilizer_subgroup {G : Type u_1} [Group G] (s : Subgroup G) : stabilizer G ↑s = s

@[simp]

theorem AddAction.stabilizer_addSubgroup {G : Type u_1} [AddGroup G] (s : AddSubgroup G) : stabilizer G ↑s = s

@[simp]

theorem MulAction.stabilizer_op_subgroup {G : Type u_1} [Group G] (s : Subgroup G) : stabilizer Gᵐᵒᵖ ↑s = s.op

@[simp]

theorem AddAction.stabilizer_op_addSubgroup {G : Type u_1} [AddGroup G] (s : AddSubgroup G) : stabilizer Gᵃᵒᵖ ↑s = s.op

@[simp]

theorem MulAction.stabilizer_subgroup_op {G : Type u_1} [Group G] (s : Subgroup Gᵐᵒᵖ) : stabilizer G ↑s = s.unop

@[simp]

theorem AddAction.stabilizer_addSubgroup_op {G : Type u_1} [AddGroup G] (s : AddSubgroup Gᵃᵒᵖ) : 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 α) : stabilizer G ↑s = stabilizer G s

@[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

@[simp]

theorem MulAction.stabilizer_finset_empty {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [DecidableEq α] : stabilizer G ∅ = ⊤

@[simp]

theorem AddAction.stabilizer_finset_empty {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [DecidableEq α] : stabilizer G ∅ = ⊤

@[simp]

theorem MulAction.stabilizer_finset_univ {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] [DecidableEq α] [Fintype α] : stabilizer G Finset.univ = ⊤

@[simp]

theorem AddAction.stabilizer_finset_univ {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] [DecidableEq α] [Fintype α] : stabilizer G Finset.univ = ⊤

@[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

@[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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem MulAction.mul_stabilizer_self {G : Type u_1} [CommGroup G] (s : Set G) : s * ↑(stabilizer G s) = s

@[simp]

theorem AddAction.add_stabilizer_self {G : Type u_1} [AddCommGroup G] (s : Set G) : s + ↑(stabilizer G s) = s

theorem MulAction.stabilizer_image_coe_quotient {G : Type u_1} [CommGroup G] (s : Set G) : stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) = ⊥

theorem AddAction.stabilizer_image_coe_quotient {G : Type u_1} [AddCommGroup G] (s : Set G) : stabilizer (G ⧸ stabilizer G s) (QuotientAddGroup.mk '' s) = ⊥