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.

13 results · all verified · 10 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 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Sheaf Operations Exactness Ringed Spaces and Module Pullback

1 · Prerequisites

2 · Summary

This page collects the standard sheaf-theoretic operations attached to a continuous map and then adds the ringed-space structure needed for module pullback. The route stays concrete: direct and inverse image are defined on sections, stalks control exactness, and extension by zero is kept separate from ordinary direct image.

The second half passes from sheaves of abelian groups to sheaves of modules on ringed and locally ringed spaces. Tensor products, internal Hom, pullback, and gluing are written in the same local language so that later affine- and scheme-level pages can cite them without rebuilding the sheaf machinery.

3 · Logical flowchart

4 · Definitions, theorems and proofs

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

Direct image of a sheaf along a continuous map

Definition

Let f:XY be a continuous map, and let F be a presheaf on X. The direct image presheaf fF on Y is defined on an open set VY by

(fF)(V):=F(f1(V)).

If VV, the restriction map

(fF)(V)(fF)(V)

is the restriction map of F for the inclusion f1(V)f1(V).

Thus direct image is just precomposition of the presheaf with the inverse-image map on open sets.

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

Direct image preserves sheaves and objectwise algebraic structure

Statement

Let f:XY be a continuous map.

  1. If F is a sheaf on X, then fF is a sheaf on Y.
  2. If F is a sheaf of groups, rings, or modules on X, then fF is a sheaf of the same kind on Y.

Facts & Assumptions

Given: A continuous map f:XY.

[F1]

The direct image is defined by (fF)(V)=F(f1(V)) (Direct image of a sheaf along a continuous map).

[L1]

A sheaf is exactly a presheaf whose compatible local sections glue uniquely on every open cover (A sheaf on a topological space).

[L2]

A sheaf of groups, rings, or modules is a set-valued sheaf together with objectwise algebraic operations preserved by restriction (Presheaves and sheaves of groups, rings, and modules).

Proof

technique · direct
1.1

Let F be a sheaf on X, let V=iVi be an open cover in Y, and let si(fF)(Vi)=F(f1(Vi)) be compatible on overlaps. By [F1], the sets f1(Vi) cover f1(V), so [L1] gives a unique section sF(f1(V)) restricting to every si. This section is exactly an element of (fF)(V), so fF is a sheaf.

F1L1givenconstruct
2.1

If F is a sheaf of groups, rings, or modules, then each section set of fF is literally the corresponding section set of F over a preimage open set. Hence the algebraic operations are inherited objectwise, and the restriction maps are the same homomorphisms as before. By [L2] and step 1.1, fF is a sheaf of the same kind.

F1L2step 1.1
3.1

Steps 1.1 and 2.1 prove both assertions.

step 1.1step 2.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Inverse image presheaf and inverse image sheaf

Definition

Let f:XY be a continuous map, and let G be a presheaf on Y. The inverse-image presheaf

fpG

on X is defined by

(fpG)(U):=limf(U)VG(V),

where V runs over the open neighbourhoods of f(U) in Y, ordered by reverse inclusion. If UU, then every neighbourhood of f(U) is a neighbourhood of f(U), so there is a natural restriction map (fpG)(U)(fpG)(U).

The inverse image sheaf of a sheaf G on Y is the sheafification of this presheaf:

f1G:=a(fpG).

When U is open in X and V is an open set of Y with f(U)V, there is a canonical map

G(V)(fpG)(U)

into the colimit class represented by V.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Inverse image is left adjoint to direct image on sheaves

Statement

Let f:XY be a continuous map, let G be a sheaf on Y, and let F be a sheaf on X. Then there is a natural bijection HomX(f1G,F)HomY(G,fF).

Facts & Assumptions

Given: A continuous map f:XY, a sheaf G on Y, and a sheaf F on X.

[F1]

The direct image satisfies (fF)(V)=F(f1(V)) (Direct image of a sheaf along a continuous map).

[F2]

The inverse image is the sheafification of the neighbourhood-colimit presheaf fpG (Inverse image presheaf and inverse image sheaf).

[L1]

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

Proof

technique · direct
1.1

Let α:f1GF be a sheaf morphism. By [F2] and [L1], α corresponds uniquely to a presheaf morphism α~:fpGF.

F2L1given
1.2

