Timeline for How is the morphism of composition in the enriched category of modules constructed?
Current License: CC BY-SA 4.0
25 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 28, 2021 at 15:13 | vote | accept | Sergei Akbarov | ||
| Sep 26, 2021 at 15:58 | comment | added | Sergei Akbarov | Peter, I have another suspicion for the explanation of why your calculations are simpler: your connection between $-\otimes-$ and $V(-,-)$ is a bit unusual: $V(A\otimes M,N)=V(M,V(A,N))$. Not $V(A\otimes M,N)=V(A,V(M,N))$ as in Kelly's book and in the websites. Is this indeed important for simplification? | |
| Sep 26, 2021 at 12:12 | comment | added | Sergei Akbarov | I see. OK, Peter, I need some time to look at all this, thank you! | |
| Sep 26, 2021 at 11:22 | comment | added | Peter LeFanu Lumsdaine | @SergeiAkbarov: Yes, $\cdot$ is composition. In my note about definitions, I didn’t mean your definition was specifically different; just that a lot of concepts can be defined in several equivalent but slightly different ways — e.g. an adjunction can be defined in terms of natural bijections of hom-sets, or representability of the functors $C(X,U(-))$, or unit + counit + triangle equalities; similarly, the definition of monoidal closed category can be given several ways. You were asking me to break things down to “the axioms”; I didn’t know precisely which version of the axioms you wanted. | |
| Sep 26, 2021 at 10:41 | comment | added | Sergei Akbarov | Peter, by the dot $g\cdot f$ do you mean the composition $g\circ f$? | |
| Sep 26, 2021 at 10:39 | comment | added | Sergei Akbarov | Peter, I would say, Kelly is not for beginners. After your words about different definitions, I checked them and I don't see differences betwen what I use and what Kelly and the websites write... | |
| Sep 26, 2021 at 10:31 | comment | added | Peter LeFanu Lumsdaine | But the one tool I use constantly, which it seems you’re not so fluent with, is naturality of transpose, and in particular the co-unit formula for transpose. Generally, for $\newcommand{\x}{\otimes}g\cdot f : A \to B \to [X,C]$, the transpose $\widehat{g\cdot f}$ is $\hat{g}\cdot (X \x f) : X \x A \to X \x B \to C$ — this is just naturality of the transpose operation. Now taking $g = 1_{[X,C]}$ gives a general formula for the transpose: $\hat{f} = \widehat{1_{[X,C]}}\cdot (X \x f) : X \x A \to X \x [X,C] \to C$, and $\widehat{1_{[X,C]}}$ is $\mathrm{ev}_{X,C}$, the adjunction co-unit. | |
| Sep 26, 2021 at 10:26 | comment | added | Peter LeFanu Lumsdaine | @SergeiAkbarov: I recommend Kelly’s Basic Concepts of Enriched Category Theory. Regarding methods: I wouldn’t say the difference is diagrams vs. chains of formulas. The big diagram shouldn’t expand much — the unmarked squares are just bifunctoriality of tensor. And the was I think of this are, from most important to least, (1) algebraic/λ-calculus in the internal language, like at the start of my answer (for intuition, even if I’m not using it formally); (2) diagrams; (3) chains of formulas in the category itself. [cont’d] | |
| Sep 26, 2021 at 8:01 | comment | added | Sergei Akbarov | Actually, if you also could recommend a textbook for the beginners, that would be great. I do not see such a book. | |
| Sep 26, 2021 at 7:51 | comment | added | Sergei Akbarov | For example, in that big diagram that you gave, I would begin to prove the commutativity of each fragment by writing it out and completing it to a diagram whose fragments are commutative by the definition of a closed category (or have already been proved earlier). Could you resolve my doubts: is this the difference in our methods? Is it true that if we do this, then the original plan (like your big diagram) grows to a large number of diagrams? Or is our discrepancy in something else? | |
| Sep 26, 2021 at 7:51 | comment | added | Sergei Akbarov | Peter, thank you for this addition, and excuse me for not replying before, I was working. However I again need some time for translation so that I could understand this. I have a conjecture of what I am doing wrong: probably the whole point is that I do not write out chains of formulas, like you, but replace them with diagrams. | |
| Sep 24, 2021 at 16:14 | comment | added | Peter LeFanu Lumsdaine | @SergeiAkbarov: I’ve added a proof that my definition agrees with Martin’s definition you linked (which, as you say, amounts essentially to the lemma you give in the question). But I don’t see what you mean that my definition is “not independent” — I think with the definition I give, everything in the main proof follows directly, not needing any mention of Martin’s definition? | |
| Sep 24, 2021 at 16:10 | history | edited | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |
Added explanation of why my definition agrees with that linked by OP
|
| Sep 20, 2021 at 6:05 | comment | added | Sergei Akbarov | Peter, and your definition of $_AV(M,N)$ seems to be not independent: the existence of the universal morphism $_AV(M,N)\to V(M,N)$ such that the two ways from $A\otimes M\otimes {_AV(M,N)}$ to $N$ coincide, follows from Martin's construction... If I don't miss something. And again to prove this we need this Lemma. | |
| Sep 19, 2021 at 19:30 | comment | added | Sergei Akbarov | Peter, yes I would be grateful, if you could clarify this equivalence. | |
| Sep 19, 2021 at 19:28 | comment | added | Peter LeFanu Lumsdaine | I find the definition I used slightly simpler, so I recommend just taking it as primary, in which case you don’t need the lemma :-) But yes, the two do coincide as your lemma says (and that takes just one fairly small diagram) — I can add more explanation later, when I have more time, if you’re still stuck on that. It’s a good exercise with internal homs, though! | |
| Sep 19, 2021 at 19:28 | comment | added | Sergei Akbarov | Peter, yes, I use the construction that Martin suggested at MSE. And I am stuck in the equivalence of these two definitions. How do people prove it? | |
| Sep 19, 2021 at 19:24 | comment | added | Peter LeFanu Lumsdaine | @SergeiAkbarov: It depends how you define the objects $\newcommand{\AV}{{}_A V}\AV(M,N)$ — in particular, how you give the maps $V(M,N) \to V(A \otimes M,N)$ for the equaliser. I was assuming the definition where those maps are given as the transposes of the maps $A \otimes M \otimes V(M,N) \to N$ that appear in my ⊛ hexagons — so then the hexagons commute by definition. I guess you’re following Martin Brandenburg’s definition here — in that case, yes, you need to show his definition agrees with mine, which is roughly your lemma. (cont’d) | |
| Sep 19, 2021 at 19:12 | comment | added | Sergei Akbarov | Peter, you are right with this big diagram, but those little fragments, that you mark by $\circledast$, are corollaries of my Lemma, isn't it? So I would think that this lemma is necessary anyway. Or am I mistaken? | |
| Sep 19, 2021 at 12:45 | comment | added | Sergei Akbarov | Peter, I need some time to analyze this. | |
| Sep 19, 2021 at 11:17 | history | edited | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |
fixed typo in math
|
| Sep 19, 2021 at 11:07 | comment | added | Peter LeFanu Lumsdaine | @fosco: Actually, working roughly through it, I don’t feel your linked exercise is really a counterexample — it feels like the ratio (size of algebraic proof):(size of categorical proof) is pretty typical, similar to this question. Our familiarity with ring algebra makes the algebraic proof feel like a one-liner — but written out fully in terms of the (near-)ring axioms, it takes well over a dozen steps. (The first approach I thought of used 26; with a little thought I’ve got it down to 18.) So it’s not shocking that the categorical proof is long, especially if taken head-on. | |
| Sep 19, 2021 at 10:32 | comment | added | Peter LeFanu Lumsdaine | @fosco: Certainly — I meant it as a rule of thumb, not an absolute generality. | |
| Sep 19, 2021 at 10:23 | comment | added | fosco | > "a simple algebraic proof should become a reasonably simple categorical proof." It should, but there are notable exceptions : i.postimg.cc/3wFV3xyt/immagine-2021-09-19-122224.png | |
| Sep 19, 2021 at 10:05 | history | answered | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |
