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

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

Statement

Let j:U↪X 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 Hom⁡X(j!F,G)≅Hom⁡U(F,j−1G).
  2. The functor j! is exact on sheaves of abelian groups.

Facts & Assumptions

Given: An open inclusion j:U↪X.

[F1]

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

[F2]

A section of j!F over an open V⊆X is a section of F(V∩U) 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.1F1F2given

Let Φ:j!F→G be a morphism on X. If W⊆U is open, then [F2] gives (j!F)(W)=F(W), so the components ΦW define a morphism F→j−1G on U.

1.2F1F2construct

Conversely, let Ψ:F→j−1G be a morphism on U. For an open set V⊆X and a section s∈(j!F)(V), use Ψ to obtain a section on V∩U. For each point x∈V∖U, the support condition in [F2] gives an open neighbourhood Wx⊆V with s∣Wx∩U=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!F→G.

1.3F2given

Let x∈X. If x∈U, then the neighbourhoods of x that lie inside U are cofinal among all neighbourhoods of x, so (j!F)x≅Fx. If x∉U and s∈(j!F)(V) for some neighbourhood V of x, then [F2] gives an open neighbourhood Wx⊆V with s∣Wx∩U=0, so the germ of s at x is zero. Therefore (j!F)x=0.

2.1step 1.1step 1.2

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 j−1.

3.1L1step 1.3∎

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 0→0→0→0. Hence [L1] implies that j! preserves exact sequences.

Depends on

Used by

Dependency tree · two levels

12 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