Timeline for How does a theory give rise to a category with finite products?
Current License: CC BY-SA 4.0
24 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 25 at 13:57 | comment | added | Todd Trimble | Renan, I'm only just seeing this question. If you're looking for some sort of synthetic description of morphisms, like "morphisms in the category of rings are defined to be functions between their underlying sets that preserve the ring operations", then there is no such description. The objects and morphisms of Lawvere's category are constructed formally by recursively applied rules, just like types and terms and formulas for a first-order theory are built up recursively. | |
| S Dec 25, 2020 at 20:01 | history | bounty ended | CommunityBot | ||
| S Dec 25, 2020 at 20:01 | history | notice removed | CommunityBot | ||
| S Dec 17, 2020 at 18:56 | history | bounty started | Renan Mezabarba | ||
| S Dec 17, 2020 at 18:56 | history | notice added | Renan Mezabarba | Improve details | |
| Dec 17, 2020 at 3:23 | comment | added | David Roberts♦ | "Lawvere presents a fixed-point theorem that generalizes both Cantor's theorem and Gödel's (first) Incompleteness Theorem." <--- Strictly speaking, the contrapositive of Lawvere's fixed-point theorem is the generalisation of the other two. | |
| Dec 17, 2020 at 1:56 | comment | added | Renan Mezabarba | Okay... I need a drink (mind blowing right now). | |
| Dec 17, 2020 at 1:54 | comment | added | Alec Rhea | I think Zhen is saying with $2$ that the projection is literally the projection from the binary product $A^n\times2^m$ into either its first factor $A^n$ or second factor $2^m$. | |
| Dec 16, 2020 at 23:42 | comment | added | Renan Mezabarba | Anyway, the other points you made were really helpful. So thanks again. :) | |
| Dec 16, 2020 at 23:36 | comment | added | Renan Mezabarba | @ZhenLin "The projections are the ones in the definition of binary products". I think that this is my problem with this kind of description. See, obviously the projections of a product in any category have to satisfy the definition of binary products... My point is: with the definition of what is an arrow in this category, one should be able to understand which arrows do the job of projections. Am I wrong? | |
| Dec 16, 2020 at 23:09 | comment | added | Zhen Lin | Actually, there are more arrows $2^4 \to 2$ than just boolean functions – rather they are (equivalence classes of) predicates with 4 propositional variables. But you get the idea. | |
| Dec 16, 2020 at 23:02 | comment | added | Zhen Lin | 1. The objects have that form because the category has finite products and is generated by $A$ and $2$. 2. The projections are the ones in the definition of binary products. 3. An arrow $A^3 \to A^2$ is a pair of of arrows $A^3 \to A$, i.e. a pair of (equivalence classes of) terms with 3 variables. 4. An arrow $2^4 \to 2^3$ is a triple of arrows $2^4 \to 2$, i.e. a triple of boolean functions with 4 variables. | |
| Dec 16, 2020 at 21:18 | history | edited | Renan Mezabarba |
edited tags
|
|
| Dec 16, 2020 at 21:11 | history | migrated | from math.stackexchange.com (revisions) | ||
| Dec 16, 2020 at 21:00 | comment | added | Renan Mezabarba | @AsafKaragila it does, indeed. It is like the arrows are the equivalence classes of the Lindenbaum algebra, while the objects are theses artificial $A$ and $2$. But it still feels ineffable to me... | |
| Dec 16, 2020 at 18:33 | comment | added | Asaf Karagila♦ | The whole thing has a bit of a Lindenbaum algebra feel to it. | |
| Dec 13, 2020 at 1:33 | comment | added | varkor | @NoahSchweber: the morphisms of a Lawvere theory are entirely abstract. Lawvere is taking the morphisms $X \to 2$ to be predicates in a first-order logic, but their semantic intent is entirely opaque to the cartesian category. You could take the morphisms to be whatever you wanted. | |
| Dec 13, 2020 at 1:29 | comment | added | varkor | @NoahSchweber: could you elaborate? It seems to me that the category $\mathbf C$ Lawvere is defining in the paper mentioned is a 2-sorted Lawvere theory (with the sorts being $A$ and $2$). | |
| Dec 13, 2020 at 1:13 | comment | added | Renan Mezabarba | Although the suggested references are nice, it seems they do not address the category defined in the article: they deal with the general context (Lawvere theories) in which the category $C$ fits... Anyway, thanks again. | |
| Dec 12, 2020 at 15:52 | comment | added | Renan Mezabarba | I'll check these too. Thank you. | |
| Dec 12, 2020 at 15:45 | comment | added | varkor | These are known as Lawvere theories. The book Algebraic theories is a good introduction (Chapter 11 specifically covers the concept Lawvere mentions here) and The Category Theoretic Understanding of Universal Algebra is a nice survey paper. Lawvere's thesis is not a particularly accessible starting point. | |
| Dec 12, 2020 at 15:44 | comment | added | Renan Mezabarba | I'll check there, thank you. | |
| Dec 12, 2020 at 15:36 | comment | added | Zhen Lin | Lawvere’s thesis is one possible place to start. | |
| Dec 12, 2020 at 14:14 | history | asked | Renan Mezabarba | CC BY-SA 4.0 |