Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorTobyBartels
   • CommentTimeAug 4th 2010
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI've started [[infinitary Lawvere theory]] following [this n-Forum discussion](http://www.math.ntnu.no/~stacey/Vanilla/nForum/comments.php?DiscussionID=1673).

   I’ve started infinitary Lawvere theory following this n-Forum discussion.

2. • CommentRowNumber2.
   • CommentAuthorAndrew Stacey
   • CommentTimeAug 5th 2010
   • PermaLink
   Author: Andrew Stacey
   Format: MarkdownItexEdits and Questions: 1. The definition of __sorts__: Do we want "equipped with" or "there exists a"? Namely, should an explicit set of sorts be built in to the definition? 2. Relating to that, for an $S$-sorted theory, should the functor $S \to \mathcal{D}$ be injective (in whatever appropriate sense)? Perhaps not, since if not then we can regard a single sorted theory as a degenerate case of a $2$-sorted theory. 3. Still on $S$-sorted theories, there seemed to be a bit missing: the image of $S$ in $\mathcal{D}$ should be the/a subcategory of sorts. I've put something in appropriate to the fact that we say "equipped with" at the moment. 4. Started on the proof that models of the Lawvere theory form an algebraic (monadic?) category, but not gotten all the details (that I know of) down yet.

   Edits and Questions:

   1. The definition of sorts: Do we want “equipped with” or “there exists a”? Namely, should an explicit set of sorts be built in to the definition?
   2. Relating to that, for an $S$-sorted theory, should the functor $S \to \mathcal{D}$ be injective (in whatever appropriate sense)? Perhaps not, since if not then we can regard a single sorted theory as a degenerate case of a $2$-sorted theory.
   3. Still on $S$-sorted theories, there seemed to be a bit missing: the image of $S$ in $\mathcal{D}$ should be the/a subcategory of sorts. I’ve put something in appropriate to the fact that we say “equipped with” at the moment.
   4. Started on the proof that models of the Lawvere theory form an algebraic (monadic?) category, but not gotten all the details (that I know of) down yet.
3. • CommentRowNumber3.
   • CommentAuthorAndrew Stacey
   • CommentTimeAug 5th 2010
   • PermaLink
   Author: Andrew Stacey
   Format: MarkdownItexLittle bit more on the proof of the adjunction. I'm not done yet but it's bedtime. I'm probably putting in far too much detail, but I'd rather do that to start with since this sort of thing is fairly new to me so _I_ want to be sure that all the i's are crossed and all the t's dotted before pruning the proof down to something more reasonable. Presumably the next step is to show that it is a [[monadic adjunction]]. Is that obvious due to its being a sort of functor category?

   Little bit more on the proof of the adjunction. I’m not done yet but it’s bedtime. I’m probably putting in far too much detail, but I’d rather do that to start with since this sort of thing is fairly new to me so I want to be sure that all the i’s are crossed and all the t’s dotted before pruning the proof down to something more reasonable.

   Presumably the next step is to show that it is a monadic adjunction. Is that obvious due to its being a sort of functor category?

4. • CommentRowNumber4.
   • CommentAuthorTobyBartels
   • CommentTimeAug 6th 2010
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItex1. I think definitely equipped with. Already in an unsorted Lawvere therory, you want to know which object is $R$. 2. You can always make $S \to \mathcal{D}$ injective on the nose by replacing $\mathcal{D}$ with an equivalent category, but I don't think that there's any point in even mentioning that. Surely we do not want to make $S \to \mathcal{D}$ injective up to isomorphism, since that fails in some examples. 3. I agree with your edit, I left out a clause. 4. I'd say [[monadic category]] as the most precise term (and one that we expect to be correct). I haven't read your details yet.

   1. I think definitely equipped with. Already in an unsorted Lawvere therory, you want to know which object is $R$.
   2. You can always make $S \to \mathcal{D}$ injective on the nose by replacing $\mathcal{D}$ with an equivalent category, but I don’t think that there’s any point in even mentioning that. Surely we do not want to make $S \to \mathcal{D}$ injective up to isomorphism, since that fails in some examples.
   3. I agree with your edit, I left out a clause.
   4. I’d say monadic category as the most precise term (and one that we expect to be correct). I haven’t read your details yet.
