Sheaves · The Lumenary

Lens

MotivationH

Everywhere locally, nowhere globally

On the punctured plane $X = \C \setminus \{0\}$ , does $z$ have a logarithm — a holomorphic $\ell$ with $e^{\ell(z)} = z$ ? Near every point, yes: on any disc avoiding $0$ there is a branch of $\log z$ , unique up to adding $2\pi i k$ . On all of $X$ , no: following a branch once around the origin adds $2\pi i$ . The question "does a solution exist?" has a local answer (yes, everywhere) and a global answer (no), and the gap between them is a topological invariant of $X$ — the class of the loop around $0$ .

Many problems have this shape: solving a differential equation, finding a potential for a vector field with zero curl, choosing a consistent orientation, building a meromorphic function with prescribed poles (Mittag-Leffler), patching local coordinates into a manifold. A sheaf is the structure that records what exists locally and how local pieces restrict and glue. Its global sections are the global solutions, its stalks describe what happens at a point, and its cohomology measures the obstructions in between.

Sheaves are also a bridge. Topologically they are spaces lying over $X$ (étale spaces, covering spaces); geometrically they are how algebraic and complex geometry define their spaces (a scheme is a space with a sheaf of rings); categorically they form a topos, a universe of "sets varying over $X$ " with its own logic. This lesson builds on point-set topology and limits and colimits.

IntuitionH

Restrict, compare, glue

Think of an atlas. Each page is a map of a region; a map of a region can be cut down to a map of any smaller region; and if maps of two regions agree where the regions overlap, they combine into one map of the union — in exactly one way. Replace "map of a region" by "continuous function on an open set", or "solution of a differential equation on an open set", or "branch of $\log z$ on an open set", and you have the three ingredients of a sheaf:

sections $F(U)$ over each open set $U$ ;
restriction $s \mapsto s|_V$ to smaller open sets $V \subseteq U$ , compatible with restricting in stages;
gluing: sections over the pieces of an open cover that agree on overlaps come from exactly one section over the union.

Gluing on the line. A function s₁ on U₁ and a function s₂ on U₂ agree on the overlap U₁ ∩ U₂ (shaded); together they define exactly one function on U₁ ∪ U₂.

Not every natural assignment glues. Bounded functions do not: the function $x$ is bounded on every bounded interval, and these local pieces agree, but they glue to an unbounded function on $\R$ . Boundedness is a global condition; continuity is local. Sheaves are exactly the assignments defined by local conditions.

DefinitionsH

Definitions

Let $X$ be a topological space and $\mathcal{O}(X)$ the poset of its open sets, viewed as a category with an arrow $V \to U$ when $V \subseteq U$ .

Definition— presheaf

A presheaf (of sets) on $X$ is a functor $F : \mathcal{O}(X)^{\mathrm{op}} \to \cat{Set}$ : a set $F(U)$ of sections for each open $U$ and a restriction map $F(U) \to F(V)$ , $s \mapsto s|_V$ , for each $V \subseteq U$ , with $s|_U = s$ and $(s|_V)|_W = s|_W$ . Elements of $F(X)$ are global sections. A morphism of presheaves $\varphi : F \to G$ is a natural transformation: maps $\varphi_U : F(U) \to G(U)$ commuting with restriction. Presheaves of abelian groups, rings or modules are defined in the same way.

Definition— sheaf

A presheaf $F$ is a sheaf if for every open $U$ and every open cover $U = \bigcup_{i \in I} U_i$ :

(Locality) if $s, t \in F(U)$ satisfy $s|_{U_i} = t|_{U_i}$ for all $i$ , then $s = t$ ;
(Gluing) if $s_i \in F(U_i)$ satisfy $s_i|_{U_i \cap U_j} = s_j|_{U_i \cap U_j}$ for all $i, j$ , then there is $s \in F(U)$ with $s|_{U_i} = s_i$ for all $i$ .

Equivalently, the diagram below is an equaliser in $\cat{Set}$ , where $e(s) = (s|_{U_i})_i$ , $p((s_i)_i) = (s_i|_{U_i \cap U_j})_{i,j}$ and $q((s_i)_i) = (s_j|_{U_i \cap U_j})_{i,j}$ . Sheaves form a full subcategory $\mathrm{Sh}(X)$ of the presheaf category $\mathrm{PSh}(X)$ .

The sheaf condition:

e

is injective (locality) and its image is exactly the set where

p

and

q

agree (gluing).

Definition— stalk; germ

The stalk of a presheaf $F$ at $x \in X$ is the colimit over open neighbourhoods of $x$ ,

F_x = \operatorname*{colim}_{U \ni x} F(U) = \Big( \bigsqcup_{U \ni x} F(U) \Big) \Big/ \sim, \qquad (s \in F(U)) \sim (t \in F(V)) \iff s|_W = t|_W \text{ for some open } x \in W \subseteq U \cap V .

The class $s_x$ of $s$ is its germ at $x$ . A morphism $\varphi$ induces maps $\varphi_x : F_x \to G_x$ on stalks.

Definition— étale space

The étale space of $F$ is $\mathrm{Et}(F) = \bigsqcup_{x \in X} F_x$ with the topology generated by the sets $\{ s_x : x \in U \}$ for $s \in F(U)$ , and projection $\pi : \mathrm{Et}(F) \to X$ . Every section $s \in F(U)$ becomes a continuous section $x \mapsto s_x$ of $\pi$ over $U$ , and $\pi$ is a local homeomorphism.

Definition— direct image; skyscraper

For a continuous map $f : X \to Y$ and a sheaf $F$ on $X$ , the direct image $f_*F$ is the sheaf $V \mapsto F(f^{-1}(V))$ on $Y$ . For a point $x \in X$ and a set $A$ , the skyscraper sheaf $x_*A$ has sections $A$ over open sets containing $x$ and a single point otherwise.

Worked examplesH

Examples and non-examples

Example— Sheaves of functions

For any space $Y$ , $U \mapsto C(U, Y)$ (continuous maps) is a sheaf: functions that agree on overlaps define one function on the union, and continuity can be checked locally (Proposition 2). The same holds for smooth functions on a manifold, holomorphic functions on a complex manifold, solutions of a linear differential equation, and sections $U \to E$ of any continuous map $p : E \to X$ . In each case the defining condition is local.

Example— Constant presheaves, and the sheaf of locally constant functions

The constant presheaf $U \mapsto A$ , with all restrictions the identity, fails to be a sheaf if $A$ has at least two elements: the empty set is covered by the empty family, and gluing then forces $F(\varnothing)$ to be a single point (Proposition 1). Repairing this by setting $F(\varnothing) = \{*\}$ does not help: if $U = U_1 \sqcup U_2$ with $U_1, U_2$ disjoint, non-empty and open, the sections $a \in F(U_1)$ and $b \neq a \in F(U_2)$ agree on the empty overlap but do not glue to a single element of $A$ . The sheaf that does the job is the sheaf $\underline{A}$ of locally constant functions $U \to A$ , with $\underline{A}(U) = A^{\pi_0(U)}$ when $U$ is locally connected. It is the sheafification of the constant presheaf (Corollary 6).

