Zulip Chat Archive

Stream: Is there code for X?

Topic: fintype.equiv_congr


view this post on Zulip Kevin Buzzard (Aug 10 2020 at 13:06):

example (X Y : Type)
  (e : X  Y) : fintype X  fintype Y := sorry

Do we have this?

view this post on Zulip Chris Hughes (Aug 10 2020 at 13:11):

fintype.of_equiv

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 13:20):

That's the function, not the equiv

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 13:20):

Do we even have ext for fintype?

@[ext] def fintype.ext {X : Type u} (a : fintype X) (b : fintype X) :
a.elems = b.elems  a = b :=
begin
  tactic.unfreeze_local_instances,
  cases a; cases b; simp
end

def fintype.equiv_congr (X : Type u) (Y : Type v) (e : X  Y) :
  fintype X  fintype Y :=
{ to_fun := λ fX, @fintype.of_equiv Y X fX e,
  inv_fun := λ fY, @fintype.of_equiv X Y fY e.symm,
  left_inv := begin
    intro h,
    cases h with S hS,
    ext x,
    congr'
  end,
  right_inv := begin
    rintro S, hS,
    ext x,
    congr'
  end }

Is this PR'able?

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 13:20):

Does it have the right name?

view this post on Zulip Reid Barton (Aug 10 2020 at 14:04):

I expect the proofs can be by cc

view this post on Zulip Joseph Myers (Aug 10 2020 at 19:15):

ext for fintype is subsingleton.elim, you don't need a.elems = b.elems (and instance (α : Type*) : subsingleton (fintype α) is already in mathlib).

view this post on Zulip Mario Carneiro (Aug 10 2020 at 19:35):

What Joseph says. I suggest PR'ing this version:

def fintype.equiv_congr {X Y} (e : X  Y) : fintype X  fintype Y :=
{ to_fun := λ fX, @fintype.of_equiv Y X fX e,
  inv_fun := λ fY, @fintype.of_equiv X Y fY e.symm,
  left_inv := λ _, by apply subsingleton.elim,
  right_inv := λ _, by apply subsingleton.elim }

view this post on Zulip Mario Carneiro (Aug 10 2020 at 19:41):

Or more generally:

def subsingleton.mk_equiv {α β} [subsingleton α] [subsingleton β]
  (f : α  β) (g : β  α) : α  β :=
f, g, λ _, by cc, λ _, by cc

def fintype.equiv_congr {X Y} (e : X  Y) : fintype X  fintype Y :=
subsingleton.mk_equiv (λ fX, @fintype.of_equiv Y X fX e) (λ fY, @fintype.of_equiv X Y fY e.symm)

view this post on Zulip Yury G. Kudryashov (Aug 13 2020 at 01:45):

AFAIR, we already have the first equiv.

view this post on Zulip Yury G. Kudryashov (Aug 13 2020 at 01:47):

https://leanprover-community.github.io/mathlib_docs/data/equiv/basic.html#equiv_of_subsingleton_of_subsingleton

view this post on Zulip Reid Barton (Aug 13 2020 at 01:51):

btw isn't equiv_rw supposed to do things like this?

view this post on Zulip Scott Morrison (Aug 13 2020 at 05:36):

Yes, equiv_rw does this, but it needs an additional instance about fintype:

import tactic.equiv_rw
import data.fintype.basic

instance equiv_functor_fintype : equiv_functor fintype :=
{ map := λ α β e s, by exactI fintype.of_bijective e e.bijective, }

def fintype.equiv_congr (X : Type) (Y : Type) (e : X  Y) :
  fintype X  fintype Y :=
by { equiv_rw e, refl, }

This isn't merely pushing the work around, because the equiv_functor_fintype instance means that equiv_rw can do more complicated things too, if the fintype is "deeper":

example (X Y : Type) (e : X  Y) :
  fintype X  punit  fintype Y  punit :=
by { equiv_rw e, refl }

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 07:07):

Oh cool! Can we prove that something isomorphic to a Noetherian local ring is Noetherian local?

view this post on Zulip Kenny Lau (Aug 13 2020 at 07:19):

Kevin Buzzard said:

Oh cool! Can we prove that something isomorphic to a Noetherian local ring is Noetherian local?

again this is transfer territory right

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 07:21):

Why isn't it an equiv_rw on is_local?

view this post on Zulip Scott Morrison (Aug 13 2020 at 08:16):

Because the current version of equiv_rw only knows about equiv. It can't cope with "extra" information, e.g. that it is a morphism of rings as well as being an equivalence.

view this post on Zulip Scott Morrison (Aug 13 2020 at 08:17):

I should get back to my hygienic branch at some point...

view this post on Zulip Scott Morrison (Aug 15 2020 at 05:05):

I put this instance in #3783.


Last updated: May 16 2021 at 05:21 UTC