Monadic structure of finsupp

Stream: maths

[Yaël Dillies]

Working on proving the docs#locally_finite_order instance on finsupp, Bhavik noticed that finset is a monad in the category of types with a zero whose morphisms are given by docs#finsupp. But is it a strong monad? That is, can you fill in that sorry in a sensible fashion?

import data.finsupp.basic

open_locale pointwise

variables {ι α : Type*} [has_zero α]

def finsupp.map_finset (f : ι →₀ α) : finset ι →₀ finset α := sorry

[Anne Baanen]

Wouldn't docs#finset.image work here?

[Anne Baanen]

Ah of course not, since we want to get a finsupp out :P

[Anne Baanen]

I think there's only one option that would be natural in ι: send everything to 0.

[Yaël Dillies]

That's what I fear too.

[Anne Baanen]

Suppose ι is infinite and map_finset sends some s ≠ ∅ to something nonzero. Then by naturality, all s of the same cardinality also map to something nonzero, but there are infinitely many of them.

[Yaël Dillies]

Okay, so what if fintype ι?

[Yaël Dillies]

Note however that 0 = {0}, not ∅. See docs#finset.has_zero

[Yaël Dillies]

It makes a lot of sense in that context!

[Anne Baanen]

Then finset ι is also finite and finsupp of something finite is equivalent to →. So you get exactly docs#finset.image :P

[Yaël Dillies]

Oh yeah, boring

[Anne Baanen]

I guess there are two natural options: send everything to 0 or send everything to 0 except ∅ which is sent to ∅.

[Yaël Dillies]

This definition of 0 is a godsend to me. For example, this definition makes sense:

/-- Given a finitely supported function `f : ι →₀ finset α`, one can define the finset
`f.pi` of all finitely supported functions whose value at `i` is in `f i` for all `i`. -/
def pi (f : ι →₀ finset α) : finset (ι →₀ α) := f.support.finsupp f

(I also defined finset.finsupp earlier)

[Anne Baanen]

Hmm, Hoogle doesn't know an operation of that shape. I guess it's like an exponential object but not quite?

[Yaël Dillies]

It's docs#finset.pi but with a better type and bundled as a finsupp

[Yaël Dillies]

I don't know enough about exponential objects to tell more.

[Bhavik Mehta]

Generally an expression of that form won't exist for a monad, but when it does (in a ccc) it can be used to show a (Haskell) applicative upgrades to a monad (of course assuming some naturality commutative diagrams)

[Bhavik Mehta]

finsupp.pi is something like giving a commutator in one direction for the monad over the exponential, in other words a nat trans from (exp compose finset) to (finset compose exp) - it was actually the form of this type that made me notice the monad that Yaël mentions