Example— Bounded functions

$U \mapsto \{\text{bounded continuous } U \to \R\}$ satisfies locality but not gluing: the restrictions of $f(x) = x$ to the intervals $(n - 1, n + 1)$ are bounded and compatible, but there is no bounded function on $\R$ restricting to them.

Example— Branches of the logarithm and a twisted sheaf on the circle

On $X = \C \setminus \{0\}$ let $L(U)$ be the set of continuous (equivalently holomorphic) branches of $\log z$ on $U$ . Every point has a neighbourhood with $L(U) \neq \varnothing$ , but $L(X) = \varnothing$ . Similarly, on $S^1 = \R/\Z$ let $T(U)$ be the continuous functions $s$ on the preimage of $U$ in $\R$ with values in $\Z$ and $s(t + 1) = -s(t)$ . Locally $T$ looks like the sheaf $\underline{\Z}$ of locally constant integers, with every stalk $\cong \Z$ ; but a global section would be a constant integer equal to its own negative, so $T(S^1) = \{0\}$ . A non-zero sheaf can have no non-zero global sections.

Example— Finite spaces

On a finite space every point $x$ has a smallest open neighbourhood $U_x$ , so $F_x = F(U_x)$ . The pseudocircle $\{a, b, c, d\}$ , with open sets $\varnothing, \{a\}, \{b\}, \{a, b\}, \{a, b, c\}, \{a, b, d\}$ and the whole space, is a finite model of the circle (McCord, 1966); sheaves on it can be checked exhaustively, as in the computation section.

ProofH

Gluing, germs and stalks

Theorem— Proposition 1 (the empty set)

If $F$ is a sheaf, then $F(\varnothing)$ has exactly one element.

Proof

The empty set is covered by the empty family ( $I = \varnothing$ ). The compatibility condition is vacuous, so gluing gives some $s \in F(\varnothing)$ , and locality, which is also vacuous, says that any two elements of $F(\varnothing)$ are equal.

∎

Theorem— Proposition 2 (continuity is local)

For every space $Y$ , the presheaf $U \mapsto C(U, Y)$ on $X$ is a sheaf.

Proof

Let $U = \bigcup_i U_i$ . Locality: if $s|_{U_i} = t|_{U_i}$ for all $i$ then $s(x) = t(x)$ for every $x \in U$ , as $x$ lies in some $U_i$ . Gluing: given continuous $s_i : U_i \to Y$ agreeing on overlaps, define $s(x) = s_i(x)$ for any $i$ with $x \in U_i$ ; this is well defined because $s_i(x) = s_j(x)$ when $x \in U_i \cap U_j$ . For continuity, let $W \subseteq Y$ be open; then $s^{-1}(W) = \bigcup_i s_i^{-1}(W)$ , and each $s_i^{-1}(W)$ is open in $U_i$ , hence in $X$ because $U_i$ is open. So $s$ is continuous and $s|_{U_i} = s_i$ .

∎

Theorem— Theorem 3 (sections are determined by germs)

Let $F$ be a sheaf and $s, t \in F(U)$ . If $s_x = t_x$ for every $x \in U$ , then $s = t$ .

Proof

For each $x \in U$ , $s_x = t_x$ means there is an open $W_x$ with $x \in W_x \subseteq U$ and $s|_{W_x} = t|_{W_x}$ . The sets $W_x$ cover $U$ , so $s = t$ by locality.

∎

Theorem— Theorem 4 (isomorphisms are detected on stalks)

A morphism of sheaves $\varphi : F \to G$ is an isomorphism if and only if $\varphi_x : F_x \to G_x$ is bijective for every $x \in X$ .

Proof

An isomorphism clearly induces bijections on colimits. Conversely, assume every $\varphi_x$ is bijective; we show every $\varphi_U$ is bijective, and then the inverses $\varphi_U^{-1}$ automatically commute with restriction.

Injective. If $\varphi_U(s) = \varphi_U(t)$ , then $\varphi_x(s_x) = \varphi_x(t_x)$ , so $s_x = t_x$ for all $x \in U$ , and $s = t$ by Theorem 3.

Surjective. Let $t \in G(U)$ . For each $x \in U$ , surjectivity of $\varphi_x$ gives a section $s^{(x)} \in F(V_x)$ , $x \in V_x$ , with $\varphi(s^{(x)})_x = t_x$ ; shrinking $V_x$ we may assume $\varphi_{V_x}(s^{(x)}) = t|_{V_x}$ . On an overlap $V_x \cap V_y$ , the sections $s^{(x)}$ and $s^{(y)}$ both map to $t|_{V_x \cap V_y}$ , so they agree by the injectivity just proved. By gluing there is $s \in F(U)$ with $s|_{V_x} = s^{(x)}$ , and then $\varphi_U(s)$ and $t$ agree on every $V_x$ , so $\varphi_U(s) = t$ by locality in $G$ .

∎

The hypothesis that $F$ is a sheaf is essential: the inclusion of the constant presheaf $A$ into $\underline{A}$ is bijective on all stalks but not an isomorphism. And "surjective on stalks" does not imply "surjective on sections" (see the exponential sequence below): the proof of surjectivity used injectivity, i.e. bijectivity, on stalks.

Theorem— Theorem 5 (sheafification)

Every presheaf $F$ has a sheaf $F^+$ and a morphism $\theta : F \to F^+$ such that every morphism from $F$ to a sheaf $G$ factors uniquely through $\theta$ . In other words, sheafification $F \mapsto F^+$ is left adjoint to the inclusion $\mathrm{Sh}(X) \hookrightarrow \mathrm{PSh}(X)$ . Moreover $\theta_x : F_x \to F^+_x$ is bijective for every $x$ .

Proof

Let $F^+(U)$ be the set of functions $\sigma : U \to \bigsqcup_{x \in U} F_x$ with $\sigma(x) \in F_x$ that are locally germs of sections: every $x \in U$ has an open neighbourhood $W \subseteq U$ and some $s \in F(W)$ with $\sigma(y) = s_y$ for all $y \in W$ . (These are exactly the continuous sections of the étale space.) Restriction is restriction of functions, and $\theta_U(s) = (x \mapsto s_x)$ .

$F^+$ is a sheaf: functions agreeing on overlaps glue uniquely to a function, and the defining condition is local, so the glued function satisfies it — the same argument as Proposition 2. Stalks: every germ of $F^+$ at $x$ is represented near $x$ by some $\theta(s)$ , so $\theta_x$ is surjective; if $\theta(s)$ and $\theta(t)$ have the same germ at $x$ then $s_x = t_x$ , so $\theta_x$ is injective. Universal property: given $\varphi : F \to G$ with $G$ a sheaf, and $\sigma \in F^+(U)$ locally of the form $\theta(s^{(i)})$ on a cover $W_i$ , the sections $\varphi(s^{(i)}) \in G(W_i)$ have the same germs on overlaps, so they agree there by Theorem 3 and glue to a unique $\varphi^+(\sigma) \in G(U)$ ; this defines $\varphi^+ : F^+ \to G$ with $\varphi^+ \theta = \varphi$ , and uniqueness follows because $\varphi^+$ is forced on the local pieces $\theta(s^{(i)})$ .

∎

Theorem— Corollary 6 (sheafifying a constant presheaf)

The sheafification of the constant presheaf with value $A$ is the sheaf $\underline{A}$ of locally constant functions $U \to A$ .

Proof

For $x \in X$ , the stalk of the constant presheaf is $A$ (all restriction maps are the identity, and every neighbourhood system is non-empty). A section of $F^+$ over $U$ is therefore a function $\sigma : U \to A$ that is locally equal to a constant section, i.e. a locally constant function. Over $U = \varnothing$ there is exactly one (empty) function, as Proposition 1 requires.

∎

Theorem— Theorem 7 (sheaves form a topos)

$\mathrm{Sh}(X)$ is a Grothendieck topos: it has all limits and colimits, it is cartesian closed, and it has a subobject classifier $\Omega$ with $\Omega(U) = \{ \text{open subsets of } U \}$ .

Limits of sheaves are computed sectionwise; colimits are sheafified sectionwise colimits; the internal hom is $\mathcal{H}om(F, G)(U) = \operatorname{Hom}(F|_U, G|_U)$ . A subsheaf $S \subseteq F$ is classified by sending $s \in F(U)$ to the largest open $V \subseteq U$ with $s|_V \in S(V)$ — the "set of points where $s$ belongs to $S$ " (Mac Lane–Moerdijk, Chapters II and III). This is the starting point of elementary topos theory, where truth values become open sets.

ExplanationH

A preview of sheaf cohomology

For sheaves of abelian groups, a sequence $0 \to F' \to F \to F'' \to 0$ is called exact if it is exact on every stalk. Taking global sections preserves exactness on the left but not on the right, and sheaf cohomology $H^n(X, F)$ measures the failure.

Example— The exponential sequence

On $X = \C \setminus \{0\}$ let $\mathcal{O}$ be the sheaf of holomorphic functions and $\mathcal{O}^\times$ that of nowhere-vanishing ones (a group under multiplication). The sequence

0 \to 2\pi i \underline{\Z} \to \mathcal{O} \xrightarrow{\ \exp\ } \mathcal{O}^\times \to 1

is exact on stalks, because every non-vanishing holomorphic germ has a logarithm on a small disc. But $\exp : \mathcal{O}(X) \to \mathcal{O}^\times(X)$ is not surjective: $z$ is not $e^{\ell}$ for any holomorphic $\ell$ on $X$ . The long exact sequence $\cdots \to \mathcal{O}(X) \to \mathcal{O}^\times(X) \to H^1(X, \underline{\Z}) \to \cdots$ sends $z$ to the generator of $H^1(X, \underline{\Z}) \cong \Z$ : its winding number.

Definition— Čech cohomology

For a sheaf of abelian groups $F$ and an open cover $\mathcal{U} = (U_i)_{i \in I}$ with $I$ totally ordered, set $U_{i_0 \cdots i_p} = U_{i_0} \cap \dots \cap U_{i_p}$ and $\check C^p(\mathcal{U}, F) = \prod_{i_0 \lt \dots \lt i_p} F(U_{i_0 \cdots i_p})$ , with differential $(\delta c)_{i_0 \cdots i_{p+1}} = \sum_{k=0}^{p+1} (-1)^k\, c_{i_0 \cdots \widehat{i_k} \cdots i_{p+1}} \big|_{U_{i_0 \cdots i_{p+1}}}$ . The Čech cohomology $\check H^p(\mathcal{U}, F)$ is the cohomology of this complex. By the sheaf axioms, $\check H^0(\mathcal{U}, F) = F(X)$ .

Example— The circle

Cover $S^1$ by two open arcs $U_1, U_2$ whose intersection is two disjoint arcs, and take $F = \underline{\Z}$ . Then $\check C^0 = \underline{\Z}(U_1) \times \underline{\Z}(U_2) = \Z^2$ and $\check C^1 = \underline{\Z}(U_1 \cap U_2) = \Z^2$ , and $\delta(a, b) = (b - a, b - a)$ . The kernel is the diagonal, so $\check H^0 = \Z$ (global locally constant functions), and the cokernel is $\Z^2 / \{(c, c)\} \cong \Z$ , so $\check H^1 = \Z$ . A cocycle $(m, n)$ describes "local constants that jump by $m$ on one overlap and $n$ on the other"; only the difference $n - m$ survives, and it is the obstruction to gluing — the same integer as the winding number above.

On a manifold, when the cover is good (all non-empty finite intersections are contractible), Čech cohomology of $\underline{\Z}$ agrees with singular cohomology. The general definition is Grothendieck's: $H^n(X, -)$ are the right derived functors of the global sections functor $F \mapsto F(X)$ on sheaves of abelian groups. The de Rham theorem is a theorem about sheaves: on a smooth manifold the sequence $0 \to \underline{\R} \to \Omega^0 \xrightarrow{d} \Omega^1 \xrightarrow{d} \cdots$ is exact on stalks — that is precisely the Poincaré lemma — and the sheaves $\Omega^k$ have no higher cohomology (partitions of unity), so $H^k(M, \underline{\R})$ is computed by global forms: $H^k(M; \R) \cong H^k_{\mathrm{dR}}(M)$ .

Formal mathematicsF

Sheaves in Lean

