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.

@[instance_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) ⋯

source

@[instance_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) ⋯

source

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}

Instances For

source

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}

Instances For

source

@[simp]

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

a ∈ s.mulStab ↔ a • s = s

source

@[simp]

theorem Finset.mem_addStab {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nonempty) :

a ∈ s.addStab ↔ a +ᵥ s = s

source

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

s.mulStab ⊆ s / s

source

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

s.addStab ⊆ s - s

source

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

s.mulStab ⊆ s / {a}

source

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

s.addStab ⊆ s - {a}

source

@[simp]

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

↑s.mulStab = ↑(MulAction.stabilizer α ↑s)

source

@[simp]

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

↑s.addStab = ↑(AddAction.stabilizer α ↑s)

source

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

source

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

source

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

source

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

source

theorem Finset.mem_mulStab' {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nonempty) :

a ∈ s.mulStab ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s

source

theorem Finset.mem_addStab' {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nonempty) :

a ∈ s.addStab ↔ ∀ ⦃b : α⦄, b ∈ s → a +ᵥ b ∈ s

source

@[simp]

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

∅.mulStab = ∅

source

@[simp]

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

∅.addStab = ∅

source

@[simp]

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

{a}.mulStab = 1

source

@[simp]

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

{a}.addStab = 0

source

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

s.mulStab.Nonempty → s.Nonempty

source

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

s.addStab.Nonempty → s.Nonempty

source

@[simp]

theorem Finset.one_mem_mulStab {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} :

1 ∈ s.mulStab ↔ s.Nonempty

source

@[simp]

theorem Finset.zero_mem_addStab {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} :

0 ∈ s.addStab ↔ s.Nonempty

source

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.

source

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

s.Nonempty → 0 ∈ s.addStab

Alias of the reverse direction of Finset.zero_mem_addStab.

source

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

s.mulStab.Nonempty

source

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

s.addStab.Nonempty

source

@[simp]

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

s.mulStab.Nonempty ↔ s.Nonempty

source

@[simp]

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

s.addStab.Nonempty ↔ s.Nonempty

source

@[simp]

theorem Finset.card_mulStab_eq_one {α : Type u_2} [Group α] [DecidableEq α] {s : Finset α} :

s.mulStab.card = 1 ↔ s.mulStab = 1

source

@[simp]

theorem Finset.card_addStab_eq_zero {α : Type u_2} [AddGroup α] [DecidableEq α] {s : Finset α} :

s.addStab.card = 1 ↔ s.addStab = 0

source

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

s.mulStab.Nontrivial ↔ s.mulStab ≠ 1

source

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

s.addStab.Nontrivial ↔ s.addStab ≠ 0

source

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

s.mulStab ⊆ (s * t).mulStab

source

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

s.addStab ⊆ (s + t).addStab

source

@[simp]

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

s.mulStab * s = s

source

@[simp]

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

s.addStab + s = s

source

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

s * t ⊆ t ↔ s ⊆ t.mulStab

source

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

s + t ⊆ t ↔ s ⊆ t.addStab

source

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

s ⊆ t.mulStab → s * t ⊆ t

source

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

s ⊆ t.addStab → s + t ⊆ t

source

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

a • s.mulStab = s.mulStab

source

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

a +ᵥ s.addStab = s.addStab

source

@[simp]

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

s.mulStab * s.mulStab = s.mulStab

source

@[simp]

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

s.addStab + s.addStab = s.addStab

source

theorem Finset.inter_mulStab_subset_mulStab_union {α : Type u_2} [Group α] [DecidableEq α] {s t : Finset α} :

s.mulStab ∩ t.mulStab ⊆ (s ∪ t).mulStab

source

theorem Finset.inter_addStab_subset_addStab_union {α : Type u_2} [AddGroup α] [DecidableEq α] {s t : Finset α} :

s.addStab ∩ t.addStab ⊆ (s ∪ t).addStab

source

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

s.mulStab ⊆ {a} / s

source

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

s.addStab ⊆ {a} - s

source

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

t.mulStab ⊆ (s * t).mulStab

source

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

t.addStab ⊆ (s + t).addStab

source

@[simp]

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

s * s.mulStab = s

source

@[simp]

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

s + s.addStab = s

source

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

source

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

source

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

a • s.mulStab ⊆ s

source

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

a +ᵥ s.addStab ⊆ s

source

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

s * t ⊆ s ↔ t ⊆ s.mulStab

source

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

s + t ⊆ s ↔ t ⊆ s.addStab

source

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

t ⊆ s.mulStab → s * t ⊆ s

source

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

t ⊆ s.addStab → s + t ⊆ s

source

@[simp]

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

s.mulStab.mulStab = s.mulStab

source

@[simp]

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

s.addStab.addStab = s.addStab

source

@[simp]

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

(a • s).mulStab = s.mulStab

source

@[simp]

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

(a +ᵥ s).addStab = s.addStab

source

theorem Finset.mulStab_image_coe_quotient {α : Type u_2} [CommGroup α] [DecidableEq α] {s : Finset α} (hs : s.Nonempty) :

(image QuotientGroup.mk s).mulStab = 1

source

theorem Finset.addStab_image_coe_quotient {α : Type u_2} [AddCommGroup α] [DecidableEq α] {s : Finset α} (hs : s.Nonempty) :

(image QuotientAddGroup.mk s).addStab = 0

source

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

source

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

source

theorem Finset.preimage_image_quotientMk_mulStabilizer {α : Type u_2} [CommGroup α] (s : Finset α) :

QuotientGroup.mk ⁻¹' QuotientGroup.mk '' ↑s = ↑s

source

theorem Finset.preimage_image_quotientMk_addStabilizer {α : Type u_2} [AddCommGroup α] (s : Finset α) :

QuotientAddGroup.mk ⁻¹' QuotientAddGroup.mk '' ↑s = ↑s

source

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

(Set.range fun (a : α) => a • s.mulStab).PairwiseDisjoint id

source

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

(Set.range fun (a : α) => a +ᵥ s.addStab).PairwiseDisjoint id

source

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)

source

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)

source

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

t.mulStab.card ∣ (s * t.mulStab).card

source

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

t.addStab.card ∣ (s + t.addStab).card

source

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

s.mulStab.card ∣ s.card

source

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

s.addStab.card ∣ s.card

source

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

s.mulStab.card ≤ s.card

source

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

s.addStab.card ≤ s.card

source

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

source

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

source

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.

source

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.

source

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

source

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

source

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.

source

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.

source

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

source

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

source

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

source

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

Documentation

MiscYD.AddCombi.Kneser.MulStab

Stabilizer of a finset #

Main declarations #