Sheaf Cohomology as Sheafification

This note is not part of the original lecture course; it grew out of discussions about understanding sheaf cohomology from a derived / animated perspective. The treatment follows Lurie’s Spectral Algebraic Geometry ([lurie-sag] ) and Mathew’s work on Galois groups in stable homotopy theory ([mathew-galois] ). Conventions Throughout we work in the derived setting and drop the $\mathrm{R}$-prefix on all functors. Concretely: All limits, colimits, and tensor products are derived. The symbol $\otimes$ denotes derived tensor product; the classical tensor product is recovered as $\pi_0(- \otimes -)$. $\Gamma(X, \mathcal{F})$ denotes derived global sections; the classical $\Gamma$ is $H^0(X, \mathcal{F}) \coloneqq \pi_0\,\Gamma(X, \mathcal{F})$. $\Hom_R(M, N)$ denotes derived $\Hom$, so $\operatorname{Ext}^i_R(M, N) = \pi_{-i}\Hom_R(M, N)$. $\mathrm{Mod}_R$ denotes the $\infty$-category of (left) module spectra over a connective $\mathbb{E}_\infty$-ring $R$ (equivalently, $\mathsf{D}(R)$ when $R$ is discrete). Presheaves take values in a stable presentable category $\mathcal{D}$ — typically $\mathsf{D}(\mathbb{Z})$, $\mathsf{Sp}$, or $\mathrm{Mod}_R$ for a base ring. The classical $1$-categorical theory is recovered by passing to $\pi_0$ at the end. ...

December 27, 2025 · 11 min · Ou Liu

Synthetic category theory and type theory

This page aims to explain how type theory can be understood within the framework of synthetic category theory. The content of this page is derived from my questions to Tashi during the second exercise class and Tashi’s responses. I would like to express my gratitude to Tashi here. We focus on the following two questions: Question I. How should we understand the notion of isofibration (hereafter referred to as a fibration) in synthetic category theory? Question II. Do we still have a weak factorization system in this context? Next, we will answer these questions through the lens of type theory and the categorical perspective of synthetic category theory. ...

December 24, 2025 · 6 min · Ou Liu