Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: 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.

Finite fibres and an open immersion do not make a map finite

Statement refuted

False claim: a quasi-finite morphism of classical varieties that is an open immersion is finite.

Facts & Assumptions

Assume the Axiom of Choice.

Given: AC, an algebraically closed field k, the affine line Ak1 with coordinate ring k[t], the principal open U=D(t)=Ak1∖{0}, and the inclusion j ⁣:U↪Ak1.

[F1]

U=D(t) with its regular functions is an affine variety with coordinate ring k[t,t−1]=k[t]t, realized as the closed graph {ts=1}⊆A1×A1, and j is the restriction of the projection, with pullback the inclusion k[t]↪k[t,t−1] (Every nonempty principal open is a classical affine variety, Affine morphisms are contravariantly equivalent to coordinate-ring homomorphisms).

[F2]

A morphism of classical varieties is quasi-finite when every closed-point fibre is a finite set; empty fibres are allowed (Quasi-finite classical morphisms).

[F3]

A finite morphism of classical varieties is closed: the image of every closed subset is closed (Finite morphisms are closed with finite fibres).

[F4]

The closed subsets of the affine line are the finite subsets and the whole line (On the affine line, the classical Zariski topology is cofinite); since k is algebraically closed, hence infinite, the set A1∖{0} is infinite and therefore not closed in A1. Its closure is all of A1.

[F7]

AC is inherited through the classical localization, normalization, or finite-morphism suppliers cited above (The Axiom of Choice).

Counterexample

1.1F1F2givenF7

The map j is an open immersion and is quasi-finite: it is the inclusion of the principal open U [F1], and its fibres are singletons over the points of k× and empty over 0, so every closed-point fibre is finite [F2].

1.2F1F3F4given

The map j is not finite. If it were finite, then by [F3] its image would be closed in A1; but its image is A1∖{0}, which by [F4] is infinite and hence not closed. Equivalently, the coordinate-ring inclusion k[t]↪k[t,t−1] would make k[t,t−1] a finite k[t]-module, which it is not: a finite generating set of Laurent polynomials has a bounded negative exponent, and no finite k[t]-span contains all powers t−n.

2.1F2F3step 1.1step 1.2∎

The inclusion j ⁣:A1∖{0}↪A1 is therefore an open immersion with finite fibres that is not finite, refuting the claim; the missing hypothesis is properness (equivalently, closedness of the map), which is exactly what [F3] supplies for finite morphisms and what fails for this open immersion.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

44 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