Stabilizer of a finset

This file defines the stabilizer of a finset of a group as a finset.

Main declarations

• Finset.mulStab: The stabilizer of a nonempty finset as a finset.

@[implicit_reducible]

instance Finset.instDecidablePredMemSubgroupStabilizerSetCoe_miscYD {α : Type u_2} [Group α] [DecidableEq α] (s : Finset α) : DecidablePred fun (x : α) => x ∈ MulAction.stabilizer α ↑s

Equations

• s.instDecidablePredMemSubgroupStabilizerSetCoe_miscYD a = decidable_of_iff (a ∈ MulAction.stabilizer α s) ⋯

@[implicit_reducible]

instance Finset.instDecidablePredMemAddSubgroupStabilizerSetCoe_miscYD {α : Type u_2} [AddGroup α] [DecidableEq α] (s : Finset α) : DecidablePred fun (x : α) => x ∈ AddAction.stabilizer α ↑s

Equations

• s.instDecidablePredMemAddSubgroupStabilizerSetCoe_miscYD a = decidable_of_iff (a ∈ AddAction.stabilizer α s) ⋯

def Finset.mulStab {α : Type u_2} [Group α] [DecidableEq α] (s : Finset α) : Finset α

The stabilizer of s as a finset. As an exception, this sends ∅ to ∅.

Equations

• s.mulStab = {a ∈ s / s | a • s = s}

def Finset.addStab {α : Type u_2} [AddGroup α] [DecidableEq α] (s : Finset α) : Finset α

The stabilizer of s as a finset. As an exception, this sends ∅ to ∅.

Equations

• s.addStab = {a ∈ s - s | a +ᵥ s = s}

@[simp]

theorem Finset.mem_mulStab {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nonempty) : a ∈ s.mulStab ↔ a • s = s

@[simp]

theorem Finset.mem_addStab {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nonempty) : a ∈ s.addStab ↔ a +ᵥ s = s

theorem Finset.mulStab_subset_div {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} : s.mulStab ⊆ s / s

theorem Finset.addStab_subset_sub {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} : s.addStab ⊆ s - s

theorem Finset.mulStab_subset_div_right {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) : s.mulStab ⊆ s / {a}

theorem Finset.addStab_subset_sub_right {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) : s.addStab ⊆ s - {a}

@[simp]

theorem Finset.coe_mulStab {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} (hs : s.Nonempty) : ↑s.mulStab = ↑(MulAction.stabilizer α ↑s)

@[simp]

theorem Finset.coe_addStab {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} (hs : s.Nonempty) : ↑s.addStab = ↑(AddAction.stabilizer α ↑s)

theorem Finset.mem_mulStab_iff_subset_smul_finset {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nonempty) : a ∈ s.mulStab ↔ s ⊆ a • s

theorem Finset.mem_addStab_iff_subset_vadd_finset {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nonempty) : a ∈ s.addStab ↔ s ⊆ a +ᵥ s

theorem Finset.mem_mulStab_iff_smul_finset_subset {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nonempty) : a ∈ s.mulStab ↔ a • s ⊆ s

theorem Finset.mem_addStab_iff_vadd_finset_subset {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nonempty) : a ∈ s.addStab ↔ a +ᵥ s ⊆ s

theorem Finset.mem_mulStab' {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nonempty) : a ∈ s.mulStab ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s

theorem Finset.mem_addStab' {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nonempty) : a ∈ s.addStab ↔ ∀ ⦃b : α⦄, b ∈ s → a +ᵥ b ∈ s

@[simp]

theorem Finset.mulStab_empty {α : Type u_2} [Group α] [DecidableEq α] : ∅.mulStab = ∅

@[simp]

theorem Finset.addStab_empty {α : Type u_2} [AddGroup α] [DecidableEq α] : ∅.addStab = ∅

@[simp]

