Transferring Instances along Equivs

Stream: Is there code for X?

[Ken Lee]

Say I have (M N : Type u) (f : M equiv N) [monoid M], is there a way of transfering the monoid structure of M via f to N without "typing everything out"?

In my situation, I have a monoid instance on M = (punit --> N).

[Adam Topaz]

tactic#transport

[Ken Lee]

Beautiful. Thanks!

[Ken Lee]

actually, why is this a tactic and not a definition?

[Adam Topaz]

You can use this for other kinds of algebraic structures as well (which is only possible in lean with metaprogramming)

[Adam Topaz]

If you want a definition for monoids only, you can make one yourself using this tactic

[Adam Topaz]

import tactic
import algebra

def transport_monoid {α β : Type*} (e : α ≃ β) [monoid α] : monoid β := by transport using e

example {α β : Type*} (e : α ≃ β) [monoid α] : e 1 = (by letI := transport_monoid e; exact (1 : β)) := rfl

example {α β : Type*} (e : α ≃ β) [monoid α]
  (b c : β) : e (e.symm b * e.symm c) = by letI := transport_monoid e; exact (b * c) := rfl

[Eric Wieser]

Does docs#function.injective.monoid help?

[Eric Wieser]

Or docs#equiv.monoid

[Eric Wieser]

Which is the version without needing a tactic

[Ken Lee]

it's okay. transport doesn't look like it's gonna do anything crazy like tidy. I was just wondering why it's in the meta, and not within the type theory.

[Eric Wieser]

It's in the meta because writing all of docs#equiv.monoid, docs#equiv.group, etc by hand would be super tedious. Except we did that anyway, so I'm not really sure why we have both.

[Ken Lee]

but is it possible to have a single transport function within the type theory that allows you to transfer across any kind of structure across equivs?

[Adam Topaz]

Depends on the definition of structure. If you encode things in terms of universal algebra, then yes, but then translating back to the structures like monoids, groups, etc. as they're usually defined in mathlib still would require meta code.

[Aaron Anderson]

@Adam Topaz I’m moving toward that with #7754...

[Adam Topaz]

I would be happy to start porting this stuff I did a while ago here https://github.com/adamtopaz/UnivAlg once we settle on a way to work with first order structures!

[Scott Morrison]

I had planned about a year ago to steadily make tactic#equiv_rw (the real trick underlying tactic#transport) more and more powerful. There is a lot that can be done here! (There's not reason it can't deal with quantifiers, and if could also be a lot cleverer about using equivs-with-structure.) But I got distracted by other things.

[Scott Morrison]

If you look in the test file for transport you'll see it happily transports lie_ring, etc., --- so it exists because it is / is-intended-to-be a general purpose tool.

[Scott Morrison]

The hard coded things like docs#equiv.monoid predate it.

[Adam Topaz]

Does it transport things like topological spaces?

[Scott Morrison]

No, but that was the example I was last working on. (Obviously not hard coding something for topological spaces, but teaching it to cope with the relevant sorts of quantifiers/dependencies.)

[Scott Morrison]

I really wanted to transport compactness across a homeomorphism (again, by a metaprogram that had never heard of spaces, homeomorphisms, or compactness). Certainly doable, just takes some work.