Zulip Chat Archive

Stream: Is there code for X?

Topic: Transfer instance through equivalences


view this post on Zulip Nicolò Cavalleri (Aug 25 2020 at 11:01):

If I have an equivalence between two types and a instance of e.g. has_add on one of the two types, there is a natural way of defining e.g. has_add on the other type. Is there a way to do this in Lean already or should I define a equiv.lift_has_add (or a better name) for any structure that I am interested to define this for?

example (X Y : Type*) [has_add X] (e : X \equiv Y) : has_add Y

view this post on Zulip Reid Barton (Aug 25 2020 at 11:02):

docs#equiv.has_add

view this post on Zulip Reid Barton (Aug 25 2020 at 11:03):

these are all just written manually at the moment

view this post on Zulip Nicolò Cavalleri (Aug 25 2020 at 11:06):

Ok thanks, so if I want to define this for e.g. lie algebras, I need to import the lie algebra file in that file? Wouldn't it be better to define every such def in the file where the class is defined? (I mean in the long term that file will have a huge number of imports I guess...)

view this post on Zulip Reid Barton (Aug 25 2020 at 11:12):

I think all these classes were in the core library when this file was written. For things like Lie algebras it would be better to put the construction with the definition of Lie algebra, yes. (I guess you could have a file data.equiv.lie but I don't see much point.)

view this post on Zulip Reid Barton (Aug 25 2020 at 11:17):

But I'm pretty sure whatever defines has_zero, for example, can't import data.equiv

view this post on Zulip Nicolò Cavalleri (Aug 25 2020 at 11:21):

Reid Barton said:

I think all these classes were in the core library when this file was written. For things like Lie algebras it would be better to put the construction with the definition of Lie algebra, yes. (I guess you could have a file data.equiv.lie but I don't see much point.)

Ok great thanks! Could it be a good idea to move the non-core definitions in the appropriate files, for consistency and to find them more easily? (If such thing existed for a monoid I was expecting to find it into the file where monoids are defined)

view this post on Zulip Reid Barton (Aug 25 2020 at 11:32):

that's also likely impossible for import reasons

view this post on Zulip Reid Barton (Aug 25 2020 at 11:32):

or at least impossible without further reorganizations

view this post on Zulip Scott Morrison (Aug 25 2020 at 11:56):

You can also use the transport tactic. It is a bit limited / buggy, but most of the instances like equiv.has_add get generated correctly.

view this post on Zulip Scott Morrison (Aug 25 2020 at 11:58):

If you look in test/transport/basic.lean there are some examples, e.g. moving a Lie ring across an equiv.


Last updated: May 17 2021 at 15:13 UTC