## Stream: general

### Topic: monadic ASCII art for integration

#### Patrick Massot (Aug 29 2020 at 20:48):

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 (Aug 29 2020 at 20:50):

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

#### Heather Macbeth (Aug 29 2020 at 20:57):

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 (Aug 29 2020 at 20:58):

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

#### Heather Macbeth (Aug 29 2020 at 21:00):

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 (Aug 29 2020 at 21:00):

There are many bundled functions spaces.

#### Heather Macbeth (Aug 29 2020 at 21:01):

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

#### Heather Macbeth (Aug 29 2020 at 21:01):

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

#### Heather Macbeth (Aug 29 2020 at 21:02):

(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 (Aug 29 2020 at 21:03):

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

#### Heather Macbeth (Aug 29 2020 at 21:06):

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 (Aug 29 2020 at 21:07):

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

#### Patrick Massot (Aug 29 2020 at 21:07):

It may work actually, like the magic has_uncurry class.

#### Heather Macbeth (Aug 29 2020 at 21:07):

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

#### Heather Macbeth (Aug 29 2020 at 21:08):

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

#### Heather Macbeth (Aug 29 2020 at 21:23):

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 (Aug 29 2020 at 21:32):

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 (Aug 29 2020 at 21:45):

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 (Aug 29 2020 at 21:57):

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 (Aug 29 2020 at 22:12):

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 (Aug 29 2020 at 22:14):

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 (Aug 29 2020 at 22:15):

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 (Aug 29 2020 at 22:16):

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 (Aug 29 2020 at 22:17):

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

#### Adam Topaz (Aug 29 2020 at 22:18):

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

#### Heather Macbeth (Aug 29 2020 at 22:20):

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 (Aug 29 2020 at 22:22):

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 (Aug 29 2020 at 22:25):

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 (Aug 29 2020 at 22:27):

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 (Aug 29 2020 at 22:29):

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 (Aug 29 2020 at 22:29):

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

#### Adam Topaz (Aug 29 2020 at 22:31):

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

#### Adam Topaz (Aug 29 2020 at 22:31):

The disjoint union being indexed over E.

#### Heather Macbeth (Aug 29 2020 at 22:32):

And the morphisms are induced by the linear maps

Yeah

#### Adam Topaz (Aug 29 2020 at 22:34):

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

#### Heather Macbeth (Aug 29 2020 at 22:34):

$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 ...

(deleted)

#### Adam Topaz (Aug 29 2020 at 22:35):

The identity is given by the identity linear map

#### Heather Macbeth (Aug 29 2020 at 22:35):

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

#### Adam Topaz (Aug 29 2020 at 22:35):

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

#### Heather Macbeth (Aug 29 2020 at 22:36):

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

Yeah exactly

#### Heather Macbeth (Aug 29 2020 at 22:38):

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

#### Adam Topaz (Aug 29 2020 at 22:43):

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 (Aug 29 2020 at 22:46):

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