Zulip Chat Archive

Stream: general

Topic: monadic ASCII art for integration


view this post on Zulip 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:EFL : E \to F and a "map" f:L1(X,E)f : L^1(X, E) to get Lf:L1(X,F)L \circ f : L^1(X, F). Of course none of these are actual functions, LL is a bundled function and ff 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?

view this post on Zulip Reid Barton (Aug 29 2020 at 20:50):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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, ...

view this post on Zulip Patrick Massot (Aug 29 2020 at 21:00):

There are many bundled functions spaces.

view this post on Zulip Heather Macbeth (Aug 29 2020 at 21:01):

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

view this post on Zulip Heather Macbeth (Aug 29 2020 at 21:01):

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

view this post on Zulip Heather Macbeth (Aug 29 2020 at 21:02):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 29 2020 at 21:07):

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

view this post on Zulip Patrick Massot (Aug 29 2020 at 21:07):

It may work actually, like the magic has_uncurry class.

view this post on Zulip Heather Macbeth (Aug 29 2020 at 21:07):

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

view this post on Zulip Heather Macbeth (Aug 29 2020 at 21:08):

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

view this post on Zulip 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, ...

view this post on Zulip 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 (αfb1)fb2=αf(b1b2)(\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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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:EFL:E\to F), and the Lenses would be measurable functions (eg fL1(X,E)f \in L^1(X,E)). Then as desired, Isos compose with Lenses to give Lenses. But -- the Lenses are not closed under composition!

view this post on Zulip 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.

view this post on Zulip Bhavik Mehta (Aug 29 2020 at 22:15):

Heather Macbeth said:

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

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

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Aug 29 2020 at 22:17):

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

view this post on Zulip Adam Topaz (Aug 29 2020 at 22:18):

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

view this post on Zulip Heather Macbeth (Aug 29 2020 at 22:20):

Bhavik Mehta said:

Heather Macbeth said:

(If I am composing an object of C2,αC^{2,\alpha} with a smooth function, I unambiguously want another object in C2,α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 x\sqrt{x} is C12C^{\tfrac{1}{2}} but its self-composition x4\sqrt[4]{x} is not.

view this post on Zulip Heather Macbeth (Aug 29 2020 at 22:22):

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 :)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Aug 29 2020 at 22:29):

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 L1(X,E)L^1(X,E) 's?

view this post on Zulip Heather Macbeth (Aug 29 2020 at 22:29):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Aug 29 2020 at 22:31):

The disjoint union being indexed over E.

view this post on Zulip Heather Macbeth (Aug 29 2020 at 22:32):

And the morphisms are induced by the linear maps

view this post on Zulip Adam Topaz (Aug 29 2020 at 22:33):

Yeah

view this post on Zulip Adam Topaz (Aug 29 2020 at 22:34):

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

view this post on Zulip Heather Macbeth (Aug 29 2020 at 22:34):

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

view this post on Zulip Adam Topaz (Aug 29 2020 at 22:34):

(deleted)

view this post on Zulip Adam Topaz (Aug 29 2020 at 22:35):

The identity is given by the identity linear map

view this post on Zulip Heather Macbeth (Aug 29 2020 at 22:35):

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

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Aug 29 2020 at 22:36):

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

view this post on Zulip Adam Topaz (Aug 29 2020 at 22:36):

Yeah exactly

view this post on Zulip 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?

view this post on Zulip 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 ff would be an object in this category, and the LL would be a morphism.

view this post on Zulip Heather Macbeth (Aug 29 2020 at 22:46):

Too bad!

view this post on Zulip Adam Topaz (Aug 29 2020 at 23:09):

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

view this post on Zulip Anne Baanen (Aug 30 2020 at 10:52):

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

view this post on Zulip Chris Wong (Aug 30 2020 at 10:56):

Or lmap.


Last updated: May 13 2021 at 19:20 UTC