# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorDavid_Corfield
• CommentTimeNov 25th 2019

Minor edit to trigger a discussion thread.

• CommentRowNumber2.
• CommentAuthorDavid_Corfield
• CommentTimeNov 25th 2019

Previous discussion, here and here.

• CommentRowNumber3.
• CommentAuthorGuest
• CommentTimeMar 2nd 2020

whoever before has wondered about the elusive integral notation for the coend, your time has come :)

Consider this example: let $C$ be the category of finite dimensional vector spaces over a field $k$. Let $F : C \times C^{op} \rightarrow C$ be the functor sending $(V, W)$ to $V \otimes W^*$. Then $\int^{V \in C} F(V, V) \cong k$. The structure maps $\epsilon_V$ in the coend are $\text{ev} : V \otimes V^* \rightarrow k$ sending $v \otimes f$ to $f(v)$.

In this case, and others, the recipient of the integration pairing is canonically a coend of $\text{Hom}(W, V) \cong V^* \otimes W$. What I am (hesitantly) suggesting is that the coend

$\int^{V \in C} V^* \otimes V$

and its structure maps

$\epsilon_X : V^* \otimes V \rightarrow k$

are the universal construction by which the intensives and the extensives are integrated against each other.

Note: the coend $\int^C \text{Hom}(W, V)$ is far more general than the integration pairing, but seems to match it in many cases.

Little conjecture: Let $D$ be the category of Banach spaces with short maps as morphisms. Let $F : D \times D^{op} \rightarrow D$ be the functor sending $(V, W)$ to $V \hat{\otimes} W^*$. Then $\int^{V \in D} F(V, V) \cong \mathbb{R}$.The structure maps $\epsilon_V$ are $\text{ev} : V \hat{\otimes} V^* \rightarrow k$ sending $v \otimes f$ to $f(v)$. Let CH be the category of compact hausdorff spaces and let $X$ be an object in CH. Let $V = [X, \mathbb{R}]_{\text{CH}}$, an object in $D$. An element in $V^*$ is a choice of integral (a choice of which extensive property to integrate against), and for $\phi \in V^*$ and $f \in V$,

$\phi(v) = \text{ev} (v \otimes \phi) =: \int v d \phi$

• CommentRowNumber4.
• CommentAuthorDean
• CommentTimeMar 2nd 2020

(P.S. I wrote the last post, but I wasn’t signed in.)

• CommentRowNumber5.
• CommentAuthorGuest
• CommentTimeMar 2nd 2020
Oh, and in the above little conjecture, the dual spaces are spaces of bounded maps.
• CommentRowNumber6.
• CommentAuthorDavid_Corfield
• CommentTimeMar 3rd 2020

Loregian’s book on coends opens with this kind of comparison.

Hmm, with the end as ’subspace of invariants for the action’ and coend as ’the space of orbits of said action’ is a HoTT rendition possible? I guess a starting point is:

In complete analogy to how limits are right adjoint functors to the diagonal functor, ends are right adjoint functors to the hom functor.

• CommentRowNumber7.
• CommentAuthorDavid_Corfield
• CommentTimeMar 3rd 2020
• (edited Mar 3rd 2020)

I see there’s section 2.2.2 of Combinatorial species and labelled structures on ’Coends in HoTT’. [Right, I see the Haskell community write as homotopy (co)limits: exists x. p x x, forall x. p x x.]

• CommentRowNumber8.
• CommentAuthorGuest
• CommentTimeMar 3rd 2020

Proposition: Let $V$ be a monoidal closed category with tensor $\otimes_V$ and internal hom $[X, Y]_V$. Suppose that the Kan extension $\text{Lan}_{\text{Id}_V} (\text{Id}_V)$ exists and is pointwise. Then

$X \cong \text{Id}_V (X) \cong \text{Lan}_{\text{Id}_V} (\text{Id}_V) (X) \cong \int^{Y \in V} [Y, X]_V \otimes_V Y$

Let $\text{Ban}_1$ be the category of Banach spaces and short maps. $\text{Ban}_1$ has an internal Hom consisting of bounded maps (Write $[-, -]$ for external Hom and $\text{Hom}(-, -)$ for internal Hom). Internal Hom has a left adjoint, projective tensor product.

Theorem: $\text{Lan}_{\text{Id}_{\text{Ban}_1}}(\text{Id}_{\text{Ban}_1})$ exists and is pointwise, so that

$\mathbb{R} \cong \text{Id}_D (\mathbb{R}) \cong \text{Lan}_{\text{Id}_D} (\text{Id}_D) \cong \int^{V \in D} [V, \mathbb{R}] \otimes_D V$

where $\otimes_D$ is projective tensor product.

• CommentRowNumber9.
• CommentAuthorGuest
• CommentTimeMar 3rd 2020
That should be $\int^{V \in D} \text{Hom}(V, \mathbb{R}) \otimes_D V$.

I will add this and its proof -- is that ok?
1. I have added the coend-integral comparison to section 3 of the intensive/extensive property page.

This includes the theorem mentioned in (8) in our nform discussion here.

I wrote it in terms of Lawvere metrics instead of metrics.

edeany@umich.edu