Posts

The computational content of equality in Martin-Löf type theory

If you ask a type theorist what "axioms" their system assumes, you may get a look of indignation. Type theorists take pride in assuming no axioms. Instead, a type theory has grammatical rules which allow the user to define types and terms. An "axiom" in the context of type theory refers to an assumption that a certain type is inhabited, even when it is impossible to construct a term of the given type purely by following the grammatical rules. The distinction may sound like mere semantics; but a type theory is a programming language, and the constructions of the grammar have computational content even when their logical meaning is ignored. One need not appeal to any kind of logical principles in justifying the terms; one can justify them only in terms of programming. Equality in (intensional) Martin-Löf type theory is strangely behaved. In MLTT, proofs of equality are mathematical objects in their own right that can be referred to within the theory. In particular,...

Kan extensions and coends in the enriched case

I have been thinking about the nerve-realization theorem. See here: https://ncatlab.org/nlab/show/nerve+and+realization This blog post is about my attempts to think through it. The theorem is just about the usual coend formula for the left Kan extension, except that it studies a complicated case where some of the categories are enriched and some are not; on the other hand it is simpler in that one of the functors is fixed to be some variant of the Yoneda embedding.  In their notation, $\mathcal{C}$ is enriched but $S$ may not be. For example, a simplicial Abelian group or a simplicial topological space are functors from an unenriched category to a category that is enriched ($\mathbf{Ab}$) or at least somewhat enriched (hom sets in $\mathbf{Top}$ can be equipped with the compact open topology) Let $M$ be a small category. Let $\mathcal{A}$ be a co-complete category. Let $T: M\to \mathcal{A}$ be a functor. Theorem:   Let $R : \mathcal{A}\to \hat{M}=[M^{op},\mathbf{Sets}]$ be def...

An example of a forcing argument in geometry - down-to-earth uses of topos theory

Topos theory leads with the slogan - ``unification of logic and geometry.'' This theory has been more effective in marketing than in actually giving effective cross-fertilization between the two fields. A subject in between $A$ and $B$ may draw on both fruitfully and give back to both fruitfully, but it is most exciting when it really serves as a bridge between $A$ and $B$, allowing you to transfer ideas back and forth. The notion of ``Kripke model'' is one of the oldest proposed semantics for forcing. Some category theorists have noticed that a Kripke model (let's say a model of a first order theory) over an index set $I$ with partial-ordering relation $\leq$ can be viewed as a functor from $I$ as a poset category into the category of sets, or a presheaf depending on your orientation of $I$. This observation has led to a development of a general forcing semantics in an elementary topos; a good reference is Sheaves in Geometry and Logic by Mac Lane and Moerdijk, in ...

Godement, Part V - Monads and Homological Algebra

In https://unity-of-opposites.blogspot.com/2020/06/godement-part-iv-definition-of-monads.html we introduced the Godement monad. To recap, if $X$ is any topological space, and we form the disjoint union of points $X^\delta = \coprod_{x\in X} x$ equipped with the discrete topology, there is a canonical map $i :X^\delta\to X$ which is the identity on points. This gives rise to two adjoint functors between the corresponding sheaf categories, the direct image functor and the inverse image functor. Their composition gives rise to an endofunctor on $Sh(X)$; this endofunctor is a monad, $T$. Its unit is the unit of the adjunction. Given any sheaf $\mathcal{F}$, the sequence of sheaves $T^{n+1}(\mathcal{F})$ is naturally endowed with the structure of a cosimplicial object, with augmentation map $\mathcal{F}\to T(\mathcal{F})$. By purely formal abstract nonsense, (and all the more beautiful for how trivial it is) the resulting cochain complex given by taking alternating sums of the coface maps ...

Godement, Part IV - definition of monads, examples

A monad is a monoid in a category of endofunctors. In the previous post, we have established a very general notion of monoid which is suitable for many applications. For example, the category of chain complexes $R$-modules can be equipped with a monoidal product which associates to each pair $(C,C')$ of chain complexes the total complex $Tot(C\otimes C')$ of the double complex $(C\otimes C')_{i,j}= C_i\otimes C_j'$. The unit of this monoidal product is the complex with $R$ in dimension $0$ and $0$'s in all other dimension. A DG-algebra is precisely a monoid with respect to this monoidal product. For a given category $\mathcal{C}$, the functor category $[\mathcal{C};\mathcal{C}]$ is naturally equipped with thestructure of a strict monoidal category, whose monoidal product $\otimes$ is precisely functor composition, $F\otimes G= F\circ G$; and whose unit $1$ is precisely the identity functor $id_{\mathcal{C}}$. It is easily verified that this is functorial simulta...

Brief survey of duality in manifolds

Let $X$ be a topological manifold. Theorem: Let $x$ be a point in $X$. There is a small open neighborhood $U$ of $x$ such that for every $x'$ in $U$, there is a homeomorphism of $X$ with itself carrying $x'$ to $x$. Actually, we can say something substantially stronger, but it's a bit more subtle and harder to digest. Theorem: Let $x$ be a point in $X$. There is a small open neighborhood $U$ of $x$, such that for each $x'\in U$, there exists a homeomorphism $f_{x'}$ from $X$ to itself, carrying $x'$ to $x$; moreover, this family of homeomorphisms can be chosen such that the disjoint union $f= \coprod_{x'\in U}f_{x'} : U\times X\to U\times X$ is a homeomorphism of $U\times X$ with itself, carrying $(x', y)$ to $(x',f_{x'}(y))$, and in particular sending $(x',x')$ to $(x',x)$. The proof is an elegant geometrical construction. Let $\delta(U)\subset U\times X$ be the set of ordered pairs $(x,x)$ with $x\in U$. Then the homeomor...

A response to an undergrad - What do I study?

An undergrad that I was a T.A. for recently asked me what my research is in. I decided to write up an answer as a blog post, in a way that is accessible to the average early undergrad student in STEM. I study logic. More specifically, I study semantics. In linear algebra, you start off with a certain formal algebraic language, the language of vector spaces - it has certain distinguished constant symbols you are permitted to use, like "0" for the zero vector, or any real number; you are permitted to use variables v, w, ... that range across the vectors; there are also special symbols that represent functions, like "+", for addition. There are also certain axioms, written in the language. One also has a list of formal logical laws that allow you to combine the axioms in various ways to derive theorems in the theory of linear algebra. Linear algebra from this point of view is the collection of all formal statements in the language of linear algebra that c...