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 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 sheaves 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: formal immersion of smooth manifolds

Bottom of Page

1 to 15 of 15

  1.  
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 21st 2018

    Made a start here.

    v1, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJul 21st 2018

    replaced various occurences of “map” by more specific terms (bundle morphism, smooth function, continuous function)

    Added plural redirect.

    diff, v2, current

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 23rd 2018

    I added mention of the result that the 2-sphere can be everted in 3-space.

    Now is there any possibility of proving this with differential cohesive HoTT? A proof would give us a recipe for an eversion.

    diff, v5, current

    • CommentRowNumber4.
    • CommentAuthorRichard Williamson
    • CommentTimeJul 23rd 2018
    • (edited Jul 23rd 2018)

    There is a constructive eversion via the Roseman moves of 2-knot theory. Scott Carter has more than one book discussing it, it is a beautiful topic. But I would be astonished if HoTT can express it.

    I would love a proof assistant for knot theory, and would even try to write one, but I have no idea even in theory how to formulate a good syntactics that captures both local moves and less local considerations. Somehow the fact that diagrammatic knot theory lives in the plane, and the geometric manipulations that are possible in the plane, seem essential, and I have no idea how to capture this 2D aspect syntactically.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJul 23rd 2018
    • (edited Jul 23rd 2018)

    Now is there any possibility of proving this with differential cohesive HoTT?

    Sounds like a major research program. For comparison, the problems that I started to make a list of (here) are meant to be essentially “formalization ready”: We have a formal classical proof, or at least a detailed sketch of one. It’ still a bit of work from there to a computer checked proof, but at least there is a clear strategy.

    Here you seem to be asking pretty generic questions, in comparison. Any questions relating to the actual smooth nn-spheres will first need to solve the problem of narrowing in the synthetic language on the “standard model”, modeled on standard smooth manifolds.

    As I had tried to say elsewhere, maybe one way to approach this is to impose the following axioms to differential cohesion:

    1. ask shape to be homotopy localization at a homogeneous type 𝔸 1\mathbb{A}^1 (as in Def. 4.8 in Felix’s arXiv:1806.05966)

    2. ask for an identification ♭(𝔸 1)≃ℝ Cauchy 1\flat(\mathbb{A}^1) \simeq \mathbb{R}^1_{Cauchy}

    3. require that composed with the counit ℝ Cauchy 1≃♭(𝔸)→A\mathbb{R}^{1}_{Cauchy} \simeq \flat(\mathbb{A}) \to A this respects homogeneous type structure.

    Intuitively it seems that this should make 𝔸 n\mathbb{A}^n-manifolds (Def. 7.1), hence in particular nn-spheres, behave much like actual smooth nn-manifolds, maybe enough so to prove some classical theorem.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 23rd 2018

    Added mention of the fibration of Imm f(M,N)Imm^f(M,N) over Map(M,N)Map(M, N), where the fiber over ff is Hom Vect M inj(TM,f *TN)Hom^{inj}_{Vect_M}(T M, f^{\ast}T N).

    Imm f(M,N)Imm^f(M,N) is often studied as better behaved than Imm(M,N)Imm(M,N).

    diff, v6, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJul 23rd 2018

    Do you happen have a more precise source for this than Francis’ note? It remains a little unclear what kind of “fibering” he is referring to, and what exactly the space Map(M,N)Map(M,N) is.

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 23rd 2018

    In Lecture 3 he specifies that the fibering is the forgetful map to smooth functions of manifolds. But he notes also that

    The base space Map sm(M,N)Map^{sm}(M,N) is a comparatively easy space to study since it is homotopy equivalent to all continuous maps Map(M,N)Map(M,N)

    Meanwhile, this paper sets out defining formal immersions in terms of underlying continuous maps. Hmm, is there consensus?

    Anyway the story needs to continue to see how Smale’s theory is an example of the h-principle, for some open Diff(M)Diff(M)-invariant differential relation on MM, a section of which is a formal immersion.

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 23rd 2018

    the space of all formal immersions fibers over the space of smooth maps M→NM \to N, with fiber over some f:M→Nf:M \to N being the space of injective maps TM→f *TNT M \to f^{\ast}T N over MM. The space of smooth maps is homotopy equivalent to the space of all continuous maps (due to integrating against a smoothing kernel), whose homotopy type might be more accessible (for example vanish). (Homotopy Sheaves and h-Principles).

    So let’s keep with smooth maps, and point out the homotopy equivalence to all continuous maps.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJul 23rd 2018

    Okay, thanks! That would be good to make explicit in the entry. What kind of fibration is it?

    • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 24th 2018

    I’m not sure exactly.

    I added that Smale-Hirsch immersion theory is an h-principle situation.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJul 24th 2018

    Okay, let’s maybe make a note to check later. Also, this will depend on the actual choice of spaces, not just their homotopy types. (I mean, if there is to be a chance to formalize the argument, these details will matter.)

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 24th 2018

    Sure.

    To my amateur eye it seems that there might be parts of this domain which are amenable to differential cohesive formalization. I’m not sure at what degree of generality it would be best to attack. Some statements at least seem expressible:

    Consider a smooth nn-manifold MM and a smooth fibration over it, E→ME \to M, and ℛ\mathcal{R} a subspace of the kk-th jet space of EE, i.e., a differential relation. If MM is open as a manifold, and ℛ\mathcal{R} is an open subspace and is Diff(M)Diff(M)-invariant, then the image (under formation of kk-jets) of smooth sections of EE in smooth sections of ℛ\mathcal{R} is weakly homotopy equivalent to smooth sections of ℛ\mathcal{R}.

    Is that expressible with your additional axioms from #5?

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJul 24th 2018

    The proposition itself (not its proof) will have a fairly straightforward expression in HoTT equipped with an infinitesimal shape modality, not needing any further axioms.

    Now the proof, I don’t know. Very likely this will require further axioms. To see that, it would be useful to have a very clean version of the classical proof of this fact laid out, and its key ingredients isolated.

    • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 25th 2018
    • (edited Jul 25th 2018)

    A proof is given in Holonomic approximation and Gromov’s h-principle, but I doubt that would be easy to formalize, and also quite concisely here.

1 to 15 of 15

  1.