Zulip Chat Archive

Stream: general

Topic: Generating isomorphisms?

Kevin Buzzard (Mar 04 2018 at 17:47):

I have some definition definition foo (X : Type) : Type := blah

Kevin Buzzard (Mar 04 2018 at 17:47):

If I have two types X and Y plus isomorphisms f:X\to Y and g:Y\to X (i.e. the composites both ways are the identity functions)

Kevin Buzzard (Mar 04 2018 at 17:48):

can I deduce that foo X is isomorphic to foo Y? Does this even make sense?

Kevin Buzzard (Mar 04 2018 at 17:53):

an isomorphism version of eq.subst?

Kevin Buzzard (Mar 04 2018 at 17:54):

Or does this have to somehow be proved on a case by case basis?

Kevin Buzzard (Mar 04 2018 at 17:55):

Mathematicians are so happy to identify objects which are canonically isomorphic and I find this much more of a struggle in Lean.

Gabriel Ebner (Mar 04 2018 at 17:57):

can I deduce that foo X is isomorphic to foo Y?

Yes, if you define isomorphic as "there exist isomorphisms f and g such that ...". :smile:

This notion of isomorphism does not allow you to substitute isomorphic structures in arbitrary contexts, though.

Kevin Buzzard (Mar 04 2018 at 17:58):

yes this is absolutely how I want to define isomorphic.

Kevin Buzzard (Mar 04 2018 at 17:58):

How do I construct the map foo X -> foo Y?

Gabriel Ebner (Mar 04 2018 at 17:59):

The axiom of univalence would allow you to lift isomorphisms to equality, then you can substitute in arbitrary contexts.

Gabriel Ebner (Mar 04 2018 at 17:59):

Ooops, sorry missed the foo part.

Kevin Buzzard (Mar 04 2018 at 17:59):

Oh great :-)

Kevin Buzzard (Mar 04 2018 at 17:59):

I don't see any reason why I should be able to get a map foo X -> foo Y just given a map X -> Y

Kevin Buzzard (Mar 04 2018 at 17:59):

but can I use the inverse somehow?

Kevin Buzzard (Mar 04 2018 at 18:00):

Or is what I want not even true?

Gabriel Ebner (Mar 04 2018 at 18:00):

So yeah, univalence is the axiomatic principle that would allow you to do that (in HoTT).

Gabriel Ebner (Mar 04 2018 at 18:00):

In Lean, you need to prove it yourself for each instance, such as foo here.

Mario Carneiro (Mar 04 2018 at 18:00):

It's definitely not true in general; for example if foo X was X = nat

Mario Carneiro (Mar 04 2018 at 18:01):

(not true without univalence that is)

Mario Carneiro (Mar 04 2018 at 18:03):

@Gabriel Ebner do you know if you can get a contradiction in classical lean from X ~= Y -> X = Y?

Gabriel Ebner (Mar 04 2018 at 18:20):

This is an interesting question. I think it is strictly weaker than univalence because it is not an isomorphism. It looks inconsistent, but I don't immediately see how to derive a contradiction from it.

Last updated: Dec 20 2023 at 11:08 UTC