LemmaStatement: Literature-sourcedProof: Literature-sourced

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.

Elmanto–Morrow weight-one comparison input

PDF p. 4: Property (2)

Statement

Let $F$ be $Q$ or $F_{p}$ for a prime $p$ , and let $X$ be a quasi-compact quasi-separated $F$ -scheme. There is a natural comparison map $R Γ_{N i s} (X, G_{m}) [- 1] ⟶ Z (1)_{m o t} (X)$ whose cofiber has zero cohomology in every degree at most three. The target is the Elmanto–Morrow complex of Elmanto–Morrow motivic complex input, and $G_{m}$ is the small-Nisnevich sheaf of units.

External input

The existence of this particular natural map and the cofiber bound are imported from Elmanto–Morrow, Corollary 7.11, with its map from (5.1). Their proof is not reconstructed here.

Facts & Assumptions

Given: A prime field $F$ and a qcqs $F$ -scheme $X$ .

Goal: State and apply the imported comparison under its exact hypotheses.

[F1]

The cited corollary supplies the comparison map and cofiber bound for every qcqs $F$ -scheme.

Proof

1.1F1given

The given $F$ and $X$ satisfy the hypotheses in [F1].

2.1F1givenstep 1.1∎

Applying that external input gives the displayed map, naturality, and the stated cofiber bound. This step invokes the published result and does not constitute a local proof of it.

Depends on

Used by · 1

Motivic weight one

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.

External dependencies

Elden Elmanto and Matthew Morrow, Motivic cohomology of equicharacteristic schemes · Theorem 1.1(6); Corollary 7.11 and its proof; comparison map (5.1)

For every qcqs scheme X over a prime field F, the natural comparison RΓ_Nis(X,G_m)[-1] → Z(1)_mot(X) has cofiber supported in cohomological degrees greater than 3.

Hypotheses: F is Q or F_p for a prime p; X is quasi-compact and quasi-separated over F; the motivic complex and comparison map are those constructed by Elmanto and Morrow.

Reading limits: The introduction, Theorem 1.1(6), and the statement and short proof of Corollary 7.11 were read. The underlying construction of map (5.1), Corollary 7.10, and their substantial proofs were not reconstructed or independently checked.

Sources

Elden Elmanto and Matthew Morrow, Motivic cohomology of equicharacteristic schemes · Theorem 1.1(6); Corollary 7.11 and its proof; comparison map (5.1)