theorem Finset.mulStab_singleton {α : Type u_2} [Group α] [DecidableEq α] (a : α) : {a}.mulStab = 1

@[simp]

theorem Finset.addStab_singleton {α : Type u_2} [AddGroup α] [DecidableEq α] (a : α) : {a}.addStab = 0

theorem Finset.Nonempty.of_mulStab {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} : s.mulStab.Nonempty → s.Nonempty

theorem Finset.Nonempty.of_addStab {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} : s.addStab.Nonempty → s.Nonempty

@[simp]

theorem Finset.one_mem_mulStab {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} : 1 ∈ s.mulStab ↔ s.Nonempty

@[simp]

theorem Finset.zero_mem_addStab {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} : 0 ∈ s.addStab ↔ s.Nonempty

theorem Finset.Nonempty.one_mem_mulStab {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} : s.Nonempty → 1 ∈ s.mulStab

Alias of the reverse direction of Finset.one_mem_mulStab.

theorem Finset.Nonempty.zero_mem_addStab {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} : s.Nonempty → 0 ∈ s.addStab

theorem Finset.Nonempty.mulStab {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} (h : s.Nonempty) : s.mulStab.Nonempty

theorem Finset.Nonempty.addStab {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} (h : s.Nonempty) : s.addStab.Nonempty

@[simp]

theorem Finset.mulStab_nonempty {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} : s.mulStab.Nonempty ↔ s.Nonempty

@[simp]

theorem Finset.addStab_nonempty {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} : s.addStab.Nonempty ↔ s.Nonempty

@[simp]

theorem Finset.card_mulStab_eq_one {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} : s.mulStab.card = 1 ↔ s.mulStab = 1

@[simp]

theorem Finset.card_addStab_eq_zero {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} : s.addStab.card = 1 ↔ s.addStab = 0

theorem Finset.Nonempty.mulStab_nontrivial {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} (h : s.Nonempty) : s.mulStab.Nontrivial ↔ s.mulStab ≠ 1

theorem Finset.Nonempty.addStab_nontrivial {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} (h : s.Nonempty) : s.addStab.Nontrivial ↔ s.addStab ≠ 0

theorem Finset.subset_mulStab_mul_left {α : Type u_2} [Group α] [DecidableEq α] {s t : Finset α} (ht : t.Nonempty) : s.mulStab ⊆ (s * t).mulStab

theorem Finset.subset_addStab_add_left {α : Type u_2} [AddGroup α] [DecidableEq α] {s t : Finset α} (ht : t.Nonempty) : s.addStab ⊆ (s + t).addStab

@[simp]

theorem Finset.mulStab_mul {α : Type u_2} [Group α] [DecidableEq α] (s : Finset α) : s.mulStab * s = s

@[simp]

theorem Finset.addStab_add {α : Type u_2} [AddGroup α] [DecidableEq α] (s : Finset α) : s.addStab + s = s

theorem Finset.mul_subset_right_iff {α : Type u_2} [Group α] [DecidableEq α] {s t : Finset α} (ht : t.Nonempty) : s * t ⊆ t ↔ s ⊆ t.mulStab

theorem Finset.add_subset_right_iff {α : Type u_2} [AddGroup α] [DecidableEq α] {s t : Finset α} (ht : t.Nonempty) : s + t ⊆ t ↔ s ⊆ t.addStab

theorem Finset.mul_subset_right {α : Type u_2} [Group α] [DecidableEq α] {s t : Finset α} : s ⊆ t.mulStab → s * t ⊆ t

theorem Finset.add_subset_right {α : Type u_2} [AddGroup α] [DecidableEq α] {s t : Finset α} : s ⊆ t.addStab → s + t ⊆ t

theorem Finset.smul_mulStab {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s.mulStab) : a • s.mulStab = s.mulStab

theorem Finset.vadd_addStab {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s.addStab) : a +ᵥ s.addStab = s.addStab

@[simp]

