Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
whoever before has wondered about the elusive integral notation for the coend, your time has come :)
Consider this example: let be the category of finite dimensional vector spaces over a field . Let be the functor sending to . Then . The structure maps in the coend are sending to .
In this case, and others, the recipient of the integration pairing is canonically a coend of . What I am (hesitantly) suggesting is that the coend
and its structure maps
are the universal construction by which the intensives and the extensives are integrated against each other.
Note: the coend is far more general than the integration pairing, but seems to match it in many cases.
Little conjecture: Let be the category of Banach spaces with short maps as morphisms. Let be the functor sending to . Then .The structure maps are sending to . Let CH be the category of compact hausdorff spaces and let be an object in CH. Let , an object in . An element in is a choice of integral (a choice of which extensive property to integrate against), and for and ,
Your thoughts?
(P.S. I wrote the last post, but I wasn’t signed in.)
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.
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.]
Proposition: Let be a monoidal closed category with tensor and internal hom . Suppose that the Kan extension exists and is pointwise. Then
Let be the category of Banach spaces and short maps. has an internal Hom consisting of bounded maps (Write for external Hom and for internal Hom). Internal Hom has a left adjoint, projective tensor product.
Theorem: exists and is pointwise, so that
where is projective tensor product.
1 to 10 of 10