Counting embeddings

The injective maps α → β between finite types correspond to the embeddings α ↪ β, so there are (card β).descFactorial (card α) of them. We restate Fintype.card_embedding_eq for the subtype of injective functions, the form in which counts over injective tuples Fin n → V are taken.

We also count embeddings into prescribed cells. Given a family c : ι → Finset V of cells, we count the embeddings f : ι ↪ V with f i ∈ c i for every i. When the cells are taken from a pairwise disjoint family, injectivity only constrains indices sharing a cell, so the count factors over the cells: a cell A hosting m indices contributes the falling factorial (#A).descFactorial m, and an unused cell contributes one. In particular, distinct cells contribute just their sizes, and in general the count is at most the product of the sizes of the cells.

Finally, we bound the embeddings with prescribed values on part of the domain. An embedding f : β ↪ V with f ∘ e = x along an embedding e : α ↪ β is determined by its values off the range of e, so there are at most card V ^ (card β - card α) of them. When β is a linear order, summing over the (card β).choose m increasing tuples g : Fin m ↪o β bounds the embeddings sending some increasing m-tuple into a prescribed set T of m-tuples.

Main results

• Fintype.card_subtype_injective: there are (card β).descFactorial (card α) injective maps α → β.
• Equiv.embeddingMemEquivPi: over a pairwise disjoint family of cells, the embeddings into the cells are the families of embeddings, one for each cell, of the indices assigned to that cell.
• Nat.card_embedding_mem_eq_prod_descFactorial: the count over a pairwise disjoint family of cells is the product of falling factorials of the cell sizes at the occurrence counts.
• Nat.card_embedding_mem_eq_prod_of_injective: for distinct disjoint cells, the count is the product of the cell sizes.
• Nat.card_embedding_mem_le_prod: the count never exceeds the product of the cell sizes.
• Function.Embedding.natCard_embedding_comp_eq_le: at most card V ^ (card β - card α) embeddings f : β ↪ V satisfy f ∘ e = x.
• Finset.natCard_embedding_exists_comp_mem_le: at most (card β).choose m * #T * card V ^ (card β - m) embeddings send some increasing m-tuple into T.
• Finset.card_filter_injective_exists_mem_le: at most n * #B * card V ^ (n - 1) injective n-tuples meet a prescribed set B of vertices.

theorem Fintype.card_subtype_injective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [Fintype { f : α → β // Function.Injective f }] : card { f : α → β // Function.Injective f } = (card β).descFactorial (card α)

There are (card β).descFactorial (card α) injective maps α → β; for instance |V| (|V| - 1) (|V| - 2) injective triples Fin 3 → V. This is Fintype.card_embedding_eq for the subtype of injective functions.

def Equiv.embeddingMemEquivPi {ι : Type u_1} {V : Type u_2} (c : ι → Finset V) {s : Finset (Finset V)} (hs : ∀ (i : ι), c i ∈ s) (hdisj : (↑s).PairwiseDisjoint id) : { f : ι ↪ V // ∀ (i : ι), f i ∈ c i } ≃ ((A : ↥s) → { i : ι // c i = ↑A } ↪ ↥↑A)

Embeddings into disjoint cells, cell by cell. If the cells c i lie in a pairwise disjoint family s, an embedding f : ι ↪ V with f i ∈ c i for all i is the same as a family, indexed by the cells A ∈ s, of embeddings of the indices assigned to A into A.

@[simp]

theorem Equiv.embeddingMemEquivPi_apply_apply_coe {ι : Type u_1} {V : Type u_2} {c : ι → Finset V} {s : Finset (Finset V)} (hs : ∀ (i : ι), c i ∈ s) (hdisj : (↑s).PairwiseDisjoint id) (f : { f : ι ↪ V // ∀ (i : ι), f i ∈ c i }) (A : ↥s) (x : { i : ι // c i = ↑A }) : ↑(((embeddingMemEquivPi c hs hdisj) f A) x) = ↑f ↑x

@[simp]

theorem Equiv.embeddingMemEquivPi_symm_apply_coe_apply {ι : Type u_1} {V : Type u_2} {c : ι → Finset V} {s : Finset (Finset V)} (hs : ∀ (i : ι), c i ∈ s) (hdisj : (↑s).PairwiseDisjoint id) (g : (A : ↥s) → { i : ι // c i = ↑A } ↪ ↥↑A) (i : ι) : ↑((embeddingMemEquivPi c hs hdisj).symm g) i = ↑((g ⟨c i, ⋯⟩) ⟨i, ⋯⟩)

theorem Nat.card_embedding_mem_eq_prod_descFactorial {ι : Type u_1} {V : Type u_2} [Finite ι] (c : ι → Finset V) {s : Finset (Finset V)} (hs : ∀ (i : ι), c i ∈ s) (hdisj : (↑s).PairwiseDisjoint id) : Nat.card { f : ι ↪ V // ∀ (i : ι), f i ∈ c i } = ∏ A ∈ s, A.card.descFactorial (Function.occCount c A)

Embeddings into disjoint cells. If the cells c i lie in a pairwise disjoint family s, then the embeddings f : ι ↪ V with f i ∈ c i for all i are counted cell by cell: each cell A ∈ s contributes the falling factorial of its size at the number of indices assigned to it.

theorem Nat.card_embedding_mem_eq_prod_of_injective {ι : Type u_1} {V : Type u_2} [Fintype ι] {c : ι → Finset V} (hc : Function.Injective c) {s : Finset (Finset V)} (hs : ∀ (i : ι), c i ∈ s) (hdisj : (↑s).PairwiseDisjoint id) : Nat.card { f : ι ↪ V // ∀ (i : ι), f i ∈ c i } = ∏ i : ι, (c i).card

Embeddings into distinct disjoint cells. If the cells c i are pairwise distinct members of a pairwise disjoint family, the embeddings f : ι ↪ V with f i ∈ c i for all i are counted by the product of the cell sizes.

theorem Nat.card_embedding_mem_le_prod {ι : Type u_1} {V : Type u_2} [Fintype ι] (c : ι → Finset V) : Nat.card { f : ι ↪ V // ∀ (i : ι), f i ∈ c i } ≤ ∏ i : ι, (c i).card

The embeddings f : ι ↪ V with f i ∈ c i for all i are at most as many as the product of the cell sizes, the number of all maps with this property.

theorem Function.Embedding.natCard_embedding_comp_eq_le {V : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [Fintype V] (e : α ↪ β) (x : α → V) : Nat.card { f : β ↪ V // ⇑f ∘ ⇑e = x } ≤ Fintype.card V ^ (Fintype.card β - Fintype.card α)

An embedding f : β ↪ V with prescribed values f ∘ e = x along an embedding e : α ↪ β is determined by its values off the range of e, so there are at most card V ^ (card β - card α) of them.

theorem Finset.natCard_embedding_exists_comp_mem_le {V : Type u_1} {β : Type u_2} [Fintype β] [LinearOrder β] [Fintype V] {m : ℕ} (T : Finset (Fin m → V)) : Nat.card { f : β ↪ V // ∃ (g : Fin m ↪o β), ⇑f ∘ ⇑g ∈ T } ≤ (Fintype.card β).choose m * T.card * Fintype.card V ^ (Fintype.card β - m)

At most (card β).choose m * #T * card V ^ (card β - m) embeddings f : β ↪ V of a finite linear order send some increasing m-tuple of β into a prescribed set T of m-tuples: there are (card β).choose m increasing tuples g, and for each of them and each x ∈ T at most card V ^ (card β - m) embeddings satisfy f ∘ g = x.

theorem Finset.card_filter_injective_exists_mem_le {V : Type u_1} [Fintype V] [DecidableEq V] {n : ℕ} (B : Finset V) : {x : { x : Fin n → V // Function.Injective x } | ∃ (i : Fin n), ↑x i ∈ B}.card ≤ n * B.card * Fintype.card V ^ (n - 1)

Among injective n-tuples, at most n * #B * card V ^ (n - 1) meet B in some coordinate. This is the singleton-tuple case of natCard_embedding_exists_comp_mem_le, in the subtype form used for ordered injective tuples.