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.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 26th 2012

    I can understand the operation of unfolding an entity in terms of coalgebra. E.g., for the endofunctor on Set, F(X) = 1 + X, I can unfold a potentially infinite stream of 1s, writing ’stop’ and ending, or ’1’ and taking the predecessor.

    Can I think of unfolding a connected topological space into its Postnikov system in a similar way?

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeMar 26th 2012
    • (edited Mar 26th 2012)

    I am not sure if we can get this from a single endofunctor. But the Postnikov tower of an object XX

    τ 3Xτ 2Xτ 1Xτ 0X \cdots \to \tau_3 X \to \tau_2 X \to \tau_1 X \to \tau_0 X

    comes from a tower of endofunctors

    Hτ 3Hτ 2Hτ 1Hτ 0H, \cdots \mathbf{H} \stackrel{\tau_3}{\to} \mathbf{H} \stackrel{\tau_2}{\to} \mathbf{H} \stackrel{\tau_1}{\to} \mathbf{H} \stackrel{\tau_0}{\to} \mathbf{H} \,,

    where H\mathbf{H} is the ambient \infty-topos and where τ n\tau_n is the n-truncation \infty-functors.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeMar 26th 2012

    I think a closer analogy would be to the coinductive definition of an \infty-category: a set together with hom-\infty-categories and composition. Each unfolding peels off one layer of structure “at the bottom” (first the objects, then the 1-morphisms, then the 2-morphisms, etc.).

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeMar 26th 2012

    That seems to give the skeletal filtration instead of the coskeletal/Postnikov tower.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeMar 26th 2012

    That’s true! But it still seems to me to be closer to what David was asking, because the functor F in F(X)=1+X is not the “operation of unfolding”, but rather that which defines the structure under consideration (here, \infty-groupoids) as a coinductive object.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMar 26th 2012

    That reminds me of something related (or maybe not so related, I am not sure) that I wanted to ask you:

    I seem to remember that a while back you said something like: it’s unclear how to define internal categories in HTT in, notably, the complete Segal space style, because it requires coding an infinite amount of data. Right?

    Is that really so? Even outside HTT, in practice we never “code” an infinite amount of data, because we never can. While there is a countable number of objects/types involved in an internal Segal-style category, we never define one by listing these explicitly one-by-one. Instead, we always fall back to some finite algorithm that would produce one.

    But even before coding examples, could you remind me what the problem is, if any, of coding the definition ? I would imagine we start with an \mathbb{N}-dependent type (of morphisms), then have some ×\mathbb{N} \times \mathbb{N}-dependent type of maps (simplicial structure) maps, and so forth.

    Where does one run into problems?

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeMar 26th 2012

    The problem is that the “and so forth” stands for an infinite list of things (higher homotopy coherence of the simplicial structure maps).

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2012

    stands for an infinite list of things

    But it just says: for all nn \in \mathbb{N}, a certain morphism is weak equivalence. A can’t see why this could not be coded. It’s just some condition parametrized over the type \mathbb{N}.

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 27th 2012

    Thanks, Urs and Mike. I had the suspicion that the closest analogy would be to the coinductive Trimble ω\omega-category construction, but wondered if we could peel things off the other way. So there’s no hope of defining truncation in terms of a single endofunctor.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMar 27th 2012

    @Urs, I must not understand what you meant by

    I would imagine we start with an \mathbb{N}-dependent type (of morphisms), then have some ×\mathbb{N}\times\mathbb{N}-dependent type of maps (simplicial structure) maps

    Actually, what is it you are trying to define? I thought you were describing a simplicial object (so I assumed that by “morphisms” you meant “objects”).

    @David, I probably wouldn’t put it so strongly as “no hope”, but it seems that right now, we don’t know how to do it. (-:

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2012

    Mike,

    yes, a simplicial object satisfiying the Segal condition. Why can’t this be coded in Coq?

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeMar 27th 2012

    The problem is not the Segal condition, the problem is the “simplicial object”. The Segal condition says “for all n, a certain morphism is an equivalence” — probably no problem with that. But please tell me how you plan to encode a simplicial object?

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2012
    • (edited Mar 27th 2012)

    But please tell me how you plan to encode a simplicial object?

    "Plan" is a good word. Here is one plan:

    first I imagine I’d encode the easy bit: the notion of simplicial 0-truncated objects (all whose components are 0-truncated). I hear this has been done already, with the aim of building models for HoTT inside HoTT. (Maybe I should assume for this that there is a subcategory of discrete objects? Of course I’d be happy with making that assumption.) Similarly I’d define globular 0-truncated objects and, using Street’s combinatorics, the globular nerve operation, all on these degreewise 0-truncated structures.

    Then I imagine that I can get hold of the simplicial 0-truncated object which is the nerve of Δ\Delta, as well as of its globularization N G(Δ)N_G(\Delta).

    Then I’d imaging that I can say that a simplicial object is

    • For every term vN G(Δ) 0 v \in N_G(\Delta)_0 a type X vX_v.

    • For all nn \in \mathbb{N} and every term σN G(Δ) n+1\sigma \in N_G(\Delta)_{n+1}, a term in Id n(source 0(σ)target 0(σ))Id^{n} (source_0(\sigma) \to target_0(\sigma)) (the nn-fold identity type on the function type between the 0-source type of σ\sigma and the 0-target type of σ\sigma).

    • Together with a choice of the relevant equivalences.

    So, in summary: I first say "simplicial 0-truncated object", which should be straightforward since we may indeed speak of simplicial identities in this case. Then I’d define a specific simplicial 0-truncated object and use that now as a blueprint from which to read off, degree by degree, the "infinite amount of coherence data".

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMar 27th 2012

    Where did you hear that simplicial 0-truncated objects have been done? I agree that it should not be as hard (in fact, I’ve been working on something similar).

    I think the problem then with your plan is saying what you mean precisely by “nn-fold identity type” and/or “relevant equivalences” (depending on how you partition up the important information between those two things). I don’t know how to convince you that this is hard other than by saying “try to do it!”

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2012

    Where did you hear that simplicial 0-truncated objects have been done?

    Over coffee, from a colleague who is in contact with the person who supposedly did it. I’ll get back to you tomorrow with details.

    • CommentRowNumber16.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 28th 2012

    Mike and I had a little discussion on the cafe about trying to construct simplicial objects, but I can’t find it. I suggested using the decalage, I think, but it didn’t go anywhere (or I didn’t think about it long enough, most likely the former).

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMar 28th 2012

    I suggested using the decalage,

    To accoumplish what?

    • CommentRowNumber18.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 28th 2012
    • (edited Mar 28th 2012)

    To define simplicial objects in Coq. I should say, use the decalage, truncated simplicial objects and maps of truncated simplicial objects so we define simplicial objects and the map from the decalage jointly. Unfortunately my google-foo and n-category-cafe-searching-foo have let me down.

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeMar 28th 2012

    fu?

    • CommentRowNumber20.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 29th 2012
    • (edited Mar 29th 2012)

    …if you like….

    And here’s me thinking you’d found the discussion.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeMar 29th 2012

    Was that not the discussion you were thinking of?

    • CommentRowNumber22.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 29th 2012

    Sorry, I didn’t see the link because I was using my phone on the bus. I thought it was a linguistic comment on my post. That is exactly the one, thanks!

    @Urs - I hope you can make something of my idea, or perhaps a completely different approach is needed, say along the lines you mentioned (0-truncated objects etc).

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeMar 29th 2012
    • (edited Mar 29th 2012)

    I hope you can make something of my idea,

    A coinductive definition as Mike and maybe you (not sure if I understood yet!) allude to would probably be way more elegant than what I was sketching. I am not so much interested in picking an implementation, since I won’t do it any time soon anyway!

    I was more interested in understanding if in principle there is any obstacle to formulating categories internal to Coq, an obstacle due to the definition involving “an infinite amount” of information. It would seem to me that also outside of Coq we can never make a definition that genuinely involves an infinite amount of data. If it looks as if we do, then always because some finite algorithms for producing that data are secretly understood in the background, maybe so secretly that we don’t notice it anymore.

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeMar 29th 2012

    Urs, I agree that we never actually write down an infinite amount of data (obviously, we only have finite paper…). I see that I should have been more specific about the problem. The problem is that in formalizing an infinite amount of coherence data in a “homotopically coherent diagram” (or any homotopically coherent structure), it seems as though we need to use some notion of strict identity. E.g. the source of the associator constraint has to be f(gh)f \circ (g\circ h). We could ask it to only be isomorphic/equivalent, but then that isomorphism/equivalence has to have an exactly specified source and target, etc.

    We had a discussion about this sort of thing a while ago at evil, with the point being made that we can make do with type dependency as a replacement for a notion of strict identity. That is, rather than saying that “the source of the associator is f(gh)f\circ (g\circ h) and its target is (fg)h(f\circ g)\circ h”, which regarded as a statement involves strict equality, we give the associator the dependent type Hom(f(gh),(fg)h)Hom(f\circ (g\circ h), (f\circ g)\circ h). In principle, and in informal mathematics, this works great. However, when formalizing in type theory, we don’t have fully general language to talk internally about type dependency.

    For instance, type theory cannot formalize the statement “the map ff is a fibration (i.e. display map, dependent type)”. We can say “let f:ABf\colon A\to B be a fibration” by way of introducing the variable ff and the type AA (by translating it into “let F:BTypeF\colon B\to Type be a dependent type”) but not assert that some already-known map is a fibration. A natural numbers type allows us to talk about “an infinite family of objects” {X n} nN\{X_n\}_{n\in N} as an NN-indexed type X:NTypeX\colon N\to Type, and a family of morphisms f n:X n+1X nf_{n}\colon X_{n+1} \to X_{n} as a dependent function f:n:N,X(n+1)X(n)f\colon \forall n\colon N, X(n+1) \to X(n). But there is no obvious way to talk about an infinite tower of fibrations

    X n+1X nX 0 \dots \twoheadrightarrow X_{n+1}\twoheadrightarrow X_n \twoheadrightarrow \dots \twoheadrightarrow X_0

    This is where the drive to coinduction comes from, because there is a way to formalize such a thing coinductively:

    CoInductive tower : Type :=
    | lift : forall X0 : Type, (X0 -> tower) -> tower.
    

    But for more complicated infinite structures involving fibrations, there’s no general formula for how to coinductivify them that I know of.

    Does that help at all? I wouldn’t say that there is an “in principle obstacle” in the sense of an argument that it can’t be done, but I think this is an “in principle” reason why it is difficult, and why no one has done it yet. (-: