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.
    • CommentAuthorbgavran
    • CommentTimeDec 19th 2023

    About a year ago I created a github repository listing some notable endofunctors and their initial algebras and terminal coalgebras, as I couldn’t find anything like this already. This helped me get a better understanding of the landscape of these concepts.

    I decided to put that list in a more prominent place, and encourage edits.

    v1, current

    • CommentRowNumber2.
    • CommentAuthorbgavran
    • CommentTimeDec 19th 2023

    I want to mention that this is a compendium over a few twitter threads (https://twitter.com/bgavran3/status/1513217904191410190), and there might be slight errors, or inaccuracies. At this point my only goal was to get it on nLab, so these can be ironed out.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeDec 19th 2023

    Just to mention that David Corfield and myself have added more hyperlinks to the keywords in the entry. There is room to add yet more e.g. for binary tree, list, and Moore machine. With these added, maybe the rightmost column of the table is superfluous and could be deleted to save space.

    If the entry is meant to remain a bare table, then I would be inclined to not have it as a stand-alone entry but to eventually !include it into the Examples-section at initial algebra of an endofunctor and terminal coalgebra of an endofunctor, so that it becomes part of these entries.

    • CommentRowNumber4.
    • CommentAuthorbgavran
    • CommentTimeDec 22nd 2023

    Just to mention that David Corfield and myself have added more hyperlinks to the keywords in the entry. There is room to add yet more e.g. for binary tree, list, and Moore machine. With these added, maybe the rightmost column of the table is superfluous and could be deleted to save space.

    Thanks. I agree with the hypothesis. Perhaps we can see how the page evolves.

    If the entry is meant to remain a bare table, then I would be inclined to not have it as a stand-alone entry but to eventually !include it into the Examples-section at initial algebra of an endofunctor and terminal coalgebra of an endofunctor, so that it becomes part of these entries.

    I understand. The goal was to have a side-by-side comparison of initial-vs-terminal, which is the reason why I did not put the table in the examples section of either page.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeDec 22nd 2023

    The goal was to have a side-by-side comparison

    Yes. All the more would it be worthwhile to include the table into these entries.

    No worries, I can do this.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeDec 22nd 2023
    • (edited Dec 22nd 2023)

    Maybe to clarify: This would mean your entry here remains a separate page just as it is, but that we use the !include-command to have it display inside these other entries, too.

    The only prerequisite for this is that you keep it a bare table as it is at the moment, without adding much page-infrastructure to it (which apparently you don’t intend to add anyways), which was my question in #3 (“If the entry is meant to remain a bare table,…”)

  1. As defined in the stream article on the nLab, streams are the terminal coalgebra of the functor X1+A×XX \mapsto 1 + A \times X, not the functor XA×XX \mapsto A \times X. So streams belong in the same row as lists

    Robert Fain

    diff, v18, current

  2. Rather, there is already a example of XX+XX \mapsto X + X, which is the same as the endofunctor X2×XX \mapsto 2 \times X where 22 is the finite set with two elements, and has initial algebra \emptyset and terminal algebra 2 2^\mathbb{N} according to this list. If this entry on this list are correct, then generalizing from 22 to any set AA, the terminal coalgebra of the endofunctor XA×XX \mapsto A \times X is the sequence set A A^\mathbb{N}.

    Robert Fain

    diff, v20, current

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 23rd 2023

    I put in \emptyset in the entry beginning “linearly ordered sets”, because that’s clearly correct (one checks initiality directly).

    diff, v21, current

    • CommentRowNumber10.
    • CommentAuthorbgavran
    • CommentTimeDec 24th 2023
    • (edited Dec 24th 2023)

    Maybe to clarify: This would mean your entry here remains a separate page just as it is, but that we use the !include-command to have it display inside these other entries, too. The only prerequisite for this is that you keep it a bare table as it is at the moment, without adding much page-infrastructure to it (which apparently you don’t intend to add anyways), which was my question in #3 (“If the entry is meant to remain a bare table,…”)

    I see. That aligns with my plans; I wasn’t planning anything more than a bare table.

    As defined in the stream article on the nLab, streams are the terminal coalgebra of the functor X↦1+A×X, not the functor X↦A×X. So streams belong in the same row as lists

    I’ve never checked the definition of stream on nLab, but it does not agree with what I learned to be a stream from functional programming (specifically, Idris, though I believe there are more easily found resources), which that it’s a productive function, i.e. one which will never terminate.

    (So I believe I think we agree that there is a distinction to be made between a potentially infinite list (i.e. one which could terminate) given by the functor X ↦ 1 + A x X and an infinite “list” (I call that streams, but not sure what’s a good name otherwise) (i.e. one which always goes on forever) given by the functor X↦A×X, it’s just a matter of naming them)

    • CommentRowNumber11.
    • CommentAuthorMadeleine Birchfield
    • CommentTimeDec 24th 2023
    • (edited Dec 24th 2023)

    The nLab’s current definition of stream comes from Toby Bartels in 2011, who had a habit of writing definitions without referencing the existing literature. In many cases the already existing definition in the literature is different from Bartels’s definition, so it might be the case that streams are indeed defined as the final coalgebra of the action monad.

  3. In Agda, streams are defined as:

    record Stream (A : Set) : Set where

    \quadcoinductive

    \quadfield

    \qquadhd : A

    \qquadtl : Stream A

    https://agda.readthedocs.io/en/latest/language/coinduction.html

    • CommentRowNumber13.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 24th 2023
    • (edited Dec 24th 2023)

    My memory accords with bgravan’s and (I take it) Madeleine’s. If I were tasked with naming the elements of the terminal coalgebra of X1+A×XX \mapsto 1 + A \times X (or of XB+A×XX \mapsto B + A \times X), I might call them “behaviors” – but there’s a good chance that term is already taken.

  4. putting streams in the right row in the list

    Thomas Wilson

    diff, v27, current

  5. For the endofunctor X1+A×XX \mapsto 1 + A \times X, in place of stream I put “cofree coalgebra of AA” and linked to cofree coalgebra.

    Thomas Wilson

    diff, v27, current

    • CommentRowNumber16.
    • CommentAuthorMadeleine Birchfield
    • CommentTimeDec 24th 2023
    • (edited Dec 24th 2023)

    (I take it) Madeleine’s

    I don’t really know myself, since I don’t work in the subfields of mathematics which use the word “stream”, however defined. For me, A A^\mathbb{N} is just the set of (infinite) sequences in AA, and I don’t encounter the other kind of stream in the wild so I have no need to use it.

    But Toby Bartels has introduced other usages of mathematical terminology in the nLab which do not really correspond to the usage elsewhere in the world (cf. linear order - which are reflexive elsewhere but irreflexive in the nLab).

    It is likely, judging by the reaction of Hurkyl and other nLab members here and in https://nforum.ncatlab.org/discussion/17572/stream/#Item_0, that both definitions are used in different areas of mathematics - which probably warrants turning stream into a disambiguation page of some sort or mentioning both definitions in the article.

    This would make stream similar to setoid, which for the longest time on the nLab was defined by Toby Bartels as a set equipped with an pseudo-equivalence relation, but is also used to refer to a set equipped with an equivalence relation - and both definitions are used in the literature.

    • CommentRowNumber17.
    • CommentAuthorHurkyl
    • CommentTimeDec 24th 2023
    • (edited Dec 24th 2023)

    My familiarity with streams comes more from the applied than theoretical context (i.e. when I’m acting as a programmer rather than as a mathematician). I’m sure I’ve seen it in mathematical contexts too, but I don’t really recall where; I can only comment that when I read “coalgebra for 1+A×X1 + A \times X” my reaction is that’s obviously right, and “coalgebra for A×XA \times X” my reaction is that’s obviously wrong.

    (The main point of this caveat is that the nLab might have been the context where I encountered it. I’m pretty sure it’s not the only place, but I can’t say so definitively)

    The main connotation of a stream is that it’s a sequence of data, but the actual data type need not actually store the data. Instead, it provides an interface letting you progress through the sequence, and it will obtain/generate more data as needed, or signal that you’ve reached the end of the stream.

    While the typical application is I/O of some sort, it is also one way to provide access to an infinite sequence of data. So, given my understanding, I don’t find it surprising that someone would decide to call an infinite sequence data type a “stream”.

    I will note that the code in the Agda reference page linked above has a comment noting that Stream is a type representing infinite streams (emphasis mine). So, I do think the author of that page had the similar understanding that streams can be finite sequences as well.

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 24th 2023

    Regarding the question mark in the entry for the endofunctor XIXX \mapsto I \sqcup X on a closed symmetric monoidal category: I doubt one can can give a snappy uniform description for all cases, and so it’s unclear what should be put in the table. But (assuming for simplicity that the underlying category EE is complete): whenever the coproduct functor preserves limits of inverse ω\omega-chains, for example when the coproduct +:E×EE+: E \times E \to E preserves connected limits, which is the case for example on any extensive category EE, then also ()+A:EE(-) + A: E \to E preserves inverse limit of ω\omega-chains for any object AA, and so by Adamek’s theorem, the terminal coalgebra of ()+A(-) + A will, as an object of EE, be the inverse limit of the diagram

    1+nA1+(n1)A1+A!1\ldots \to 1 + n \cdot A \to 1 + (n-1) \cdot A \to \ldots \to 1 + A \stackrel{!}{\to} 1

    where the map f n:1+(n+1)A1+nAf_n: 1 + (n+1) \cdot A \to 1 + n \cdot A for n>0n \gt 0 is f n1+Af_{n-1} + A. For E=SetE = Set, you can think of the inverse limit as 1+A1 + \mathbb{N} \cdot A. In this case E=SetE = Set, given a coalgebra (X,β:XA+X)(X, \beta: X \to A + X), the coalgebra map f:X1+Af: X \to 1 + \mathbb{N} \cdot A sends xXx \in X to (n,a)(n, a) when the iterate β n(x)\beta^n(x) [viewing β\beta as given by a partial map XXX \to X together with a partial map XAX \to A] is defined in XX but β n+1(x)=aA\beta^{n+1}(x) = a \in A, and sends xx to the point *1\ast \in 1 if β n(x)\beta^n(x) is defined in XX for all nn \in \mathbb{N}.

    I expect the same description can be formulated and holds if EE is infinitary extensive, but I’ve not examined this carefully. (Meanwhile, the inverse limit description should hold in considerable generality even outside the extensive context, but by no means in absolute generality.)

    None of this has anything really to do with closed symmetric monoidal structure mentioned in the entry.

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeJan 3rd 2024

    I have adjusted the lead-in sentence to work within any ambient entry

    and then, as discussed in #3 and following, I have !include-ed this list of examples into the Examples-sections at initial algebra of an endofunctor and terminal coalgebra for an endofunctor

    diff, v31, current