preorder on ulift

Stream: Is there code for X?

[Johan Commelin]

I couldn't find a suitable instance in mathlib. Is this really missing?

failed to synthesize type class instance for
ι : ulift ℕ → ℝ≥0
⊢ preorder (ulift ℕ)

[Kevin Buzzard]

This sounds right: it came up in a recent Zulip discussion, maybe nobody PRed the code that was generated in the thread

[Johan Commelin]

I also need

semi_normed_group (ulift.{v} V)

[Johan Commelin]

@Scott Morrison Is this something that transfer can do already?

[Johan Commelin]

This opens up a whole can of worms about putting bornologies and uniformities on ulift.

[Kevin Buzzard]

here is a link to the previous discussion (in the #lean4 stream but I think it's about Lean 3? That's what I was talking about, at least!)

[Eric Wieser]

Note that docs#ulift now lists all the instances that we do have, which should make it easier to spot the ones we don't

[Johan Commelin]

wc -l tmp/ulift_instances
97 tmp/ulift_instances

[Eric Wieser]

Probably we need a new order/ulift.lean file

[Johan Commelin]

That's at least an order of magnitude off the mark that it should be

[Eric Wieser]

What makes you say that?

[Johan Commelin]

I think we have over 970 interesting classes in our hierarchy

[Eric Wieser]

How easy is it to count that?

[Johan Commelin]

rg "^class" | wc -l
956

[Johan Commelin]

That's a first approximation

[Johan Commelin]

Anyways, it would be very helpful for LTE if someone could provide that semi_normed_group instances with the right defeqs.

[Eric Wieser]

Does LTE need both that and the order instances?

[Eric Wieser]

Eric Wieser said:

Probably we need a new order/ulift.lean file

Note this span off a new thread, https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Instance.20files

[Eric Wieser]

The conclusion was to create algebra/order/ulift.lean, but put ulift.preorder next to docs#pi.preorder or docs#prod.preorder.

[Scott Morrison]

(And no, @Johan Commelin, the transport tactic cannot cope with semi_normed_group. There is some low hanging fruit that would let it make further progress. Just providing the equiv_functor instance for filter, for example. Scratch that equiv_functor filter is available already.)

[Eric Wieser]

Isn't tactic#transport useless for ulift? I think docs#equiv_functor isn't universe polymorphic

[Eric Wieser]

Either way, we basically never seem to use the transport tactic for this kind of thing, and instead use things like docs#function.injective.add_comm_group

[Eric Wieser]

Or docs#normed_group.induced

[Scott Morrison]

No, transport and equiv_functor are universe polymorphic.

[Scott Morrison]

It's just we never put enough work into it, because there is a surprising lack of need for transporting structures across equivalences...

[Scott Morrison]

(I tested that I can transport add_comm_group over equiv.ulift.)

[Eric Rodriguez]

equiv_functor is not, iirc, docs#equiv.option_congr or something like that talks about it

[Scott Morrison]

Is not what?

[Johan Commelin]

Scott, thanks for testing.

[Eric Rodriguez]

Universe-polymorphic, sorry

[Eric Wieser]

docs#equiv_functor.map requires both sides of the equiv to be in the same universe

[Eric Wieser]

So sincetransport works, it's because it does the ulifting internally:

import tactic.transport

def {u v} it_does_work (α : Type u) [add_comm_group α] : add_comm_group (ulift.{v} α) :=
by transport using (@equiv.ulift α).symm

[Johan Commelin]

@Scott Morrison so what would be needed to make it transport semi normed groups?

[Eric Wieser]

(IMO) There's no point (other than being able to say "look, transport could do this too")

[Eric Wieser]

Just use docs#semi_normed_group.induced

[Johan Commelin]

Thanks, that at least solves the LTE issue.

[Eric Wieser]

Note that nothing
Johan Commelin said:

Anyways, it would be very helpful for LTE if <snip>

Presumably eventually there'll be a paper that comes out of LTE; have there been any thoughts about crediting non-LTE mathlib contributors in such a paper? Obviously this particular change is trivial, but if someone were to make 100 such changes that might start to make the question relevant

[Johan Commelin]

There have been some thoughts, but no conclusive thoughts.

[Johan Commelin]

In general, I think I would rather err on the side of being too generous with crediting :wink:

[Eric Wieser]

I suppose one option would be to add a contributor list appendix like the Scipy paper did

[Eric Wieser]

Eric Wieser said:

Just use docs#semi_normed_group.induced

Added in #14217

[Eric Wieser]

(which adds 14 new instances)

[Eric Wieser]

I'll leave the order ones to someone else

[Kevin Buzzard]

I love how the old trick ("stop being focussed on transferring data over equivalences, data often transfers over far more general classes of morphisms") keeps coming up again and again.

[Eric Wieser]

Looks like I forgot the normed_field instance in that PR, but I guess that's a problem for whoever finds themselves needing it