To keep every definition visible, the independent part of the formalisation uses a small notion of presheaf of types on the open sets of a space, with the sheaf condition stated as "compatible local sections glue uniquely" — a single ∃! that packages locality and gluing. (Mathlib's TopCat.Presheaf is a functor (Opens X)ᵒᵖ ⥤ C; its sheaf condition is equivalent to ours for presheaves of types.)

PresheafLean 4Formally verified

/-- A **presheaf of sets** on `X`: a set of sections `sec U` for every open `U`, and restriction
maps `sec V → sec U` for `U ⊆ V`, such that restricting to `U` itself does nothing and restricting
in two steps is restricting in one. Equivalently, a functor `O(X)ᵒᵖ → Set`
(Mathlib: `TopCat.Presheaf (Type v) X`). -/
structure Presheaf (X : Type u) [TopologicalSpace X] where
  /-- The sections over each open set. -/
  sec : Opens X → Type v
  /-- Restriction from `V` to a smaller open set `U`. -/
  res : ∀ {U V : Opens X}, U ≤ V → sec V → sec U
  /-- Restricting to the same open set is the identity. -/
  res_id : ∀ (U : Opens X) (s : sec U), res (le_refl U) s = s
  /-- Restriction is transitive: `(s|_V)|_U = s|_U`. -/
  res_res : ∀ {U V W : Opens X} (hUV : U ≤ V) (hVW : V ≤ W) (s : sec W),
    res hUV (res hVW s) = res (hUV.trans hVW) s

Axioms used: propext, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

IsSheafLean 4Formally verified

/-- The **sheaf condition**: whenever opens `Uᵢ ⊆ V` cover `V` and sections `sᵢ ∈ F(Uᵢ)` agree
on every overlap `Uᵢ ∩ Uⱼ`, there is exactly one section `t ∈ F(V)` restricting to every `sᵢ`.
"Exactly one" packages both axioms: *gluing* (existence) and *locality* (uniqueness). This is the
statement that `F(V) → ∏ F(Uᵢ) ⇉ ∏ F(Uᵢ ∩ Uⱼ)` is an equaliser. -/
def IsSheaf (F : Presheaf.{u, v} X) : Prop :=
  ∀ (V : Opens X) (ι : Type u) (U : ι → Opens X) (hU : ∀ i, U i ≤ V) (_hcov : V ≤ ⨆ i, U i)
    (s : ∀ i, F.sec (U i)),
    (∀ i j, F.res inf_le_left (s i) = F.res inf_le_right (s j)) →
      ∃! t : F.sec V, ∀ i, F.res (hU i) t = s i

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

Proposition 1, and the failure of constant presheaves at the empty set:

sec_emptyLean 4Proved here from basic factsFormally verified

/-- **A sheaf has exactly one section over the empty set.** The empty set is covered by the empty
family; the compatibility condition is vacuous, so "exactly one gluing" means exactly one section
over `∅`. -/
theorem sec_empty (F : Presheaf.{u, v} X) (hF : IsSheaf F) :
    Nonempty (F.sec ⊥) ∧ ∀ s t : F.sec ⊥, s = t := by
  obtain ⟨t, -, huniq⟩ := hF ⊥ PEmpty (fun i => i.elim) (fun i => i.elim) bot_le
    (fun i => i.elim) (fun i => i.elim)
  exact ⟨⟨t⟩, fun s s' => (huniq s (fun i => i.elim)).trans (huniq s' (fun i => i.elim)).symm⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

constPresheafLean 4Formally verified

/-- The **constant presheaf** with value `A`: every open set, including `∅`, gets the set `A`, and
every restriction map is the identity. -/
def constPresheaf (A : Type v) : Presheaf.{u, v} X where
  sec _ := A
  res _ a := a
  res_id _ _ := rfl
  res_res _ _ _ := rfl

Axioms used: propext, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

const_not_sheafLean 4Proved here from basic factsFormally verified

/-- **Constant presheaves are usually not sheaves.** If `A` has two different elements, the
constant presheaf has two sections over `∅`, but a sheaf has only one. (Even after repairing the
value at `∅`, gluing fails on any disconnected open set; the sheafification is the sheaf of
locally constant functions — see the lesson.) -/
theorem const_not_sheaf (A : Type v) (a b : A) (hab : a ≠ b) :
    ¬ IsSheaf (constPresheaf (X := X) A) := by
  intro hF
  exact hab ((sec_empty _ hF).2 a b)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

Proposition 2: continuous maps into any space form a sheaf. The glued map is built with Mathlib's ContinuousMap.liftCover, which is exactly the "continuity is local" argument of the proof.

contPresheafLean 4Formally verified

/-- The **presheaf of continuous maps** into a space `Y`: over `U`, the continuous maps `U → Y`;
restriction is restriction of functions. -/
def contPresheaf (Y : Type v) [TopologicalSpace Y] : Presheaf.{u, max u v} X where
  sec U := C(U, Y)
  res h f := f.comp ⟨fun x => ⟨x.1, h x.2⟩, by fun_prop⟩
  res_id _ _ := rfl
  res_res _ _ _ := rfl

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

cont_isSheafLean 4Proved here from basic factsFormally verified

/-- **Continuous functions form a sheaf: continuity is local.** Compatible continuous maps
`sᵢ : Uᵢ → Y` define a single function on `V = ⋃ Uᵢ` (well defined because they agree on
overlaps), which is continuous because it is continuous near every point; and two functions that
agree on every `Uᵢ` agree on `V`. The gluing is Mathlib's `ContinuousMap.liftCover`. -/
theorem cont_isSheaf (Y : Type v) [TopologicalSpace Y] :
    IsSheaf (contPresheaf (X := X) Y) := by
  intro V ι U hU hcov s hcomp
  -- every point of `V` lies in some `Uᵢ`
  have hmem : ∀ x : V, ∃ i, (x : X) ∈ U i := fun x => by
    simpa [Opens.mem_iSup] using hcov x.2
  -- the pieces `Uᵢ`, seen as subsets of `V`, and the local maps on them
  let S : ι → Set V := fun i => {x | (x : X) ∈ U i}
  let φ : ∀ i, C(S i, Y) := fun i => (s i).comp ⟨fun x => ⟨x.1.1, x.2⟩, by fun_prop⟩
  -- compatibility on overlaps
  have hφ : ∀ i j (x : V) (hxi : x ∈ S i) (hxj : x ∈ S j), φ i ⟨x, hxi⟩ = φ j ⟨x, hxj⟩ := by
    intro i j x hxi hxj
    exact congrArg (fun f : C((U i ⊓ U j : Opens X), Y) => f ⟨x.1, hxi, hxj⟩) (hcomp i j)
  -- each `Sᵢ` is open in `V`, so the pieces form a neighbourhood cover
  have hS : ∀ x : V, ∃ i, S i ∈ nhds x := fun x => by
    obtain ⟨i, hi⟩ := hmem x
    exact ⟨i, ((U i).isOpen.preimage continuous_subtype_val).mem_nhds hi⟩
  refine ⟨ContinuousMap.liftCover S φ hφ hS, ?_, ?_⟩
  · -- the glued map restricts to each `sᵢ`
    intro i
    refine ContinuousMap.ext (X := U i) (Y := Y) fun x => ?_
    exact ContinuousMap.liftCover_coe (S := S) (φ := φ) (hφ := hφ) (hS := hS) (i := i)
      (⟨⟨x.1, hU i x.2⟩, x.2⟩ : S i)
  · -- any other map with the same restrictions is equal to it
    intro t ht
    refine ContinuousMap.ext (X := V) (Y := Y) fun x => ?_
    obtain ⟨i, hi⟩ := hmem x
    have h1 := congrArg (fun f : C(U i, Y) => f ⟨x.1, hi⟩) (ht i)
    have h2 := ContinuousMap.liftCover_coe (S := S) (φ := φ) (hφ := hφ) (hS := hS) (i := i)
      (⟨x, hi⟩ : S i)
    exact h1.trans h2.symm

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

Theorem 3, with germs defined by agreement on a neighbourhood: choose a neighbourhood for each point, observe that they cover, and apply uniqueness of gluing.

SameGermLean 4Formally verified

