Alphabeta Math
LemmaStatement: 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.

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

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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