Conversely, let β:GfF be a sheaf morphism. For an open UX, represent an element of (fpG)(U) by a pair (V,s) with f(U)V and sG(V), and define β~U([V,s]):=βV(s)UF(U), where the restriction is taken from F(f1(V)) to F(U). If (V,s) and (V,s) represent the same colimit class, then on some smaller open neighbourhood WVV of f(U) one has sW=sW, so βV(s)U=βV(s)U. Thus β~ is well defined and natural in U.

F1F2givenconstruct
2.1

For an open set VY and a section sG(V), let [V,s] denote its class in (fpG)(f1(V)), and define βV(s):=α~f1(V)([V,s])F(f1(V))=(fF)(V). If VV, naturality of α~ shows βV(sV)=βV(s)V, so the βV define a morphism β:GfF.

F1F2step 1.1construct
2.2

By [F2] and [L1], the presheaf morphism β~:fpGF factors uniquely through a sheaf morphism α:f1GF.

F2L1step 1.2construct
3.1

The constructions of steps 2.1 and 2.2 are inverse, because both are recovered from the same formula on representative classes [V,s]. Therefore HomX(f1G,F)HomY(G,fF) naturally in both sheaves.

step 2.1step 2.2
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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 an inverse image sheaf is the stalk over the image point

Statement

Let f:XY be a continuous map, let G be a sheaf on Y, and let xX. Then there is a canonical isomorphism

(f1G)xGf(x).

Facts & Assumptions

Given: A continuous map f:XY, a sheaf G on Y, and a point xX.

[F1]

The inverse image sheaf is the sheafification of the presheaf fpG (Inverse image presheaf and inverse image sheaf).

[F2]

A stalk is the colimit of sections over neighbourhoods of the point (The stalk of a presheaf at a point).

[L1]

Sheafification preserves stalks (Sheafification preserves stalks).

Proof

technique · direct
1.1

By [F1] and [L1], it is enough to identify the stalk (fpG)x.

F1L1given
1.2

If tG(V) with f(x)V, then xf1(V) and t defines a class [V,t](fpG)(f1(V)). Sending the germ tf(x) to the germ of [V,t] at x gives a map Φ:Gf(x)(fpG)x. If two representatives agree on a smaller neighbourhood of f(x), then their induced sections agree on the inverse image of that smaller neighbourhood, so Φ is well defined.

F1F2construct
1.3

Conversely, represent a germ in (fpG)x by a section [V,t](fpG)(U) with xU and f(U)V. Since f(x)V, the section t has a germ tf(x)Gf(x). This depends only on the original germ at x, because equality of germs in (fpG)x means equality after restricting to some smaller neighbourhood of x, hence after restricting t and t to some common neighbourhood of f(x). Thus there is a map Ψ:(fpG)xGf(x).

F1F2construct
2.1

The maps Φ and Ψ are inverse on representatives, so (fpG)xGf(x). Step 1.1 then gives (f1G)xGf(x).

step 1.1step 1.2step 1.3
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Restriction of a sheaf to an open subspace

Definition

Let j:UX be the inclusion of an open subspace, and let F be a sheaf on X. The restriction of F to U is the inverse image sheaf

FU:=j1F.

For an open set WU, one may identify (FU)(W) with F(W): because U is open in X, the set W is also open in X, and in the neighbourhood-colimit defining j1F the open set W itself is a neighbourhood of j(W)=W.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Extension by zero for abelian sheaves on an open subspace

Definition

Let j:UX be the inclusion of an open subspace, and let F be a sheaf of abelian groups on U.

For an open set VX, define (j!F)(V):={sF(VU):Supp(s) is closed in V}. Equivalently, s lies in (j!F)(V) exactly when for every xVU there exists an open neighbourhood WxV with

sWxU=0.

Restriction maps are inherited from F, so j!F is a subsheaf of jF. When VU, the support condition is vacuous and

(j!F)(V)=F(V).

This is the extension by zero of F along j. It is distinct in general from the ordinary direct image jF.

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

A skyscraper sheaf of abelian groups at a point

Definition

Let X be a topological space, let xX, and let A be an abelian group. The skyscraper sheaf at x with value A is the sheaf

ix,A