theorem Finset.mulStab_mul_mulStab {α : Type u_2} [Group α] [DecidableEq α] (s : Finset α) : s.mulStab * s.mulStab = s.mulStab

@[simp]

theorem Finset.addStab_add_addStab {α : Type u_2} [AddGroup α] [DecidableEq α] (s : Finset α) : s.addStab + s.addStab = s.addStab

theorem Finset.inter_mulStab_subset_mulStab_union {α : Type u_2} [Group α] [DecidableEq α] {s t : Finset α} : s.mulStab ∩ t.mulStab ⊆ (s ∪ t).mulStab

theorem Finset.inter_addStab_subset_addStab_union {α : Type u_2} [AddGroup α] [DecidableEq α] {s t : Finset α} : s.addStab ∩ t.addStab ⊆ (s ∪ t).addStab

theorem Finset.mulStab_subset_div_left {α : Type u_2} [CommGroup α] [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) : s.mulStab ⊆ {a} / s

theorem Finset.addStab_subset_sub_left {α : Type u_2} [AddCommGroup α] [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) : s.addStab ⊆ {a} - s

theorem Finset.subset_mulStab_mul_right {α : Type u_2} [CommGroup α] [DecidableEq α] {s t : Finset α} (hs : s.Nonempty) : t.mulStab ⊆ (s * t).mulStab

theorem Finset.subset_addStab_add_right {α : Type u_2} [AddCommGroup α] [DecidableEq α] {s t : Finset α} (hs : s.Nonempty) : t.addStab ⊆ (s + t).addStab

@[simp]

theorem Finset.mul_mulStab {α : Type u_2} [CommGroup α] [DecidableEq α] (s : Finset α) : s * s.mulStab = s

@[simp]

theorem Finset.add_addStab {α : Type u_2} [AddCommGroup α] [DecidableEq α] (s : Finset α) : s + s.addStab = s

@[simp]

theorem Finset.mul_mulStab_mul_mul_mul_mulStab_mul {α : Type u_2} [CommGroup α] [DecidableEq α] {s t : Finset α} : s * (s * t).mulStab * (t * (s * t).mulStab) = s * t

@[simp]

theorem Finset.add_addStab_add_add_add_addStab_add {α : Type u_2} [AddCommGroup α] [DecidableEq α] {s t : Finset α} : s + (s + t).addStab + (t + (s + t).addStab) = s + t

theorem Finset.smul_finset_mulStab_subset {α : Type u_2} [CommGroup α] [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) : a • s.mulStab ⊆ s

theorem Finset.vadd_finset_addStab_subset {α : Type u_2} [AddCommGroup α] [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) : a +ᵥ s.addStab ⊆ s

theorem Finset.mul_subset_left_iff {α : Type u_2} [CommGroup α] [DecidableEq α] {s t : Finset α} (hs : s.Nonempty) : s * t ⊆ s ↔ t ⊆ s.mulStab

theorem Finset.add_subset_left_iff {α : Type u_2} [AddCommGroup α] [DecidableEq α] {s t : Finset α} (hs : s.Nonempty) : s + t ⊆ s ↔ t ⊆ s.addStab

theorem Finset.mul_subset_left {α : Type u_2} [CommGroup α] [DecidableEq α] {s t : Finset α} : t ⊆ s.mulStab → s * t ⊆ s

theorem Finset.add_subset_left {α : Type u_2} [AddCommGroup α] [DecidableEq α] {s t : Finset α} : t ⊆ s.addStab → s + t ⊆ s

@[simp]

theorem Finset.mulStab_idem {α : Type u_2} [CommGroup α] [DecidableEq α] (s : Finset α) : s.mulStab.mulStab = s.mulStab

@[simp]

theorem Finset.addStab_idem {α : Type u_2} [AddCommGroup α] [DecidableEq α] (s : Finset α) : s.addStab.addStab = s.addStab

@[simp]

