Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Is this well defined?

Bruno Gavranović (Apr 16 2023 at 16:22):

Consider the category of real finite-dimensional vector spaces $\mathbf{FVect}$ with tensor product as the monoidal product.
Consider the category of euclidean spaces and differentiable maps $\mathbf{Euc}$ with the cartesian product as the monoidal product.
Then it looks the identity embedding $I : \mathbf{FVect} \to \mathbf{Euc}$ becomes lax monoidal, i.e.

$$(I, \mu, \epsilon) : (\mathbf{FVect}, \otimes, \mathbb{R}) \to (\mathbf{Euc}, \times, 1)$$

Explicitly, the laxator $\mu_{\mathbb{R}^n, \mathbb{R^m}}$ is a morphism in $\mathbf{Euc}$ of type

$$I(\mathbb{R}^n) \times I(\mathbb{R}^m) \to I(\mathbb{R^n} \otimes \mathbb{R}^m)$$

which is equivalent to a differentiable function $\mathbb{R}^{n + m} \to \mathbb{R^{nm}}$. We have a good candidate for it -- the outer product which maps $(v, w) \mapsto v w^{\intercal}$. That is, for each component $(i, j)$ of the codomain we compute $v_i w_j$. Note that this is not linear, but is bilinear, and clearly differentiable.
The laxator is a map in $\mathbf{Euc}$ of type $1 \to \mathbb{R}$ which picks out 1, the multiplicative identity.

It looks like this is well-defined, and works. But I've never seen anyone talk or discuss it! Tagging @Jules Hedges since he came up with it

John Baez (Apr 16 2023 at 22:02):

What's a "Euclidean space" for you? I would think of it as a finite-dimensional real affine space with a metric of a certain nice sort, since Euclidean geometry uses a metric. For example, a Euclidean group is the automorphism group of a Euclidean space in my sense.

But you can't mean "Euclidean group" in this sense, since linear maps between finite-dimensional real vector spaces don't need to preserve the metric (mainly since they don't need to have a metric).

John Baez (Apr 16 2023 at 22:02):

I think instead of "Euclidean space" the standard term you're looking for is (finite-dimensional real) [[affine space]].

Dylan Braithwaite (Apr 16 2023 at 22:06):

John Baez said:

I think instead of "Euclidean space" the standard term you're looking for is (finite-dimensional real) [[affine space]].

I think Bruno is thinking of a category containing finite dimensional vector spaces with smooth maps between them rather than linear or affine maps

John Baez (Apr 16 2023 at 22:08):

That sounds reasonable. I just found the name Euc a bit distracting, since it makes me think of Euclidean geometry, the Euclidean group, and stuff like that.

John Baez (Apr 16 2023 at 22:11):

If we understand this category Euc correctly, it's the one Urs Schreiber calls [[CartSp]], or more precisely $\mathsf{CartSp}_{\rm{smooth}}$.

John Baez (Apr 16 2023 at 22:14):

Anyway, if this is what Euc means then yes, there seems to be a lax monoidal functor from $(\mathsf{FVect}, \otimes)$ to $(\mathsf{Euc}, \times)$.

John Baez (Apr 16 2023 at 22:15):

The laxator is the universal bilinear map $V \times W \to V \otimes W$, which people talk about whenever they explain the universal property of the tensor product.

John Baez (Apr 16 2023 at 22:17):

E.g.:

• Wikipeda, Tensor product: universal property.

Bruno Gavranović (Apr 16 2023 at 23:58):

That's strange, I first picked up the term $\mathbf{Euc}$ from Backprop as Functor. I thought it was a standard terminology for a standard kind of a category, but I've received pushback/confusion from a few people when I told them this.

Bruno Gavranović (Apr 17 2023 at 00:00):

Anyhow - that's great to hear! I've seen the universal property of the tensor product a number of times, but I've never seen it stated as a lax monoidal functor.

John Baez (Apr 17 2023 at 00:03):

I have a feeling that you are doing a fancy version of something where you use $\mathsf{Set}$ instead of $\mathsf{Euc}$.

Namely, there's a forgetful functor from $\mathsf{Vect}$ to $\mathsf{Set}$, and the tensor product on $\mathsf{Vect}$ is defined in a way that makes the left adjoint $L: \mathsf{Set} \to \mathsf{Vect}$ be strong monoidal.

John Baez (Apr 17 2023 at 00:04):

Then there's a great little theorem saying the right adjoint of a strong monoidal functor is lax monoidal!

John Baez (Apr 17 2023 at 00:04):

So the right adjoint, the forgetful functor $R : \mathsf{Vect} \to \mathsf{Set}$, is automatically lax monoidal.

John Baez (Apr 17 2023 at 00:05):

What you are doing next is restricting attention to $\mathsf{FVect}$ and noticing that the image of $R$ lies in a very nice subcategory of $\mathsf{Set}$, but with the same (cartesian) monoidal structure.

Bruno Gavranović (Apr 17 2023 at 14:55):

John Baez said:

Then there's a great little theorem saying the right adjoint of a strong monoidal functor is lax monoidal!

Ah, this is the whole story of vertical (lax monoidal) and horizontal (oplax monoidal) morphisms in a double category, since here we've got a shadow of the adjunction in a double category, making our oplax monoidal additionally strong (since it needs to be at least lax).

Bruno Gavranović (Apr 17 2023 at 14:55):

Yes, it sounds plausible that this is exactly what I'm doing.

Matteo Capucci (he/him) (Apr 20 2023 at 10:59):

Bruno Gavranović said:

John Baez said:

Then there's a great little theorem saying the right adjoint of a strong monoidal functor is lax monoidal!

Ah, this is the whole story of vertical (lax monoidal) and horizontal (oplax monoidal) morphisms in a double category, since here we've got a shadow of the adjunction in a double category, making our oplax monoidal additionally strong (since it needs to be at least lax).

(Notice though that lax+oplax $\neq$ strong, e.g. the Nashator is lax monoidal structure on a functor which is also oplax monoidal but the oplax structure is only left inverse to the lax one)