Thesis advisor: Julia Elisenda Grigsby / Thesis advisor: David Treumann / In 2010, Seidel and Smith used their localization framework for Floer homologies to prove a Smith-type rank inequality for the symplectic Khovanov homology of 2-periodic links in the 3-sphere. Hendricks later used similar geometric techniques to prove analogous rank inequalities for the knot Floer homology of 2-periodic links. We use combinatorial and space-level techniques to prove analogous Smith-type inequalities for various flavors of Khovanov homology for periodic links in the 3-sphere of any prime periodicity. First, we prove a graded rank inequality for the annular Khovanov homology of 2-periodic links by showing grading obstructions to longer differentials in a localization spectral sequence. We remark that the same method can be extended to p-periodic links. Second, in joint work with Matthew Stoffregen, we construct a Z/p-equivariant stable homotopy type for odd and even, annular and non-annular Khovanov homologies, using Lawson, Lipshitz, and Sarkar's Burnside functor construction of a Khovanov stable homotopy type. Then, we identify the fixed-point sets and apply a version of the classical Smith inequality to obtain spectral sequences and rank inequalities relating the Khovanov homology of a periodic link with the annular Khovanov homology of the quotient link. As a corollary, we recover a rank inequality for Khovanov homology conjectured by Seidel and Smith's work on localization and symplectic Khovanov homology. / Thesis (PhD) — Boston College, 2019. / Submitted to: Boston College. Graduate School of Arts and Sciences. / Discipline: Mathematics.

This thesis presents a characterization of those categories with weak factorization systems that can interpret the theory of intensional dependent type theory with Σ, Π, and identity types. We use display map categories to serve as models of intensional dependent type theory. If a display map category (C, D) models Σ and identity types, then this structure generates a weak factorization system (L, R). Moreover, we show that if the underlying category C is Cauchy complete, then (C, R) is also a display map category modeling Σ and identity types (as well as Π types if (C, D) models Π types). Thus, our main result is to characterize display map categories (C, R) which model Σ and identity types and where R is part of a weak factorization system (L, R) on the category C. We offer three such characterizations and show that they are all equivalent when C has all finite limits. The first is that the weak factorization system (L, R) has the properties that L is stable under pullback along R and all maps to a terminal object are in R. We call such weak factorization systems type theoretic. The second is that the weak factorization system has what we call an Id-presentation: it can be built from certain categorical structure in the same way that a model of Σ and identity types generates a weak factorization system. The third is that the weak factorization system (L, R) is generated by a Moore relation system. This is a technical tool used to establish the equivalence between the first and second characterizations described. To conclude the thesis, we describe a certain class of convenient categories of topological spaces (a generalization of compactly generated weak Hausdorff spaces). We then construct a Moore relation system within these categories (and also within the topological topos) and thus show that these form display map categories with Σ and identity types (as well as Π types in the topological topos).

No description available.

Seja p um \'S POT. 3\' - fibrado principal sobre uma esfera \'S POT. n\' , com n \' >OU=\' 4 . O objetivo deste trabalho é calcular os tipos de homotopia do grupo de gauge \'G IND. p\' desses fibrados p, estendendo o resultado determinado por A. Kono [25] quando n = 4. Apresentamos fórmulas explícitas para o operador bordo na seqüência exata de homotopia associada com a aplicação avaliação ev : m(\'S POT. n\' , B \'S POT. 3\' ) \'SETA\' B \'S POT. 3\' , traduzindo o problema nos cálculos envolvendo grupos de homotopia de esferas. Calculamos todos os casos clássicos, ou seja, aqueles que podem ser avaliados usando as informações encontradas no livro de H. Toda [46], determinando o tipo de homotopia do grupo de gauge desses fibrados para cada n \' > OU =\' 25 / Let p be a principal \'S POT. 3\' - bundle over a sphere \'S POT. n\' , with n\' > or =\' 4\'. The subject of this work is to calculate the homotopy type of the gauge group \'G IND. p\' of these bundles p, extending the result determined by A. Kono [25] when n = 4. We present explicit formulas for the boundary operator in the homotopy exact sequence associated with the evaluation map ev : m(\'S POT. n\' , B \'S POT. 3\' ) \' ARROW\' B \'S POT. 3\' , translating that problem into calculations involving homotopy groups of sphere. We calculate all the classical cases, namely those that can be dealt with using the information in the book of H. Toda [46], determining the homotopy type of the gauge group of these bundles for each n \'> or = 25

