fintype.equiv_congr

Stream: Is there code for X?

[Kevin Buzzard]

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

Do we have this?

[Chris Hughes]

fintype.of_equiv

[Kevin Buzzard]

That's the function, not the equiv

[Kevin Buzzard]

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?

[Kevin Buzzard]

Does it have the right name?

[Reid Barton]

I expect the proofs can be by cc

[Joseph Myers]

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

[Mario Carneiro]

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 }

[Mario Carneiro]

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)

[Yury G. Kudryashov]

AFAIR, we already have the first equiv.

[Yury G. Kudryashov]

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

[Reid Barton]

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

[Scott Morrison]

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 }

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

Why isn't it an equiv_rw on is_local?

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

I put this instance in #3783.