data.equiv.transfer_instance

Stream: general

[Yury G. Kudryashov]

I have a few questions about definitions in data.equiv.transfer_instance.

1. Do lets in definitions like docs#equiv.monoid affect definitional equality?
2. Is there an easy way to get rid of those lets? Does it mean using @? Or somehow call clean?
3. Should we make all these definitions @[reducible]?

My goal is to fix this file (e.g., make equiv.monoid aware of npow), move advanced stuff (e.g., local rings) to a new file, and use equiv.semigroup etc for ulift instances and additive structures on opposite M.

[Eric Wieser]

What's the advantage of using the stuff in this file vs docs#function.injective.monoid etc?

[Eric Wieser]

I think data.equiv.transfer_instance has quite heavy imports, making it impractical to use for low-level things like opposite and ulift

[Yury G. Kudryashov]

I was going to split instances up to group (or group_with_zero) from instances that need heavy imports.

[Yury G. Kudryashov]

function.injective.monoid does not support nsmul. I can add injective.monoid_smul etc that take nsmul as an explicit argument.

[Johan Commelin]

That would be great. Note that the current version (for comm_ring) is used by Witt vectors. So the nsmul-free versions should maybe stick around. Or can we do something with default arguments?

[Eric Wieser]

I think we should just fix the arguments on the injective versions

[Eric Wieser]

default arguments sound good to me

[Yury G. Kudryashov]

I think that we should have two separate definitions: injective.monoid and injective.monoid_smul.

[Yury G. Kudryashov]

In one case we get axioms from try_refl_tac; in the other case we get them from f (x ^ n) = f x ^ n.

[Eric Wieser]

We used to have something like that for monoid and monoid_div etc, but then we got rid of the former and removed _div from the latter.

[Eric Wieser]

So I don't think that's where we want to end up, but it's ok as an intermediate step to keep the PR under control

[Yury G. Kudryashov]

#10152

[Yury G. Kudryashov]

It's on top of #10147, so it makes no sense to review it now.

[Yury G. Kudryashov]

The relevant commit is https://github.com/leanprover-community/mathlib/pull/10152/commits/d6067983eab0ac4c1a740a2c631805aa598a3338

[Eric Wieser]

How about taking [has_pow M ℕ] instead of npow : ℕ → M → M? (Or whatever the argument order actually is)

[Yury G. Kudryashov]

I'll think about it tomorrow. I'm too sleepy now.