Timeline for Multiplication and division by a morphism under the “inner composition” in closed monoidal categories
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 1, 2019 at 18:27 | comment | added | Mike Shulman | Now all we need is for someone to give a proof with string diagrams! | |
| Jul 1, 2019 at 14:54 | comment | added | Sergei Akbarov | Peter, I understood this at last! This follows from the two identities that must be proved separately: $$ \psi^{-1}_{A',B',C'}\big(\gamma\circ\omega\circ(\alpha\otimes\beta)\big)=[\beta,\gamma]\circ\psi^{-1}_{A,B,C}(\omega)\circ\alpha $$ and $$ \psi^{-1}_{X,A,B}\left(\operatorname{ev}^B_A\circ\ (\varphi\otimes 1_A)\right)=\varphi. $$ However your words about "different definitions" remain puzzling for me, I think, the explanation will be crearer without them. | |
| Jul 1, 2019 at 12:06 | comment | added | Peter LeFanu Lumsdaine | If you’re not familiar with the equivalence between these different definitions, I really recommend working them out yourself — it’s a very useful exercise, and the equivalence is used implicitly all over the place (like I was using it here). But if it’s still unclear, then I suggest asking a new question at math.SE about it — we’ve gone on a bit too long in comments here :-) | |
| Jul 1, 2019 at 12:01 | comment | added | Peter LeFanu Lumsdaine | Given this, I am taking $ev_{X,Y} : [X,Y] \otimes X \to Y$ to be the map corresponding to $1_{[X,Y]}$ under $\psi_{[X,Y],X,Y}$. It follows by naturality that for arbitrary $X,Y,Z$, the bijection $\psi_{X,Y,Z}$ sends $f : X \to [Y,Z]$ to $ev_{Y,Z} \circ (f \otimes 1_Y) : X \otimes Y \to Z$. Whatever other presentation of the definition you are using, you should be able to prove that it gives this definition; the proof should roughly be like the proofs that different definitions of adjoint are equivalent, as discussed at e.g. ncatlab.org/nlab/show/adjoint+functor | |
| Jul 1, 2019 at 11:57 | comment | added | Peter LeFanu Lumsdaine | @SergeiAkbarov: We are both talking about the “usual definition” — the point is that this definition can be presented in several slightly different ways, but the equivalences between them are very standard, and so the differences are not usually thought of as significant. Specifically, I’m assuming the definition given at the nlab: that there’s a natural bijection $\psi_{X,Y,Z} : C(X,[Y,Z]) \cong C(X \otimes Y, Z)$. [cont’d] | |
| Jul 1, 2019 at 11:32 | comment | added | Sergei Akbarov | Peter, this is where the misunderstanding lies. I was asking about a general symmetric closed monoidal category, which I understand in the sense of usual definition, i.e. a category with the given functors $\otimes$ and $[\cdot,\cdot]$. You seem to have in mind another definition (which I don't know), where $\operatorname{ev}_{\cdot,\cdot}$ is given (and axiomatized) instead of $[\cdot,\cdot]$. So for me this equation requires a proof. | |
| Jul 1, 2019 at 10:52 | comment | added | Peter LeFanu Lumsdaine | …then that equation must proved some other way, e.g. by naturality, or the unit/counit equations of the adjunction, or similar. There are many equivalent ways to present the internal hom-functor, coming (in part) from the different ways to present adjunctions, and the fact that adjoints are automatically functorial when they exist. | |
| Jul 1, 2019 at 10:50 | comment | added | Peter LeFanu Lumsdaine | Yes, that is the equation I meant by “the defining equation for $[\varphi,1_D]$”. If the operation $[A,B]$ is introduced as characterised by its universal property, then the operation sending $f : X' \to X$ and $g : Y \to Y'$ to $[f,g] : [X,Y] \to [X',Y']$ is usually defined as “the map corresponding to $g \circ ev_{X',Y} \circ (1_[X,Y] \otimes f) : [X,Y] \otimes X' \to Y'$”, in other words by the equation $ev_{X',Y'} \circ ([f,g] \otimes 1_{Y'}) = g \circ ev_{X',Y} \circ (1_[X,Y] \otimes f)$. If the operation $[f,g]$ is introduced/assumed some other way (e.g. functoriality), then [cont’d] | |
| Jun 30, 2019 at 15:18 | comment | added | Sergei Akbarov | Peter, I feel like a schoolboy near you. :) As far as I understand, you call this $$\operatorname{ev}_{B,D}\circ([\varphi,1_D]\otimes 1_B)=\operatorname{ev}_{C,D}\circ(1_{[C,D]}\otimes\varphi)$$ -- the defining equation for $[\varphi,1_D]$. Excuse me my ignorance, why is this true? (Actually, in my understanding the operation $(A,B)\mapsto [A,B]$ is not defined, it is introduced axiomatically, so this identity must be proved.) | |
| Jun 30, 2019 at 14:54 | comment | added | Peter LeFanu Lumsdaine | In the result you reached, split up $([\varphi,1_D] \otimes ev_{A,B})$ as $([\varphi,1_D] \otimes 1_B) \circ (1_{[C,D]} \otimes ev_{A,B})$, and then use the defining equation of $[\varphi,1_D]$. The way to find this is to notice that you should expect to need the defining equation of $[\varphi,1_D]$, so look at that equation, and then try to think how to get your result into a form where you can use that equation. | |
| Jun 30, 2019 at 14:46 | comment | added | Sergei Akbarov | I don't understand something. I come to the result $\operatorname{ev}_{B,D}\circ[\varphi,1_D]\otimes\operatorname{ev}_{A,B}$. Why is this equal to $\operatorname{ev}_{C,D} \circ (1_{[C,D]} \otimes \varphi) \circ (1_{[C,D]} \otimes\operatorname{ev}_{A,B})$? | |
| Jun 30, 2019 at 14:23 | comment | added | Peter LeFanu Lumsdaine | Notice that in the first calculation, the two key steps use the equalities $ev_{A,D}( \bullet_{A,C,D} \otimes 1_A) = ev_{C,D} \circ (1_{[C,D]} \otimes ev_{A,C})$ and $ev_{A,C} \circ ([1_A,\varphi] \otimes 1_A) = \varphi \circ ev_{A,B}$. These equalities are essentially the definitions of $\bullet_{A,C,D}$ and $[1_A,\varphi]$ in terms of their exponential transpose maps. All other steps are just monoidal category laws. The second calculation is very analogous, but its two key steps use the defining equalities of $\bullet_{A,B,D}$ and $[\varphi,1_D]$. | |
| Jun 30, 2019 at 13:03 | comment | added | Sergei Akbarov | Peter, I don't understand why the second calculation gives the same result. | |
| Jun 30, 2019 at 12:08 | history | answered | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |