Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
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.

Rigidity for a proper geometrically integral factor

Statement

Assume the Axiom of Choice. Let X be a proper geometrically integral k-scheme of finite type, with x0∈X(k). Let Y be a connected finite-type k-scheme and Z a separated finite-type k-scheme. If a k-morphism f:X×kY→Z is constant on X×k{y0} for some y0∈Y(k), then f=f(x0,−)∘pr⁡Y.

Facts & Assumptions

[F1]

A proper geometrically integral scheme has global functions equal to the base field, under AC. This applies after every field extension. (Global functions on proper integral schemes form a finite extension of the base field)

[F2]

Global sections of a quasi-compact separated k-scheme commute with scalar extension to any k-algebra. Morphisms into affine schemes correspond to ring maps on global sections. (Global sections commute with extension of scalars over a field, Morphisms to an affine scheme and global sections)

[F3]

A proper map is closed after base change; a flat map locally of finite presentation is open after base change. The projection X×kY→Y has both properties: properness is stable under base change, and a finite-type scheme over a field is flat and of finite presentation. (Proper morphisms are closed, Flat finite-presentation morphisms are open)

[F4]

The diagonal of a separated scheme is closed. (Separated morphism of schemes)

Proof

Given: X,x0,Y,Z,f,y0 as in the statement, and AC.

1.1F3F4given

Let E be the closed equalizer of f and f(x0,−)∘pr⁡Y, obtained by pulling back the diagonal of Z. Write p:X×kY→Y and C=Y∖p((X×kY)∖E). By [F3], p is open, so C is closed. A point y belongs to C exactly when the whole topological fibre of p over y lies in E. That fibre is geometrically integral and thus reduced, so the two morphisms agree on it scheme theoretically: the ideal of the equalizer vanishes at every point and is zero on a reduced scheme. In particular y0∈C.

2.1F1F2F3step 1.1

Fix y∈C. Its fibre has image the single point f(x0,y). Choose an affine open W⊂Z containing that point. The closed subset f−1(Z∖W) has closed image under the proper projection p. Its image omits y, so an affine open neighbourhood U=Spec⁡R of y avoids that image. Consequently f(X×kU)⊂W. By [F1] and [F2], Γ(X×kU,O)=k⊗kR=R. The map to the affine W therefore factors through U, and evaluating at x0 identifies the factor as f(x0,−)∣U. Thus U⊂C, proving that C is open.

3.1step 1.1step 2.1given∎

Since Y is connected and C is nonempty, open, and closed, C=Y. The factorization in step 2.1 holds on an open neighbourhood of every point, hence glues to the asserted equality of morphisms on all of X×kY. AC is carried from the proper global-functions and morphism suppliers; no stronger field or projectivity assumption is used.

Depends on

Used by

Dependency tree · two levels

54 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