Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04
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.

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 U⊆X be open, and let s∈F(U). Then s=0 in F(U)⟺sx=0 in Fx for every x∈U.

Facts & Assumptions

Given: A sheaf of groups F, an open set U, and a section s∈F(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). Here 0x (also written 0 in Fx) denotes the germ of an identity section. This is independent of the neighbourhood used: any two identity sections restrict to the identity on their intersection by [F1], and so have the same germ. No group operation on the stalk is needed for this notation.

Proof

technique · direct
1.1F1F2

If s=0 in F(U), then for every x∈U the induced germ is sx=0x by the definition of 0x in [F2].

1.2F2given

Assume sx=0 for every x∈U. Fix x∈U. By lem-germ-equivalence-relation, equality of the two germ classes means that their representatives agree on some open neighbourhood Vx⊆U of x, so s∣Vx=0∣Vx. The sets Vx cover U.

2.1L1step 1.1step 1.2∎

On the open cover {Vx}x∈U, the sections s and 0 have the same restriction by step 1.2. Locality in [L1] therefore gives s=0 in F(U). For U=∅, this uses the empty cover, which is included in [L1]. Together with step 1.1, this proves both directions.

Depends on

Used by

Dependency tree · two levels

11 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