theorem Finset.mulStab_smul {α : Type u_2} [CommGroup α] [DecidableEq α] (a : α) (s : Finset α) : (a • s).mulStab = s.mulStab

@[simp]

theorem Finset.addStab_vadd {α : Type u_2} [AddCommGroup α] [DecidableEq α] (a : α) (s : Finset α) : (a +ᵥ s).addStab = s.addStab

theorem Finset.mulStab_image_coe_quotient {α : Type u_2} [CommGroup α] [DecidableEq α] {s : Finset α} (hs : s.Nonempty) : (image QuotientGroup.mk s).mulStab = 1

theorem Finset.addStab_image_coe_quotient {α : Type u_2} [AddCommGroup α] [DecidableEq α] {s : Finset α} (hs : s.Nonempty) : (image QuotientAddGroup.mk s).addStab = 0

theorem Finset.preimage_image_quotientMk_stabilizer_eq_mul_mulStab {α : Type u_2} [CommGroup α] [DecidableEq α] {t : Finset α} (ht : t.Nonempty) (s : Finset α) : QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑s) = ↑s * ↑t.mulStab

theorem Finset.preimage_image_quotientMk_stabilizer_eq_add_addStab {α : Type u_2} [AddCommGroup α] [DecidableEq α] {t : Finset α} (ht : t.Nonempty) (s : Finset α) : QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' ↑s) = ↑s + ↑t.addStab

theorem Finset.preimage_image_quotientMk_mulStabilizer {α : Type u_2} [CommGroup α] (s : Finset α) : QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑s) = ↑s

theorem Finset.preimage_image_quotientMk_addStabilizer {α : Type u_2} [AddCommGroup α] (s : Finset α) : QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' ↑s) = ↑s

theorem Finset.pairwiseDisjoint_smul_finset_mulStab {α : Type u_2} [CommGroup α] [DecidableEq α] (s : Finset α) : (Set.range fun (a : α) => a • s.mulStab).PairwiseDisjoint id

theorem Finset.pairwiseDisjoint_vadd_finset_addStab {α : Type u_2} [AddCommGroup α] [DecidableEq α] (s : Finset α) : (Set.range fun (a : α) => a +ᵥ s.addStab).PairwiseDisjoint id

theorem Finset.disjoint_smul_finset_mulStab_mul_mulStab {α : Type u_2} [CommGroup α] [DecidableEq α] {s t : Finset α} {a : α} : ¬a • s.mulStab ⊆ t * s.mulStab → Disjoint (a • s.mulStab) (t * s.mulStab)

theorem Finset.disjoint_vadd_finset_addStab_add_addStab {α : Type u_2} [AddCommGroup α] [DecidableEq α] {s t : Finset α} {a : α} : ¬a +ᵥ s.addStab ⊆ t + s.addStab → Disjoint (a +ᵥ s.addStab) (t + s.addStab)

theorem Finset.card_mulStab_dvd_card_mul_mulStab {α : Type u_2} [CommGroup α] [DecidableEq α] (s t : Finset α) : t.mulStab.card ∣ (s * t.mulStab).card

theorem Finset.card_addStab_dvd_card_add_addStab {α : Type u_2} [AddCommGroup α] [DecidableEq α] (s t : Finset α) : t.addStab.card ∣ (s + t.addStab).card

theorem Finset.card_mulStab_dvd_card {α : Type u_2} [CommGroup α] [DecidableEq α] (s : Finset α) : s.mulStab.card ∣ s.card

theorem Finset.card_addStab_dvd_card {α : Type u_2} [AddCommGroup α] [DecidableEq α] (s : Finset α) : s.addStab.card ∣ s.card

theorem Finset.card_mulStab_le_card {α : Type u_2} [CommGroup α] [DecidableEq α] {s : Finset α} : s.mulStab.card ≤ s.card

theorem Finset.card_addStab_le_card {α : Type u_2} [AddCommGroup α] [DecidableEq α] {s : Finset α} : s.addStab.card ≤ s.card

theorem Finset.card_mulStab_dvd_card_mulStab {α : Type u_2} [CommGroup α] [DecidableEq α] {s t : Finset α} (hs : s.Nonempty) (h : s.mulStab ⊆ t.mulStab) : s.mulStab.card ∣ t.mulStab.card

theorem Finset.card_addStab_dvd_card_addStab {α : Type u_2} [AddCommGroup α] [DecidableEq α] {s t : Finset α} (hs : s.Nonempty) (h : s.addStab ⊆ t.addStab) : s.addStab.card ∣ t.addStab.card

theorem Finset.card_mulStab_mul_card_image_coe' {α : Type u_2} [CommGroup α] [DecidableEq α] (s t : Finset α) [DecidableEq (α ⧸ MulAction.stabilizer α ↑t)] : t.mulStab.card * (image QuotientGroup.mk s).card = (s * t.mulStab).card

A version of Lagrange's theorem.

theorem Finset.card_addStab_add_card_image_coe' {α : Type u_2} [AddCommGroup α] [DecidableEq α] (s t : Finset α) [DecidableEq (α ⧸ AddAction.stabilizer α ↑t)] : t.addStab.card * (image QuotientAddGroup.mk s).card = (s + t.addStab).card

A version of Lagrange's theorem.

theorem Finset.card_mul_card_eq_mulStab_card_mul_coe {α : Type u_2} [CommGroup α] [DecidableEq α] (s t : Finset α) : (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card

theorem Finset.card_add_card_eq_addStab_card_add_coe {α : Type u_2} [AddCommGroup α] [DecidableEq α] (s t : Finset α) : (s + t).card = (s + t).addStab.card * (image QuotientAddGroup.mk (s + t)).card

theorem Finset.card_mulStab_mul_card_image_coe {α : Type u_2} [CommGroup α] [DecidableEq α] (s t : Finset α) : (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card

A version of Lagrange's theorem.

theorem Finset.card_addStab_add_card_image_coe {α : Type u_2} [AddCommGroup α] [DecidableEq α] (s t : Finset α) : (s + t).addStab.card * (image QuotientAddGroup.mk s + image QuotientAddGroup.mk t).card = (s + t).card

A version of Lagrange's theorem.

theorem Finset.subgroup_mul_card_eq_mul_of_mul_stab_subset {α : Type u_2} [CommGroup α] [DecidableEq α] (s : Subgroup α) [DecidablePred fun (x : α) => x ∈ s] (t : Finset α) (hst : ↑s ⊆ ↑t.mulStab) : Nat.card ↥s * (image QuotientGroup.mk t).card = t.card

theorem Finset.addSubgroup_add_card_eq_add_of_add_stab_subset {α : Type u_2} [AddCommGroup α] [DecidableEq α] (s : AddSubgroup α) [DecidablePred fun (x : α) => x ∈ s] (t : Finset α) (hst : ↑s ⊆ ↑t.addStab) : Nat.card ↥s * (image QuotientAddGroup.mk t).card = t.card

theorem Finset.mulStab_quotient_commute_subgroup {α : Type u_2} [CommGroup α] [DecidableEq α] (s : Subgroup α) [DecidablePred fun (x : α) => x ∈ s] (t : Finset α) (hst : ↑s ⊆ ↑t.mulStab) : image QuotientGroup.mk t.mulStab = (image QuotientGroup.mk t).mulStab

theorem Finset.addStab_quotient_addCommute_addSubgroup {α : Type u_2} [AddCommGroup α] [DecidableEq α] (s : AddSubgroup α) [DecidablePred fun (x : α) => x ∈ s] (t : Finset α) (hst : ↑s ⊆ ↑t.addStab) : image QuotientAddGroup.mk t.addStab = (image QuotientAddGroup.mk t).addStab