mapping a fintype into a finset

Stream: Is there code for X?

[Sebastien Gouezel]

I'd like to map injectively a fintype to another fintype, knowing that the cardinal of the former is smaller than the cardinal of the latter. Is there a function doing this somewhere?

[Eric Wieser]

There's docs#fintype.card_le_of_embedding which goes in the other direction...

[Riccardo Brasca]

You can use docs#fintype.equiv_fin together with docs#fin.cast_le, but maybe there is something more direct.

[Sebastien Gouezel]

Thanks for the pointers. I'll go with

lemma fin.exists_injective_of_le_card_fintype
  {α : Type*} [fintype α] {k : ℕ} (hk : k ≤ fintype.card α) :
  ∃ (f : fin k → α), function.injective f :=
⟨_, (fintype.equiv_fin α).symm.injective.comp (fin.cast_le hk).injective⟩

lemma fin.exists_injective_of_le_card_finset {α : Type*} (s : finset α) (k : ℕ) (hk : k ≤ s.card) :
  ∃ (f : fin k → α), function.injective f ∧ range f ⊆ s :=
begin
  rw ← fintype.card_coe at hk,
  rcases fin.exists_injective_of_le_card_fintype hk with ⟨f, hf⟩,
  exact ⟨(λ x, (f x : α)), function.injective.comp subtype.coe_injective hf,
    by simp [range_subset_iff]⟩
end

[Kyle Miller]

This seems like it should be near docs#function.embedding.is_empty_of_card_lt:

import data.fintype.basic

lemma function.embedding.nonempty_of_card_le {α β : Type*} [fintype α] [fintype β]
  (h : fintype.card α ≤ fintype.card β) : nonempty (α ↪ β) :=
begin
  let fa := (fintype.equiv_fin α).to_embedding,
  let fb := (fintype.equiv_fin β).symm.to_embedding,
  exact ⟨fa.trans ((fin.cast_le h).to_embedding.trans fb)⟩,
end

[Kyle Miller]

Then, for example,

noncomputable
def the_function {α β : Type*} [fintype α] [fintype β]
  (h : fintype.card α ≤ fintype.card β) : α → β :=
(function.embedding.nonempty_of_card_le h).some

lemma the_function_prop {α β : Type*} [fintype α] [fintype β]
  (h : fintype.card α ≤ fintype.card β) : function.injective (the_function h) :=
(function.embedding.nonempty_of_card_le h).some.injective

[Eric Wieser]

It should be possible to get trunc version that's computable, right?

[Riccardo Brasca]

There is docs#fintype.trunc_equiv_fin

[Eric Wieser]

def function.embedding.trunc_of_card_le {α β : Type*} [fintype α] [fintype β] [decidable_eq α]
  [decidable_eq β]
  (h : fintype.card α ≤ fintype.card β) : trunc (α ↪ β) :=
(fintype.trunc_equiv_fin α).bind $ λ ea,
  (fintype.trunc_equiv_fin β).map $ λ eb,
    ea.to_embedding.trans ((fin.cast_le h).to_embedding.trans eb.symm.to_embedding

[Eric Wieser]

Then use that to prove the nonempty lemma and provide the noncomputable def

[Eric Wieser]

Unfortunate do notation doesn't work there as α and β are in different universes

[Sebastien Gouezel]

#9346. Thanks to all!