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.

source

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' := ⋯ }

Instances For

source

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' := ⋯ }

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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 := Set.powersetCard.ofFinEmb n α, map_smul' := ⋯ }

Instances For

source

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 := Set.powersetCard.ofFinEmb n α, map_vadd' := ⋯ }

Instances For

source

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

source

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

source

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)

source

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)

source

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)

source

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)

source

theorem Set.powersetCard.isPretransitive {α : Type u_2} {n : ℕ} [DecidableEq α] :

MulAction.IsPretransitive (Equiv.Perm α) ↑(powersetCard α n)

source

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.

Equations

Set.powersetCard.mulActionHom_compl G α hm = { toFun := ⇑(Set.powersetCard.compl hm), map_smul' := ⋯ }

Instances For

source

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)ᶜ

source

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

source

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

source

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)

source

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.

Equations

Set.powersetCard.mulActionHom_singleton G α = { toFun := ⇑Set.powersetCard.ofSingleton, map_smul' := ⋯ }

Instances For

source

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.

Equations

Set.powersetCard.addActionHom_singleton G α = { toFun := ⇑Set.powersetCard.ofSingleton, map_vadd' := ⋯ }

Instances For

source

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

Function.Bijective ⇑(mulActionHom_singleton G α)

source

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

Function.Bijective ⇑(addActionHom_singleton G α)

source

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.

source

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.

source

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.

Documentation

Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Combinations #