Combinations

Combinations in a type are finite subsets of given cardinality. This file provides some API for handling them, especially in the context of a group action.

• Set.powersetCard α n is the set of all Finset α with cardinality n. The name is chosen in relation with Finset.powersetCard which corresponds to the analogous structure for subsets of given cardinality of a given Finset, as a Finset.

• Set.powersetCard.card proves that the Nat.card-cardinality of this set is equal to (Nat.card α).choose n.

• Set.powersetCard.subMulAction: When a group G acts on α, the SubMulAction of G on powersetCard α n.

This induces a MulAction G (powersetCard α n) instance. Then:

• Set.powerSetCard.mulActionHom_of_embedding: the equivariant map from Fin n ↪ α to powersetCard α n.

• Set.powersetCard.isPretransitive_of_isMultiplyPretransitive shows the pretransitivity of that action if the action of G on α is n-pretransitive.

• Set.powersetCard.isPretransitive shows that Equiv.Perm α acts pretransitively on powersetCard α n, for all n.

• Set.powersetCard.compl: Given an equality m + n = Fintype.card α, the complement of an n-combination, as an m-combination. This map is an equivariant map with respect to a group action on α.

• Set.powersetCard.mulActionHom_singleton: The obvious map from α to powersetCard α 1, as an equivariant map.

def Set.powersetCard (α : Type u_2) (n : ℕ) : Set (Finset α)

The type of combinations of n elements of a type α.

See also Finset.powersetCard.

Equations

• Set.powersetCard α n = {s : Finset α | s.card = n}

@[simp]

theorem Set.powersetCard.mem_iff {α : Type u_2} {n : ℕ} {s : Finset α} : s ∈ powersetCard α n ↔ s.card = n

instance Set.powersetCard.instSetLikeElemFinset {α : Type u_2} {n : ℕ} : SetLike (↑(powersetCard α n)) α

Equations

• Set.powersetCard.instSetLikeElemFinset = SetLike.instSubtype

instance Set.powersetCard.instPartialOrderElemFinset {α : Type u_2} {n : ℕ} : PartialOrder ↑(powersetCard α n)

Equations

• Set.powersetCard.instPartialOrderElemFinset = PartialOrder.ofSetLike (↑(Set.powersetCard α n)) α

@[simp]

theorem Set.powersetCard.coe_coe {α : Type u_2} {n : ℕ} {s : ↑(powersetCard α n)} : ↑↑s = ↑s

theorem Set.powersetCard.mem_coe_iff {α : Type u_2} {n : ℕ} {s : ↑(powersetCard α n)} {a : α} : a ∈ ↑s ↔ a ∈ s

theorem Set.powersetCard.card_eq {α : Type u_2} {n : ℕ} (s : ↑(powersetCard α n)) : (↑s).card = n

theorem Set.powersetCard.ncard_eq {α : Type u_2} {n : ℕ} (s : ↑(powersetCard α n)) : (↑s).ncard = n

theorem Set.powersetCard.coe_nonempty_iff {α : Type u_2} {n : ℕ} {s : ↑(powersetCard α n)} : (↑s).Nonempty ↔ 1 ≤ n

theorem Set.powersetCard.coe_nontrivial_iff {α : Type u_2} {n : ℕ} {s : ↑(powersetCard α n)} : (↑s).Nontrivial ↔ 1 < n

theorem Set.powersetCard.eq_iff_subset {α : Type u_2} {n : ℕ} {s t : ↑(powersetCard α n)} : s = t ↔ ↑s ⊆ ↑t

theorem Set.powersetCard.exists_mem_notMem {α : Type u_2} {n : ℕ} (hn : 1 ≤ n) (hα : ↑n < ENat.card α) {a b : α} (hab : a ≠ b) : ∃ (s : ↑(powersetCard α n)), a ∈ s ∧ b ∉ s

def Set.powersetCard.subMulAction (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] (n : ℕ) [DecidableEq α] : SubMulAction G (Finset α)

Set.powersetCard α n as a SubMulAction of Finset α.

Equations

