Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass
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.

Chow groups of projective space

Statement

Assume the Axiom of Choice (The Axiom of Choice) inherited from the proper/quasi-finite and scheme base-change suppliers. Let k be a field and n≥0. Then for every d: Ad(Pkn)={Z⋅[Pd],0≤d≤n,0,otherwise, where Pd⊆Pn is a d-dimensional linear subspace and [Pd] its class (Rational equivalence and the Chow group of cycles, Algebraic cycles and the cycle group of a scheme of finite type over a field). In particular the degree homomorphism deg⁡:A0(Pkn)→ ≅ Z,∑xmx[x]⟼∑xmx[κ(x):k], is an isomorphism; its inverse sends 1 to [P0] for any k-rational point, and every 0-cycle whose support consists of k-rational points has class (∑xmx) [P0]. For k=C this is the classical cellular decomposition. More generally, Ad(Akn)=Z for d=n and Ad(Akn)=0 otherwise: homotopy invariance shifts degrees by n, and A∗(Spec⁡k) is Z in degree 0, so every cycle on affine space of dimension less than n is rationally equivalent to zero. For n=1, a closed point of degree greater than one is the principal divisor of its monic irreducible polynomial; linear polynomials suffice for rational points.

Facts & Assumptions

Given: the Axiom of Choice; a field k and n≥0; the linear subspaces Pd⊆Pn.

[L1]

The localization sequence Am(Z)→i∗Am(T)→j∗Am(U)→0 is exact for a closed immersion i:Z↪T with open complement U, and the projection T×Ar→T induces Am(T)≅Am+r(T×Ar) (Localization sequence for Chow groups and homotopy invariance of affine space).

[L2]

First Chern classes of invertible sheaves define graded cap operations c1(L)∩−:Am(X)→Am−1(X) which are additive and commute with proper pushforward and flat pullback; on an integral W with a rational section s not vanishing identically, c1(L)∩[W]=[div⁡L(s)] (Intersection with an invertible sheaf and the first Chern class).

[L3]

Proper pushforward of a closed point x to Spec⁡k is [κ(x):k] times the fundamental class of the point, by the norm-degree definition (Proper pushforward of cycles and the norm formula, Rational equivalence and the Chow group of cycles).

[L4]

The standard affine charts of Pkn are affine n-space, and Pkn∖H≅Akn for a coordinate hyperplane H (Relative projective space from standard charts, Projective space is Proj of a polynomial ring, Twisting sheaf on Proj).

Proof

technique · direct; use localization and homotopy invariance for the affine and projective decompositions, and the cap operation of $\mathcal O(1)$ followed by degree for independence
1.1L1L4givenalgebra

Affine space. Applying homotopy invariance [L1] successively in the n coordinates gives Ad(Akn)≅Ad−n(Spec⁡k), which is Z for d=n and 0 otherwise; the top class is [An] and for n=1 every closed point is the principal divisor of its monic irreducible polynomial in k[t], which is linear precisely for a rational point.

2.1L1step 1.1givenalgebra

Generation of the Chow groups of projective space. For n=0, projective space is Spec⁡k and the assertion is immediate. Assume n≥1. Let H=Pn−1⊆Pn be a coordinate hyperplane with complement An. Localization [L1] gives the exact sequence Ad(Pn−1)→i∗Ad(Pn)→j∗Ad(An)→0. For d<n the group Ad(An) vanishes by step 1.1, so i∗ is surjective, and induction on n proves that Ad(Pn) is generated by the class [Pd] of a d-dimensional linear subspace: in the hyperplane the class of a d-dimensional linear subspace generates by induction, and its pushforward is the class of the corresponding linear subspace of Pn; the induction starts at n=d, where Pd has no hyperplane below it. For d=n the same exact sequence reads 0=An(Pn−1)→An(Pn)→An(An)≅Z→0 by step 1.1, so An(Pn)=Z[Pn] is generated by the top class, and the cycle group Zn(Pn)=Z[Pn] admits no nonzero rational equivalences because none of its subvarieties has dimension n+1. For d<0 or d>n there are no integral closed subschemes of dimension d, so Ad(Pn)=0.

3.1L2L3step 2.1algebra

Independence. Fix d with 0≤d≤n and let c1=c1(O(1))∩−; by [L2] the iterated cap c1d maps Am(Pn) to Am−d(Pn), is additive, and is defined by cutting with d coordinate hyperplanes in general position. On the linear subspace Pd, the d coordinate hyperplanes cut it in a single k-rational point, so c1d[Pd]=[P0], and the degree homomorphism deg⁡:A0(Pn)→Z of [L3] sends [P0] to 1; hence deg⁡∘c1d is a homomorphism Ad(Pn)→Z sending the generator [Pd] of step 2.1 to 1. A cyclic group admitting a homomorphism onto Z with generator mapping to 1 is infinite cyclic, so Ad(Pn)=Z⋅[Pd].

4.1L3step 3.1givenalgebra∎

The degree isomorphism and closed points. By steps 2.1 and 3.1, A0(Pn) is generated by [P0] for a k-rational point; for a closed point x with residue field κ(x), proper pushforward to Spec⁡k is multiplication by [κ(x):k] by [L3], so [x]=[κ(x):k][P0] and deg⁡ is the stated isomorphism; a 0-cycle supported on k-rational points has class (∑xmx)[P0]. The computation over C is the classical cellular decomposition under the same identification.

Depends on

Used by

Dependency tree · two levels

61 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