defined on an open set VX by (ix,A)(V)={A,xV,0,xV. If VV and both opens contain x, the restriction map is the identity on A. If xV, the restriction map to 0 is the unique zero homomorphism.

Thus a skyscraper sheaf has the value A precisely on opens that meet the chosen point.

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

A ringed space

Definition

A ringed space is a pair

(X,OX)

consisting of a topological space X and a sheaf of commutative rings OX on X.

The sheaf OX is called the structure sheaf of the ringed space.

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

Morphisms of ringed spaces

Definition

Let (X,OX) and (Y,OY) be ringed spaces. A morphism of ringed spaces

(f,f):(X,OX)(Y,OY)

consists of

  1. a continuous map f:XY, and
  2. a morphism of sheaves of rings f:OYfOX on Y.

Equivalently, for every open set VY there are ring homomorphisms

fV:OY(V)OX(f1(V))

compatible with restriction.

Composition is defined by composing the continuous maps and the corresponding morphisms into the direct images of structure sheaves.

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

A locally ringed space

Definition

A locally ringed space is a ringed space (X,OX) such that every stalk OX,x is a local ring in the sense of A local ring is a nonzero commutative ring with a unique maximal ideal.

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

Morphisms of locally ringed spaces

Definition

Let (f,f):(X,OX)(Y,OY) be a morphism of ringed spaces between locally ringed spaces. It is a morphism of locally ringed spaces if for every point xX the induced stalk map

fx:OY,f(x)OX,x

is a local ring homomorphism, meaning that the maximal ideal of OY,f(x) maps into the maximal ideal of OX,x.

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

A local morphism of stalks induces a residue-field map

Statement

Let

(f,f):(X,OX)(Y,OY)

be a morphism of locally ringed spaces, and let xX. Then the local stalk map

fx:OY,f(x)OX,x

induces a field homomorphism

κ(f(x))κ(x)

between residue fields.

Facts & Assumptions

Given: A morphism of locally ringed spaces (f,f):(X,OX)(Y,OY) and a point xX.

[F1]

A local ring has a unique maximal ideal, and its residue field is the quotient by that ideal (A local ring is a nonzero commutative ring with a unique maximal ideal).

[F2]

In a morphism of locally ringed spaces, the stalk map fx:OY,f(x)OX,x sends the maximal ideal of the source into the maximal ideal of the target (Morphisms of locally ringed spaces).

Proof

technique · direct
1.1

Let mf(x) and mx be the maximal ideals of the two stalks. By [F2], the composite OY,f(x)fxOX,xOX,x/mx kills mf(x), so it factors through the quotient OY,f(x)/mf(x).

F1F2given
2.1

By [F1], the source and target quotients in step 1.1 are exactly the residue fields κ(f(x)) and κ(x). Therefore step 1.1 is the desired field homomorphism κ(f(x))κ(x).

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

Modules on a ringed space

Definition

Let (X,OX) be a ringed space.

An OX-module is a sheaf F of abelian groups on X such that for every open set UX the section group F(U) is an OX(U)-module, and for every inclusion VU the restriction map

F(U)F(V)

is OX(U)-linear after restricting scalars along OX(U)OX(V).

A morphism of OX-modules is a morphism of the underlying sheaves of abelian groups whose components are OX(U)-linear on every open set U.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Tensor product of sheaves of modules

Definition

Let (X,OX) be a ringed space, and let F,G be OX-modules. The tensor-product presheaf

Fp,OXG

is defined by (Fp,OXG)(U):=F(U)OX(U)G(U) for each open set UX, with restriction induced from the restriction maps of F and G.

The tensor-product sheaf is the sheafification of this presheaf: FOXG:=a(Fp,OXG).

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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 tensor product sheaf is the tensor product of the stalks

Statement

Let (X,OX) be a ringed space, let F,G be OX-modules, and let xX. Then there is a canonical isomorphism of OX,x-modules (FOXG)xFxOX,xGx.

Facts & Assumptions

Given: A ringed space (X,OX), two OX-modules F,G, and a point xX.

[F1]

The sheaf tensor product is the sheafification of the presheaf UF(U)OX(U)G(U) (Tensor product of sheaves of modules).

[F2]

Stalks are germs of sections over neighbourhoods of the point (The stalk of a presheaf at a point).

[L1]

Sheafification preserves stalks (Sheafification preserves stalks).

Proof

technique · direct
1.1

By [F1] and [L1], it is enough to identify the stalk of the tensor-product presheaf UF(U)OX(U)G(U).

F1L1given
1.2

For every neighbourhood U of x, the germ maps F(U)Fx, G(U)Gx, and OX(U)OX,x induce an OX(U)-balanced pairing into FxOX,xGx. Hence there is a homomorphism F(U)OX(U)G(U)FxOX,xGx, and these maps are compatible with restriction. Therefore they induce a map Φ:(Fp,OXG)xFxOX,xGx.

F2construct
1.3

Conversely, if sxFx and txGx are represented by sections sF(U) and tG(U) on the same neighbourhood U of x, define Ψ(sxtx):=(st)x. If the representatives are changed on a smaller neighbourhood, the represented germ of st is unchanged there, so Ψ is well defined on simple tensors and extends linearly to a homomorphism Ψ:FxOX,xGx(Fp,OXG)x.

F2construct
2.1

On a simple tensor represented on one neighbourhood, Φ and Ψ plainly undo each other. Since both sides are generated by simple tensors, they are inverse isomorphisms. Combining this with step 1.1 gives the stated isomorphism for the sheaf tensor product.

step 1.1step 1.2step 1.3
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05 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 internal Hom sheaf of two module sheaves

Definition

Let (X,OX) be a ringed space, and let F,G be OX-modules. The internal Hom sheaf

HomOX(F,G)

is the sheaf on X defined by UHomOXU(FU,GU) for each open set UX.

Restriction to a smaller open set VU sends a morphism FUGU to its restriction FVGV. Multiplication by a local section aOX(U) acts on a morphism φ by either pre- or post-composition with multiplication by a, giving HomOX(F,G) the structure of an OX-module.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-05 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.

Pullback of a module along a morphism of ringed spaces

Definition

Let

(f,f):(X,OX)(Y,OY)

be a morphism of ringed spaces, and let G be an OY-module. The pullback of G along f is the OX-module fG:=OXf1OYf1G.

Here the ring map

f1OYOX

is the morphism corresponding to f under the inverse/direct-image adjunction Inverse image is left adjoint to direct image on sheaves. The inverse-image construction is taken with its algebraic structure: applying the neighbourhood-colimit construction to the restriction-compatible ring operations of OY, and then sheafifying, makes f1OY a sheaf of rings. The same construction makes f1G an f1OY-module (Presheaves and sheaves of groups, rings, and modules).

Consequently OX is an f1OY-algebra, the displayed sheaf tensor product is well typed, and it carries the asserted OX-module structure.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Pullback of modules is left adjoint to pushforward

Statement

Let

(f,f):(X,OX)(Y,OY)

be a morphism of ringed spaces, let G be an OY-module, and let F be an OX-module. Then there is a natural bijection HomOX(fG,F)HomOY(G,fF).

Facts & Assumptions

Given: A morphism of ringed spaces (f,f):(X,OX)(Y,OY), an OY-module G, and an OX-module F.

[F1]

The pullback is fG=OXf1OYf1G (Pullback of a module along a morphism of ringed spaces).

[L1]

Extension of scalars is left adjoint to restriction of scalars for a ring map (Extension of scalars is left adjoint to restriction of scalars).

[L2]

Inverse image is left adjoint to direct image on sheaves (Inverse image is left adjoint to direct image on sheaves).

[L3]

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

Proof

technique · direct
1.1

Let α:fGF be an OX-linear morphism. By [F1] and [L3], α is equivalent to a morphism from the tensor-product presheaf UOX(U)(f1OY)(U)(f1G)(U) into the sheaf F.

F1L3given
1.2

Conversely, let β:GfF be an OY-linear morphism. By [L2], it corresponds to an f1OY-linear morphism β~:f1GF. Applying [L1] on each open set gives a morphism from the tensor-product presheaf of [F1] into F, and then [L3] factors it uniquely through the sheafification fG. This yields an OX-linear morphism α:fGF.

F1L1L2L3givenconstruct
2.1

Applying [L1] on each open set UX converts the map of step 1.1 into an (f1OY)(U)-linear map (f1G)(U)F(U), compatible with restriction. Hence step 1.1 is equivalent to an f1OY-linear sheaf morphism α~:f1GF.

L1step 1.1
3.1

By [L2], the underlying sheaf morphism α~ corresponds to a sheaf morphism β:GfF. Because the maps in step 2.1 are (f1OY)(U)-linear, the corresponding components βV are OY(V)-linear. Thus β is a morphism of OY-modules.

L2step 2.1
4.1

The constructions in steps 3.1 and 1.2 are inverse because each stage is built from an adjunction with the standard mutually inverse formulas. Therefore HomOX(fG,F)HomOY(G,fF) naturally in both variables.

step 2.1step 3.1step 1.2
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Kernel sheaves are objectwise, while cokernels and images are sheafified

Definition

Let φ:FG be a morphism of sheaves of abelian groups on a topological space X.

The kernel sheaf is the subsheaf

ker(φ)F

defined objectwise by

ker(φ)(U):=ker ⁣(φU:F(U)G(U)).

The cokernel presheaf is

Ucoker ⁣(φU:F(U)G(U)),

and the cokernel sheaf coker(φ) is its sheafification.

The image presheaf is

Uim ⁣(φU:F(U)G(U)),

and the image sheaf im(φ) is its sheafification.

For sheaves of modules on a ringed space, the same formulas are taken in the corresponding module categories on each open set.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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 abelian groups, and likewise sheaves of modules on a ringed space, form abelian categories

Statement

Let X be a topological space.

  1. The category of sheaves of abelian groups on X is an abelian category.
  2. If (X,OX) is a ringed space, then the category of OX-modules is also an abelian category.

Facts & Assumptions

Given: A topological space X, and for the second assertion a ringed space (X,OX).

[F1]

An abelian category is an additive category in which every morphism has a kernel and a cokernel and every coimage-to-image comparison is an isomorphism (Abelian category).

[F2]

Kernel sheaves are computed objectwise, while cokernel and image sheaves are sheafifications of the corresponding objectwise presheaves (Kernel sheaves are objectwise, while cokernels and images are sheafified).

[L1]

For every ring R, the category R-Mod is abelian (Modules over a ring form an abelian category).

[L2]

Sheafification preserves stalks (Sheafification preserves stalks).

[L3]

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

Proof

technique · direct
1.1

In both categories, sums and zero morphisms are defined sectionwise, the zero sheaf is a zero object, and finite direct sums are obtained by taking direct sums on every open set. Hence both categories are additive.

givenconstruct
2.1

By [F2], every morphism has a kernel and a cokernel. The same item also gives the image sheaf by sheafifying the objectwise image presheaf, and the coimage is the cokernel of the kernel inclusion.

F2step 1.1
3.1

Let φ:FG be a morphism in either category. At a point xX, the stalks of the kernel, cokernel, image, and coimage from step 2.1 are the usual kernel, cokernel, image, and coimage of the stalk map φx, because kernels are objectwise and [L2] identifies stalks after sheafification. By [L1], module categories are abelian, and the abelian-group case is the special case of modules over Z, so the canonical map coim(φx)im(φx) is an isomorphism for every x.

F2L1L2step 2.1
4.1

The sheaf morphism coim(φ)im(φ) is therefore an isomorphism on every stalk, so [L3] makes it an isomorphism globally. Together with steps 1.1 and 2.1, [F1] shows that both categories are abelian.

F1L3step 1.1step 2.1step 3.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Exact sequences of sheaves

Definition

Let X be a topological space. A sequence of sheaves of abelian groups on X is exact when it is exact in the abelian category of Sheaves of abelian groups, and likewise sheaves of modules on a ringed space, form abelian categories, equivalently in the sense of Exact sequence and short exact sequence in an abelian category.

Thus a sequence

Fi1FiFi+1

is exact at Fi when the image sheaf of the first morphism equals the kernel sheaf of the second.

The same language applies to OX-modules on a ringed space.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-05 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 sequence of abelian sheaves is exact exactly when it is exact on every stalk

Statement

Let

Fi1di1FidiFi+1

be a sequence of sheaves of abelian groups on a topological space X. Then the sequence is exact if and only if, for every point xX, the stalk sequence

(Fi1)x(di1)x(Fi)x(di)x(Fi+1)x

is exact.

Facts & Assumptions

Given: A sequence of sheaves of abelian groups on X.

[F1]

Exactness of a sequence of sheaves means exactness in the abelian category of sheaves, so at each middle term the image sheaf equals the kernel sheaf (Exact sequences of sheaves).

[F2]

Stalks are germs of neighbourhood sections (The stalk of a presheaf at a point).

[L1]

Kernels are objectwise, while images and cokernels are obtained by sheafifying the corresponding presheaves (Kernel sheaves are objectwise, while cokernels and images are sheafified).

[L2]

Sheafification preserves stalks (Sheafification preserves stalks).

[L3]

A morphism of sheaves is an isomorphism exactly when it is so on every stalk (A morphism of sheaves is an isomorphism exactly when it is an isomorphism on every stalk).

Proof

technique · direct
1.1

Assume the sheaf sequence is exact. At each middle term Fi, [F1] says that the canonical map im(di1)ker(di) is an isomorphism. Using [F2] for the stalk construction and then [L1] and [L2], its stalk at x is the canonical map im((di1)x)ker((di)x), so the stalk sequence is exact at x. Since x was arbitrary, the whole stalk sequence is exact.

F1F2L1L2given
1.2

Conversely, assume every stalk sequence is exact. For each middle term, consider the canonical morphism im(di1)ker(di). Using [F2] for the stalk construction and then [L1] and [L2], its stalk at x is im((di1)x)ker((di)x), which is an isomorphism by the stalkwise exactness hypothesis. Therefore [L3] implies that im(di1)ker(di) is an isomorphism of sheaves.

F2L1L2L3given
2.1

By [F1], step 1.2 is exactly the assertion that the original sequence is exact. Together with step 1.1, this proves the equivalence.

F1step 1.1step 1.2
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-05 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.

Global sections are left exact but need not preserve epimorphisms

Statement

Let X be a topological space. If

0FFF

is exact in sheaves of abelian groups on X, then

0Γ(X,F)Γ(X,F)Γ(X,F)

is exact. However, there exists an epimorphism of sheaves of abelian groups on some space X whose induced map on global sections is not surjective.

Facts & Assumptions

Given: A topological space X.

[F1]

Global sections are sections over the whole space: Γ(X,F)=F(X) (Sections, restrictions, and global sections of a presheaf).

[L2]

Exactness of sheaves means image equals kernel at each interior term (Exact sequences of sheaves).

Proof

technique · direct
1.1

Suppose 0FFF is exact. By [L1], the kernel of the map Γ(X,F)Γ(X,F) is the section group of the kernel sheaf at X. By [L2], that kernel sheaf is the image of FF, so its sections over X are exactly the image of Γ(X,F)Γ(X,F). Together with [F1], this is the displayed left exactness.

F1L1L2given
1.2

For the failure of surjectivity, let X=S1, let C be the sheaf of continuous real-valued functions on S1, and let Z be the subsheaf of locally constant integer-valued functions. Let Q be the quotient sheaf obtained by sheafifying the presheaf VC(V)/Z(V). Every germ of a section of Q is represented locally by a continuous real-valued function, so the canonical map CQ is locally surjective and hence an epimorphism of sheaves.

F1construct
1.3

Cover the circle by the arcs U0=S1{(1,0)} and U1=S1{(1,0)}. Choose continuous angle functions θ0:U0(1/2,1/2) and θ1:U1(0,1) with e2πiθi(z)=z. On one connected component of U0U1 the difference θ1θ0 is 0, and on the other it is 1, so the classes of θ0 and θ1 agree in the quotient presheaf and glue to a global section qΓ(X,Q). If q had a lift gΓ(X,C), then gθi would be an integer-valued continuous function on the connected arc Ui, hence a constant ni. On the two components of U0U1 this would force n0n1 to be both 0 and 1, a contradiction. Thus Γ(X,C)Γ(X,Q) is not surjective.

constructcontradiction
2.1

Step 1.1 gives left exactness, and step 1.3 gives an epimorphism whose global sections map is not surjective.

step 1.1step 1.3
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Extension by zero is left adjoint to restriction and is exact on abelian sheaves

Statement

Let j:UX be the inclusion of an open subspace.

  1. For every sheaf of abelian groups F on U and every sheaf of abelian groups G on X, there is a natural bijection HomX(j!F,G)HomU(F,j1G).
  2. The functor j! is exact on sheaves of abelian groups.

Facts & Assumptions

Given: An open inclusion j:UX.

[F1]

Restriction to U is the inverse image sheaf j1 (Restriction of a sheaf to an open subspace).

[F2]

A section of j!F over an open VX is a section of F(VU) whose support is closed in V (Extension by zero for abelian sheaves on an open subspace).

[L1]

Exactness of abelian sheaf sequences can be tested stalkwise (A sequence of abelian sheaves is exact exactly when it is exact on every stalk).

Proof

technique · direct
1.1

Let Φ:j!FG be a morphism on X. If WU is open, then [F2] gives (j!F)(W)=F(W), so the components ΦW define a morphism Fj1G on U.

F1F2given
1.2

Conversely, let Ψ:Fj1G be a morphism on U. For an open set VX and a section s(j!F)(V), use Ψ to obtain a section on VU. For each point xVU, the support condition in [F2] gives an open neighbourhood WxV with sWxU=0, so we may assign the zero section of G on Wx. These local sections agree on overlaps, so they glue uniquely to a section of G(V). This defines a morphism j!FG.

F1F2construct
1.3

Let xX. If xU, then the neighbourhoods of x that lie inside U are cofinal among all neighbourhoods of x, so (j!F)xFx. If xU and s(j!F)(V) for some neighbourhood V of x, then [F2] gives an open neighbourhood WxV with sWxU=0, so the germ of s at x is zero. Therefore (j!F)x=0.

F2given
2.1

The constructions in steps 1.1 and 1.2 are inverse, because on opens contained in U they both recover the original morphism on F, and outside U the support condition forces the extension to vanish locally. Therefore j! is left adjoint to j1.

step 1.1step 1.2
3.1

Apply step 1.3 to a short exact sequence on U. At points of U the stalk sequence after j! is the original exact stalk sequence, and outside U it is 0000. Hence [L1] implies that j! preserves exact sequences.

L1step 1.3
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-05 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.

Pullback of modules is right exact, and flat stalk maps make it exact

Statement

Let

(f,f):(X,OX)(Y,OY)

be a morphism of ringed spaces. Then the pullback functor

f:Mod(OY)Mod(OX)

is right exact. Moreover, if every stalk ring map

OY,f(x)OX,x

is flat, then f is exact.

Facts & Assumptions

Given: A morphism of ringed spaces (f,f):(X,OX)(Y,OY).

[F1]

The pullback is fG=OXf1OYf1G (Pullback of a module along a morphism of ringed spaces).

[F2]

A ring map is flat exactly when tensoring with the target module is exact (Flat and faithfully flat modules and ring homomorphisms).

[L1]

The stalk of an inverse image is the stalk over the image point (The stalk of an inverse image sheaf is the stalk over the image point).

[L2]

The stalk of a tensor-product sheaf is the tensor product of the stalks (The stalk of a tensor product sheaf is the tensor product of the stalks).

[L3]

Exactness of sheaf sequences is equivalent to stalkwise exactness (A sequence of abelian sheaves is exact exactly when it is exact on every stalk).

[L4]

Tensoring with a fixed module is right exact (Tensoring is right exact).

Proof

technique · direct
1.1

Let MMM0 be an exact sequence of OY-modules, and fix xX with y=f(x). By [L1], the stalk sequence after applying f1 is MyMyMy0, which is exact because the original sequence is exact at every stalk. Hence f1 is exact on the underlying sheaves.

L1L3given
2.1

By [F1] and [L2], the stalk of the pulled-back sequence at x is OX,xOY,yMyOX,xOY,yMyOX,xOY,yMy0. Step 1.1 gives exactness before tensoring, so [L4] makes this sequence right exact. Since this holds for every x, [L3] shows that f is right exact.

F1L2L3L4step 1.1
3.1

Assume every stalk ring map OY,f(x)OX,x is flat. By [F2], for each xX the functor OX,xOY,f(x) is exact on OY,f(x)-modules. Applying this to the exact stalk sequence from step 1.1 shows that the sequence in step 2.1 is exact at every x. Therefore [L3] implies that f is exact.

F2L3step 1.1step 2.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05 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 gluing datum for sheaves on an open cover

Definition

Let X be a topological space with an open cover X=iUi. A gluing datum for sheaves on this cover consists of

  1. a sheaf Fi on each open set Ui, and
  2. for each pair (i,j), an isomorphism of sheaves on UiUj, φij:FiUiUj  FjUiUj,

such that

  1. φii=idFi, and
  2. on every triple overlap UiUjUk one has φjkφij=φik.

The same definition applies to sheaves of abelian groups, rings, or modules.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Compatible local sheaves glue uniquely up to unique isomorphism

Statement

Let X=iUi be an open cover, and let

(Fi,φij)

be a gluing datum for sheaves on that cover. Then there exists a sheaf F on X together with isomorphisms

FUi  Fi

whose induced overlap identifications are the given φij. This glued sheaf is unique up to unique isomorphism.

The same objectwise construction gives the analogous gluing result for sheaves of abelian groups, commutative rings, and modules on a fixed ringed space.

Facts & Assumptions

Given: An open cover X=iUi and a gluing datum (Fi,φij) on it.

[F1]

A gluing datum consists of local sheaves and overlap isomorphisms satisfying identity and cocycle conditions (A gluing datum for sheaves on an open cover).

[L1]

A sheaf is exactly a presheaf whose compatible local sections glue uniquely on open covers (A sheaf on a topological space).

Proof

technique · direct
1.1

For an open set WX, define F(W) to be the set of families (si) with siFi(WUi) such that on every overlap WUiUj one has φij(siWUiUj)=sjWUiUj. Restriction is taken componentwise. This defines a presheaf on X.

F1construct
1.2

Fix k. If WUk, the map F(W)Fk(W) sending (si) to sk is an isomorphism: given tFk(W), define si:=φki(tWUi), and [F1] makes these sections compatible. Therefore FUkFk, and the overlap maps are exactly the prescribed φij.

F1construct
2.1

Let W=αWα and let (si(α)) be compatible sections of the presheaf from step 1.1 on the cover. For each fixed i, the sections si(α)Fi(WαUi) are compatible, so [L1] glues them uniquely to a section siFi(WUi). The cocycle condition from [F1] is preserved under these gluings, hence (si) is a glued section of F(W). Uniqueness is again componentwise, so the presheaf is a sheaf. If the Fi carry abelian-group, ring, or module structures and each φij preserves them, then the componentwise operations on the families (si) make the glued sheaf a sheaf of the same kind.

F1L1step 1.1
3.1

If G is another sheaf with the same local identifications, then on every open W its sections are exactly the compatible families of local sections on the cover {WUi}. By [L1], the correspondence of step 1.1 is therefore forced, so there is a unique isomorphism GF. This proves uniqueness up to unique isomorphism.

L1step 1.1step 1.2
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Compatible open pieces of ringed or locally ringed spaces glue

Statement

Let {(Xi,Oi)}iI be ringed spaces, or locally ringed spaces, together with open subsets UijXi and isomorphisms

φij:(Uij,OiUij)  (Uji,OjUji)

satisfying the usual identity and cocycle conditions on triple overlaps. Then these data glue to a ringed space, respectively a locally ringed space, covered by open subsets identified with the Xi.

Facts & Assumptions

Given: Compatible gluing data of ringed spaces or locally ringed spaces.

[F1]

A ringed space is a topological space with a sheaf of rings, and a locally ringed space is one whose stalks are local rings (A ringed space, A locally ringed space).

[F2]

Morphisms of locally ringed spaces are morphisms of ringed spaces whose stalk maps are local (Morphisms of locally ringed spaces).

[L1]

Compatible local sheaves glue uniquely up to unique isomorphism (Compatible local sheaves glue uniquely up to unique isomorphism).

Proof

technique · direct
1.1

Form the disjoint union iXi and impose the equivalence relation generated by xiφij(xi) whenever xiUij, using the underlying homeomorphisms of the isomorphisms φij. The identity and cocycle hypotheses make this an equivalence relation. Let X be the quotient space. The image Vi of each Xi in X is open, the Vi cover X, and the quotient map qi:XiVi is a homeomorphism because identifications occur only along open subsets via homeomorphisms.

givenconstruct
2.1

Transport each structure sheaf Oi to the open subset Vi via qi, obtaining a sheaf of rings on Vi. The ringed-space isomorphisms on the overlaps induce isomorphisms of these sheaves on ViVj, and the cocycle condition is exactly the compatibility required by [L1]. Hence [L1] glues the local structure sheaves to a sheaf of rings OX on X, making each qi an isomorphism of ringed spaces (Xi,Oi)(Vi,OXVi).

F1L1step 1.1construct
3.1

If the input pieces are locally ringed spaces, let xX and choose i with xVi. Because qi is a homeomorphism onto an open neighbourhood of x, the stalk OX,x identifies with the stalk of Oi at the corresponding point of Xi. That stalk is local by [F1], so every stalk of OX is local. Thus (X,OX) is locally ringed.

F1step 2.1
4.1

Any other glued ringed or locally ringed space has the same quotient-topology description as in step 1.1 and the same locally compatible structure sheaf. By the uniqueness clause of [L1], it is uniquely isomorphic to (X,OX). This proves existence and uniqueness in both the ringed and locally ringed settings.

F2L1step 1.1step 2.1step 3.1
RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Inverse image of sheaves and pullback of modules are not the same construction

The notation f1 and f describes two different operations.

The inverse image f1G only uses the underlying continuous map f:XY and is defined for any sheaf on Y (Inverse image presheaf and inverse image sheaf). It changes the topological base space but does not yet change scalars.

The pullback fG is defined only after choosing a morphism of ringed spaces, and for modules it adds the scalar extension

OXf1OY

to the inverse image (Pullback of a module along a morphism of ringed spaces).

Thus f1 is the sheaf-theoretic inverse image, whereas f is the module-theoretic pullback built from f1 plus tensoring.

5 · Examples, counterexamples and false statements

None yet.

Sources