# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: fintype.equiv_congr

#### Kevin Buzzard (Aug 10 2020 at 13:06):

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

Do we have this?

#### Chris Hughes (Aug 10 2020 at 13:11):

`fintype.of_equiv`

#### Kevin Buzzard (Aug 10 2020 at 13:20):

That's the function, not the equiv

#### 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?

#### Kevin Buzzard (Aug 10 2020 at 13:20):

Does it have the right name?

#### Reid Barton (Aug 10 2020 at 14:04):

I expect the proofs can be `by cc`

#### 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).

#### 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 }
```

#### 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)
```

#### Yury G. Kudryashov (Aug 13 2020 at 01:45):

AFAIR, we already have the first equiv.

#### Yury G. Kudryashov (Aug 13 2020 at 01:47):

#### Reid Barton (Aug 13 2020 at 01:51):

btw isn't `equiv_rw`

supposed to do things like this?

#### 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 }
```

#### Kevin Buzzard (Aug 13 2020 at 07:07):

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

#### 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

#### Kevin Buzzard (Aug 13 2020 at 07:21):

Why isn't it an equiv_rw on `is_local`

?

#### 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.

#### Scott Morrison (Aug 13 2020 at 08:17):

I should get back to my `hygienic`

branch at some point...

#### Scott Morrison (Aug 15 2020 at 05:05):

I put this instance in #3783.

Last updated: May 16 2021 at 05:21 UTC