min and max of finsupps

Stream: Is there code for X?

[Stuart Presnell]

Do we have min and max operations on finsupps α →₀ M (where M satisfies some suitable conditions)?

[Yaël Dillies]

M linear order is what you need.

[Stuart Presnell]

That's what I guessed, but it seems that these operations don't exist (yet)

[Yaël Dillies]

We're also missing the (very similar) multiset.min/multiset.max. cc @Mantas Baksys

[Eric Wieser]

Don't we have docs#finsupp.linear_order?

[Eric Wieser]

Oh, the operation you're looking for is ⊔, if that exists

[Eric Wieser]

docs#finsupp.has_sup

[Eric Wieser]

Ignore my above messages. Can you explain what you want max to mean on finsupps? Are you asking for the elementwise max? Or for f.support.max id?

[Stuart Presnell]

I was thinking about elementwise operations, i.e. where (min f g)(a) = min (f a) (g a).

[Stuart Presnell]

So (for finsupps into nat, at least) I think the support of the min/max is the intersection/union of the supports respectively.

[Stuart Presnell]

I haven't thought properly about what this should be when 0 isn't the minimal element of M.

[Stuart Presnell]

(For avoidance of #xy, what I'm primarily interested in is the situation where the two finsupps are a.factorization and b.factorization, and I want to produce the finsupp whose value at each prime is the minimum of their respective values, which should then be the factorization of gcd a b.)

[Yaël Dillies]

Yeah, you want inf

[Yaël Dillies]

inf on finsupp is the pointwise inf, which in your case is the pointwise min. But min on finsupp doesn't make sense (it's not a linear order), so you're stuck with inf.

[Stuart Presnell]

Excellent, thanks

[Eric Wieser]

Stuart Presnell said:

I was thinking about elementwise operations, i.e. where (min f g)(a) = min (f a) (g a).

docs#finsupp.inf_apply is basically this statement