Combinations

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

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

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α.

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

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

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

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.

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.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.mulActionHom_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.

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

theorem Set.powersetCard.mem_mulActionHom_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 ∈ (mulActionHom_compl G α hm) s ↔ a ∉ s

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

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

noncomputable 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.

noncomputable 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.

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.