fintype across equiv

Stream: Is there code for X?

[Yakov Pechersky]

Do we have the following?

example {α β : Type*} [fintype α] (h' : α ≃ β) : fintype β :=
{ elems := (finset.univ : finset α).map h'.to_embedding,
  complete := by simp }

[Yakov Pechersky]

I'd call it equiv.fintype but that's taken by the instance [fintype α] [fintype β] : fintype (α ≃ β) := sorry that exists

[Adam Topaz]

We have fintype across injective maps, so you can use the fact that an equiv is injective

[Adam Topaz]

docs#fintype.of_injective I think?

[Yakov Pechersky]

Oh, it's noncomputable =C

[Adam Topaz]

Oh and docs#fintype.of_equiv

[Yakov Pechersky]

Ah, right after, of_equiv

[Yakov Pechersky]

A follow up, is there something that can lift a fintype out of a quotient? Like in the following example:

instance fintype.multiset_nodup {α : Type*} [fintype α] : fintype {s : multiset α // s.nodup} :=
fintype.of_equiv (finset α) ⟨λ s, ⟨s.val, s.nodup⟩, λ s, ⟨s.val, s.prop⟩,
  λ _, by { ext, simp [finset.mem_def] },
  λ _, by { ext, simp [finset.mem_def] } ⟩

instance fintype.list_nodup : fintype {l : list α // nodup l} := sorry

[Adam Topaz]

There might just be a fintype instance on a quotient given a fintype instance on the original type?

[Adam Topaz]

Oh that's not what you want, sorry. You want to go the other way!

[Yakov Pechersky]

Yeah, I want to show that nodup lists have a fintype, and then lower it into a different quotient than multiset.

[Yakov Pechersky]

Here's as neat as I could get it, I think it's doing the right thing

variables {α : Type*} [fintype α]

instance fintype.multiset_nodup : fintype {s : multiset α // s.nodup} :=
fintype.of_equiv (finset α) ⟨λ s, ⟨s.val, s.nodup⟩, λ s, ⟨s.val, s.prop⟩,
  λ _, by { ext, simp [finset.mem_def] },
  λ _, by { ext, simp [finset.mem_def] } ⟩

def multiset.finset_list {α : Type*} [decidable_eq α] (s : multiset α) : finset (list α) :=
quotient.lift_on s (λ l, l.permutations.to_finset)
  (λ l₁ l₂ (h : l₁ ~ l₂), by {
    ext,
    simp only [mem_permutations, mem_to_finset],
    exact ⟨λ h', h'.trans h, λ h', h'.trans h.symm⟩ })

@[simp] lemma finset_list_coe {α : Type*} [decidable_eq α] (l : list α) :
  (l : multiset α).finset_list = l.permutations.to_finset := rfl

@[simp] lemma mem_finset_list {α : Type*} [decidable_eq α] {s : multiset α} {l : list α} :
  l ∈ s.finset_list ↔ (l : multiset α) = s :=
begin
  induction s using quotient.induction_on,
  simp
end

instance fintype.list_nodup [decidable_eq α] : fintype {l : list α // nodup l} :=
{ elems := (finset.univ : finset {s : multiset α // s.nodup}).bUnion
    (λ s, finset.subtype (λ (l : list α), l.nodup) s.val.finset_list),
  complete := by simp }