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 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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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.
    • CommentAuthormaxsnew
    • CommentTimeAug 24th 2022

    Init fixed point operator

    v1, current

    • CommentRowNumber2.
    • CommentAuthormaxsnew
    • CommentTimeAug 24th 2022

    A definition (perhaps novel but obvious) that works in a cartesian multicategory

    v1, current

    • CommentRowNumber3.
    • CommentAuthormaxsnew
    • CommentTimeAug 24th 2022

    I’m very curious if it’s possible to define a similar version of traced monoidal category that works in an arbitrary (symmetric?) multicategory.

    • CommentRowNumber4.
    • CommentAuthorSam Staton
    • CommentTimeAug 25th 2022

    Added reference to iteration theory.

    diff, v2, current

    • CommentRowNumber5.
    • CommentAuthorSam Staton
    • CommentTimeAug 25th 2022

    Correction: we know a fixed point operator on a Lawvere theory is the same thing as a Conway theory. (Hmm. Maybe Max, your fixed point operator for a one-object cartesian multicategory isn’t the same as a fixed point operator on the corresponding Lawvere theory regarded as a category with products. i.e. maybe a fixed point operator on a cartesian multicategory isn’t as strong as a fixed point operator on the corresponding cartesian category. Unsure about how to deal with mutually recursive definitions. Didn’t think about it for very long though and may have missed a trick.)

    diff, v2, current

    • CommentRowNumber6.
    • CommentAuthormaxsnew
    • CommentTimeAug 25th 2022

    I missed that page, these should probably be merged into one.

    As to mutual vs single fixed points, it’s a good question. The definition I took is from Simpson and Plotkin and I simply noticed that the definition made sense in an arbitrary cartesian multicategory. What I overlooked though is that of course because they were working with a cartesian category, they were really defining all mutual fixed points as well, so my definition isn’t clearly equivalent to theirs.

    However, I thought mutual fixed points wouldn’t be needed, because (1) you can define them by Bekič’s construction, and (2) Simpson and Plotkin show that in a cartesian category the version of the axioms I gave satisfies “Bekič’s property”, i.e., that a fixed point of a product can be defined as a nested fixed point.

    I have a sketch on the board that this proof works for my multicategory axioms, so if the multicategory is representable, then a fixed point of a product is equal to a nested fixed point. I’ll need to think to figure out whether or not I can extend that argument to the equivalence with Conway operators.

    • CommentRowNumber7.
    • CommentAuthormaxsnew
    • CommentTimeAug 25th 2022

    Update: I looked at this morning and it got a little too gnarly for me. If we call my definition a multi-FPO, then I am fairly convinced that multi-FPO on a representable cartesian multicategory MM is equivalent to trace on MM as a cartesian monoidal category.

    What I am not totally convinced of is that a multi-FPO on MM is the same thing as a (multi-sorted) Conway operator, which is equivalent to a trace on Ctx(M)Ctx(M). Maybe there’s some abstract argument (I pray) but I don’t see one. You can define the data of a Conway operator by induction on the length of the context, but the equations for dinaturality/diagonal lemma got too gnarly for me to justify figuring out when I don’t have a strong reason.

    • CommentRowNumber8.
    • CommentAuthorSam Staton
    • CommentTimeAug 28th 2022
    Thanks! Would be interesting to somehow understand, but I agree it's often very fiddly.
    • CommentRowNumber9.
    • CommentAuthormaxsnew
    • CommentTimeSep 29th 2022

    X-refererences

    diff, v3, current