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: Aug 03 2023 at 10:10 UTC