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.

• Nat.Combination α n is the set of all Finset α with cardinality n.

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

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

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

• EmbeddingToCombination.map: the equivariant map from Fin n ↪ α to n.Combination α.

• Nat.Combination.isPretransitive_of_IsMultiplyPretransitive shows the pretransitivity of that action if the action of G on α is n-pretransitive.

• Nat.Combination.isPretransitive shows that Equiv.Perm α acts pretransitively on n.Combination α, for all n.

• Nat.Combination.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 α.

• Nat.toCombination_one_equivariant: The obvious map from α to 1.Combination α, as an equivariant map.

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

The type of combinations of n elements of a type α

Equations

• Nat.Combination α n = {s : Finset α | s.card = n}

@[simp]

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

instance Nat.Combination.instSetLikeElemFinset {α : Type u_2} {n : ℕ} : SetLike (↑(Combination α n)) α

Equations

• Nat.Combination.instSetLikeElemFinset = SetLike.instSubtype

@[simp]

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

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

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

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

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

Nat.Combination α n as a SubMulAction of Finset α.

Equations

• Nat.Combination.subMulAction G α n = { carrier := Nat.Combination α n, smul_mem' := ⋯ }

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

Nat.Combination α n as a SubAddAction of Finsetα.

Equations

• Nat.Combination.subAddAction G α n = { carrier := Nat.Combination α n, vadd_mem' := ⋯ }

instance Nat.Combination.instMulActionElemFinsetOfDecidableEq (G : Type u_1) [Group G] {α : Type u_2} [MulAction G α] {n : ℕ} [DecidableEq α] : MulAction G ↑(Combination α n)

Equations

• Nat.Combination.instMulActionElemFinsetOfDecidableEq G = (Nat.Combination.subMulAction G α n).mulAction

instance Nat.Combination.instAddActionElemFinsetOfDecidableEq (G : Type u_1) [AddGroup G] {α : Type u_2} [AddAction G α] {n : ℕ} [DecidableEq α] : AddAction G ↑(Combination α n)

Equations

• Nat.Combination.instAddActionElemFinsetOfDecidableEq G = (Nat.Combination.subAddAction G α n).addAction

@[simp]

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

@[simp]

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

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

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

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

theorem Nat.Combination.mulAction_faithful {G : Type u_3} [Group G] {α : Type u_4} [MulAction G α] {n : ℕ} [DecidableEq α] (hn : 1 ≤ n) (hα : ↑n < ENat.card α) {g : G} : MulAction.toPerm g = 1 ↔ MulAction.toPerm g = 1

theorem Nat.Combination.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 ↑(Combination α n)

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

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

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

Equations

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

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

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

Equations

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

theorem Nat.Combination.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 Nat.Combination.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 Nat.Combination.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 Nat.Combination.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 Nat.Combination.card (α : Type u_2) {n : ℕ} : Nat.card ↑(Combination α n) = (Nat.card α).choose n

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

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

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

A variant of Nat.Combination.nontrivial that uses Nat.card.

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

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

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

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

The complement of a combination, as an equivariant map.

Equations

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

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

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

theorem Nat.Combination.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 Nat.Combination.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 Nat.Combination.mulActionHom_singleton (G : Type u_1) [Group G] (α : Type u_2) [MulAction G α] [DecidableEq α] : α →ₑ[id] ↑(Combination α 1)

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

Equations

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

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

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

Equations

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

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

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