Not signed in (Sign In)

Start a new discussion

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 bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics 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 foundations functional-analysis functor galois-theory 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 lie-theory limit limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal modal-logic model model-category-theory monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number 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 string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory 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.
    • CommentAuthorUrs
    • CommentTimeDec 9th 2011

    I have added to continuum a paragraph titled In cohesive homotopy type theory.

    This is a simple observation and idea that I have been carrying around for a while. Several people are currently thinking about ways to axiomatize the reals in (homotopy) type theory.

    With cohesive homotopy type theory there is what looks like an interesting option for an approach different to the other ones: one can ask more generally about line objects 𝔸 1\mathbb{A}^1 that look like continua.

    One simple way to axiomatize this would be to say:

    1. 𝔸\mathbb{A} is a ring object;

    2. it is geometrically contractible, Π𝔸*\mathbf{\Pi} \mathbb{A} \simeq *.

    The last condition reflects the “continuumness”. For instance in the standard model Smooth∞Grpd for smooth homotopy cohesion, this distibuishes 𝔸=,\mathbb{A} = \mathbb{Z}, \mathbb{Q} from 𝔸=,\mathbb{A} = \mathbb{R}, \mathbb{C}.

    So while this axiomatization clearly captures one aspect of “continuum” very elegantly, I don’t know yet how far one can carry this in order to actually derive statements that one would want to make, say, about the real numbers.

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 30th 2012
    • (edited Sep 30th 2012)

    I just saw this page. A remark that you might like is that if 𝔸\mathbb{A} is a path-connected internal ring in (say) TopTop, then it is automatically contractible. Actually, all we really need is that there is a path α:I𝔸\alpha: I \to \mathbb{A} that connects the additive identity 00 to the multiplicative identity 11, since then

    I×𝔸α×1𝔸×𝔸mult𝔸I \times \mathbb{A} \stackrel{\alpha \times 1}{\to} \mathbb{A} \times \mathbb{A} \stackrel{mult}{\to} \mathbb{A}

    defines a contracting homotopy.

    The reason I’m bringing this up is that the first section of continuum mentions connectedness but not at all contractibility. The two are brought together when we have a ring object.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeSep 30th 2012

    Thanks, good point. I have added a remark on this.

    I have tried to state it in generality: if there is a subobject I𝔸 1I \hookrightarrow \mathbb{A}^1 which is itself geometrically contractible and contains the elements 0 and 1, then this implies already that the ring object 𝔸 1\mathbb{A}^1 is geometrically conctractible.

    (This needs of the axioms of cohesion the statement that Π\Pi preserves products! )

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 30th 2012

    Of course, i:I𝔸i: I \to \mathbb{A} doesn’t have to be a subobject. All we need is an interval (a cospan *I*\ast \to I \leftarrow \ast such that II is geometrically contractible) together with a cospan map from the interval cospan to the cospan *0𝔸1*\ast \stackrel{0}{\to} \mathbb{A} \stackrel{1}{\leftarrow} \ast.

    If you don’t object, I’ll add this in.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeSep 30th 2012

    Sure, very good.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 30th 2012

    Okay, I added something in. Not knowing the best terminology, I referred to a map from an interval type (left,right,I)(left, right, I) to the bipointed type (0,1,𝔸 1)(0, 1, \mathbb{A}^1). By the way, I changed in this section “continuum” to “line continuum”, to avoid conflict with the way that “continuum” was being used in the previous section. Hope that’s okay with you.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeSep 30th 2012

    Thanks. I had entirely forgotten that we have interval type.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeSep 30th 2012
    • (edited Sep 30th 2012)

    Wait, we have to be careful here. The unit interval [0,1]TopMfdETopinftyGrpd[0,1] \in TopMfd \hookrightarrow ETop\inftyGrpd is not (the interpretation of) an interval type. Instead Π([0,1])Grpd\Pi([0,1]) \in \infty Grpd is:

    the difference is that an interval type is required to have its endpoints be equivalent by morphism. But in [0,1][0,1] there are no non-trivial morphisms at all.

    I’ll edit at continuum a bit more to reflect this.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeOct 1st 2012

    This is nice!

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeSep 27th 2013

    Added this pointer:

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeSep 28th 2013

    He didn’t mention the higher inductive-inductive Cauchy reals! (-: Although I suppose he also didn’t mention the problem with the Cauchy reals that they solve (lack of Cauchy-completeness), while they don’t solve the problem with the Cauchy reals that he did mention (undesirable behavior in models).

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)