/-- Two sections over `U` have the **same germ at `x`** if they agree on some smaller open
neighbourhood of `x`. The stalk `F_x` is the set of equivalence classes. -/
def SameGerm (F : Presheaf.{u, v} X) {U : Opens X} (x : X) (s t : F.sec U) : Prop :=
  ∃ (W : Opens X) (hWU : W ≤ U), x ∈ W ∧ F.res hWU s = F.res hWU t

Axioms used: propext, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

eq_of_sameGermLean 4Proved here from basic factsFormally verified

/-- **A section of a sheaf is determined by its germs.** If `s, t ∈ F(U)` have the same germ at
every point of `U`, choose for each `x` a neighbourhood `W_x` on which they agree. The `W_x` cover
`U`, and `s` and `t` both glue the compatible family `s|_{W_x}`, so by uniqueness `s = t`. -/
theorem eq_of_sameGerm (F : Presheaf.{u, v} X) (hF : IsSheaf F) {U : Opens X} (s t : F.sec U)
    (h : ∀ x ∈ U, SameGerm F x s t) : s = t := by
  -- choose the neighbourhoods
  choose W hWU hxW heq using fun x : U => h x.1 x.2
  -- the family `s|_{W_x}` is compatible
  have hcomp : ∀ i j : U, F.res inf_le_left (F.res (hWU i) s)
      = F.res inf_le_right (F.res (hWU j) s) := by
    intro i j
    rw [F.res_res, F.res_res]
  -- the `W_x` cover `U`
  have hcov : U ≤ ⨆ x : U, W x := fun x hx =>
    Opens.mem_iSup.mpr ⟨⟨x, hx⟩, hxW ⟨x, hx⟩⟩
  obtain ⟨g, -, huniq⟩ := hF U U W hWU hcov (fun x => F.res (hWU x) s) hcomp
  exact (huniq s fun _ => rfl).trans (huniq t fun x => (heq x).symm).symm

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

Mathlib's sheaf theory supplies the rest. Its version of Theorem 3 uses the stalk defined as a colimit; Theorem 4 and the sheafification adjunction of Theorem 5 are in the library, as are a subobject classifier for sheaf categories (one of the topos axioms of Theorem 7) and the étale space, which is a covering space when the sheaf is locally constant:

functions_isSheafLean 4Applies a library theoremFormally verified

/-- In Mathlib's language: the presheaf `U ↦ (U → T)` of *all* functions into a type `T` is a
sheaf. This applies `TopCat.Presheaf.toType_isSheaf`. -/
theorem functions_isSheaf (X : TopCat.{u}) (T : Type u) : (X.presheafToType T).IsSheaf :=
  TopCat.Presheaf.toType_isSheaf X T

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

section_extLean 4Applies a library theoremFormally verified

/-- Mathlib's version of `eq_of_sameGerm`: two sections of a sheaf of sets with equal germs at
every point coincide. This applies `TopCat.Presheaf.section_ext`, where the germ is the canonical
map from sections into the stalk, defined as a colimit. -/
theorem section_ext {X : TopCat.{u}} (F : TopCat.Sheaf (Type u) X) (U : Opens X)
    (s t : F.1.obj (op U))
    (h : ∀ (x : X) (hx : x ∈ U), F.presheaf.germ U x hx s = F.presheaf.germ U x hx t) :
    s = t :=
  TopCat.Presheaf.section_ext F U s t h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

iso_iff_stalksLean 4Applies a library theoremFormally verified

/-- **A morphism of sheaves is an isomorphism if and only if it is an isomorphism on every
stalk.** This applies Mathlib's `TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso`. -/
theorem iso_iff_stalks {X : TopCat.{u}} {F G : TopCat.Sheaf (Type u) X} (f : F ⟶ G) :
    IsIso f ↔ ∀ x : X, IsIso ((TopCat.Presheaf.stalkFunctor (Type u) x).map f.1) :=
  TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso f

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

sheafification_adjunctionLean 4Applies a library theoremFormally verified

/-- **Sheafification is left adjoint to the inclusion of sheaves into presheaves.** This applies
Mathlib's `CategoryTheory.sheafificationAdjunction` for the Grothendieck topology of open covers
of `X`. -/
theorem sheafification_adjunction (X : TopCat.{u}) :
    Nonempty (presheafToSheaf (Opens.grothendieckTopology X) (Type u) ⊣
      sheafToPresheaf (Opens.grothendieckTopology X) (Type u)) :=
  ⟨sheafificationAdjunction _ _⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

subobject_classifierLean 4Applies a library theoremFormally verified

/-- **Sheaves form a topos (one axiom of it).** The category of sheaves of sets on `X` has a
subobject classifier — the sheaf `Ω` with `Ω(U)` the set of open subsets of `U`. This applies
Mathlib's instance for sheaves on an essentially small site (in `Mathlib.CategoryTheory.Topos`). -/
theorem subobject_classifier (X : TopCat.{u}) :
    HasSubobjectClassifier (Sheaf (Opens.grothendieckTopology X) (Type u)) :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

etale_coveringLean 4Applies a library theoremFormally verified

/-- **Locally constant sheaves are covering spaces.** If every point has a neighbourhood `U` on
which all germ maps `F(U) → F_y` are bijective (as for the sheaf of locally constant functions),
then the projection from the étale space of `F` to `X` is a covering map. This applies Mathlib's
`TopCat.Presheaf.EtaleSpace.isCoveringMap_base`. -/
theorem etale_covering {X : TopCat.{u}} (F : TopCat.Presheaf (Type u) X)
    (hF : ∀ x, ∃ U : Opens X, x ∈ U ∧ ∀ y (hyU : y ∈ U), Function.Bijective (F.germ U y hyU)) :
    IsCoveringMap (TopCat.Presheaf.EtaleSpace.base (F := F)) :=
  TopCat.Presheaf.EtaleSpace.isCoveringMap_base hF

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Sheaves.leanTry it in the Lean web editor

What is and is not formalised. Formalised independently: Proposition 1, the failure of the constant presheaf, Proposition 2 and Theorem 3, for our self-contained notion of sheaf. From Mathlib: the sheaf of functions, Theorem 3 with colimit stalks, Theorem 4, the sheafification adjunction, the subobject classifier of $\mathrm{Sh}(X)$ , and étale spaces of locally constant sheaves as covering spaces. Not formalised here: the equivalence between our IsSheaf and Mathlib's, Corollary 6, the topos structure in full, and sheaf cohomology (Mathlib has sheaf cohomology via derived functors in general, but we do not use it).

ComputationC

Sheaves on a finite space, exhaustively

On a finite space the sheaf condition involves finitely many covers, so it can be checked completely. The experiment works on the pseudocircle: it tests the constant presheaf, the constant presheaf repaired at $\varnothing$ , and the locally constant functions against every cover of every open set; computes the stalks $F_x = F(U_x)$ ; and computes Čech $H^0$ and $H^1$ of $\underline{\Z/2}$ for the cover by the two minimal neighbourhoods $U_c = \{a, b, c\}$ and $U_d = \{a, b, d\}$ , whose intersection $\{a, b\}$ has two components — the finite analogue of the two-arc cover of the circle.

