monadic ASCII art for integration

Stream: general

[Patrick Massot]

Given real vector spaces E and F equipped with a ton of additional structures and X a measured space, I get a map "composing" a continuous linear map $L : E \to F$ and a "map" $f : L^1(X, E)$ to get $L \circ f : L^1(X, F)$. Of course none of these are actual functions, $L$ is a bundled function and $f$ is an equivalence class of functions, bundled with some more props. Should I be using monadic ascii art? Something like L <$> f or f >>= L?

[Reid Barton]

Imagine the world we could be living in if Unicode had just added a subscript ${}_{*}$

[Heather Macbeth]

Can you take one of the many unicode variants to ∘ and use that? The day will come when such constructions are used all the time, by people whose active mental model of these things is just as functions.

[Patrick Massot]

I could try that, but I fear we will end up with many variants, like our many decorated arrows.

[Heather Macbeth]

Are there that many variants? Equivalence classes under measurability; maybe bundled objects of a function + the fact that it belongs to a certain function space, ...

[Patrick Massot]

There are many bundled functions spaces.

[Heather Macbeth]

Of course! But can one use ∘ for all of them?

[Heather Macbeth]

(I don't know how notation works. But couldn't Lean figure it out?)

[Heather Macbeth]

(If I am composing an object of $C^{2,\alpha}$ with a smooth function, I unambiguously want another object in $C^{2,\alpha}$.)

[Patrick Massot]

Maybe we could add a has_fancy_composition type class, but I fear there will be universe issues.

[Heather Macbeth]

I would like Lean to have a list of triples A, B, C, together with the theorem (definition?) that an A and a B can be fancy-composed to get a C.

[Patrick Massot]

Yes, this is what the type class should be able to do

[Patrick Massot]

It may work actually, like the magic has_uncurry class.

[Heather Macbeth]

Can one then use ∘ for all kinds of fancy-composition?

[Heather Macbeth]

For example, it seems to cause no problems to use ≤ for all kinds of order.

[Heather Macbeth]

Is there a problem with associativity? Does one need compatibility theorems, if one has A, B, C, a fancy-composition of A and B to X, a fancy-composition of B and C to Y, a fancy-composition of X and C, ...

[Heather Macbeth]

The simple version (still good enough for many applications) might be to have only left-fancy-compositions of A and B to B (with axiom that $(\alpha \circ_f b_1)\circ_f b_2=\alpha \circ_f(b_1\circ b_2)$) and right-fancy-compositions of A and B to A.

[Bhavik Mehta]

The "fancy composition" desire here reminds me of the use of lenses in Haskell - there are Isos and Lenses and Prisms and Traversals: every Iso is a Lens and a Prism, every Lens is a Traversal and every Prism is a Traversal, and each of these is closed under composition (ie composing a Lens with a Lens gives you a Lens, etc). Now when you compose a Iso with a Lens, you automatically get a Lens, and when you compose a Lens with a Prism, you automatically get a Traversal, and this is all done by the typeclass system nicely - which seems like the situation you have here...

[Kevin Buzzard]

Patrick Massot said:

Maybe we could add a has_fancy_composition type class, but I fear there will be universe issues.

Eventually people will want to prove things for real numbers, and then all of a sudden everyone will be forced into Type for some silly reason, and then all the universe issues will magically disappear.

[Heather Macbeth]

Bhavik Mehta said:

The "fancy composition" desire here reminds me of the use of lenses in Haskell - there are Isos and Lenses and Prisms and Traversals: every Iso is a Lens and a Prism, every Lens is a Traversal and every Prism is a Traversal, and each of these is closed under composition (ie composing a Lens with a Lens gives you a Lens, etc). Now when you compose a Iso with a Lens, you automatically get a Lens, and when you compose a Lens with a Prism, you automatically get a Traversal, and this is all done by the typeclass system nicely - which seems like the situation you have here...

