[HoTT] What is knot in HOTT?

[José Manuel Rodriguez Caballero]

Dear HoTT group,

  I'm thinking in the following question: What is the type-theoretic definition of a knot in HoTT?

Thank you in advance if you have some answers.

Sincerely yours,

Jose Manuel Rodriguez Caballero

[Egbert Rijke]

Dear Jose,

One idea I have been playing around with is to define a knot to consist of a map S1 -> S3 together with a type X equipped with maps S1 x S1 -> X and X -> S3, and a homotopy witnessing that the square

S1 x S1 ----------> X

   |                |

   |                |

   V                V

  S1 -------------> S3

commutes, and is a pushout square. The idea is that a knot is a topological embedding of S1 into S3. We can fatten its image up to an embedding from S1 x D2 -> S3, where D2 is the unit disc. Its boundary is the torus S1 x S1, and the embedding S1 x D2 -> S3 also has a complement. Then S3 should be the homotopy pushout of S1 and the complement of the subspace S1 x D2 in S3.

The problem is of course representing known knots in this way, which I don't really know how to do. For example, what is the homotopy type of the complement of the trefoil. This is probably known in the existing literature about knots, but I must admit that I don't know it. And also, what is the embedding S1 -> S3 for the trefoil knot? The fiber inclusion of the Hopf fibration perhaps? That would be a guess.

I would be very interested to hear if others have ideas on this topic. And just to repeat myself, I also don't know for sure if the above is a correct representation of a knot in HoTT.

With kind regards,

Egbert

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Ali Caglayan]

From what I have seen knot-theory has been very resistant to homotopy theoretic ideas (not classical ones). One 'clean' way of working with knot theory is to do so in the context of differential geometry. Cohesive HoTT supposedly can develop adequate differential geometry but at the moment it is very undeveloped.

One of the difficulties with knot theory is that (classical) homotopy theory in HoTT isn't really done with real numbers and interval objects, which is needed if you want to define notions of ambient isotopy and such.

I think the main difficulty here might be that HoTT is great at doing (synthetic) homotopy but not topology. The two can be easily confused. How do you take the complement of a space for example?

I could be wrong however but this is the conclusion I got when I tried thinking about HoTT knots.

[Michael Shulman]

This does seem like the kind of problem that Cohesive HoTT is designed
to solve. You could define a knot in a purely topological way as a
map from the topological circle to the topological 3-sphere, fatten it
up into a tubular neighborhood to express the topological 3-sphere as
a pushout of the tubular neighborhood of the topological circle and a
complement, then apply the shape functor which preserves pushouts to
obtain the homotopy-theoretic data described by Egbert with the
homotopical 3-sphere as a pushout of the homotopical circle and some
other space.

> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an

> email to HomotopyTypeThe...@googlegroups.com.

[Daniel R. Grayson]

Quillen identified the complement of the trefoil knot with SL(2,R)/SL(2,Z), and the proof is

on page 84 of Milnor's book "Introduction to algebraic K-theory".

[Egbert Rijke]

Just for the record, a trivial but nice observation: the unknot is the representation of S3 as the join of S1 with itself:

           p2

S1 x S1 ------> S1

   |            |

   | p1         |

   V            V

  S1 ---------> S3

Unfortunately, no-one has studied SL(2,R) and SL(2,Z) in HoTT yet. Although a trival way to obtain them is through cohesive HoTT would be nice if it were possible to define these spaces directly as higher inductive types.

Best,

Egbert

On Thu, Jul 19, 2018 at 1:56 PM, Daniel R. Grayson <danielrich...@gmail.com> wrote:

Quillen identified the complement of the trefoil knot with SL(2,R)/SL(2,Z), and the proof is

on page 84 of Milnor's book "Introduction to algebraic K-theory".

--

You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

egbertrijke.com

[José Manuel Rodriguez Caballero]

Maybe the connection between knots and primes can be stated in terms of SL(2,R) and SL(2,Z), because these groups are essential in number theory, e.g., modular forms, quadratic forms.

José M

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

[Urs Schreiber]

On 7/19/18, Michael Shulman <shu...@sandiego.edu> wrote:

> This does seem like the kind of problem that Cohesive HoTT is designed
> to solve.

Indeed, or rather that "differentially cohesive HoTT" is designed to solve:

The space of equivalence classes of knots of shape Sigma(= S^1) in
X(=S^3) should be the 0-truncation of the "shape" of the sub-type of
the function type Sigma -> X on those that are embeddings of smooth
manifolds.

We may formalize "smooth manifold" types Sigma, X and "embedding of
smooth manifolds" in HoTT using an "infinitesimal shape modality"
"Im", as in

Felix Wellen's work
ncatlab.org/schreiber/show/thesis+Wellen

to produce a type

(Sigma -> X)_emb

Then applying a shape modality to this

shape (Sigma -> X)_emb

yields a type whose paths should be interpreted as smooth isotopies.
Hence the 0-truncation of this type


Knot_Sigma(X) := | shape (Sigma -> X)_emb |_0

should be the type of equivalence classes of Sigma-shaped knots in X.

This would make sense for any Sigma and X. Indeed, the main problem
from this angle seems to be to axiomatize the generic manifold types
Sigma and X to behave enough like S^1 and S^3 such that one can draw
usual conclusions.