5. • CommentRowNumber5.
   • CommentAuthorAndrew Stacey
   • CommentTimeAug 6th 2010
   • PermaLink
   Author: Andrew Stacey
   Format: MarkdownItexI've finished with the proof of the adjunction. As I said, probably a messy proof. Next stop, monadicity. Any opinions on what'll be the easiest to prove? I see from [[monadicity theorem]] that there's a few choices.

   I’ve finished with the proof of the adjunction. As I said, probably a messy proof.

   Next stop, monadicity. Any opinions on what’ll be the easiest to prove? I see from monadicity theorem that there’s a few choices.

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeAug 6th 2010
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexIt occurs to me that, while an $S$-sorted theory should be equipped with an $S$-indexed family of sorts, a general many-sorted infinitary Lawvere theory should not be equipped with a family of sorts. Compare [this Café comment by Mike](http://golem.ph.utexas.edu/category/2010/07/what_is_a_theory.html#c034008); Lawvere theories are at the last stage, where we have generated all additional types (objects) that must exist in our doctrine and are not remembering which are the generating ones, any more than we remember which are the generating operations or axioms. In other words, the existence of $\mathcal{R}$ in the most general case is simply a smallness criterion. If we were working with finitary Lawvere theories, then we'd just say ‘small’ and be done with it. On the other hand, when in doubt, one should always say ‘equipped with’. One can always define the morphisms later to ignore this equipment. So an equivalence of $S$-sorted Lawvere theories must preserve the $S$ sorts, while an equivalence of many-sorted Lawvere theories might not. Anyway, I edited the article a bit to reflect this.

   It occurs to me that, while an $S$-sorted theory should be equipped with an $S$-indexed family of sorts, a general many-sorted infinitary Lawvere theory should not be equipped with a family of sorts. Compare this Café comment by Mike; Lawvere theories are at the last stage, where we have generated all additional types (objects) that must exist in our doctrine and are not remembering which are the generating ones, any more than we remember which are the generating operations or axioms.

   In other words, the existence of $\mathcal{R}$ in the most general case is simply a smallness criterion. If we were working with finitary Lawvere theories, then we’d just say ‘small’ and be done with it.

   On the other hand, when in doubt, one should always say ‘equipped with’. One can always define the morphisms later to ignore this equipment. So an equivalence of $S$-sorted Lawvere theories must preserve the $S$ sorts, while an equivalence of many-sorted Lawvere theories might not.

   Anyway, I edited the article a bit to reflect this.

7. • CommentRowNumber7.
   • CommentAuthorAndrew Stacey
   • CommentTimeAug 6th 2010
   • PermaLink
   Author: Andrew Stacey
   Format: MarkdownItexI mostly agree with you. What I hesitate about is the forgetful functor from $Prod[\mathcal{D},Set]$. Where should it land up? At the moment, I have it landing in $[S,Set]$, but that relies on a choice of $S$. Perhaps this is inevitable: if the theory were 1-sorted then you'd want to end up with a definite set which would mean evaluating the functor on a definite object. So if we want the forgetful functor to be part of the deal of $Prod[\mathcal{D},Set]$ then we need to choose a subcategory of sorts. Hmmm, maybe I should go and read that "What is a theory?" discussion.

   I mostly agree with you. What I hesitate about is the forgetful functor from $Prod[\mathcal{D},Set]$. Where should it land up? At the moment, I have it landing in $[S,Set]$, but that relies on a choice of $S$. Perhaps this is inevitable: if the theory were 1-sorted then you’d want to end up with a definite set which would mean evaluating the functor on a definite object.

   So if we want the forgetful functor to be part of the deal of $Prod[\mathcal{D},Set]$ then we need to choose a subcategory of sorts.

   Hmmm, maybe I should go and read that “What is a theory?” discussion.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeAug 6th 2010
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex@Toby #6, I think that's an interesting question irrespective of finitarity or even many-sortedness. Is an ordinary "Lawvere theory" equipped with a generating object, or such that there exists a generating object? I think that's the difference between the last two levels of embodiment: the "multicategory" level and the "fully embodied" level. A Lawvere theory, as a category with finite products, is fully embodied -- but if we consider its generating object as structure and require morphisms to preserve that structure, we get a 2-category of Lawvere theories equivalent to that of finite-product-multicategories, at one lower level of embodiment. Just like if we consider, say, the category of free groups with specified generators and group homomorphisms that take generators to generators, we get something equivalent to Set. The conceptual relationship is clear to me, but I'm not sure whether one viewpoint or the other is implied by the terminology "Lawvere theory." IIRC even back in Lawvere's original work introducing the concept, he considered both types of morphisms of theories, those preserving the generator and those not.

   @Toby #6, I think that’s an interesting question irrespective of finitarity or even many-sortedness. Is an ordinary “Lawvere theory” equipped with a generating object, or such that there exists a generating object? I think that’s the difference between the last two levels of embodiment: the “multicategory” level and the “fully embodied” level. A Lawvere theory, as a category with finite products, is fully embodied – but if we consider its generating object as structure and require morphisms to preserve that structure, we get a 2-category of Lawvere theories equivalent to that of finite-product-multicategories, at one lower level of embodiment. Just like if we consider, say, the category of free groups with specified generators and group homomorphisms that take generators to generators, we get something equivalent to Set. The conceptual relationship is clear to me, but I’m not sure whether one viewpoint or the other is implied by the terminology “Lawvere theory.” IIRC even back in Lawvere’s original work introducing the concept, he considered both types of morphisms of theories, those preserving the generator and those not.

9. • CommentRowNumber9.
   • CommentAuthorAndrew Stacey
   • CommentTimeAug 6th 2010
   • PermaLink
   Author: Andrew Stacey
   Format: MarkdownItexOkay, so there's some value in allowing for both. But am I right that we need the sorts in order to define the forgetful functor when trying to make $Prod[\mathcal{D},Set]$ in to an algebraic category over something?

   Okay, so there’s some value in allowing for both.

   But am I right that we need the sorts in order to define the forgetful functor when trying to make $Prod[\mathcal{D},Set]$ in to an algebraic category over something?

10. • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeAug 6th 2010
    • (edited Aug 6th 2010)
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex@ Andrew I think that you're phrasing the conjecture wrong. It should state that *unsorted* infinitary Lawvere theories correspond to monads on $Set$ (or monadic categories over $Set$). Then $S$-sorted infinitary Lawvere theories correspond to monads on $Set^S$, not on $Set$ at all. I'm not sure that many-sorted infinitary Lawvere theories correspond precisely to anything in this way. @ Mike The theorem that finitary Lawvere theories correspond to finitary monads on $Set$ requires that we preserve the generating object; that's what I was going on. If you're not going to preserve it, then I'm not sure why you wouldn't at the same time generalise to all small categories with finite products. (Maybe I should see what Lawvere does with that.)

    @ Andrew

    I think that you’re phrasing the conjecture wrong. It should state that unsorted infinitary Lawvere theories correspond to monads on $Set$ (or monadic categories over $Set$). Then $S$-sorted infinitary Lawvere theories correspond to monads on $Set^S$, not on $Set$ at all. I’m not sure that many-sorted infinitary Lawvere theories correspond precisely to anything in this way.

    @ Mike

    The theorem that finitary Lawvere theories correspond to finitary monads on $Set$ requires that we preserve the generating object; that’s what I was going on. If you’re not going to preserve it, then I’m not sure why you wouldn’t at the same time generalise to all small categories with finite products. (Maybe I should see what Lawvere does with that.)

11. • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeAug 6th 2010
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex@ Andrew again I see that you have written in the assumption that the assignment of sorts is injective. But I don't see where you actually use this. There are counterexamples. I think that the simplest is the theory of a [[subsingleton]], which has one type (so unsorted), no operations, and one equation ($x = y$). Here we have $R \cong R^n$ for all $n \geq 1$. (You can even get $R \cong R^n$ for all $n$ if you add a single $0$-ary operation to get the theory of a singleton.)

    @ Andrew again

    I see that you have written in the assumption that the assignment of sorts is injective. But I don’t see where you actually use this.

    There are counterexamples. I think that the simplest is the theory of a subsingleton, which has one type (so unsorted), no operations, and one equation ($x = y$). Here we have $R \cong R^n$ for all $n \geq 1$. (You can even get $R \cong R^n$ for all $n$ if you add a single $0$-ary operation to get the theory of a singleton.)

12. • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeAug 6th 2010
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexMaybe to avoid even suggesting that one might want to preserve the collection of sorts, we should *define* a many-sorted infinitary Lawvere theory to be any category $\mathcal{D}$ with all small products such that both $\mathcal{D}$ and $Prod[\mathcal{D},Set]$ are locally small. Having eliminated the sorts as such, the term ‘many-sorted’ is a bit odd here, but this is just the red herring principle; this is the *general* notion of infinitary Lawvere theory, living at the fully embodied level. Then it is a theorem that (for each small set $S$) the underlying category of each $S$-sorted infinitary Lawvere theory is a many-sorted infinitary Lawvere theory; and it is a conjecture that each many-sorted infinitary Lawvere theory is the underlying category of some $S$-sorted infinitary Lawvere theory (for some small set $S$), which hopefully we can prove in analogy with Freyd & Street.

    Maybe to avoid even suggesting that one might want to preserve the collection of sorts, we should define a many-sorted infinitary Lawvere theory to be any category $\mathcal{D}$ with all small products such that both $\mathcal{D}$ and $Prod[\mathcal{D},Set]$ are locally small. Having eliminated the sorts as such, the term ‘many-sorted’ is a bit odd here, but this is just the red herring principle; this is the general notion of infinitary Lawvere theory, living at the fully embodied level.

    Then it is a theorem that (for each small set $S$) the underlying category of each $S$-sorted infinitary Lawvere theory is a many-sorted infinitary Lawvere theory; and it is a conjecture that each many-sorted infinitary Lawvere theory is the underlying category of some $S$-sorted infinitary Lawvere theory (for some small set $S$), which hopefully we can prove in analogy with Freyd & Street.

13. • CommentRowNumber13.
    • CommentAuthorAndrew Stacey
    • CommentTimeAug 6th 2010
    • PermaLink
    Author: Andrew Stacey
    Format: MarkdownItexToby #10: I agree. Toby #11: I thought I might need that to be the case in order that the components in the underlying graded set be somehow independent. But today I decided that that wasn't necessary: if I take the category of, say, groups and decide that I'm going to think of it as 2-sorted, then I get a category over $Set^2$. If I take two sets, $X$ and $Y$, then I still get a free group on the pair $(X,Y)$, but because the two components have to be isomorphic[1], it's actually the free group on $X \coprod Y$. [1] For simplicity, I'm assuming that the 2 sorts could both generate the whole category in question. Okay, so we have: * multi-sorted infinitary Lawvere theory: category with small products such that there exists a small generating subcategory * (unsorted) infinitary Lawvere theory: category with small products such that there exists a generating object * $S$-sorted infinitary Lawvere theory: category with small products and a functor from $S$ whose image is a generating subcategory * $1$-sorted infinitary Lawvere theory: category with small products with an object which generates it Is that right?

    Toby #10: I agree.

    Toby #11: I thought I might need that to be the case in order that the components in the underlying graded set be somehow independent. But today I decided that that wasn’t necessary: if I take the category of, say, groups and decide that I’m going to think of it as 2-sorted, then I get a category over $Set^2$. If I take two sets, $X$ and $Y$, then I still get a free group on the pair $(X,Y)$, but because the two components have to be isomorphic[1], it’s actually the free group on $X \coprod Y$.

    [1] For simplicity, I’m assuming that the 2 sorts could both generate the whole category in question.

    Okay, so we have:

    • multi-sorted infinitary Lawvere theory: category with small products such that there exists a small generating subcategory
    • (unsorted) infinitary Lawvere theory: category with small products such that there exists a generating object
    • $S$-sorted infinitary Lawvere theory: category with small products and a functor from $S$ whose image is a generating subcategory
    • $1$-sorted infinitary Lawvere theory: category with small products with an object which generates it

    Is that right?

14. • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeAug 6th 2010
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexRight, with two caveats: 1. I would like to prove that a category $\mathcal{D}$ with small products has a small generating subcategory whenever both $\mathcal{D}$ and $Prod[\mathcal{D},Set]$ are locally small. The converse holds, so this would give another definition of (1). Right now I'm pessimistic, since Freyd & Street could not prove an analogous result about sites (and their argument, which I now understand, does not obviously generalise). 2. I don't really see the point of this item, as distinct from (4), although presumably Lawvere saw some point to it (in the finitary case). In particular, (4) is the thing that corresponds to a monad on $Set$, not (2). 3. No caveat here! 4. See (2). (I have implicitly numbered your unnumbered list above.) Also, we should be careful using the word ‘generate’ here, since we're not talking about a [[generating set]]. It's OK here, where we all know what we mean, but we should avoid it on the Lab itself. I will try to say ‘span’ (the verb) instead.

    Right, with two caveats:

    1. I would like to prove that a category $\mathcal{D}$ with small products has a small generating subcategory whenever both $\mathcal{D}$ and $Prod[\mathcal{D},Set]$ are locally small. The converse holds, so this would give another definition of (1). Right now I’m pessimistic, since Freyd & Street could not prove an analogous result about sites (and their argument, which I now understand, does not obviously generalise).
    2. I don’t really see the point of this item, as distinct from (4), although presumably Lawvere saw some point to it (in the finitary case). In particular, (4) is the thing that corresponds to a monad on $Set$, not (2).
    3. No caveat here!
    4. See (2).

    (I have implicitly numbered your unnumbered list above.)

    Also, we should be careful using the word ‘generate’ here, since we’re not talking about a generating set. It’s OK here, where we all know what we mean, but we should avoid it on the Lab itself. I will try to say ‘span’ (the verb) instead.

15. • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeAug 7th 2010
    • (edited Aug 7th 2010)
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex@ Mike re the category of free groups Once you say that a group is free on $3$ generators, what more is there to say about such a group? It is not only determined up to isomorphism, but up to *unique* isomorphism, the unique isomorphism that fixes each generator. So while one can certainly talk about arbitrary group endomorphisms (or arbitrary endo-functions, for that matter) of this group, I would not think of these as morphisms normally. Actually, free groups are a little *too* trivial here; let's consider finitely generated groups instead. Being finitely generated is a size condition, like the size condition that we wish to impose on many-sorted infinitary Lawvere theories, that makes reference to a generating family. In both cases, the question is whether the morphisms pay attention to which generating family is chosen. Again, I would take as morphisms between groups generated by $3$ generators are the group homomorphisms that preserve the generators. (Such a morphism is again unique if it exists, but it may not exist. So really I am looking at the poset of quotient groups of the free group on $3$ generators.) Again, one can look at arbitrary group homomorphisms, or even arbitrary functions, between them, but I wouldn't think of these as morphisms normally. But for arbitrary finitely generated groups, I think that I would want the morphisms to really be all group homomorphisms. Even if I restrict to homomorphisms that map generators to generators, this is still more general than homomorphisms that fix generators (which doesn't even make sense in this context).

    @ Mike re the category of free groups

    Once you say that a group is free on $3$ generators, what more is there to say about such a group? It is not only determined up to isomorphism, but up to unique isomorphism, the unique isomorphism that fixes each generator. So while one can certainly talk about arbitrary group endomorphisms (or arbitrary endo-functions, for that matter) of this group, I would not think of these as morphisms normally.

    Actually, free groups are a little too trivial here; let’s consider finitely generated groups instead. Being finitely generated is a size condition, like the size condition that we wish to impose on many-sorted infinitary Lawvere theories, that makes reference to a generating family. In both cases, the question is whether the morphisms pay attention to which generating family is chosen.

    Again, I would take as morphisms between groups generated by $3$ generators are the group homomorphisms that preserve the generators. (Such a morphism is again unique if it exists, but it may not exist. So really I am looking at the poset of quotient groups of the free group on $3$ generators.) Again, one can look at arbitrary group homomorphisms, or even arbitrary functions, between them, but I wouldn’t think of these as morphisms normally.

    But for arbitrary finitely generated groups, I think that I would want the morphisms to really be all group homomorphisms. Even if I restrict to homomorphisms that map generators to generators, this is still more general than homomorphisms that fix generators (which doesn’t even make sense in this context).