Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge pass (gpt-6-sol)audited 2026-09-27
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.

Relative projective space from standard charts

Definition

Fix n≥0. For i∈{0,…,n} let Bi=Z[t0,…,tn]/(ti−1)≅Z[xℓ(i):ℓ≠i], where xℓ(i) denotes the class of tℓ/ti, so that Ui:=Spec⁡Bi is an affine scheme with coordinates xℓ(i) for ℓ≠i. For i≠j let Dj(i)⊆Ui be the distinguished open where xj(i) is invertible. Over it the formula xℓ(i)=tℓti=tℓ/tjti/tj=xℓ(j)xi(j) for ℓ≠i,j, together with xj(i)=1/xi(j), defines a Z-algebra isomorphism (Bi)xj(i)⟶(Bj)xi(j),xℓ(i)↦xℓ(j)/xi(j)  (ℓ≠i,j),xj(i)↦1/xi(j), and these morphisms identify the open subschemes Dj(i)⊆Ui and Di(j)⊆Uj by A principal localization identifies its spectrum with a distinguished open. This is the reciprocal of the analogous formula with i,j interchanged, and on a triple overlap Ui∩Uj∩Uk both composites send xℓ(i) to xℓ(k)/xi(k), so the identity and cocycle conditions of Gluing affine schemes along compatible open isomorphisms hold and the affine schemes Ui glue to a scheme, denoted PZn, whose open subschemes Ui form an affine cover and are its standard charts.

For an arbitrary base scheme S define PSn=S×Spec⁡ZPZn, with structure morphism the projection to S (Existence of all scheme fibre products, Schemes and morphisms over a base), and call the open subschemes UiS=S×Spec⁡ZUi the standard charts over S; each is affine over S, and they form an open cover of PSn. When S=Spec⁡A is affine, each UiS is the affine scheme Spec⁡A[xℓ(i):ℓ≠i]. Because base change preserves open immersions and fibre products, the transition isomorphisms on UiS∩UjS are the base changes of the displayed ones, so the charts and their overlaps commute with base change.

For n=0 there is one chart U0=Spec⁡Z[t0]/(t0−1)≅Spec⁡Z, no gluing takes place, and PZ0=Spec⁡Z, so PS0≅S. For S=∅ the product is empty, so P∅n=∅. For n≥1 the constructions for the pairs (i,j) and (j,i) are reciprocal as displayed, and the case i=j is the identity on Ui.

Depends on

Used by

Dependency tree · two levels

19 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