@Bhavik Mehta this is very interesting! But I am not sure it's the same. To take Patrick's original example, maybe the Isos would be continuous linear maps (eg $L:E\to F$), and the Lenses would be measurable functions (eg $f \in L^1(X,E)$). Then as desired, Isos compose with Lenses to give Lenses. But -- the Lenses are not closed under composition!

[Heather Macbeth]

I was actually wondering if there's a category theory construction that deals with this -- and you are probably the right person to ask.

[Bhavik Mehta]

Heather Macbeth said:

(If I am composing an object of $C^{2,\alpha}$ with a smooth function, I unambiguously want another object in $C^{2,\alpha}$.)

Ah I think you're right, I was basing my idea off of this, rather than Patrick's original example

[Heather Macbeth]

Given two categories (here: normed spaces and measure spaces), one wants a class of morphism-like things from one category to the other

[Heather Macbeth]

which behave well under (say, pre-) compositions with morphisms in one of the categories.

[Adam Topaz]

Something like this comes to mind: https://ncatlab.org/nlab/show/Grothendieck+fibration

[Heather Macbeth]

Bhavik Mehta said:

Heather Macbeth said:

(If I am composing an object of $C^{2,\alpha}$ with a smooth function, I unambiguously want another object in $C^{2,\alpha}$.)

Ah I think you're right, I was basing my idea off of this, rather than Patrick's original example

One actually has the same problem here, for example $\sqrt{x}$ is $C^{\tfrac{1}{2}}$ but its self-composition $\sqrt[4]{x}$ is not.

[Heather Macbeth]

Adam Topaz said:

Something like this comes to mind: https://ncatlab.org/nlab/show/Grothendieck+fibration

@Adam Topaz I am very interested but it will take me some time to make sense of this :)

[Adam Topaz]

A straightforward thing one can do in this case is take a Sigma type of all L^1(X,E) as E varies, and define some category generated by morphisms given by composition with linear functions from E to F.

[Bhavik Mehta]

I think this could get messy if you have more than two sides though, I'm not sure if that case is relevant however

[Heather Macbeth]

Adam Topaz said:

A straightforward thing one can do in this case is take a Sigma type of all L^1(X,E) as E varies, and define some category generated by morphisms given by composition with linear functions from E to F.

Could you explain in more detail? (Sorry.) The objects of the category are the individual $L^1(X,E)$ 's?

[Heather Macbeth]

Or individual elements of the $L^1(X, E)$ 's?

[Adam Topaz]

The type of objects is the disjoint union of the L^1(X,E) as E varies.

[Adam Topaz]

The disjoint union being indexed over E.

[Heather Macbeth]

And the morphisms are induced by the linear maps

[Adam Topaz]

Yeah

[Adam Topaz]

Actually I think the morphisms are literally just the ones induced by the linear maps

[Heather Macbeth]

$L : E \to F$ induces a functional $L^1(X,E)\to L^1(X, F)$, and such things are the morphisms in the category ...

[Adam Topaz]

(deleted)

[Adam Topaz]

The identity is given by the identity linear map

[Heather Macbeth]

OK, this is very interesting, can it be used to solve Patrick's problem? :smiley:

[Adam Topaz]

There is a natural functor from this category to the category of all E's with linear maps

[Heather Macbeth]

The functor being, "take only the target space"?

[Adam Topaz]

Yeah exactly

[Heather Macbeth]

So could one give a name to this construction, and then use the same Lean notation for all its occurrences?

[Adam Topaz]

In terms of Patrick's original question regarding notation, this is would be a bit strange, since the $f$ would be an object in this category, and the $L$ would be a morphism.

[Heather Macbeth]

Too bad!

[Adam Topaz]

(On second thought, I don't think that the "remember only the target space" is functorial.)

[Anne Baanen]

For what it's worth, the ascii art used by haskellers is (^<<)

[Chris Wong]

Or lmap.