Not sure about that. One might be tempted to use Mike's "real
cohesion", but that probably does not admit a non-trivial
"infinitesimal shape modality" (being based on the topological real
line, instead of the smooth one).

Incidentally, just yesterday I tentatively started compiling a list
with "open problems and further directions in cohesive homotopy
theory". Just added a brief item on knot theory there:

https://ncatlab.org/schreiber/show/Some+thoughts+on+the+future+of+modal+homotopy+type+theory#KnotTheory

Related discussion on the nForum

https://nforum.ncatlab.org/discussion/8747/open-problems-in-axiomatic-cohesion/#Item_1

Best wishes,
urs

[Michael Shulman]

On Fri, Jul 20, 2018 at 3:27 AM, 'Urs Schreiber' via Homotopy Type
Theory <HomotopyT...@googlegroups.com> wrote:
> Indeed, the main problem
> from this angle seems to be to axiomatize the generic manifold types
> Sigma and X to behave enough like S^1 and S^3 such that one can draw
> usual conclusions.

Once we have the "smooth real numbers", wouldn't we just define S^1
and S^3 in terms of them as usual? Or are you saying that the problem
is in characterizing the smooth reals inside differential cohesion?

[Urs Schreiber]

> Once we have the "smooth real numbers", wouldn't we just define S^1
> and S^3 in terms of them as usual? Or are you saying that the problem
> is in characterizing the smooth reals inside differential cohesion?

Yes.

Possibly one could make progress by declaring shape to be homotopy
localization at some type A^1 of which we only demand that it be
homogeneous (as in Def. 4.8 in arxiv.org/abs/1806.05966) and then
focus attention on A^n-manifolds (as in Def. 7.1).

One could maybe declare that a smooth n-sphere to be an A^n-manifold
whose shape is equivalent to Disc(S^n). Classically, this should work
away from dimensions in which there are exotic spheres, hence in
particular for the case n <= 3 of relevance in knot theory.

Best wishes,
urs

[Michael Shulman]

It seems to me that especially if we want to construct *particular*
knots, we would need the smooth reals to at least be a ring and
probably to support trigonometric functions.

[Joyal, André]

Of course, braids, knots and tangles can be constructed algebraically
using braided monoidal categories.

________________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Michael Shulman [shu...@sandiego.edu]
Sent: Friday, July 20, 2018 10:54 AM
To: Urs Schreiber
Cc: Homotopy Type Theory
Subject: Re: [HoTT] What is knot in HOTT?

[Urs Schreiber]

> It seems to me that especially if we want to construct *particular*
> knots, we would need the smooth reals to at least be a ring and
> probably to support trigonometric functions.

One could require an isomorphism

Disc(A) = R_{Cauchy}

such that combined with the counit

A --> Disc(A) = R_Cauchy

this respects the homogeneous type structure on both sides (i.e the
postulated one on the left, the canonical one given by addition on the
right).

To test such choices of axioms, it would be very helpful to have a
concrete proposition in knot theory in mind, which one could aim for.
Preferably some very simple proposition which is still of interest.

Best,
urs

[Urs Schreiber]

Gr, here I mean "flat" where I wrote "Disc", and the counit should go
the other way around...

[Ali Caglayan]

It seems to me that "differentially cohesive HoTT", whatever it ends up being, is exactly the kind of viewpoint needed to study knot theory. The following characterisation of knot theory (I think?) due to Allen Hatcher might make this more apparent:

Knot theory is the study of path-components of the space of smooth submanifolds of S^3 diffeomorphic to S^1.

So you need to be able to talk about a space being smooth, pick a smooth structure for S^3 and S^1, what it means to be an immersion into a manifold (submanifold) and diffeomorphisms. This is just stating what knot theory ought to be, I have no idea if this viewpoint can actually tell you anything until we have some workable theory of differential cohesion. Currently we only have real-cohesive versions of HoTT.

Some starter questions would be:

 - Can you characterize the trivial knot.

 - How do you define the "connected sum" of knots.

 - How do you show every knot has an "inverse" with respect to the sum.

[andré hirschowitz]

Hi!

My guess would be that differentiability is irrelevant for knot theory.

You could rather consider closed subsets homeomorphic to S^1. For instance you could restrict your attention to "paths" consisting of injective sequences of  integral points

P1, ... , Pi, ...,  Pn=P0, where PiPi+1 is parallel to an axis and of length 1. There is probably a corresponding notion of "discrete" isotopy  among such paths, so that if two such paths are continuously isotopic, they are also discretely isotopic . As a consequence knots now live in Z^3.

So you can take the higher inductive type H with  Z^3 as  set of points, and the above  (length one) intervals as generating  equalities,  and study "synthetic knots" in there. The first thing to check is probably that any path in H is homotopic to a path obtained from a sequence of generators.

I am not sure at all that such a synthetic knot theory could be fruitful  May-be more interesting is to fill the holes in the H above by adding generating 2-cells  one for each elementary square and 3-cells  one for each elementary cube. It is not so clear how to do it if you want these cells to be "invertible"   More generally given a triangulated variety of dimension 3, you may try to specify as above a higher-inductive type, so that you could try to formulate (and prove...) a synthetic Poincaré conjecture.

Sorry for divagating slightly too much!

ah

--

You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/b886590f-c92b-493b-8751-9b0a342e9bdf%40googlegroups.com.