Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite 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 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTobyBartels
    • CommentTimeAug 4th 2010
    • CommentRowNumber2.
    • CommentAuthorAndrew Stacey
    • CommentTimeAug 5th 2010

    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 SS-sorted theory, should the functor S𝒟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 22-sorted theory.
    3. Still on SS-sorted theories, there seemed to be a bit missing: the image of SS 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.
    • CommentRowNumber3.
    • CommentAuthorAndrew Stacey
    • CommentTimeAug 5th 2010

    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?

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeAug 6th 2010
    1. I think definitely equipped with. Already in an unsorted Lawvere therory, you want to know which object is RR.
    2. You can always make S𝒟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𝒟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.
    • CommentRowNumber5.
    • CommentAuthorAndrew Stacey
    • CommentTimeAug 6th 2010

    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.

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeAug 6th 2010

    It occurs to me that, while an SS-sorted theory should be equipped with an SS-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 SS-sorted Lawvere theories must preserve the SS sorts, while an equivalence of many-sorted Lawvere theories might not.

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

    • CommentRowNumber7.
    • CommentAuthorAndrew Stacey
    • CommentTimeAug 6th 2010

    I mostly agree with you. What I hesitate about is the forgetful functor from Prod[𝒟,Set]Prod[\mathcal{D},Set]. Where should it land up? At the moment, I have it landing in [S,Set][S,Set], but that relies on a choice of SS. 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[𝒟,Set]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.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeAug 6th 2010

    @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.

    • CommentRowNumber9.
    • CommentAuthorAndrew Stacey
    • CommentTimeAug 6th 2010

    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[𝒟,Set]Prod[\mathcal{D},Set] in to an algebraic category over something?

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeAug 6th 2010
    • (edited Aug 6th 2010)

    @ Andrew

    I think that you’re phrasing the conjecture wrong. It should state that unsorted infinitary Lawvere theories correspond to monads on SetSet (or monadic categories over SetSet). Then SS-sorted infinitary Lawvere theories correspond to monads on Set SSet^S, not on SetSet 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 SetSet 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.)

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeAug 6th 2010

    @ 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=yx = y). Here we have RR nR \cong R^n for all n1n \geq 1. (You can even get RR nR \cong R^n for all nn if you add a single 00-ary operation to get the theory of a singleton.)

    • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeAug 6th 2010

    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[𝒟,Set]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 SS) the underlying category of each SS-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 SS-sorted infinitary Lawvere theory (for some small set SS), which hopefully we can prove in analogy with Freyd & Street.

    • CommentRowNumber13.
    • CommentAuthorAndrew Stacey
    • CommentTimeAug 6th 2010

    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 2Set^2. If I take two sets, XX and YY, then I still get a free group on the pair (X,Y)(X,Y), but because the two components have to be isomorphic[1], it’s actually the free group on XYX \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
    • SS-sorted infinitary Lawvere theory: category with small products and a functor from SS whose image is a generating subcategory
    • 11-sorted infinitary Lawvere theory: category with small products with an object which generates it

    Is that right?

    • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeAug 6th 2010

    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[𝒟,Set]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 SetSet, 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.

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeAug 7th 2010
    • (edited Aug 7th 2010)

    @ Mike re the category of free groups

    Once you say that a group is free on 33 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 33 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 33 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).