In this thesis, we consider semi-algebraic sets over a real closed field R defined by quadratic polynomials. Semi-algebraic sets of R^k are defined as the smallest family of sets in R^k that contains the algebraic sets as well as the sets defined by polynomial inequalities, and which is also closed under the boolean operations (complementation, finite unions and finite intersections). We prove new bounds on the topological complexity of semi-algebraic sets over a real closed field R defined by quadratic polynomials, in terms of the parameters of the system of polynomials defining them, which improve the known results. We conclude the thesis with presenting two new algorithms along with their implementations.

Seja p um \'S POT. 3\' - fibrado principal sobre uma esfera \'S POT. n\' , com n \' >OU=\' 4 . O objetivo deste trabalho é calcular os tipos de homotopia do grupo de gauge \'G IND. p\' desses fibrados p, estendendo o resultado determinado por A. Kono [25] quando n = 4. Apresentamos fórmulas explícitas para o operador bordo na seqüência exata de homotopia associada com a aplicação avaliação ev : m(\'S POT. n\' , B \'S POT. 3\' ) \'SETA\' B \'S POT. 3\' , traduzindo o problema nos cálculos envolvendo grupos de homotopia de esferas. Calculamos todos os casos clássicos, ou seja, aqueles que podem ser avaliados usando as informações encontradas no livro de H. Toda [46], determinando o tipo de homotopia do grupo de gauge desses fibrados para cada n \' > OU =\' 25 / Let p be a principal \'S POT. 3\' - bundle over a sphere \'S POT. n\' , with n\' > or =\' 4\'. The subject of this work is to calculate the homotopy type of the gauge group \'G IND. p\' of these bundles p, extending the result determined by A. Kono [25] when n = 4. We present explicit formulas for the boundary operator in the homotopy exact sequence associated with the evaluation map ev : m(\'S POT. n\' , B \'S POT. 3\' ) \' ARROW\' B \'S POT. 3\' , translating that problem into calculations involving homotopy groups of sphere. We calculate all the classical cases, namely those that can be dealt with using the information in the book of H. Toda [46], determining the homotopy type of the gauge group of these bundles for each n \'> or = 25

This thesis consists of four papers on type theory and a formalisation of certain results from the two first papers in the Agda language. We cover topics such as models of multisets and sets in Homotopy Type Theory, and explore ideas of using type theory as a language for databases and different ways of expressing dependencies between terms. The two first papers build on work by Aczel 1978. We establish that the underlying type of Aczel’s model of set theory in type theory can be seen as a type of multisets from the perspective of Homotopy Type Theory, and we identify a suitable subtype which becomes a model of set theory in which equality of sets is the identity type. The third paper is joint work with Henrik Forssell and David I .Spivak and explores a certain model of type theory, consisting of simplicial complexes, from the perspective of database theory. In the fourth and final paper, we consider two approaches to unraveling the dependency structures between terms in dependent type theory, and formulate a few conjectures about how these two approaches relate.

Homotopy Type Theory (HoTT) is a quite recent branch of research in mathematical logic, which provides interesting connections among various areas of mathematics. It was first introduced by Vladimir Voevodsky as a means to develop synthetic homotopy theory, and further advancements suggested that it can be used as a formal foundation to mathematics. Among its notable features, inductive and higher inductive types are of great interest, e.g. allowing for the study of geometric entities (such as spheres) in the setting of HoTT. However, so far in most of the literature higher inductive types are treated in an ad-hoc way; there is no easy general schema stating what an higher inductive type is, thus hindering the study of the related proof theory. Moreover, although Martin-Löf Type Theory has been deeply and widely studied, many proof theoretic results about its specific variant used in HoTT are folklore, and the proofs are missing. In this final talk, we provide an overview on some results we obtained, aiming to address these problems. In the first part of the talk, we will discuss a normalization theorem for the type theory underlying HoTT. In the second part of the talk we will propose a general syntax schema to encapsulate a relevant class of higher inductive types, potentially allowing for future study of the proof theory of HoTT enriched with such types.

