Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 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.

The image sheaf is the sheafification of the presheaf image

Statement

Let φ:F→G 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):={ t∈G(U): for every x∈U there exists x∈V⊆U and s∈F(V) with φV(s)=t∣V }. Then J is a subsheaf of G, φ factors through J, and the canonical map aI⟶J is an isomorphism. In particular, the image sheaf is the sheafification of the objectwise image presheaf.

Facts & Assumptions

Given: A morphism of sheaves φ:F→G.

[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.1F2given

The assignment U↦I(U) is a subpresheaf of G: if t=φU(s)∈I(U) and V⊆U, then t∣V=φV(s∣V)∈I(V) by [F2].

1.2F1F2given

The assignment J is a subsheaf of G. Indeed, restriction clearly preserves local representability. If sections ti∈J(Ui) on an open cover of U agree on overlaps, then because G is a sheaf they glue to a unique t∈G(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 F→J is immediate from the definition of J.

2.1L1step 1.1step 1.2

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

2.2L1step 1.2construct

Conversely, let t∈J(U). Choose an open cover U=⋃iUi and sections si∈F(Ui) with φUi(si)=t∣Ui. 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 β:J→aI.

3.1L1step 2.1step 2.2∎

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.

Depends on

Used by

Dependency tree · two levels

10 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