• Set.powersetCard.subMulAction G α n = { carrier := Set.powersetCard α n, smul_mem' := ⋯ }

def Set.powersetCard.subAddAction (G : Type u_1) [AddGroup G] (α : Type u_2) [AddAction G α] (n : ℕ) [DecidableEq α] : SubAddAction G (Finset α)

Set.powersetCard α n as a SubAddAction of Finsetα.

Equations

• Set.powersetCard.subAddAction G α n = { carrier := Set.powersetCard α n, vadd_mem' := ⋯ }

instance Set.powersetCard.instMulActionElemFinset (G : Type u_1) [Group G] {α : Type u_2} [MulAction G α] {n : ℕ} [DecidableEq α] : MulAction G ↑(powersetCard α n)

Equations

• Set.powersetCard.instMulActionElemFinset G = (Set.powersetCard.subMulAction G α n).mulAction

instance Set.powersetCard.instAddActionElemFinset (G : Type u_1) [AddGroup G] {α : Type u_2} [AddAction G α] {n : ℕ} [DecidableEq α] : AddAction G ↑(powersetCard α n)

Equations

• Set.powersetCard.instAddActionElemFinset G = (Set.powersetCard.subAddAction G α n).addAction

@[simp]

theorem Set.powersetCard.coe_smul {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] [DecidableEq α] {n : ℕ} {g : G} {s : ↑(powersetCard α n)} : ↑(g • s) = g • ↑s

@[simp]

theorem Set.powersetCard.coe_vadd {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] [DecidableEq α] {n : ℕ} {g : G} {s : ↑(powersetCard α n)} : ↑(g +ᵥ s) = g +ᵥ ↑s

theorem Set.powersetCard.stabilizer_coe {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] [DecidableEq α] {n : ℕ} (s : ↑(powersetCard α n)) : MulAction.stabilizer G s = MulAction.stabilizer G ↑s

theorem Set.powersetCard.addAction_stabilizer_coe {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] [DecidableEq α] {n : ℕ} (s : ↑(powersetCard α n)) : AddAction.stabilizer G s = AddAction.stabilizer G ↑s

theorem Set.powersetCard.addAction_faithful {α : Type u_2} [DecidableEq α] {G : Type u_3} [AddGroup G] [AddAction G α] {n : ℕ} (hn : 1 ≤ n) (hα : ↑n < ENat.card α) {g : G} : AddAction.toPerm g = 1 ↔ AddAction.toPerm g = 1

theorem Set.powersetCard.faithfulVAdd {α : Type u_2} [DecidableEq α] {G : Type u_3} [AddGroup G] [AddAction G α] {n : ℕ} (hn : 1 ≤ n) (hα : ↑n < ENat.card α) [FaithfulVAdd G α] : FaithfulVAdd G ↑(powersetCard α n)

If an additive group G acts faithfully on α, then it acts faithfully on powersetCard α n, provided 1 ≤ n < ENat.card α.

theorem Set.powersetCard.mulAction_faithful {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {n : ℕ} [DecidableEq α] (hn : 1 ≤ n) (hα : ↑n < ENat.card α) {g : G} : MulAction.toPerm g = 1 ↔ MulAction.toPerm g = 1

theorem Set.powersetCard.faithfulSMul {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {n : ℕ} [DecidableEq α] (hn : 1 ≤ n) (hα : ↑n < ENat.card α) [FaithfulSMul G α] : FaithfulSMul G ↑(powersetCard α n)

If a group G acts faithfully on α, then it acts faithfull on powersetCard α n provided 1 ≤ n < ENat.card α.

def Set.powersetCard.mulActionHom_of_embedding (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] (n : ℕ) [DecidableEq α] : (Fin n ↪ α) →ₑ[id] ↑(powersetCard α n)

The equivariant map from embeddings of Fin n (aka arrangement) to combinations.

Equations

• Set.powersetCard.mulActionHom_of_embedding G α n = { toFun := fun (f : Fin n ↪ α) => ⟨Finset.map f Finset.univ, ⋯⟩, map_smul' := ⋯ }

def Set.powersetCard.addActionHom_of_embedding (G : Type u_1) [AddGroup G] (α : Type u_2) [AddAction G α] (n : ℕ) [DecidableEq α] : (Fin n ↪ α) →ₑ[id] ↑(powersetCard α n)

The equivariant map from embeddings of Fin n (aka arrangements) to combinations.

Equations

• Set.powersetCard.addActionHom_of_embedding G α n = { toFun := fun (f : Fin n ↪ α) => ⟨Finset.map f Finset.univ, ⋯⟩, map_vadd' := ⋯ }

theorem Set.powersetCard.coe_mulActionHom_of_embedding (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] {n : ℕ} [DecidableEq α] (f : Fin n ↪ α) : ↑((mulActionHom_of_embedding G α n).toFun f) = Finset.map f Finset.univ

theorem Set.powersetCard.coe_addActionHom_of_embedding (G : Type u_1) [AddGroup G] (α : Type u_2) [AddAction G α] {n : ℕ} [DecidableEq α] (f : Fin n ↪ α) : ↑((addActionHom_of_embedding G α n).toFun f) = Finset.map f Finset.univ

theorem Set.powersetCard.mulActionHom_of_embedding_surjective (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] {n : ℕ} [DecidableEq α] : Function.Surjective ⇑(mulActionHom_of_embedding G α n)

theorem Set.powersetCard.addActionHom_of_embedding_surjective (G : Type u_1) [AddGroup G] (α : Type u_2) [AddAction G α] {n : ℕ} [DecidableEq α] : Function.Surjective ⇑(addActionHom_of_embedding G α n)

theorem Set.powersetCard.coe_finset (α : Type u_2) (n : ℕ) [Fintype α] : powersetCard α n = ↑(Finset.powersetCard n Finset.univ)

instance Set.powersetCard.instFiniteElemFinset (α : Type u_2) (n : ℕ) [Finite α] : Finite ↑(powersetCard α n)

theorem Set.powersetCard.card (α : Type u_2) (n : ℕ) : Nat.card ↑(powersetCard α n) = (Nat.card α).choose n

theorem Set.powersetCard.nontrivial {α : Type u_2} {n : ℕ} (h1 : 0 < n) (h2 : ↑n < ENat.card α) : Nontrivial ↑(powersetCard α n)

If 0 < n < ENat.card α, then powersetCard α n is nontrivial.

theorem Set.powersetCard.nontrivial' {α : Type u_2} {n : ℕ} (h1 : 0 < n) (h2 : n < Nat.card α) : Nontrivial ↑(powersetCard α n)

A variant of Set.powersetCard.nontrivial that uses Nat.card.

theorem Set.powersetCard.eq_empty_iff {α : Type u_2} {n : ℕ} [Finite α] : powersetCard α n = ∅ ↔ Nat.card α < n

theorem Set.powersetCard.nontrivial_iff {α : Type u_2} {n : ℕ} [Finite α] : Nontrivial ↑(powersetCard α n) ↔ 0 < n ∧ n < Nat.card α

theorem Set.powersetCard.infinite (α : Type u_2) {n : ℕ} (h : 0 < n) [Infinite α] : Infinite ↑(powersetCard α n)

theorem Set.powersetCard.isPretransitive_of_isMultiplyPretransitive (G : Type u_1) [Group G] {α : Type u_2} [MulAction G α] {n : ℕ} [DecidableEq α] (h : MulAction.IsMultiplyPretransitive G α n) : MulAction.IsPretransitive G ↑(powersetCard α n)

theorem Set.powersetCard.isPretransitive_of_isMultiplyPretransitive' (G : Type u_1) [AddGroup G] {α : Type u_2} [AddAction G α] {n : ℕ} [DecidableEq α] (h : AddAction.IsMultiplyPretransitive G α n) : AddAction.IsPretransitive G ↑(powersetCard α n)

theorem Set.powersetCard.isPretransitive {α : Type u_2} {n : ℕ} [DecidableEq α] : MulAction.IsPretransitive (Equiv.Perm α) ↑(powersetCard α n)

def Set.powersetCard.compl (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] {n : ℕ} [DecidableEq α] [Fintype α] {m : ℕ} (hm : m + n = Fintype.card α) : ↑(powersetCard α n) →ₑ[id] ↑(powersetCard α m)

The complement of a combination, as an equivariant map.

Equations

• Set.powersetCard.compl G α hm = { toFun := fun (s : ↑(Set.powersetCard α n)) => ⟨(↑s)ᶜ, ⋯⟩, map_smul' := ⋯ }

theorem Set.powersetCard.coe_compl (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] {n : ℕ} [DecidableEq α] [Fintype α] {m : ℕ} {hm : m + n = Fintype.card α} {s : ↑(powersetCard α n)} : ↑((compl G α hm) s) = (↑s)ᶜ

theorem Set.powersetCard.mem_compl (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] {n : ℕ} [DecidableEq α] [Fintype α] {m : ℕ} {hm : m + n = Fintype.card α} {s : ↑(powersetCard α n)} {a : α} : a ∈ (compl G α hm) s ↔ a ∉ s

theorem Set.powersetCard.compl_compl (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] {n : ℕ} [DecidableEq α] [Fintype α] {m : ℕ} (hm : m + n = Fintype.card α) : (compl G α ⋯).comp (compl G α hm) = MulActionHom.id G

theorem Set.powersetCard.compl_bijective (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] {n : ℕ} [DecidableEq α] [Fintype α] {m : ℕ} (hm : m + n = Fintype.card α) : Function.Bijective ⇑(compl G α hm)

def Set.powersetCard.mulActionHom_singleton (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] [DecidableEq α] : α →ₑ[id] ↑(powersetCard α 1)

The obvious map from a type to its 1-combinations, as an equivariant map.

Equations

• Set.powersetCard.mulActionHom_singleton G α = { toFun := fun (x : α) => ⟨{x}, ⋯⟩, map_smul' := ⋯ }

def Set.powersetCard.addActionHom_singleton (G : Type u_1) [AddGroup G] (α : Type u_2) [AddAction G α] [DecidableEq α] : α →ₑ[id] ↑(powersetCard α 1)

The obvious map from a type to its 1-combinations, as an equivariant map.

Equations

• Set.powersetCard.addActionHom_singleton G α = { toFun := fun (x : α) => ⟨{x}, ⋯⟩, map_vadd' := ⋯ }

theorem Set.powersetCard.mulActionHom_singleton_bijective (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] [DecidableEq α] : Function.Bijective ⇑(mulActionHom_singleton G α)

theorem Set.powersetCard.addActionHom_singleton_bijective (G : Type u_1) [AddGroup G] (α : Type u_2) [AddAction G α] [DecidableEq α] : Function.Bijective ⇑(addActionHom_singleton G α)

theorem Set.powersetCard.isPreprimitive_perm {α : Type u_2} [DecidableEq α] {n : ℕ} (h_one_le : 1 ≤ n) (hn : n < Nat.card α) (hα : Nat.card α ≠ 2 * n) : MulAction.IsPreprimitive (Equiv.Perm α) ↑(powersetCard α n)

The action of Equiv.Perm α on Set.powersetCard α n is preprimitive provided 1 ≤ n < Nat.card α and Nat.card α ≠ 2 * n.

This is a consequence that the stabilizer of such a combination is a maximal subgroup.

theorem Set.powersetCard.isPretransitive_alternatingGroup {α : Type u_2} {n : ℕ} [DecidableEq α] [Fintype α] (hα : 3 ≤ Nat.card α) : MulAction.IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

If 3 ≤ Nat.card α, then alternatingGroup α acts transitively on Set.powersetCard α n.

If Nat.card α ≤ 2, then alternatinGroup α is trivial, and the result only holds in the trivial case where powersetCard α n is a subsingleton, that is, when n = 0 or Nat.card α ≤ n.

theorem Set.powersetCard.isPreprimitive_alternatingGroup {α : Type u_2} [DecidableEq α] [Fintype α] {n : ℕ} (h_three_le : 3 ≤ n) (hn : n < Nat.card α) (hα : Nat.card α ≠ 2 * n) : MulAction.IsPreprimitive ↥(alternatingGroup α) ↑(powersetCard α n)

The action of alternatingGroup α on Set.powersetCard α n is preprimitive provided 1 ≤ n < Nat.card α and Nat.card α ≠ 2 * n.