Cette thèse s'intéresse à la métathéorie de la théorie des types intuitionniste. Les systèmes que nous considérons sont des variantes de la théorie des types de Martin-Löf ou du Calcul des Constructions, et nous nous intéressons à la cohérence de ces systèmes ou encore à l'indépendance d'axiomes par rapport à ces systèmes. Le fil rouge de cette thèse est la construction de modèles syntaxiques, qui sont des modèles qui réutilisent la théorie des types pour interpréter la théorie des types. Dans une première partie, nous introduisons la théorie des types à l'aide d'un système minimal et de plusieurs extensions potentielles. Dans une seconde partie, nous introduisons les modèles syntaxiques donnés par traduction de programme et donnons plusieurs exemples. Dans une troisième partie, nous présentons Template-Coq, un plugin de métaprogrammation pour Coq. Nous montrons comment l'utiliser pour implémenter directement certains modèles syntaxiques. Enfin, dans une dernière partie, nous nous intéressons aux théories des types à deux égalités : une égalité stricte et une égalité univalente. Nous proposons une relecture des travaux de Coquand et. al. et Orton et Pitts sur le modèle cubique en introduisant la notion de fibrance dégénérée. / This thesis is about the metatheory of intuitionnistic type theory. The considered systems are variants of Martin-Löf type theory of Calculus of Constructions, and we are interested in the coherence of those systems and in the independence of axioms with respect to those systems. The common theme of this thesis is the construction of syntactic models, which are models reusing type theory to interpret type theory. In a first part, we introduce type theory by a minimal system and several possible extensions. In a second part, we introduce the syntactic models given by program translation and give several examples. In a third part, we present Template-Coq, a plugin for metaprogramming in Coq. We demonstrate how to use it to implement directly some syntactic models. Last, we consider type theories with two equalities: one strict and one univalent. We propose a re-reading of works of Coquand et.al. and of Orton and Pitts on the cubical model by introducing degenerate fibrancy.

L’objectif de cette thèse est de démontrer que π4(S3) ≃ Z/2Z en théorie des types homotopiques. En particulier, c’est une démonstration constructive et purement homotopique. On commence par rappeler les concepts de base de la théorie des types homotopiques et on démontre quelques résultats bien connus sur les groupes d’homotopie des sphères : le calcul des groupes d’homotopie du cercle, le fait que ceux de la forme πk(Sn) avec k < n sont triviaux et la construction de la fibration de Hopf. On passe ensuite à des outils plus avancés. En particulier, on définit la construction de James, ce qui nous permetde démontrer le théorème de suspension de Freudenthal et le fait qu’il existe un entier naturel n tel que π4(S3) ≃ Z/2Z. On étudie ensuite le produit smash des sphères, on construit l’anneau de cohomologie des espaces et on introduit l’invariant de Hopf, ce qui nous permet de montrer que n est égal soit à 1, soit à 2. L’invariant de Hopf nous permet également de montrer que tous les groupes de la forme π4n−1(S2n) sont infinis. Finalement, on construit la suite exacte de Gysin, ce qui nous permet de calculer la cohomologie de CP2 et de démontrer que π4(S3) ≃ Z/2Z, et que plus généralement on a πn+1(Sn) ≃ Z/2Z pour tout n ≥ 3 / The goal of this thesis is to prove that π4(S3) ≃ Z/2Z in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the basic concepts of homotopy type theory, and we prove some well-known results about the homotopy groups of spheres: the computation of the homotopy groups of the circle, the triviality of those of the form πk(Sn) with k < n, and the construction of the Hopf fibration. We then move to more advanced tools. In particular, we define the James construction which allows us to prove the Freudenthal suspension theorem and the fact that there exists a natural number n such that π4(S3) ≃ Z/nZ. Then we study the smash product of spheres, we construct the cohomology ring of a space, and we introduce the Hopf invariant, allowing us to narrow down the n to either 1 or 2. The Hopf invariant also allows us to prove that all the groups of the form π4n−1(S2n) are infinite. Finally we construct the Gysin exact sequence, allowing us to compute the cohomology of CP2 and to prove that π4(S3) ≃ Z/2Z and that more generally πn+1(Sn) ≃ Z/2Z for every n ≥ 3