Transfer instance through equivalences

Stream: Is there code for X?

[Nicolò Cavalleri]

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

[Reid Barton]

docs#equiv.has_add

[Reid Barton]

these are all just written manually at the moment

[Nicolò Cavalleri]

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

[Reid Barton]

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

[Reid Barton]

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

[Nicolò Cavalleri]

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)

[Reid Barton]

that's also likely impossible for import reasons

[Reid Barton]

or at least impossible without further reorganizations

[Scott Morrison]

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.

[Scott Morrison]

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