LemmaStatement: Literature-sourcedProof: AI-generated

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.

Smooth point classes lie in the top filtration piece

PDF p. 7: Lemma 2.9 and final square

Statement

Assume the Axiom of Choice and the size conventions of the support construction. Let $k$ be a perfect field, let $X$ be a quasi-compact quasi-separated $k$ -scheme of pure finite dimension $d$ , and let $x$ be a closed point in the smooth locus of $X \to Spec k$ . Put $U = X ∖ {x}$ . A perfect field is one whose algebraic extensions are separable; smoothness at $x$ means that $x$ has a neighbourhood smooth over $k$ .

Write $K (X / U)$ for the restriction fiber $fib (K (X) \to K (U))$ and $F^{j} K (X / U)$ for the corresponding fiber at motivic filtration stage $j$ , using the extension to arbitrary open subsets in Motivic and filtered K theory with support. Then the stage-to- $K$ map induces a surjection $π_{0} F_{m o t}^{d} K (X / U) ⟶ π_{0} K (X / U) .$ Consequently, with $K_{0} ({x}; X)$ the image of $π_{0} K (X / U) \to K_{0} (X)$ and $F_{m o t}^{d} K_{0} (X)$ the image of $π_{0} F_{m o t}^{d} K (X) \to K_{0} (X)$ , $K_{0} ({x}; X) \subseteq F_{m o t}^{d} K_{0} (X) .$ In particular, the smooth-point class map of Smooth-point K theory class map has image in this filtration subgroup. No injectivity of either support-to-global map is asserted.

Facts & Assumptions

Given: The field, scheme, point, choice and size hypotheses in the statement. Set $T = {x}$ and write $F_{T}^{j} K (X) = F^{j} K (X / U)$ . A decreasing filtration is a sequence of spectra with compatible transition maps $F^{j + 1} \to F^{j}$ ; its $j$ th graded spectrum is their cofiber. A fiber is the homotopy pullback over the zero spectrum.

Goal: Prove surjectivity from supported stage $d$ to supported $K_{0}$ , and then the global image containment.

[F1]

Motivic filtration and image groups gives a functorial tower with $F^{0} K ≃ K$ . Motivic and filtered K theory with support defines its supported stages as restriction fibers, including the homotopy-limit extension when $U$ is not quasi-compact, and identifies $π_{0}$ of the shifted supported weight- $j$ motivic spectrum with $H_{m o t, T}^{2 j, j} (X, Z)$ .

[F2]

Motivic graded pieces and spectral sequence gives, naturally for every qcqs scheme and $j \geq 0$ , the graded triangle with third term $Z (j)_{m o t} [2 j]$ . Support fibers commute with graded triangles identifies the graded spectrum of a supported tower with the fiber of the corresponding graded restriction arrow. The stable spectra interface Stable spectra and exact triangles supplies the finite limits and cofiber–fiber identification used for the open-set homotopy-limit extension.

[F3]

Motivic purity and lower-weight vanishing at a smooth closed point gives $H_{m o t, T}^{i, j} (X, Z) = 0$ for every integer $i$ and $0 \leq j < d$ under the given perfect-field, smooth-point, choice and size hypotheses.

[F4]

Stage projections, kernels and image groups gives exactness of $π_{0} F_{T}^{j + 1} K (X) \to π_{0} F_{T}^{j} K (X) \to π_{0} {gr}_{T}^{j} K (X)$ . Images of support groups in global groups and Smooth-point K theory class map specify the global image subgroup and the smooth-point map.

Proof

technique · Use lower-weight supported motivic vanishing to lift successively through the finite sequence of filtration stages, then apply the natural support-to-global square

1.1F1F2given

For each $j \geq 0$ , the natural graded triangle in [F2] applies on $X$ and on every quasi-compact open $V \subseteq U$ . Taking the homotopy limit of the triangles over these $V$ preserves fiber sequences: limits commute with the finite limits defining fibers, and in spectra cofibers and fibers differ by suspension. Thus the graded triangle also holds for the explicitly extended values on $U$ . Taking the fiber of the graded restriction arrow, [F2] identifies ${gr}_{T}^{j} K (X)$ with the shifted supported weight- $j$ motivic spectrum. Hence $π_{0} {gr}_{T}^{j} K (X) ≅ H_{m o t, T}^{2 j, j} (X, Z) .$ The identification uses the actual coherent restriction maps, not merely separate isomorphisms of groups.

2.1F3F4step 1.1

For $0 \leq j < d$ , [F3] makes the right side in step 1.1 zero. Exactness in [F4] therefore makes each transition $π_{0} F_{T}^{j + 1} K (X) \to π_{0} F_{T}^{j} K (X)$ surjective.

3.1F1step 2.1

Composing these finitely many surjections gives a surjection $π_{0} F_{T}^{d} K (X) \to π_{0} F_{T}^{0} K (X)$ . When $d = 0$ this is the identity, the empty composite. The natural stage-zero equivalences on $X$ and on the opens used to define $U$ identify $F_{T}^{0} K (X)$ with $K (X / U)$ ; compatibility of transitions identifies the composite with the stated stage-to- $K$ map. This proves the supported surjectivity.

4.1F1F4step 3.1∎

The support-to-global maps and stage-to- $K$ maps form a commutative square by the functorial fiber construction. Given an element of $K_{0} (T; X)$ , choose a supported $K_{0}$ representative and lift it to supported stage $d$ by step 3.1. Its image in global stage $d$ maps to the original element of $K_{0} (X)$ . The definition of the global image filtration therefore gives the containment. The image of the point class map is $K_{0} (T; X)$ by [F4], yielding the final assertion. This completes the proof.

Depends on

Used by · 2

Dependency tree · 3 levels

Arrows run from prerequisites to the items that use them. External source nodes link directly to the cited text. The view shows up to three dependency steps; open a prerequisite to continue.

Sources

Jean Fasel and Maria Yakerson, Vector bundles on singular surfaces and threefolds · p. 7, Lemma 2.9 and its final commutative square