The Cubical Model of Type Theory (MSc thesis)

Recently, a model for dependent type theory has been given by Coquand et al. in a variant of the category of cubical sets. In their interpretation, they give a constructive version of Kan filling, classically known from simplicial sets, by means of a newly introduced operation. This cubical model also validates the univalence axiom constructively.

We present this model in terms of classical Kripke-Joyal semantics in a topos.

The Cubical Model of Type Theory (MSc thesis)

Advertisements

Alexander Grothendieck: Necessary Solitude

These texts are available only in German.

Slides and handout of a presentation on Alexander Grothendieck, jointly prepared with my colleague Nico Formanek for the interdisciplinary seminar In Solitude and Freedom on researcher biographies (Winter term 11/12).

All images in the files are taken from Winfried Scharlau’s carefully researched multipart biography on Grothendieck (cf.  handout bibliography).

The SO(10)-Grand Unified Theory

The SO(10) GUT is constructed as an extension of the SU(5) Theory and naturally acts on the whole of $\Lambda(\mathbb C^5)$ as a representation space. In particular, in this theory the laws of hypercharges from the Standard Model arise as simple consequences by assuming the existence of right-handed neutrinos.

We construct the necessary representations from the Spin groups in even dimension. Thus, we give a brief introduction into the structure and representation theory of Clifford algebras and Spin groups.

The SO(10)-Grand Unified Theory

De Risi’s Algebraic Model for a Monadic Phenomenology

This text is only available in German.

In Geometry and Monadology (2007), Vincenzo de Risi discusses the connection between Leibnizian Metaphysics and Geometry. In Chapter 3: Phenomenology, De Risi derives necessity of space from the existence of the, inter-related, monads. These spiritual entities are both receptive and expressive. The spatial world of phenomena consists of those expressions according to the inter-monadic relations. Conversely, plurality of perceptions is just the individuation principle for monads: each monad is determined by their inner and outer perceptions.

We explain de Risi’s Model for expressivity of monads, which is founded on universal algebra. Perceptions and expressions are implemented as relations and homomorphisms. As an advantage this formalization clarifies many key arguments and principles from the Monadologie.

After laying the algebraic foundations, we consider the expressive relation between the noumenal world of monads and the phenomenal world of perceptions. We discuss the limits of finite perception as well as material limits of the expressive relation. Finally we compare the results on perceptions gained from the algebraic model with the ones on Leibniz’ theory of knowledge.

Conclusively, we put the foundational thoughts behind this phenomenology in contrast to concurrent metaphysical theories.

De Risi’s Algebraic Model for a Monadic Phenomenology

Splitting the Classical Model Category Structure on the Category of Simplicial Sets (BSc thesis)

In the newly emerging field of homotopy type theory one seeks homotopy-theoretic models

for intensional Martin-Löf type theory. An important model is provided by the category

sSet of simplicial sets where dependent types are interpreted as Kan fibrations. In particular this applies to identity types. However, when it comes to interpreting the eliminator for identity types, problems arise since for the fillers, whose existence is guaranteed by the axioms of a Quillen model structure, it is not obvious how to chose them in a way which is compatible with reindexing. We present the solution given by Vladimir Voevodsky and Thomas Streicher based on type-theoretic universes where one chooses a filler in a slice over a generic context. Since the topos $\mathbf{sSet} = \mathbf{Set}^{\Delta^\mathrm{op}}$ of simplicial sets can be considered as a universe within a larger topos $\mathbf{SET}^{\Delta^{\mathrm{op}}}$ this allows us to exhibit a pullback-stable choice of fillers in $\mathbf{sSet}$.

We also discuss Voevodsky’s Univalence Axiom claiming that isomorphic types (of some

universe) are already equal whenever they are isomorphic in a weak sense. This axiom

can be formulated in the language of intensional type theory and as shown by Voevodsky in [KLV12], it holds in the simplicial model.

Splitting the Classical Model Category Structure on the Category of Simplicial Sets (BSc thesis)

Towards Mordell’s Theorem: The Finiteness of E(Q)/2E(Q)

In this seminar paper we prove the finiteness of E(Q)/2E(Q). Here, E(Q) denotes the group of rational points of
an elliptic curve E over Q. These statements can be used to prove Mordell’s Theorem that E(Q) is finitely
generated. Structure and methods are according to Knapp: “Elliptic Curves”, Chapter IV, Sections 3, 4 and 9.

The seminar “Elliptic Curves” was held by Prof. Nils Scheithauer at TU Darmstadt in Winter Term 2010/2011.

Towards Mordell’s Theorem: The Finiteness of E(Q)/2E(Q)

Locally Compact Groups: Isomorphism Theorems & Cyclic Subgroups

This treatise was prepared for the seminar Locally Compact Groups held by PD. Dr. Ralf Gramlich and Stefan Witzel in August 2010 at TU Darmstadt. The seminar was structured according to Markus Stroppel’s book.

In Section 1 we prove several classical isomorphism theorems for topological groups. Furthermore, we
state sufficient criteria for a topological group to be isomorphic to an inner direct product. In order to do
so, we will need an open mapping theorem for topological groups which yields that every surjective morphism between
topological groups is open if the groups satisfy certain compactness properties.

We proceed in Section 2 by analyzing the structure of certain locally compact groups based on their
subgroups. Weil’s Lemma consists of two structure results for locally compact Hausdorff groups $G$. In
particular, for each $g \in G$ the cyclic group $\langle g \rangle$ is either discrete and infinite or has compact
closure in $G$. We continue by classifying certain Abelian topological groups as direct products of a free
Abelian group with an open subgroup. Additionally, we state an existence criterion for discrete subgroups of locally
compact Abelian Hausdorff groups. Finally, we give some results of purely algebraic nature.

Locally Compact Groups: Isomorphism Theorems & Cyclic Subgroup

As of March 9, 2011, there is some further material available: