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

nLab > Latest Changes: free coproduct completion

Bottom of Page

1 to 20 of 20

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeOct 12th 2021

    some bare minimum on the free coproduct cocompletion.

    The term used to redirect to the entry free cartesian category, where however the simple idea of free coproduct completion wasn’t really brought out.

    v1, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeOct 12th 2021
    • (edited Oct 12th 2021)

    added (here) the example of GSetG Set as the free coproduct completion of GOrbtG Orbt.

    v1, current

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeOct 12th 2021

    added (here) statement of Lemma 42 in:

    v1, current

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeMay 13th 2023

    added a paragraph (here) making explicit that the free coproduct completion on 𝒞\mathcal{C} is also equivalently the Grothendieck construction ∫ S∈Set∏s∈S𝒞\int_{S \in Set} \, \underset{s \in S}{\prod} \mathcal{C}.

    diff, v6, current

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeMay 13th 2023

    added pointer to

    • Jean Bénabou, §3 in: Fibered Categories and the Foundations of Naive Category Theory, The Journal of Symbolic Logic, Vol. 50 1 (1985) 10-37 [doi:10.2307/2273784]

    with a remark that this paragraph essentially describes the perspective as a Grothendieck-construction (without however using that or any related terminology).

    diff, v6, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMay 13th 2023

    added (here) an example spelling out how the coproduct completion of a category that is already extensive to start with is equivalently that of bundles over sets in that category.

    diff, v6, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeMay 13th 2023

    added (here) mentioning of the example of the 1-category of skeletal groupoids as the free coproduct completion of that of groups (or their delooping groupoids).

    diff, v6, current

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMay 13th 2023
    • (edited May 13th 2023)

    added pointer to:

    and (here) their statement that the free coproduct completion of an accessible category is itself accessible

    diff, v7, current

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeMay 13th 2023
    • (edited May 13th 2023)

    added this to the list of References:

    As categorical semantics for dependent linear type theories (in the context of quantum programming languages with “dynamic lifting”, such as proto-Quipper), the free coproduct completion of symmetric closed monoidal categories is considered in

    and its followups.

    diff, v7, current

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeMay 13th 2023

    Just for completeness, I made explicit the proof of the first quoted proposition (here),

    diff, v8, current

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeMay 22nd 2023

    added statement and dicussion (here) that the free coproduct completion of a category with products itself has products which distribute over the coproduct

    diff, v9, current

    • CommentRowNumber12.
    • CommentAuthorvarkor
    • CommentTimeMay 22nd 2023

    Mention the relation with distributive categories.

    diff, v10, current

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 22nd 2023
    • (edited May 22nd 2023)

    Thanks!

    Can we substantiate this remark (I gave it a numbered environment, here), by pointing to a proof?

    diff, v11, current

    • CommentRowNumber14.
    • CommentAuthorvarkor
    • CommentTimeMay 22nd 2023

    I’m sure it must appear explicitly somewhere in the literature – I’ll try to have a look later – but it’s implicit in Corollary 5.9 of Cockett’s Introduction to distributive categories.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeMay 22nd 2023

    Let me see if I am following.

    That corollary 5.9 seems to state that:

    If A is cartesian, the free distributive completion is 𝒮//A *\mathcal{S}//A^\ast.

    and you are claiming that this contains implicitly your statement that

    the 2-monad for free product completion distributes over the 2-monad for free coproduct cocompletion

    ?

    • CommentRowNumber16.
    • CommentAuthorvarkor
    • CommentTimeMay 22nd 2023

    Yes: there are a few more details that would need to be checked, but this statement suggests that the free product completion 2-monad lifts to the 2-category of algebras for the free coproduct cocompletion 2-monad, which is equivalent to having a distributive law. (The remaining details to check is that the multiplication and unit of the free product completion 2-monad also lift.)

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMay 23rd 2023

    The statement sounds plausible and might not be hard to prove (though just stating/unwinding the definition of distributivity of 2-monads is a mouthful!) but if we have neither proof nor reference at the moment, then we must not state it as if we did.

    So I have adjusted the wording accordingly (here). But if this motivates you to sit down and type out the proof into some nLab entry, I’d be more than happy to re-word again!

    diff, v12, current

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 23rd 2023

    All this is closely related to the huge bulk of work surrounding polynomial functors, e.g., the category of polynomial endofunctors on SetSet is equivalent to the free distributive category on one object. This might suggest pathways through the literature to get back to original sources.

    I might have a crack at a direct proof myself. Not necessarily getting into the details of distributive laws on 2-monads (I imagine some Australian has already written out the connection between composite 2-monads and 2-distributive laws – something to look up), but just observing directly that for locally small CC, letting Prod(C)=Coprod(C op) opProd(C) = Coprod(C^{op})^{op} be the small product completion, that the canonical inclusions C↪Prod(C)↪Coprod(Prod(C))C \hookrightarrow Prod(C) \hookrightarrow Coprod(Prod(C)) induce equivalences

    DistCat(Coprod(Prod(C)),D)→ProdCat(Prod(C),D)→Cat(C,D)DistCat(Coprod(Prod(C)), D) \to ProdCat(Prod(C), D) \to Cat(C, D)

    which is to say that Coprod(Prod(C))Coprod(Prod(C)) is the free distributive category on CC [I believe Urs has already written out the proof of a claim whose corollary is that Coprod(Prod(C))Coprod(Prod(C)) is in fact a distributive category].

    • CommentRowNumber19.
    • CommentAuthorBryceClarke
    • CommentTimeMay 31st 2024

    Added a reference to a paper which considers algebras in the free coproduct completion.

    diff, v19, current

    • CommentRowNumber20.
    • CommentAuthorvarkor
    • CommentTimeAug 1st 2024

    Added a description of the Fam construction as a comma category.

    diff, v21, current

1 to 20 of 20

  1.