Sheaves on finite spaces: gluing, stalks and a first H^1PythonExact computationExhaustive finite checkCounterexampleComputationally tested

"""Sheaves on finite topological spaces, checked exhaustively.

On a finite space every open cover is finite and every presheaf of finite sets
can be tested completely. We take the four-point "pseudocircle" (a finite model
of the circle), test the sheaf condition for every open set and every open
cover, compare the constant presheaf with the sheaf of locally constant
functions, compute stalks, and compute the Cech cohomology of the locally
constant sheaf Z/2 for a two-set cover. Exhaustive checks on one small space;
the general statements are the theorems of the lesson.
"""

from itertools import combinations, product

#: The pseudocircle: a, b open points, c, d closed points.
PSEUDOCIRCLE = ["a", "b", "c", "d"]
PSEUDOCIRCLE_OPENS = [set(), {"a"}, {"b"}, {"a", "b"}, {"a", "b", "c"},
                      {"a", "b", "d"}, {"a", "b", "c", "d"}]
#: A finite model of an interval: a open, c, d closed.
INTERVAL = ["a", "c", "d"]
INTERVAL_OPENS = [set(), {"a"}, {"a", "c"}, {"a", "d"}, {"a", "c", "d"}]

def opens_of(opens):
    """The open sets as frozensets, smallest first."""
    return sorted({frozenset(u) for u in opens}, key=lambda u: (len(u), sorted(u)))

def minimal_nbhd(x, opens):
    """The smallest open set containing x (it exists in a finite space)."""
    return frozenset.intersection(*[u for u in opens if x in u])

def locally_constant(u, opens, values):
    """Sections over u: functions u -> values constant on each U_x, x in u."""
    pts = sorted(u)
    sections = []
    for vals in product(values, repeat=len(pts)):
        f = dict(zip(pts, vals))
        if all(len({f[y] for y in minimal_nbhd(x, opens)}) == 1 for x in pts):
            sections.append(tuple(sorted(f.items())))
    return sections

def restrict(section, v):
    """Restrict a function (stored as sorted pairs) to the subset v."""
    return tuple((x, y) for x, y in section if x in v)

def constant_repaired(u):
    """The constant presheaf {0, 1} with a single section over the empty set."""
    return [0, 1] if u else [None]

def restrict_repaired(s, w):
    """Restriction for constant_repaired: identity, except onto the empty set."""
    return s if w else None

def sheaf_failures(opens, sec, res):
    """All (open set, cover) pairs where unique gluing fails."""
    failures = []
    for u in opens:
        subs = [w for w in opens if w <= u]
        for k in range(len(subs) + 1):
            for cover in combinations(subs, k):
                if frozenset().union(*cover) != u:
                    continue
                images = {}
                for s in sec(u):
                    key = tuple(res(s, w) for w in cover)
                    images[key] = images.get(key, 0) + 1
                compatible = [fam for fam in product(*[sec(w) for w in cover])
                              if all(res(fam[i], cover[i] & cover[j]) ==
                                     res(fam[j], cover[i] & cover[j])
                                     for i in range(k) for j in range(k))]
                if any(images.get(f, 0) != 1 for f in compatible) or \
                        len(images) != len(compatible):
                    failures.append((u, cover))
    return failures

