Alphabeta Math
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

15 results · all verified · 14 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Presheaves Sheaves Stalks and Sheafification

1 · Prerequisites

2 · Summary

This page fixes the standard sheaf vocabulary on a topological space and keeps the route deliberately concrete. Opens form the indexing category, presheaves and sheaves are written in restriction notation, stalks are built from actual neighbourhood sections, and the first local tests are phrased in germs.

The second half keeps sheafification explicit rather than hiding it behind an abstract adjoint. The plus construction separates uniqueness from existence, double-plus gives the sheaf, stalks survive unchanged, and the universal property explains why image presheaves have to be sheafified before they become image sheaves.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-04Open item page →

The category of open subsets of a topological space

Definition

Let X be a topological space (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

The open-set category Open(X) has:

  • objects: the open subsets UX;
  • morphisms: for opens V,U, a unique morphism VU when VU, and no morphism otherwise.

Composition is forced by transitivity of inclusion, and identity morphisms are the inclusions UU. Thus Open(X) is a category (Category, object, morphism, domain, codomain, identity, composition, and hom-collection).

The arrows point in the same direction as inclusion. Therefore a contravariant functor on Open(X) sends an inclusion VU to a restriction map from the larger open set to the smaller one.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

A presheaf on a topological space

Definition

Let X be a topological space. A presheaf of sets on X is a contravariant functor F:Open(X)Set (Covariant functor, identity functor, composite functor, and contravariant functor, Sets and functions form the large locally small category Set).

Equivalently, a presheaf of sets on X consists of:

  • a set F(U) for every open set UX;
  • for every inclusion VU, a restriction map ρVU:F(U)F(V),

such that ρUU=idF(U) and, whenever WVU, ρWU=ρWVρVU.

Because the arrows of Open(X) are the inclusions VU with VU, contravariance is exactly the rule that sections over a larger open set restrict to sections over a smaller one.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Sections, restrictions, and global sections of a presheaf

Definition

Let F be a presheaf on a topological space X.

An element of F(U) is called a section of F over U. We also write Γ(U,F):=F(U).

If VU and sF(U), its restriction to V is sV:=ρVU(s)F(V).

A global section of F is a section over the whole space: Γ(X,F)=F(X).

The presheaf identities imply sU=s,(sV)W=sWfor WVU.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Morphisms of presheaves

Definition

Let F and G be presheaves on a topological space X. A morphism of presheaves φ:FG is a natural transformation (Natural transformation and its components) between the two contravariant functors on Open(X).

Equivalently, it is a family of maps φU:F(U)G(U) for every open UX, such that for every inclusion VU the square F(U) φU G(U)F(V) φV G(V) commutes, that is, φV(sV)=φU(s)Vfor all sF(U).

Composition and identities are taken componentwise.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Separated presheaves

Definition

Let F be a presheaf on a topological space X.

The presheaf F is separated when uniqueness of gluing holds: for every open set UX, every open cover U=iIUi, and every pair of sections s,tF(U), sUi=tUi for all iIs=t.

Thus a separated presheaf has the locality part of the sheaf axiom, but it may still fail existence of gluing.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

A sheaf on a topological space

Definition

Let F be a presheaf on a topological space X. We say that F is a sheaf if for every open set UX and every open cover U=iIUi, including the empty cover of , the following two conditions hold.

Locality. If s,tF(U) satisfy sUi=tUifor all iI, then s=t.

Gluing. If sections siF(Ui) satisfy siUiUj=sjUiUjfor all i,jI, then there exists sF(U) such that sUi=sifor all iI.

By locality, such a section s is automatically unique. Thus a sheaf is exactly a presheaf whose compatible local sections glue uniquely.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

A set-valued sheaf has a unique section over the empty open set

Statement

Let F be a sheaf of sets on a topological space X. Then F() is a singleton.

Facts & Assumptions

Given: A sheaf F on X.

[L1]

A sheaf satisfies locality and gluing for every open cover, including the empty cover of (A sheaf on a topological space).

Proof

technique · direct
1.1

Apply [L1] to the empty cover of . The empty family of local sections is vacuously compatible, so gluing produces at least one section sF().

L1given
2.1

Let tF(). Then t also restricts to the same empty family on the empty cover. By the uniqueness part of [L1], one has t=s. Therefore F()={s}.

L1step 1.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The sheaf axiom is the equalizer condition on a cover

Statement

Let F be a presheaf of sets on a topological space X. Then F is a sheaf if and only if, for every open set UX and every open cover U=iIUi, the restriction map e:F(U)iIF(Ui),e(s)=(sUi)iI, is an equalizer of the two maps d0,d1:iIF(Ui)(i,j)I×IF(UiUj), defined by d0((si))=(siUiUj)i,j,d1((si))=(sjUiUj)i,j.

Facts & Assumptions

Given: A presheaf F, an open set U, and an open cover U=iIUi.

[L1]

A sheaf is exactly a presheaf satisfying locality and unique gluing for every open cover (A sheaf on a topological space).

[F1]

The notation sUi and siUiUj is the presheaf restriction notation (Sections, restrictions, and global sections of a presheaf).

[L2]

An equalizer of parallel maps f,g:AB is a morphism e:EA with fe=ge such that any h:TA with fh=gh factors uniquely through e (Equalizers and coequalizers as limits and colimits of a parallel pair).

Proof

technique · direct
1.1

Assume F is a sheaf. For any sF(U), the two families d0(e(s)) and d1(e(s)) are equal because both entries on UiUj are the common restriction sUiUj by [F1]. Thus d0e=d1e.

L1F1
1.2

Let (si)iIiF(Ui) satisfy d0((si))=d1((si)). Unwinding the definitions, this says exactly that siUiUj=sjUiUj for all i,j. By the gluing clause of [L1], there exists a unique sF(U) with sUi=si for all i. Hence every equalizing family factors uniquely through e, so [L2] shows that e is an equalizer.

L1L2F1
2.1

Conversely, assume e is an equalizer for every open set and cover. If s,tF(U) satisfy sUi=tUi for all i, then e(s)=e(t). Let be a singleton and define h:{}iF(Ui) by h()=e(s)=e(t). Then d0h=d1h, so [L2] gives a unique u:{}F(U) with eu=h. The two maps sending to s and to t both satisfy this condition, hence are equal and therefore s=t. So locality holds. If (si) is a compatible family on the cover, then d0((si))=d1((si)), so [L2] yields a unique sF(U) with e(s)=(si). That is exactly unique gluing. Therefore [L1] implies that F is a sheaf.

L1L2F1
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The sheaf condition can be checked on a basis with basis-refinable intersections

Statement

Let X be a topological space and let B be a basis for its topology such that whenever B,BB and xBB, there exists CB with xCBB. Let F be a presheaf on X. Then F is a sheaf if and only if the following condition holds:

for every open set UX, every cover U=iIBi by basis elements BiB, and every family siF(Bi) such that siC=sjC for every basis element CB with CBiBj, there exists a unique section sF(U) with sBi=si for all i.

Facts & Assumptions

Given: A basis B as in the statement and a presheaf F on X.

[L1]

A basis means that every open set and every point of it admit a containing basis element inside that open set (Basis and subbasis for a topology, and the topology generated by a family of sets).

[L2]

A sheaf is a presheaf with locality and unique gluing on every open cover (A sheaf on a topological space).

Proof

technique · direct
1.1

Assume F is a sheaf. Let U=iBi be a basis cover and let (si) satisfy the basis-overlap hypothesis. Fix i,j. The sets CB with CBiBj cover BiBj by [L1] and the intersection hypothesis on B. On each such C the restrictions of si and sj agree, so locality from [L2] gives siBiBj=sjBiBj. Gluing in [L2] then produces a unique sF(U) with sBi=si.

L1L2
1.2

Assume the displayed basis condition. Let U=αAUα be an arbitrary open cover and let tαF(Uα) be compatible on overlaps. For each xU, choose α(x) with xUα(x), and then choose BxB with xBxUα(x) by [L1]. Put rx:=tα(x)Bx.

L1givenchoose
1.3

By the assumed basis condition, there is a unique sF(U) with sBx=rx for every xU.

given
2.1

Let CB satisfy CBxBy. Then CUα(x)Uα(y), so compatibility of the original family gives rxC=tα(x)C=tα(y)C=ryC. Therefore the family (rx)xU satisfies the displayed basis condition for the basis cover U=xUBx.

step 1.2given
3.1

Fix αA. For each yUα, choose CyB with yCyByUα by [L1] and the basis-refinement hypothesis. Then the Cy form a basis cover of Uα. Since CyUα(y)Uα, step 2.1 gives ryCy=tα(y)Cy=tαCy. Because sCy=ryCy by step 1.3, the two sections sUα and tα restrict to the same family on the basis cover {Cy}yUα. By the uniqueness part of the assumed basis condition, sUα=tα. Since this holds for every α, the arbitrary compatible family glues uniquely, so [L2] implies that F is a sheaf.

L1L2step 2.1step 1.3givenchoose
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Presheaves and sheaves of groups, rings, and modules

Definition

Let X be a topological space. Fix a ring R when modules are under discussion.

A presheaf of groups on X is a presheaf F such that every F(U) is a group and every restriction map ρVU:F(U)F(V) is a group homomorphism (Groups and group homomorphisms form the large locally small category Grp).

A presheaf of rings on X is defined the same way with rings and ring homomorphisms (Unital rings and unit-preserving ring homomorphisms form the large locally small category Ring).

A presheaf of left R-modules on X is defined the same way with left R-modules and R-linear maps (Left modules over a fixed ring and module homomorphisms form the large locally small category R-Mod).

A sheaf of groups, sheaf of rings, or sheaf of left R-modules is such a presheaf whose underlying set-valued presheaf is a sheaf.

In particular, each sheaf of groups has a distinguished identity section on every open set; in additive notation this section is written 0, and all restrictions preserve the algebraic operations.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Sheafhood of algebraic-structure valued presheaves is detected on underlying sets

Statement

Let R be a ring, and let F be a presheaf of groups, rings, or left R-modules on a topological space X. Then F is a sheaf in the corresponding algebraic category if and only if its underlying presheaf of sets is a sheaf.

Facts & Assumptions

Given: A ring R and a presheaf F of groups, rings, or left R-modules on X.

[F1]

Such a presheaf is, by definition, a set-valued presheaf together with objectwise algebraic operations preserved by restriction maps; it is called a sheaf exactly when the underlying set-valued presheaf is a sheaf (Presheaves and sheaves of groups, rings, and modules).

[L1]

The sheaf condition itself is the locality and unique-gluing condition for the underlying sets of sections (A sheaf on a topological space).

Proof

technique · direct
1.1

If F is a sheaf of groups, rings, or left R-modules, then [F1] already says that its underlying set-valued presheaf is a sheaf.

F1
2.1

Conversely, assume the underlying set-valued presheaf is a sheaf. The sets F(U) already carry the given group, ring, or left R-module structures, and the restriction maps already preserve those structures by [F1]. Since [L1] tests only locality and gluing of the underlying sections, the assumed setwise sheaf condition is exactly the required algebra-valued sheaf condition.

F1L1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The stalk of a presheaf at a point

Definition

Let F be a presheaf on a topological space X, and let xX.

The neighbourhood category of x is the full subcategory NxOpen(X) whose objects are the open neighbourhoods of x. Its opposite category is filtered in the sense of Filtered categories and filtered colimits: it is nonempty because X itself is a neighbourhood of x, and for neighbourhoods U,V the intersection UV is again a neighbourhood of x with arrows UUV,VUV in the opposite category.

Because F is contravariant, its restriction to the neighbourhood category determines a covariant diagram on that opposite category. The stalk of F at x is the filtered colimit Fx:=limNxopF(U).

Concretely, Fx may be described as equivalence classes of pairs (U,s) with U an open neighbourhood of x and sF(U), where (U,s)(V,t) when s and t agree on some smaller open neighbourhood of x. The next lemma verifies that this is an equivalence relation.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Equality on a smaller neighbourhood defines the germ equivalence relation

Statement

Let F be a presheaf on a topological space X and let xX. For pairs (U,s) and (V,t) with xUV, define (U,s)x(V,t) when there exists an open neighbourhood W of x with WUV and sW=tW. Then x is an equivalence relation.

Facts & Assumptions

Given: A presheaf F on X and a point xX.

[F1]

The stalk is built from pairs (U,s) modulo equality on a smaller neighbourhood of x (The stalk of a presheaf at a point).

[F2]

An equivalence relation is one that is reflexive, symmetric, and transitive (Equivalence relation, equivalence class, and the quotient set A/).

Proof

technique · direct
1.1

Reflexivity holds because if (U,s) is any pair, then sU=sU, so (U,s)x(U,s). Symmetry holds because sW=tW implies tW=sW on the same neighbourhood W.

F1F2
1.2

Suppose (U,s)x(V,t) and (V,t)x(Z,r). Choose neighbourhoods W1UV and W2VZ with sW1=tW1 and tW2=rW2. Then W:=W1W2 is an open neighbourhood of x contained in UZ, and on W one has sW=tW=rW. Hence (U,s)x(Z,r).

F1given
2.1

Steps 1.1 and 1.2 show that x is reflexive, symmetric, and transitive. By [F2], it is an equivalence relation.

F2step 1.1step 1.2
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Germs of sections

Definition

Let F be a presheaf on X, let xX, and let sF(U) for some open set U containing x.

The class of the pair (U,s) in the stalk Fx is called the germ of s at x, and it is denoted by sxFx.

For every open set U containing x, this gives a canonical map F(U)Fx,ssx.

If VU is open and also contains x, then (sV)x=sx, because the two pairs (U,s) and (V,sV) agree on the smaller open neighbourhood V.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A section of a sheaf of groups is zero exactly when all of its germs are zero

Statement

Let F be a sheaf of groups on a topological space X, let UX be open, and let sF(U). Then s=0 in F(U)sx=0 in Fx for every xU.

Facts & Assumptions

Given: A sheaf of groups F, an open set U, and a section sF(U).

[F1]

A sheaf of groups has an identity section on every open set; when the group law is written additively, this section is denoted by 0, and all restrictions preserve it (Presheaves and sheaves of groups, rings, and modules).

[L1]

A sheaf is determined by local agreement of sections on an open cover (A sheaf on a topological space).

[F2]

The germ sx is the class of s in the stalk at x (Germs of sections).

Proof

technique · direct
1.1

If s=0 in F(U), then for every xU the induced germ is sx=0x because the stalk map respects restriction and the zero section by [F1] and [F2].

F1F2
1.2

Assume sx=0 for every xU. Fix xU. By [F2], equality of germs means that there exists an open neighbourhood VxU of x such that sVx=0Vx. The sets Vx cover U.

F2given
2.1

On the open cover {Vx}xU, the sections s and 0 have the same restriction by step 1.2. Locality in [L1] therefore gives s=0 in F(U). Together with step 1.1, this proves both directions.

L1step 1.1step 1.2
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Morphisms of sheaves are determined by their maps on stalks

Statement

Let φ,ψ:FG be morphisms of sheaves of sets on a topological space X. If the induced maps on stalks φx,ψx:FxGx are equal for every xX, then φ=ψ.

Facts & Assumptions

Given: Two morphisms of sheaves φ,ψ:FG.

[F1]

A morphism of presheaves is given by component maps compatible with restriction (Morphisms of presheaves).

[F2]

The stalk construction sends a morphism of presheaves to induced maps on stalks, and for every sF(U) and xU one has (φU(s))x=φx(sx) (Morphisms of presheaves, The stalk of a presheaf at a point, Germs of sections).

[F3]

Two germs at x are equal exactly when their representing sections agree on some smaller neighbourhood of x (The stalk of a presheaf at a point).

[L1]

Sections of a sheaf are equal once they agree on an open cover (A sheaf on a topological space).

Proof

technique · direct
1.1

Fix an open set UX and a section sF(U). For every xU, the hypothesis φx=ψx and [F2] give (φU(s))x=φx(sx)=ψx(sx)=(ψU(s))x.

F2given
2.1

By [F3], equality of the germs in step 1.1 means that for each xU there exists an open neighbourhood VxU such that φU(s)Vx=ψU(s)Vx. The sets Vx cover U.

F3step 1.1
3.1

By [L1], the two sections φU(s) and ψU(s) are equal on U. Since U and s were arbitrary, the component maps φU and ψU agree for every open U. Therefore φ=ψ by [F1].

F1L1step 2.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A morphism of sheaves is an isomorphism exactly when it is an isomorphism on every stalk

Statement

Let φ:FG be a morphism of sheaves of sets on a topological space X. Then φ is an isomorphism if and only if, for every xX, the induced map on stalks φx:FxGx is a bijection.

Facts & Assumptions

Given: A morphism of sheaves φ:FG.

[F1]

A morphism of presheaves is an isomorphism when it has a two-sided inverse whose components commute with restriction (Morphisms of presheaves).

[F2]

The stalk construction sends morphisms of presheaves to induced stalk maps, and for every sF(U) and xU one has (φU(s))x=φx(sx) (Morphisms of presheaves, The stalk of a presheaf at a point, Germs of sections).

[F3]

Two germs at x are equal exactly when their representing sections agree on some smaller neighbourhood of x (The stalk of a presheaf at a point).

[L2]

A sheaf is glued from local sections that agree on overlaps (A sheaf on a topological space).

Proof

technique · direct
1.1

If φ is an isomorphism with inverse ψ, then for every x the induced maps φx and ψx are inverse because taking stalks preserves composition and identities by [F2]. Hence each φx is a bijection.

F1F2
1.2

Assume now that every φx is a bijection. Fix an open set UX and a section tG(U). For each xU, choose axFx with φx(ax)=tx. Pick a representative sxF(Vx) of ax on some open neighbourhood VxU of x. Then (φVx(sx))x=tx, so [F3] lets us shrink Vx and assume φVx(sx)=tVx.

F2F3givenchoose
1.3

If s,sF(U) satisfy φU(s)=φU(s), then for every xU one has φx(sx)=φx(sx) by [F2]. Injectivity of φx gives sx=sx. By [F3], for each x there exists an open neighbourhood WxU with sWx=sWx. The sets Wx cover U, so [L2] gives s=s. Thus each φU is injective.

F2F3L2
2.1

Let x,yU. For any zVxVy, the two sections sxVxVy and syVxVy have images under φ whose germs at z both equal tz. Since φz is injective, the germs of sx and sy at z are equal. By [F3], there is a neighbourhood WzVxVy of z on which sxWz=syWz. The sets Wz cover VxVy, so [L2] gives sxVxVy=syVxVy. Therefore the family (sx) is compatible on the cover {Vx}xU of U.

F2F3L2step 1.2
3.1

By [L2], the compatible family of step 2.1 glues to a unique section ψU(t)F(U) satisfying φU(ψU(t))=t. Thus φU is surjective for every U.

L2step 2.1construct
4.1

Let VU and tG(U). Then φV(ψU(t)V)=φU(ψU(t))V=tV=φV(ψV(tV)). Step 1.3 gives injectivity of φV, so ψU(t)V=ψV(tV). Hence the maps ψU commute with restriction and define a morphism of sheaves ψ:GF. By steps 3.1 and 1.3, ψ is a two-sided inverse to φ, so [F1] shows that φ is an isomorphism. Together with step 1.1 this proves both directions.

F1step 3.1step 1.3
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The etale space of a sheaf of sets

Definition

Let F be a sheaf of sets on a topological space X.

Its etale space is the disjoint union of stalks E(F):=xXFx, equipped with the projection p:E(F)X,p(ξ)=x if ξFx.

For every open set UX and every section sF(U), define the subset [s,U]:={sx:xU}E(F).

The topology on E(F) is the topology generated by the family of all such subsets [s,U] (Basis and subbasis for a topology, and the topology generated by a family of sets).

On each set [s,U], the projection p restricts to a bijection onto U with inverse U[s,U],xsx. The next theorem shows that this bijection is in fact a homeomorphism.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Sheaves of sets are equivalent to local homeomorphisms over the base space

Statement

Let X be a topological space. A continuous map q:EX is called a local homeomorphism if every point eE has an open neighbourhood W such that q(W) is open in X and qW:Wq(W) is a homeomorphism.

  1. For every sheaf of sets F on X, the projection p:E(F)X of The etale space of a sheaf of sets is a local homeomorphism.
  2. For every local homeomorphism q:EX, the assignment U{σ:UE continuous:qσ=idU} is a sheaf of sets on X.
  3. These two constructions are inverse up to natural isomorphism, so they give an equivalence between sheaves of sets on X and spaces over X whose structure map is a local homeomorphism.

Facts & Assumptions

Given: A sheaf F on X, or a local homeomorphism q:EX.

[F1]

The etale space E(F) is the disjoint union of the stalks with basic open sets [s,U], and p:[s,U]U is a bijection (The etale space of a sheaf of sets).

[L1]

A sheaf is glued uniquely from compatible local sections on any open cover (A sheaf on a topological space).

[F2]

Morphisms of presheaves are given by restriction-compatible component maps (Morphisms of presheaves).

Proof

technique · direct
1.1

For a sheaf F, let p:E(F)X be as in [F1]. If ξ=sxE(F), then ξ[s,U] for some section sF(U). By construction p:[s,U]U is bijective. Its inverse xsx is continuous because for any smaller basic open [t,V][s,U], the preimage is the open set {xUV:sx=tx}, which is open by the sheaf locality encoded in [L1]. Hence p[s,U] is a homeomorphism onto the open set U. Since every point of E(F) lies in some [s,U], p is a local homeomorphism.

F1L1
1.2

Let q:EX be a local homeomorphism, and let Secq(U) denote its continuous sections over an open set U. Restriction of a section is again a section, so Secq is a presheaf. If two sections of Secq(U) agree on an open cover, they are equal pointwise, so locality holds. If σiSecq(Ui) are compatible on an open cover U=iUi, define σ(x)=σi(x) for xUi. Compatibility makes this well defined, and continuity is local on the cover because each σi is continuous. Thus [L1] holds, so Secq is a sheaf.

L1given
1.3

A sheaf morphism φ:FG induces a map over X E(φ):E(F)E(G),sx(φU(s))x. This is well defined by restriction compatibility. It is continuous: if E(φ)(sx) lies in a basic open [t,V], equality of the two germs lets us shrink to an open WUV on which φU(s)W=tW; then [sW,W] is a neighbourhood of sx mapped into [t,V]. Identities and compositions are preserved. Conversely, a map f:EE over X between local homeomorphisms sends a section σ to fσ, naturally in the open set, and hence induces a sheaf morphism Sec(f).

F1F2given
2.1

For a sheaf F and an open set U, send sF(U) to the section θU(s):UE(F),θU(s)(x)=sx. By step 1.1 this is continuous. If θU(s)=θU(t), then sx=tx for all xU, so [L1] gives s=t. Conversely, let σ:UE(F) be a continuous section. For each xU, choose a basic open [sx,Vx] containing σ(x). Continuity makes Wx:=UVxσ1([sx,Vx]) an open neighbourhood of x. Since p is injective on [sx,Vx] and pσ=idU, the restriction σWx equals y(sx)y. These local sections agree on overlaps because they induce the same map σ. By [L1], they glue to a unique sF(U) with θU(s)=σ. Thus θU is a bijection, natural in U.

F1L1step 1.1
3.1

For a local homeomorphism q:EX, define η:EE(Secq) by sending eE to the germ at x=q(e) of any local section through e. Such a local section exists because q is a local homeomorphism, and two choices have the same germ because on a smaller common chart they are both the inverse of q. On a chart Wq(W), the map η is a homeomorphism from W onto the basic open defined by the inverse section. Hence η is an isomorphism over X. The formula E(φ)(sx)=(φU(s))x makes the bijections θ of step 2.1 natural in F, while the formula η(f(e))=(fσ)x makes η natural in E. Thus the two functors constructed in steps 1.2 and 1.3 are quasi-inverse equivalences.

step 1.1step 1.2step 2.1step 1.3
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The plus construction for a presheaf

Definition

Let F be a presheaf on a topological space X, and let UX be open.

A germ-compatible local presentation of a section over U consists of:

  • an open cover U=iIUi;
  • sections siF(Ui);

such that for every xUiUj the germs agree: (si)x=(sj)x in Fx.

Two germ-compatible local presentations (Ui,si) and (Vj,tj) over U are called equivalent if for every xU and every choice of indices i,j with xUiVj, one has (si)x=(tj)x in Fx.

The plus construction F+ is the presheaf defined by letting F+(U) be the set of equivalence classes of germ-compatible local presentations over U. Restriction to an open subset VU is obtained by replacing the cover Ui with UiV and restricting each section si to UiV.

There is a canonical morphism of presheaves η:FF+ whose component on U sends a section sF(U) to the class of the single-chart presentation (U,s).

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The first plus construction is separated and preserves stalks

Statement

Let F be a presheaf on a topological space X, and let η:FF+ be the canonical map of The plus construction for a presheaf. Then:

  1. F+ is a separated presheaf.
  2. For every xX, the induced map on stalks ηx:Fx(F+)x is a bijection.

Facts & Assumptions

Given: A presheaf F on X and its plus construction η:FF+.

[F1]

A section of F+(U) is an equivalence class of germ-compatible local presentations over U, and ηU(s) is represented by the single-chart presentation (U,s) (The plus construction for a presheaf).

[F2]

A separated presheaf is one in which equality of sections can be checked on an open cover (Separated presheaves).

[L1]

Equality in a filtered colimit of sets is eventual at some smaller common stage (Two representatives in a filtered colimit of sets are equal exactly when they become equal at one common later stage).

Proof

technique · direct
1.1

Let σ,τF+(U) and suppose there is an open cover U=αAWα such that σWα=τWα for every α. Fix xU, and choose α with xWα. Equality on Wα means that the two restricted presentations determine the same germ at x, so σ and τ have the same germ at x. Since this holds for every xU, the two global presentations are equivalent by [F1]. Therefore σ=τ, and F+ is separated by [F2].

F1F2
1.2

To prove surjectivity of ηx, let ξ(F+)x. Choose an open neighbourhood U of x and a section σF+(U) representing ξ. Pick a local presentation (Ui,si) of σ with xUi for some index i. Then on the neighbourhood Ui the section σ equals ηUi(si) by [F1], so the germ ξ is the image of the germ of si at x. Hence ηx is surjective.

F1givenchoose
1.3

Now suppose ηx(a)=ηx(b) in (F+)x, where aFx and bFx. Represent a and b by sections sF(U) and tF(V) on neighbourhoods of x. By [L1], equality of their images in the stalk of F+ means that there exists an open neighbourhood WUV of x such that ηW(sW)=ηW(tW) in F+(W). By [F1], equality of these two single-chart classes says exactly that sW and tW have the same germ at every point of W, in particular at x. Thus a=b in Fx, so ηx is injective.

F1L1given
2.1

Steps 1.2 and 1.3 prove that every ηx is bijective, and step 1.1 proves that F+ is separated.

step 1.1step 1.2step 1.3
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The second plus construction is a sheaf

Statement

For every presheaf F on a topological space X, the double plus construction F++=(F+)+ is a sheaf.

Facts & Assumptions

Given: A presheaf F on X.

[F1]

The plus construction records germ-compatible local presentations and single-chart classes (The plus construction for a presheaf).

[L1]

The first plus construction F+ is separated (The first plus construction is separated and preserves stalks).

[F2]

A sheaf is exactly a presheaf satisfying locality and unique gluing on every open cover (A sheaf on a topological space).

Proof

technique · direct
1.1

Let U=iIUi be an open cover and let σiF++(Ui) be compatible on overlaps. For each i, choose a presentation of σi by sections τi,aF+(Vi,a) on an open cover Ui=aVi,a.

F1givenchoose
2.1

The family of all pairs (Vi,a,τi,a) covers U. Presentations belonging to one fixed i are germ-compatible by definition. If xVi,aVj,c, compatibility of σi and σj says that their restrictions to UiUj are equal; the definition of equality of plus presentations therefore gives (τi,a)x=(τj,c)xin (F+)x. Thus the combined family is a germ-compatible presentation by F+-sections and defines σ(F+)+(U)=F++(U). On each Ui, its restricted presentation is equivalent to the chosen presentation of σi, so σUi=σi.

F1step 1.1construct
3.1

Apply [L1] to the presheaf F+. It says that (F+)+=F++ is separated. Hence sections of F++(U) whose restrictions agree on the cover {Ui} are equal, so locality and uniqueness of the gluing from step 2.1 hold.

L1step 2.1
4.1

Steps 2.1 and 3.1 give gluing and locality for every open cover. Therefore [F2] shows that F++ is a sheaf.

F2step 2.1step 3.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Sheafification of a presheaf

Definition

Let F be a presheaf on a topological space X.

Its sheafification is the sheaf aF:=F++.

The canonical morphism ηF:FaF is the composite F η F+ η (F+)+=aF, where each η is the single-chart map of The plus construction for a presheaf.

By The second plus construction is a sheaf, aF is indeed a sheaf.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Sheafification is left adjoint to the inclusion of sheaves into presheaves

Statement

Let F be a presheaf on a topological space X, let ηF:FaF be its sheafification map, and let G be a sheaf on X. Then every morphism of presheaves φ:FG factors uniquely through ηF: there is a unique morphism of sheaves φ:aFG such that φ=φηF.

Facts & Assumptions

Given: A presheaf F, a sheaf G, and a morphism φ:FG.

[F1]

Sheafification is the double plus construction with unit ηF:FaF (Sheafification of a presheaf).

[L1]

The first plus construction is separated (The first plus construction is separated and preserves stalks).

[L2]

The second plus construction is a sheaf (The second plus construction is a sheaf).

Proof

technique · direct
1.1

Let σF+(U) be represented by sections siF(Ui) on an open cover U=iUi. The sections φUi(si)G(Ui) have equal germs on overlaps because the si do. Since G is a sheaf, they glue uniquely to a section φU+(σ)G(U). This is independent of the chosen presentation because equivalent presentations have the same germs at every point, and a sheaf is separated. Thus φ extends uniquely to a morphism φ+:F+G.

F1L1L2givenconstruct
2.1

Apply the same construction again to the morphism φ+:F+G. Because G is already a sheaf, this yields a morphism φ:(F+)+=aFG whose restriction along the second unit map is φ+. Composing with the first unit map gives φηF=φ.

F1step 1.1construct
3.1

To prove uniqueness, let ψ,ψ:aFG satisfy ψηF=ψηF. Fix an open set U and a section σaF(U). By [F1], σ is represented locally by sections of F+, and each such local F+-section is itself locally represented by sections of F. Therefore U admits an open cover {Ui} and sections siF(Ui) such that σUi=ηF,Ui(si) for every i. On each Ui the hypothesis gives ψU(σ)Ui=ψUi(ηF,Ui(si))=ψUi(ηF,Ui(si))=ψU(σ)Ui. Since G is a sheaf, locality forces ψU(σ)=ψU(σ). Thus ψ=ψ.

F1L2step 2.1
4.1

Steps 2.1 and 3.1 prove that every morphism FG factors uniquely through ηF. This is the stated adjoint universal property.

F1step 2.1step 3.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Sheafification preserves stalks

Statement

Let F be a presheaf on a topological space X. For every xX, the sheafification map induces a bijection ηF,x:Fx  (aF)x.

Facts & Assumptions

Given: A presheaf F on X and a point xX.

[F1]

Sheafification is aF=(F+)+ with unit ηF:FaF (Sheafification of a presheaf).

[L1]

For any presheaf, the first plus construction preserves stalks (The first plus construction is separated and preserves stalks).

[F2]

Equality in a filtered-colimit stalk is eventual on a smaller neighbourhood (Two representatives in a filtered colimit of sets are equal exactly when they become equal at one common later stage).

Proof

technique · direct
1.1

Apply [L1] to the presheaf F. This gives a bijection Fx  (F+)x.

L1given
2.1

Apply [L1] again, now to the presheaf F+. Since [L1] holds for every presheaf, it yields a bijection (F+)x  ((F+)+)x=(aF)x. The reference to [F2] is the same eventual-equality argument used inside [L1] to prove injectivity on stalks.

L1F2step 1.1
3.1

Composing the bijections of steps 1.1 and 2.1 gives the required isomorphism Fx  (aF)x. By [F1], this composite is exactly the map induced by ηF.

F1step 1.1step 2.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Sheafification is idempotent

Statement

For every presheaf F on a topological space X, the canonical map ηaF:aFa(aF) is an isomorphism. Equivalently, sheafification is idempotent: a(aF)aF.

Facts & Assumptions

Given: A presheaf F on X.

[F1]

The object aF is the sheafification of F (Sheafification of a presheaf).

[L1]

Any map from a presheaf to a sheaf factors uniquely through its sheafification (Sheafification is left adjoint to the inclusion of sheaves into presheaves).

Proof

technique · direct
1.1

Since aF is already a sheaf by [F1], apply [L1] to the identity map 1aF:aFaF. There is a unique morphism ε:a(aF)aF such that εηaF=1aF.

F1L1
2.1

Apply [L1] again to the map ηaF:aFa(aF), whose target is also a sheaf. The identity map on a(aF) is one factorization through ηaF. The composite ηaFε is another, because step 1.1 gives (ηaFε)ηaF=ηaF. By uniqueness in [L1], ηaFε=1a(aF).

L1step 1.1
3.1

Steps 1.1 and 2.1 show that ε and ηaF are two-sided inverses. Therefore ηaF is an isomorphism, so a(aF)aF.

step 1.1step 2.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Subsheaves

Definition

Let G be a sheaf of sets on a topological space X.

A subsheaf of G is a sheaf H on X together with a morphism of presheaves ι:HG (Morphisms of presheaves) such that for every open set UX, the component ιU:H(U)G(U) is injective.

Equivalently, one may identify H(U) with a subset of G(U) for every open U, with restriction maps inherited from G, and then require that these subsets define a sheaf. A subpresheaf of a sheaf need not be a subsheaf, because it may fail gluing.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The image sheaf is the sheafification of the presheaf image

Statement

Let φ:FG be a morphism of sheaves of sets on a topological space X, and let I be the presheaf image I(U):=φU(F(U))G(U). Define the image sheaf J by J(U):={tG(U): for every xU there exists xVU and sF(V) with φV(s)=tV}. Then J is a subsheaf of G, φ factors through J, and the canonical map aIJ is an isomorphism. In particular, the image sheaf is the sheafification of the objectwise image presheaf.

Facts & Assumptions

Given: A morphism of sheaves φ:FG.

[F1]

A subsheaf is a sheaf whose sections embed objectwise into the ambient sheaf (Subsheaves).

[F2]

A morphism of presheaves is a compatible family of component maps (Morphisms of presheaves).

[L1]

Maps from a presheaf to a sheaf factor uniquely through sheafification (Sheafification is left adjoint to the inclusion of sheaves into presheaves).

Proof

technique · direct
1.1

The assignment UI(U) is a subpresheaf of G: if t=φU(s)I(U) and VU, then tV=φV(sV)I(V) by [F2].

F2given
1.2

The assignment J is a subsheaf of G. Indeed, restriction clearly preserves local representability. If sections tiJ(Ui) on an open cover of U agree on overlaps, then because G is a sheaf they glue to a unique tG(U). The local witnesses for each ti also witness that t lies in J(U). Thus J is a sheaf, and [F1] makes it a subsheaf. The factorization FJ is immediate from the definition of J.

F1F2given
2.1

Since I maps into the sheaf J, [L1] gives a unique morphism α:aIJ extending the inclusion IJ.

L1step 1.1step 1.2
2.2

Conversely, let tJ(U). Choose an open cover U=iUi and sections siF(Ui) with φUi(si)=tUi. Then the sections φUi(si)I(Ui) are compatible on overlaps because they all come from t. Hence they define a section βU(t)aI(U) by the very construction of sheafification. These assignments are compatible with restriction, so they define a morphism β:JaI.

L1step 1.2construct
3.1

The composites αβ and βα are identities, because both are identities locally on the chosen image sections that generate J and aI, and both targets are sheaves. Therefore α is an isomorphism.

L1step 2.1step 2.2
RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A single stalk does not determine a global section

If two sections have the same germ at one point, they only agree on some possibly tiny neighbourhood of that point. Nothing in The stalk of a presheaf at a point or Germs of sections lets one recover the values of either section away from that neighbourhood.

For example, on the sheaf of continuous real-valued functions on R, a function supported near 2 and the zero function have the same germ at 0 but are different global sections. Stalkwise arguments therefore need either all points at once or a neighbourhoodwise statement that can be glued.

5 · Examples, counterexamples and false statements

None yet.

Sources