# Zulip Chat Archive

## Stream: general

### Topic: equiv identifying sets

#### Johan Commelin (Mar 05 2019 at 13:03):

Suppose I have two types `X Y : Type`

and an equiv `e : equiv X Y`

. And suppose I have `S : set X`

and `T : set Y`

. I want to say that `e`

identifies `S`

with `T`

. Now I can say that `e.to_fun '' S = T`

, but that doesn't seem very symmetrical. Does it make sense to have some sort of predicate that takes an `equiv`

and two sets for this job?

#### Patrick Massot (Mar 05 2019 at 13:15):

I guess it depends on the API you write for this predicate

#### Kevin Buzzard (Mar 05 2019 at 18:18):

Random related remark: I needed this when I was doing `group_equiv`

; I wanted to prove that if `group_equiv G H`

and `K`

was a normal subgroup of `G`

then `group_equiv G/K H/K'`

where `K'`

was the image of `K`

. But it's not true in general that the image of a normal subgroup is a normal subgroup, so instead I had `K`

a normal subgroup of `G`

and proved `group_equiv G/K' H/K`

where `K'`

was defined to be the pre-image of `K`

, which was known to be a normal subgroup.

#### Chris Hughes (Mar 05 2019 at 18:19):

Use preimages. They're much easier.

Last updated: Dec 20 2023 at 11:08 UTC