def cech_h1_dimension(cover, opens):
    """dim over Z/2 of H^0 and H^1 for the locally constant sheaf Z/2 and a
    cover by two open sets U, V: C^0 = F(U) x F(V) -> C^1 = F(U & V)."""
    u, v = cover
    su = locally_constant(u, opens, (0, 1))
    sv = locally_constant(v, opens, (0, 1))
    suv = locally_constant(u & v, opens, (0, 1))
    image = set()
    kernel = 0
    for s, t in product(su, sv):
        diff = tuple((x, (a + b) % 2) for (x, a), (_, b) in
                     zip(restrict(s, u & v), restrict(t, u & v)))
        image.add(diff)
        kernel += all(a == 0 for _, a in diff)
    h0 = kernel.bit_length() - 1
    h1 = (len(suv) // len(image)).bit_length() - 1
    return h0, h1

def main():
    opens = opens_of(PSEUDOCIRCLE_OPENS)
    print("Pseudocircle X = {a, b, c, d}: a, b open points; 7 open sets")
    const = sheaf_failures(opens, lambda u: [0, 1], lambda s, w: s)
    print(f"constant presheaf U -> {{0,1}}: fails on {len(const)} (U, cover):")
    print("  U = empty set, empty cover (two sections over the empty set)")
    repaired = sheaf_failures(opens, constant_repaired, restrict_repaired)
    print(f"same, one section over the empty set: fails on {len(repaired)} pairs")
    disc = [(sorted(u), [sorted(w) for w in c]) for u, c in repaired
            if len(c) == 2][0]
    print(f"  e.g. U = {disc[0]} covered by {disc[1]}: 0 on one piece and 1")
    print("  on the other agree on the (empty) overlap but do not glue")

    def lc(u):
        return locally_constant(u, opens, (0, 1))
    good = sheaf_failures(opens, lc, restrict)
    print(f"locally constant functions to {{0,1}}: {len(good)} failures")
    print()
    print("number of sections of the locally constant sheaf F:")
    names = ["".join(sorted(u)) or "{}" for u in opens]
    print("  U:    " + "".join(f"{n:>6}" for n in names))
    print("  |F(U)|" + "".join(f"{len(lc(u)):>6}" for u in opens))
    stalks = {x: len(lc(minimal_nbhd(x, opens))) for x in PSEUDOCIRCLE}
    print(f"stalks F_x = F(U_x), sizes: {stalks}")
    print()
    uc, ud = frozenset("abc"), frozenset("abd")
    h0, h1 = cech_h1_dimension((uc, ud), opens)
    print(f"Cech, cover {{abc, abd}} of the pseudocircle: dim H^0 = {h0}, "
          f"dim H^1 = {h1}")
    iopens = opens_of(INTERVAL_OPENS)
    h0i, h1i = cech_h1_dimension((frozenset("ac"), frozenset("ad")), iopens)
    print(f"Cech, cover {{ac, ad}} of the finite interval: dim H^0 = {h0i}, "
          f"dim H^1 = {h1i}")
    print()
    print("Epistemic status: exhaustive over every open set and every open")
    print("cover of these two finite spaces, so for them the statements are")
    print("proved by enumeration. That the pseudocircle is a finite model of")
    print("the circle (McCord, 1966) is a theorem; the computation only agrees")
    print("with H^1(S^1; Z/2) = Z/2.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

As in the circle example, $H^1 \cong \Z/2$ for the pseudocircle, while for a three-point "interval", whose cover has connected overlap, $H^1 = 0$ . For these finite spaces the checks are exhaustive and so amount to proofs of the specific statements; that the pseudocircle models the circle is McCord's theorem.

Explore

Explore: local potentials that do not glue

The vortex field $\big( -y/(x^2 + y^2),\ x/(x^2 + y^2) \big)$ has zero curl away from the origin, so on every disc avoiding the origin it is the gradient of a local potential — a branch of the angle $\theta$ . These local potentials are sections of a sheaf (locally constant up to an additive constant, i.e. a torsor under $\underline{\R}$ ). Drag the loop around the origin: the circulation is $2\pi$ , so the local potentials cannot be glued into a global one. Move the loop off the origin: circulation $0$ .

A vortex: locally a gradient, globally not

Circulation around the origin is 2π: the local potentials θ do not glue.

Examples

F(x, y) = (−y/(x² + y²), x/(x² + y²))

Drag the gold centre (or click anywhere) to move the loop. With the keyboard, focus the centre and use the arrow keys.

Loop radiusr = 1.6Walk once around the loop45°

Turns so far: 0.09

Circulation: ∮ F·dr ≈ 6.2832 | ∬ curl F dA ≈ −0.0322
Flux out: ∮ F·n ds ≈ 0 | ∬ div F dA ≈ 0.1043
At the centre: curl F ≈ 0, div F ≈ 0, πr² ≈ 8.042
Index: 1

All values are numerical approximations (sums around the loop and over the disc).

The two sides differ: the field must fail to be smooth (or be undefined) somewhere inside the loop, so Green’s theorem does not apply to this loop.

Index 1 ≠ 0: walking once around the loop, the arrow makes 1 net full turns (negative means clockwise). A field that is continuous on the whole disc would have to vanish inside; this one is not (see above), and the point where it breaks down carries the index instead.

The same obstruction for the logarithm: follow a continuous branch of the argument of $z - a$ around a loop. When it comes back, it has changed by $2\pi$ times the winding number, so a branch chosen at the start disagrees with itself at the end exactly when the winding number is non-zero.

Winding around a hole

Continuing a branch of arg(z − a) around the loop changes it by 2π × the winding number.

Drag a hole to move it. Press Play to send the point around the loop, or use the slider. The small square marks the start.

Position on the loop

Winding number around p₁1

(1/2πi)∮ dz/(z − p₁) ≈ 1.000 + 0.000i

Turns swept so far by each dashed arrow:

p₁: 0.00

The winding number is found by adding up the small changes in direction of the arrow from the hole to the moving point, and dividing the total by 360°. Counter-clockwise counts as positive.

Two loops in the plane with one hole can be deformed into each other, without ever crossing the hole, exactly when they have the same winding number. In the language of topology: the fundamental group of the punctured plane — like that of a circle — is the integers, π₁ = ℤ.

A link to complex analysis: think of the plane as the complex numbers and of a hole as a point a. Then (1/2πi)∮ dz/(z − a) equals the winding number around a. The values above are computed numerically along the loop.

Exercises

1. Sheaves

Warm-upHuman

Which of these presheaves of real-valued functions on $\R$ are sheaves? (Select all that apply.)

Choose all that apply

U \mapsto

continuous functions on

U

U \mapsto

smooth functions on

U

U \mapsto

bounded continuous functions on

U

U \mapsto

constant functions on

U

U \mapsto

locally constant functions on

U

U \mapsto

restrictions of polynomials to

U

2. Sheaves

Warm-upHuman

How many sections does the sheaf $\underline{\Z/2}$ of locally constant $\Z/2$ -valued functions have over $U = (0, 1) \cup (2, 3) \cup (4, 5) \subset \R$ ?

3. Sheaves

CoreHuman

In the sheaf of continuous functions on $\R$ , which pair of functions has the same germ at $0$ ?

Choose one

f(x) = \max(0, x - 1)

and

g(x) = 0

f(x) = x

and

g(x) = \sin x

f(x) = 0

and

g(x) = x^2

f(x) = |x|

and

g(x) = x

4. Sheaves

CoreHuman

On $X = \C \setminus \{0\}$ , the morphism $\exp : \mathcal{O} \to \mathcal{O}^\times$ is surjective on every stalk. Is $\exp : \mathcal{O}(X) \to \mathcal{O}^\times(X)$ surjective?

Choose one

No:

z \in \mathcal{O}^\times(X)

has no global logarithm; the obstruction is its image in

H^1(X, \underline{\Z}) \cong \Z

, the winding number.Yes, by Theorem 4: surjective on stalks implies surjective on sections.Yes, because every non-vanishing holomorphic function has a logarithm.No, because

\exp

is not surjective on stalks at

0

5. Sheaves

CoreHuman

In the proof that a morphism of sheaves $\varphi : F \to G$ which is bijective on stalks is surjective on sections, local preimages $s^{(x)} \in F(V_x)$ of $t$ are glued. Why do $s^{(x)}$ and $s^{(y)}$ agree on $V_x \cap V_y$ ?

Choose one

Both map to

t|_{V_x \cap V_y}

, and

\varphi

is injective on sections (proved first, from injectivity on stalks and Theorem 3).Because

G

is a sheaf.Because they have the same value at the points of

V_x \cap V_y

.Because

\varphi_x

is surjective.

6. Sheaves

StretchHuman

Cover $S^1$ by three open arcs $U_1, U_2, U_3$ such that each pairwise intersection is a single (connected) arc and the triple intersection is empty. What is $\dim_{\Z/2} \check H^1(\mathcal{U}, \underline{\Z/2})$ ?

7. Sheaves

CoreFormal

Given a cover U : ι → Opens X of V with hU : ∀ i, U i ≤ V and a compatible family s, which conclusion in the definition of IsSheaf captures both locality and gluing?

Choose one

∃! t : F.sec V, ∀ i, F.res (hU i) t = s i∃ t : F.sec V, ∀ i, F.res (hU i) t = s i∀ t t' : F.sec V, (∀ i, F.res (hU i) t = F.res (hU i) t') → t = t'∀ i j, F.res inf_le_left (s i) = F.res inf_le_right (s j)

8. Sheaves

CoreComputational

Sections of the sheaf of all functions on a finite set are dictionaries. Write glue(sections) that takes a list of dictionaries (functions on subsets) and returns the single dictionary on the union that restricts to each of them, or None if two of them disagree on a common point.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Every presheaf is a sheaf." Constant presheaves usually are not (they fail at the empty set, and after repair on every disconnected open set), and neither are presheaves defined by global conditions, such as bounded functions or constant functions. A presheaf is a sheaf exactly when its sections are determined by, and can be assembled from, local data.

Misconception

"A sheaf is determined by its global sections." The sheaf of holomorphic functions on the Riemann sphere has only the constants as global sections (Liouville), the same as the constant sheaf $\underline{\C}$ , yet the two sheaves are very different. The twisted sheaf $T$ on $S^1$ has $T(S^1) = 0$ , like the zero sheaf, although all its stalks are $\Z$ . Sheaves are determined by their sections over all open sets, or by their stalks together with how germs fit together.

Misconception

"A morphism that is surjective on stalks is surjective on sections." The exponential map $\mathcal{O} \to \mathcal{O}^\times$ on $\C \setminus \{0\}$ is surjective on stalks but $z$ has no global logarithm. Injectivity, by contrast, is detected on stalks (Theorem 4's proof), and isomorphisms are detected on stalks.

Misconception

"The stalk at $x$ is the value at $x$ ." A germ remembers the section on a whole (arbitrarily small) neighbourhood. The functions $0$ and $x^2$ on $\R$ have the same value at $0$ but different germs; $0$ and $\max(0, x - 1)$ have the same germ at $0$ . For holomorphic functions a germ is the same as a convergent power series, which carries much more than one value.

ViewpointsH

Viewpoints

Topology— Sheaves are spaces over X; covering spaces are locally constant sheaves

The étale space construction is an equivalence between sheaves on $X$ and local homeomorphisms $E \to X$ ; under it, sections of the sheaf are continuous sections of $E \to X$ . Locally constant sheaves correspond to covering spaces, and for connected, locally path-connected, semi-locally simply connected $X$ both correspond to sets with an action of $\pi_1(X)$ — the twisted sheaf $T$ on the circle is the $\pi_1$ -set $\Z$ on which the generator acts by $-1$ . Sheaf cohomology with constant coefficients agrees with singular cohomology on such spaces, so algebraic topology can be rebuilt sheaf-theoretically, as Leray did. See also the fundamental group.

Geometry— Spaces defined by their functions

A smooth manifold is a space with a sheaf of rings locally isomorphic to $(\R^n, C^\infty)$ , a complex manifold one locally isomorphic to $(\C^n, \mathcal{O})$ , and a scheme one locally isomorphic to the spectrum of a commutative ring with its structure sheaf; morphisms are morphisms of locally ringed spaces. Vector bundles become locally free sheaves of modules, line bundles form the Picard group $H^1(X, \mathcal{O}_X^\times)$ , and the first Chern class is the connecting map of the exponential sequence (see vector bundles). Serre's theorems on coherent sheaves and Grothendieck's cohomology made sheaves the language of algebraic geometry.

Analysis— Analytic continuation and the Cousin problems

For holomorphic functions the identity theorem makes the étale space of $\mathcal{O}$ Hausdorff — germs that agree near a point agree on connected domains — and the Riemann surface of $\sqrt z$ or $\log z$ is a connected component of this étale space: Weierstrass's analytic continuation, made into a space. The étale space of continuous (or smooth) functions is not Hausdorff: the germs of $0$ and of a smooth function vanishing only on $(-\infty, 0]$ cannot be separated at $0$ . Classical existence problems become cohomology: the Mittag-Leffler and Cousin problems ask for meromorphic functions with prescribed principal parts, and their obstruction lies in $H^1(X, \mathcal{O})$ , which vanishes on domains of holomorphy (Cartan's Theorem B, following Oka). Sato's hyperfunctions are defined as cohomology classes with coefficients in $\mathcal{O}$ .

Logic— Truth varies over a space

In the topos $\mathrm{Sh}(X)$ , a proposition about sections has as truth value the open set where it holds, and the internal logic is intuitionistic: " $s = t$ or $s \neq t$ " holds only on the union of the interior of $\{s = t\}$ and the interior of its complement, which need not be all of $X$ . Kripke models of intuitionistic logic are sheaves on posets with the Alexandrov topology, and forcing arguments can be phrased in sheaf toposes. See elementary topos theory.

Category theory— Sheaves on a site

Only the poset $\mathcal{O}(X)$ and the notion of a covering family were used. Grothendieck replaced them by a category with a Grothendieck topology, and sheaves on such a site — for example the étale site of a scheme — give the cohomology theories behind the Weil conjectures. Sheafification is a left exact left adjoint, presheaf categories are free cocompletions, and Giraud's theorem characterises the categories of sheaves on sites intrinsically. See limits and colimits.

Physics— Contextuality as a missing global section

Samson Abramsky and Adam Brandenburger (2011) described quantum measurement scenarios by a presheaf assigning to each set of jointly measurable observables (a "context") the possible outcome distributions. The empirical data form a compatible family on the cover by contexts. Bell non-locality and Kochen–Specker contextuality are precisely the failure of such a family to come from a global section — a joint outcome assignment for all observables at once — and the obstruction can sometimes be detected by Čech cohomology. This is a precise mathematical reformulation of known theorems, not a new physical claim.

Computation— Cellular sheaves and data on networks

On a graph or cell complex, a cellular sheaf assigns a vector space to each vertex and edge and linear restriction maps from vertices to incident edges (Justin Curry, 2014). Global sections are consistent assignments of data across the network, $H^1$ measures irreconcilable local measurements, and the sheaf Laplacian (Jakob Hansen and Robert Ghrist, 2019) generalises the graph Laplacian, with its kernel equal to the global sections. These ideas are used for sensor fusion, distributed consensus and signal processing on networks.

History & global context

History and global context

Leray. Jean Leray created sheaf theory, together with spectral sequences, while a prisoner of war in Oflag XVII-A in Austria (1940–45), where he organised a university for fellow prisoners; his work appeared from 1945–46 and introduced the word faisceau.
The Cartan seminar. Henri Cartan's Paris seminar (1948–51) reformulated sheaves with open sets and étale spaces and developed sheaf cohomology. In Japan, Kiyoshi Oka's work on several complex variables, including his coherence theorem (1950), led — through Cartan's Theorems A and B (1951–53) — to the solution of the Cousin problems on Stein manifolds.
Algebraic geometry. Jean-Pierre Serre's Faisceaux algébriques cohérents (1955) brought sheaves into algebraic geometry, and Alexander Grothendieck's Tôhoku paper (1957) defined sheaf cohomology by derived functors. Roger Godement's Topologie algébrique et théorie des faisceaux (1958) became the standard reference. Grothendieck's sites and toposes (SGA 4, 1963–64, with Michael Artin and Jean-Louis Verdier) extended the theory far beyond spaces.
Analysis. Mikio Sato introduced hyperfunctions (1958–59) as sheaf cohomology classes, and the Kyoto school of Sato, Masaki Kashiwara and Takahiro Kawai developed microlocal analysis and $D$ -modules in sheaf-theoretic language.
Today. Sheaves are basic in algebraic and complex geometry, representation theory (perverse sheaves), logic and topos theory, and increasingly in applied topology, network science and the foundations of quantum theory.

Everywhere locally, nowhere globally

Restrict, compare, glue

Definitions

Examples and non-examples

Gluing, germs and stalks

A preview of sheaf cohomology

Sheaves in Lean

Sheaves on a finite space, exhaustively

Explore: local potentials that do not glue

Exercises

Common misconceptions

Viewpoints

History and global context

Further reading