Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-sol)audited 2026-09-27
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.

The constant sheaf is the sheaf of locally constant functions

Statement

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) and let A be a set. A function f:U→A on an open subset U⊆X is locally constant when every x∈U has an open neighbourhood V⊆U with x∈V on which f is constant. Let Apt be the constant presheaf with value A, Apt(U)=A for every open U with all restriction maps the identity (A presheaf on a topological space), and let AX:=aApt be its sheafification (Sheafification of a presheaf), the constant sheaf with value A on X. Then:

  1. the assignment A‾loc(U):={f:U→A locally constant}, with the usual restriction maps, is a sheaf of sets on X, and for every x∈X evaluation at x is a canonical bijection A‾loc,x≅A (Locally constant functions form a sheaf with constant stalks);
  2. there is a canonical isomorphism of sheaves of sets θ:AX⟶A‾loc such that for every open U⊆X and every a∈A the section θU(ηU(a)) is the constant function with value a, where η:Apt→AX is the sheafification map;
  3. if A is an abelian group, then Apt with its group operation is a presheaf of abelian groups (Presheaves and sheaves of groups, rings, and modules) and A‾loc with pointwise addition is a sheaf of abelian groups (Sheaves of abelian groups, and likewise sheaves of modules on a ringed space, form abelian categories); the maps a↦the constant function with value a are group homomorphisms, and the group structures transported along the bijections θU make AX a sheaf of abelian groups for which every ηU and every θU is a group homomorphism.

Facts & Assumptions

[F1]

A morphism of presheaves is a family of maps commuting with restriction: φV(s∣V)=φU(s)∣V for all s∈F(U) and V⊆U (Morphisms of presheaves).

[F2]

The locally constant A-valued functions form a sheaf of sets A‾loc on X, and for every x∈X evaluation at x induces a canonical bijection A‾loc,x≅A (Locally constant functions form a sheaf with constant stalks).

[F3]

Sheafification is the double plus construction aF=F++ with canonical map ηF, and every presheaf morphism from F into a sheaf factors uniquely through ηF (Sheafification of a presheaf, Sheafification is left adjoint to the inclusion of sheaves into presheaves).

[F4]

For every presheaf F the sheafification map induces a bijection on stalks, ηF,x:Fx→(aF)x (Sheafification preserves stalks).

[F5]

The stalk at x is the filtered colimit of the section groups over the open neighbourhoods of x (The stalk of a presheaf at a point, Filtered categories and filtered colimits).

[F6]

A colimit of a diagram is an initial cocone: for every cocone (X,ξ) there is a unique morphism out of it compatible with the structure maps (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[F7]

A morphism of sheaves of sets is an isomorphism if and only if all of its induced maps on stalks are bijections (A morphism of sheaves is an isomorphism exactly when it is an isomorphism on every stalk).

[F8]

For an abelian group A the constant presheaf is a presheaf of abelian groups with the group operation of A at every open, and the category of sheaves of abelian groups on X is abelian (Presheaves and sheaves of groups, rings, and modules, Sheaves of abelian groups, and likewise sheaves of modules on a ringed space, form abelian categories).

Proof

Given: A topological space X, a set A, the constant presheaf Apt with value A, its sheafification AX=aApt with sheafification map η, and the sheaf A‾loc of locally constant functions.

1.1

Define a presheaf map φ:Apt→A‾loc by φU(a):=(x↦a), the constant function with value a on U. This is a morphism of presheaves in the sense of [F1]: for V⊆U and a∈A the restriction of the constant function with value a on U to V is again the constant function with value a, and φV(a) is that same function, so φV(a∣V)=φU(a)∣V, both sides being constant with value a; here a∣V=a because all restriction maps of Apt are the identity.

F1F2
1.2

The stalk of the constant presheaf at x∈X is A: by [F5] it is the colimit of the diagram which is constant with value A on the filtered category of open neighbourhoods of x, and a cocone from that diagram to a set S is the same thing as a single map A→S (all the structure maps of Apt are identities, so the compatibility conditions are automatic); by the explicit description of a colimit [F6] the identity of A exhibits A as a colimit, so the canonical map A→(Apt)x, a↦ the class of the constant section a over X, is a bijection.

F5F6
2.1

By [F2] the presheaf A‾loc is a sheaf of sets, so by the universal property [F3] the morphism φ factors uniquely through the sheafification map η:Apt→AX: there is exactly one morphism of sheaves of sets θ:AX→A‾loc with θ∘η=φ. In particular θU(ηU(a))=φU(a) is the constant function with value a, which is the compatibility asserted in clause 2.

F3step 1.1
2.2

Under the identifications of [step 1.2] and of the evaluation bijection of [F2], the induced map φx:(Apt)x→A‾loc,x is the identity of A: the element a corresponds to the class of the constant section with value a over X, its image under φ is the germ of the constant function with value a, and evaluation at x returns a. Hence φx is a bijection for every x∈X.

F2step 1.1step 1.2
3.1

For every x∈X the map ηx:(Apt)x→(AX)x is a bijection by [F4], and φx=θx∘ηx by [step 2.1]; since φx is a bijection by [step 2.2], the map θx is a bijection as well, being the composite of the inverse of ηx with φx.

F4step 2.1step 2.2
4.1

By [step 3.1] every induced map of θ on stalks is a bijection, so θ:AX→A‾loc is an isomorphism of sheaves of sets by [F7]. Together with [step 2.1] this is clauses 1 and 2 of the statement.

F7step 2.1step 3.1
5.1

Suppose now that A is an abelian group. Pointwise addition makes Apt a presheaf of abelian groups, all of whose restriction maps are the identity, and makes A‾loc a sheaf of abelian groups: the sum and the negative of locally constant functions are locally constant, since on a neighbourhood where each summand is constant the sum is constant, and restrictions are the corresponding group homomorphisms [F8]. Each φU is a group homomorphism because constant functions add pointwise. Transport the group operation of A‾loc(U) to AX(U) along the bijection θU of [step 4.1], declaring s+t:=θU−1(θU(s)+θU(t)) for s,t∈AX(U): this makes every θU a group isomorphism, and the restriction maps of AX are group homomorphisms because they are conjugate through θ to the restriction maps of A‾loc, which are homomorphisms, so AX is a sheaf of abelian groups; moreover ηU=θU−1∘φU is then a group homomorphism, since it is a composite of group homomorphisms and the inverse of one. This is clause 3, and the proof is complete. ∎

F8step 2.1step 4.1

Depends on

Used by

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources