ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Incidence projection has closed determinantal image

Example

Let $k$ be a field. Let $P_{k}^{1}$ be the relative projective line over $Spec k$ with standard charts $U_{0} = Spec k [u]$ and $U_{1} = Spec k [v]$ , where $u$ and $v$ are the chart coordinates $t_{1} / t_{0}$ and $t_{0} / t_{1}$ of the homogeneous coordinates $[t_{0} : t_{1}] = [s : t]$ , and let $A_{k}^{4} = Spec k [a, b, c, d]$ be the relative affine $4$ -space over $Spec k$ . Let $Z \subseteq P_{k}^{1} \times_{k} A_{k}^{4}$ be the closed subscheme cut out by the two relative equations $a s + b t = 0, c s + d t = 0,$ which on the charts means $Z \cap (U_{0} \times_{k} A_{k}^{4}) = V (a + b u, c + d u)$ and $Z \cap (U_{1} \times_{k} A_{k}^{4}) = V (a v + b, c v + d)$ . Then the projection $π : Z ⟶ A_{k}^{4}$ is proper and its image is the closed subset $V (a d - b c) \subseteq A_{k}^{4}$ . The assertion holds over every field, in particular in characteristic $2$ , and the origin $(a, b, c, d) = (0, 0, 0, 0)$ lies in the image, the fibre of $π$ over it being a copy of $P_{k}^{1}$ .

Facts & Assumptions

Given: A field $k$ ; the relative projective line $P_{k}^{1}$ over $Spec k$ with standard charts $U_{0} = Spec k [u]$ , $U_{1} = Spec k [v]$ ; the relative affine space $A_{k}^{4} = Spec k [a, b, c, d]$ ; the product $P_{k}^{1} \times_{k} A_{k}^{4}$ ; the closed subscheme $Z$ cut out by $a s + b t = 0$ and $c s + d t = 0$ , whose charts are $Z \cap (U_{0} \times_{k} A_{k}^{4}) = V (a + b u, c + d u)$ and $Z \cap (U_{1} \times_{k} A_{k}^{4}) = V (a v + b, c v + d)$ ; and the projection $π : Z \to A_{k}^{4}$ , the restriction of the second projection of the product.

[F1]

For a base scheme $S = Spec k$ the standard charts of $P_{S}^{1} = P_{Spec k}^{1}$ are $U_{0} = Spec k [x_{1}^{(0)}] = Spec k [u]$ and $U_{1} = Spec k [x_{0}^{(1)}] = Spec k [v]$ , with $u = t_{1} / t_{0}$ , $v = t_{0} / t_{1}$ , $u = 1 / v$ on the overlap; they form an open cover of $P_{k}^{1}$ . (Relative projective space from standard charts)

[F2]

Relative affine space is defined over every base scheme, and over an affine base it is $A_{Spec A}^{n} = Spec A [t_{1}, \dots, t_{n}]$ with structure morphism induced by $A ↪ A [t_{1}, \dots, t_{n}]$ ; in particular $A_{k}^{4} = Spec k [a, b, c, d]$ is a scheme over $Spec k$ . (Schemes and morphisms over a base)

[F3]

For ring maps $A \to B$ and $A \to C$ there is a canonical isomorphism $Spec B \times_{Spec A} Spec C ≅ Spec (B \otimes_{A} C)$ compatible with the projections; hence $U_{0} \times_{k} A_{k}^{4} = Spec (k [u] \otimes_{k} k [a, b, c, d]) = Spec k [u, a, b, c, d]$ and the projection to $A_{k}^{4}$ corresponds to the inclusion $k [a, b, c, d] ↪ k [u, a, b, c, d]$ , and likewise over $U_{1}$ with $v$ in place of $u$ . (Affine fibre products are spectra of tensor products)

[F4]

A morphism is a closed immersion when its underlying map is a homeomorphism onto a closed subset of its target and the structure-sheaf map is surjective; a morphism is a closed immersion exactly when its restrictions over the members of an open cover of the target are closed immersions. (Closed immersions of schemes, Closed immersions are local on the target)

[F5]

For a morphism $S^{'} \to S$ and an $S$ -scheme $X$ , the base change is the fibre product $X_{S^{'}} = X \times_{S} S^{'}$ with structure morphism the second projection. (Base change of objects, morphisms and properties)

[F6]

Assume AC. For every scheme $S$ and every $n \geq 0$ the projective-space morphism $P_{S}^{n} \to S$ is proper; in particular $P_{k}^{1} \to Spec k$ is proper. (Finite-dimensional projective space is proper over every base)

[F7]

Assume AC. Base changes of proper morphisms are proper. (Properness survives arbitrary base change)

[F8]

Assume AC. Every closed immersion is finite, hence proper; the empty closed immersion is included. (Closed immersions are proper)

[F9]

Assume AC. A composite of proper morphisms is proper. (Properness survives composition)

[F10]

A proper morphism of schemes is a closed map: the image of every closed subset of its source is closed in its target, and in particular the image of the whole source is closed. (Proper morphisms are closed)

[F11]

For commutative unital rings $A, B$ the assignment $φ \mapsto Spec (φ)$ is a natural bijection ${Hom}_{C R i n g} (A, B) ≅ {Hom}_{L R S} (Spec B, Spec A)$ , making $A \mapsto Spec A$ a contravariant equivalence with quasi-inverse global sections; a ring homomorphism $φ : A \to B$ gives the continuous contraction map $Spec B \to Spec A$ , $q \mapsto φ^{- 1} q$ . Consequently, for a field $F$ and a ring map $ψ : R \to F$ , the image of $Spec ψ$ is the point $ψ^{- 1} (0) = \ker ψ$ of $Spec R$ . (Affine schemes are contravariantly equivalent to commutative rings, The map of affine spectra induced by a ring homomorphism)

[F12]

The points of $Spec R$ are the prime ideals of $R$ , and for an ideal $I \subseteq R$ its vanishing set is $V (I) = {p \in Spec R : I \subseteq p}$ ; the sets $V (I)$ are closed under arbitrary intersections and finite unions and define the Zariski topology, so they are exactly the closed subsets. (The prime spectrum and vanishing sets, The vanishing sets define the Zariski topology on the prime spectrum)

[F13]

For a point $x$ of a locally ringed space put $κ (x) = O_{X, x} / m_{x}$ ; if $x = p$ is a point of $Spec A$ then $κ (p) ≅ A_{p} / p A_{p} ≅ Frac (A / p)$ . (The residue field at a point of an affine scheme)

[F14]

For every field $K$ and scheme $X$ , morphisms $Spec K \to X$ correspond bijectively to pairs $(x, ι)$ with $x \in X$ and a field embedding $ι : κ (x) \to K$ ; the identity embedding gives a canonical morphism $Spec κ (x) \to X$ with image $x$ , compatible with all scheme morphisms. (Field-valued points and local-ring points)

[F15]

The Axiom of Choice states that every family of nonempty sets has a choice function. (The Axiom of Choice)

AC use: F15 is assumed because F6, F7, F8 and F9 are AC-qualified; the chart computations, the case analysis over residue fields and the affine correspondences below are choice-free.

Verification

technique · direct: the two chart equations force $ad-bc=0$ on $Z$, and conversely every point of $V(ad-bc)$ is attained by solving the two linear equations over its residue field; the projection is proper, being a closed immersion into a base change of the proper morphism $\mathbb P^1_k\to\operatorname{Spec}k$, so its image is closed and the two inclusions give equality

1.1F1F3F4given

On the overlap $U_{0} \cap U_{1}$ the chart coordinates satisfy $u = 1 / v$ , $v = 1 / u$ , so $a v + b = (a + b u) / u$ and $c v + d = (c + d u) / u$ with $u$ a unit of the overlap ring $k [u, u^{- 1}, a, b, c, d]$ ; hence the two chart ideals $(a + b u, c + d u)$ and $(a v + b, c v + d)$ generate the same ideal there and the closed subschemes $V (a + b u, c + d u) \subseteq U_{0} \times_{k} A_{k}^{4}$ and $V (a v + b, c v + d) \subseteq U_{1} \times_{k} A_{k}^{4}$ glue along the overlap. The glued scheme $Z$ therefore carries a morphism $i : Z \to P_{k}^{1} \times_{k} A_{k}^{4}$ whose restrictions to the two charts are these closed immersions, and by locality of closed immersions on the target, $i$ is a closed immersion; the charts displayed in the Given are exactly its restrictions, and the two equations $a s + b t = 0$ , $c s + d t = 0$ restrict to $a + b u$ , $c + d u$ over $U_{0}$ and to $a v + b$ , $c v + d$ over $U_{1}$ .

1.2F1F2F3F11F12

Let $R_{0} = k [u, a, b, c, d] / (a + b u, c + d u)$ be the coordinate ring of the first chart $Z_{0} = Z \cap (U_{0} \times_{k} A_{k}^{4})$ and let $R_{1} = k [v, a, b, c, d] / (a v + b, c v + d)$ be that of the second. On the first chart the class of $a d - b c$ equals $(- b u) d - b (- d u) = 0$ , and on the second it equals $a (- c v) - (- a v) c = 0$ ; so $a d - b c$ lies in the kernel of each of the two ring maps $k [a, b, c, d] \to R_{j}$ describing the projections $Z_{j} \to A_{k}^{4}$ , whose images are therefore contained in $V (a d - b c)$ since a contraction of a prime contains the kernel. The charts $U_{0}, U_{1}$ cover $P_{k}^{1}$ , so $Z = Z_{0} \cup Z_{1}$ and the image $π (Z)$ is the union of the two images of the $Z_{j}$ ; hence $π (Z) \subseteq V (a d - b c)$ .

1.3F1F3F11F12F13F14

Conversely, let $p \in V (a d - b c)$ , so that $a d - b c \in p \subseteq k [a, b, c, d]$ , and put $F = κ (p) = Frac (k [a, b, c, d] / p)$ ; write $a^{'}, b^{'}, c^{'}, d^{'}$ for the images in $F$ of $a, b, c, d$ , so that $a^{'} d^{'} = b^{'} c^{'}$ . Choose $(s, t) \in F^{2}$ as follows: if $(a^{'}, b^{'}) \neq (0, 0)$ take $(s, t) = (- b^{'}, a^{'})$ ; if $(a^{'}, b^{'}) = (0, 0) \neq (c^{'}, d^{'})$ take $(s, t) = (d^{'}, - c^{'})$ ; if $(a^{'}, b^{'}) = (c^{'}, d^{'}) = (0, 0)$ take $(s, t) = (1, 0)$ . In each case $(s, t) \neq (0, 0)$ , and $a^{'} s + b^{'} t = 0 = c^{'} s + d^{'} t$ : in the first case because $- a^{'} b^{'} + b^{'} a^{'} = 0$ and $- c^{'} b^{'} + d^{'} a^{'} = a^{'} d^{'} - b^{'} c^{'} = 0$ , in the second because $a^{'} = b^{'} = 0$ and $c^{'} d^{'} - d^{'} c^{'} = 0$ , and in the third because $a^{'} = b^{'} = c^{'} = d^{'} = 0$ . At least one of $s, t$ is nonzero; suppose first that $s \neq 0$ and put $u^{'} = t / s \in F$ . The $k$ -algebra map $ψ : k [u, a, b, c, d] \to F$ with $u \mapsto u^{'}$ , $a \mapsto a^{'}$ , $b \mapsto b^{'}$ , $c \mapsto c^{'}$ , $d \mapsto d^{'}$ satisfies $ψ (a + b u) = (a^{'} s + b^{'} t) / s = 0$ and $ψ (c + d u) = (c^{'} s + d^{'} t) / s = 0$ ; by [F11] it corresponds to a morphism $Spec F \to U_{0} \times_{k} A_{k}^{4}$ whose image is the prime $\ker ψ$ , which contains $a + b u$ and $c + d u$ , hence lies in $V (a + b u, c + d u) = ∣ Z_{0} ∣ \subseteq ∣ Z ∣$ by [F12]. The composite of this morphism with the projection to $A_{k}^{4}$ corresponds to the ring map $k [a, b, c, d] \to F$ , $a \mapsto a^{'}$ , $b \mapsto b^{'}$ , $c \mapsto c^{'}$ , $d \mapsto d^{'}$ , that is, by [F13] to the canonical morphism $Spec κ (p) \to A_{k}^{4}$ of [F14], whose image is $p$ ; hence $p = π (\ker ψ)$ lies in the image of $π$ . If $s = 0$ then $t \neq 0$ , and the same computation with $v^{'} = s / t$ in the chart $U_{1}$ gives $ψ (a v + b) = (a^{'} s + b^{'} t) / t = 0$ , $ψ (c v + d) = (c^{'} s + d^{'} t) / t = 0$ and again $p \in π (Z)$ . Therefore $V (a d - b c) \subseteq π (Z)$ .

2.1F5F6F7F8F9step 1.1

Let $p : P_{k}^{1} \times_{k} A_{k}^{4} \to A_{k}^{4}$ be the second projection and let $q : P_{k}^{1} \to Spec k$ and $r : A_{k}^{4} \to Spec k$ be the structure morphisms. Since $p$ arises from the fibre product of $q$ and $r$ , it is the base change of $q$ along $r$ ; by the AC-qualified [F6] the morphism $q$ is proper, so the AC-qualified [F7] makes $p$ proper. By the AC-qualified [F8] the closed immersion $i$ of step 1.1 is proper, so the composite $π = p \circ i : Z \to A_{k}^{4}$ is a composite of proper morphisms and is proper by the AC-qualified [F9].

3.1F10F12step 1.2step 1.3step 2.1

Since $π$ is proper, [F10] shows that $π$ is a closed map; hence the image $π (Z)$ of the whole source is closed in $A_{k}^{4}$ . By step 1.2 the image is contained in $V (a d - b c)$ , and by step 1.3 it contains $V (a d - b c)$ ; since it is closed, the two inclusions give $π (Z) = V (a d - b c)$ .

4.1F1F6F7F8F9F15step 1.2step 1.3step 2.1step 3.1∎

Combining the steps, the projection $π : Z \to A_{k}^{4}$ is proper by step 2.1 and its image is exactly $V (a d - b c)$ by step 3.1. The Axiom of Choice [F15] is assumed and used only through the AC-qualified properness suppliers [F6], [F7], [F8] and [F9]; the chart computation of step 1.2 and the residue-field case analysis of step 1.3 involve no selection. The degenerate cases are covered: for $(a, b, c, d) = (0, 0, 0, 0)$ all three cases of step 1.3 admit $(s, t)$ , so the whole fibre $P_{k}^{1}$ over the origin lies in $Z$ ; the argument uses no hypothesis on the field beyond being a field, so it applies in every characteristic including $2$ , and no Noetherian, reducedness or nonemptiness hypothesis is imposed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

73 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

Stacks Project, Morphisms of Schemes §§29.11, 29.42–45 (standard reference, not scraped)
Vakil, The Rising Sea §§8.3, 11.3, 17.4 (standard reference, not scraped)