Timeline for Reference request for Linton's theorems on equational theories
Current License: CC BY-SA 4.0
26 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
May 18, 2021 at 19:23 | comment | added | Martin Brandenburg | Indeed I also mention that Lemma 10.2 in my question, but also that the proof is omitted. And as you say, it is unclear if "theories" there coincide with infinitary Lawvere theories. (With all that being said, I am really confused by F, often also E are cited as a reference for the equivalence. Perhaps it is the right thing to do, but for someone who wants to actually read a proof such a citation is not useful at all.) | |
May 18, 2021 at 19:14 | comment | added | varkor | @MartinBrandenburg: I was looking at the paper again today, and I realised I had overlooked Lemma 10.2, which does establish a relationship between the categories of monads and "theories" (for a suitable notion of theory), and in particular monad morphisms and morphisms of "theories". In this light, I think it is appropriate to attribute the full equivalence to Linton; however, Dubuc's paper is certainly the first that contains the modern monad–theory correspondence (with the modern definition of "theory"). I've updated my answer accordingly. Apologies for the confusion. | |
May 18, 2021 at 19:11 | history | edited | varkor | CC BY-SA 4.0 |
added 119 characters in body
|
May 13, 2021 at 12:57 | comment | added | varkor | Happy to help! My real name can be found on my academic webpage :) | |
May 13, 2021 at 0:09 | comment | added | Martin Brandenburg | Thanks a lot for doing this, you really helped me a lot with the research. :-) I also would like to list you in the acknowledgements of the paper, but I could not find your full name. If you want to appear there but don't want to reveal your identity here, you can email me. PS: q.uiver is really cool. | |
May 12, 2021 at 23:40 | comment | added | varkor | I emailed Dubuc, who believed he was the first to prove the full equivalence between monads and theories (rather than just the bijection between monads and theories as Linton does), so I think it worth citing both authors for the origin of the modern correspondence. | |
May 12, 2021 at 23:38 | history | edited | varkor | CC BY-SA 4.0 |
added 13 characters in body
|
May 12, 2021 at 19:05 | vote | accept | Martin Brandenburg | ||
May 12, 2021 at 14:44 | comment | added | varkor | I may email around to see whether anyone can shed light on the provenance of the precise modern statement. | |
May 12, 2021 at 14:36 | comment | added | varkor | I've added an outline of the relevant steps in Linton's result. It may be appropriate to attribute the modern form of the correspondence to Dubuc. | |
May 12, 2021 at 14:33 | history | edited | varkor | CC BY-SA 4.0 |
added 56 characters in body
|
May 12, 2021 at 14:26 | history | edited | varkor | CC BY-SA 4.0 |
Add some details about Linton's development
|
May 12, 2021 at 14:00 | comment | added | varkor | Sorry, you're right: I swapped 1 and 2 by mistake. Dubuc proves 2 and 3 in Theorem III: the equations (1) and (2) state that the equivalence commutes with taking categories of algebras. I believe that the monads are equivalent follows because taking the codensity monad of a functor means the monad structure is uniquely determined, so it suffices just to check that the left adjoint is correct. (I think there are more elegant proofs of this correspondence, but there's often a trade-off between a classical proof and an elegant one!) | |
May 12, 2021 at 13:53 | comment | added | Martin Brandenburg | Ah I just see that Dubuc "proves" 3 as well. | |
May 12, 2021 at 13:51 | history | edited | varkor | CC BY-SA 4.0 |
added 3 characters in body
|
May 12, 2021 at 13:50 | comment | added | Martin Brandenburg | Dubuc does not prove 1,3, but rather a generalization of 2 (as Theorem III), right? And it seems that Dubuc omits some details there as well: in order to check that two monads are isomorphic, it is not enough to check that the underlying functors are isomorphic. (But one might argue that, since we start with just one monad, another monad structure on the same functor has to be equal to it by some kind of "meta-coherence-theorem" which I would like to prove some day...). | |
May 12, 2021 at 13:32 | comment | added | varkor | @MartinBrandenburg: I shall try to do so a little later. | |
May 12, 2021 at 13:28 | vote | accept | Martin Brandenburg | ||
May 12, 2021 at 13:28 | |||||
May 12, 2021 at 13:26 | comment | added | Martin Brandenburg | But can you explain the connection between Linton's theorems 8.1 and 9.1 and the theorems in my question? | |
May 12, 2021 at 11:36 | comment | added | Martin Brandenburg | Alright. Thank you! | |
May 12, 2021 at 9:52 | comment | added | varkor | My understanding is that the unenriched correspondences were part of the folklore after Linton, so all that was left was the enriched versions. I agree it'd be nice to see the intermediate step, but Dubuc's paper is dated 1970, just one year after Linton's paper, so it's unlikely such a reference exists. | |
May 12, 2021 at 8:09 | comment | added | Martin Brandenburg | Thank you! Yes I already found some papers which deal with the enriched case (for example the paper by Nishizawa, Power), but I wondered if there are more classical sources. I will have closer look at the papers by Dubuc, Power and Lucyshyn-Wright in the next days. | |
May 11, 2021 at 11:00 | history | edited | varkor | CC BY-SA 4.0 |
added 463 characters in body; added 102 characters in body
|
May 11, 2021 at 10:14 | history | edited | varkor | CC BY-SA 4.0 |
edited body
|
May 10, 2021 at 22:54 | history | edited | varkor | CC BY-SA 4.0 |
Added references for categories of algebras; deleted 20 characters in body
|
May 10, 2021 at 22:45 | history | answered | varkor | CC BY-SA 4.0 |