Zulip Chat Archive

Stream: Is there code for X?

Topic: fintype_of_fintype_ne

Oliver Nash (Oct 12 2021 at 13:12):

Do we have this somewhere:

import data.fintype.basic

open_locale classical

def fintype_of_fintype_ne {α : Type*} (a : α) (h : fintype {b // b ≠ a}) : fintype α := sorry

or is there an easy solution?

Yaël Dillies (Oct 12 2021 at 13:16):

Maybe by moving fintype along the equivalence {b // b = a} ⊕ {b // b ≠ a} ≃ α?

Oliver Nash (Oct 12 2021 at 13:17):

Thanks! I'm just trying something else but if that doesn't work in five minutes, I'll try this :-)

Oliver Nash (Oct 12 2021 at 13:24):

Your idea works nicely:

noncomputable def fintype_of_fintype_ne {α : Type*} (a : α) (h : fintype {b // b ≠ a}) : fintype α :=
fintype.of_bijective (equiv.sum_compl (λ (b : α), b = a)) (equiv.bijective _)

Johan Commelin (Oct 12 2021 at 13:27):

Isn't there something like equiv.fintype?

Johan Commelin (Oct 12 2021 at 13:27):

That would make it ε shorter :rofl:

Oliver Nash (Oct 12 2021 at 13:28):

Oh yes, that should work. Let me try.

Yaël Dillies (Oct 12 2021 at 13:28):

This is the statement that the equiv type is a fintype.

Yaël Dillies (Oct 12 2021 at 13:28):

So not what you want here :wink:

Johan Commelin (Oct 12 2021 at 13:28):

Why not?

Yaël Dillies (Oct 12 2021 at 13:29):

I mean, just read it: docs#equiv.fintype

Johan Commelin (Oct 12 2021 at 13:29):

Ooh, is there docs#fintype.equiv ?

Oliver Nash (Oct 12 2021 at 13:29):

I think what Johan has in mind is something that captures the fintype.of_bijective _ (equiv.bijective _) pattern.

Eric Rodriguez (Oct 12 2021 at 13:29):

it's saying that fintype (α \equiv β) for α, β fintypes, not transferring it across

Johan Commelin (Oct 12 2021 at 13:30):

That's a useful fact, but it doesn't deserve such a useful name (-;

Yaël Dillies (Oct 12 2021 at 13:30):

If it were, it would be in https://leanprover-community.github.io/mathlib_docs/data/equiv/transfer_instance.html but I can't find anything to my surprise.

Johan Commelin (Oct 12 2021 at 13:30):

:tada: fintype.of_equiv

Eric Rodriguez (Oct 12 2021 at 13:30):

I knew I had seen something like it before!

Johan Commelin (Oct 12 2021 at 13:30):

Alas, no dot-notation for you

Johan Commelin (Oct 12 2021 at 13:31):

We should move the names around. equiv.fintype can use an underscore

Oliver Nash (Oct 12 2021 at 13:36):

A prize for any further golfing:

noncomputable def fintype_of_fintype_ne {α : Type*} (a : α) (h : fintype {b // b ≠ a}) : fintype α :=
fintype.of_equiv _ $ equiv.sum_compl $ λ b, b = a

Eric Rodriguez (Oct 12 2021 at 13:38):

noncomputable def fintype_of_fintype_ne {α : Type*} (a : α) (h : fintype {b // b ≠ a}) : fintype α :=
fintype.of_equiv _ $ equiv.sum_compl (= a)

what do I win? ;b

Oliver Nash (Oct 12 2021 at 13:39):

Ooooh :clap: Fame on Zulip?

Adam Topaz (Oct 12 2021 at 14:09):

You can also just use docs#fintype.of_injective using the injection into alpha...

Yaël Dillies (Oct 12 2021 at 14:12):

Nope, that's the wrong way around.

Oliver Nash (Oct 12 2021 at 14:12):

Doesn't that go the wrong way?

Adam Topaz (Oct 12 2021 at 14:15):

Oops yes. Ignore me. I should get some coffee

Eric Wieser (Oct 12 2021 at 14:18):

Or computably:

def fintype_of_fintype_ne
  {α : Type*} (a : α) [decidable_pred (= a)] (h : fintype {b // b ≠ a}) : fintype α :=
fintype.of_equiv _ $ equiv.sum_compl (= a)

Last updated: Dec 20 2023 at 11:08 UTC