LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Multiplication pulls back a symmetric line bundle to its square power

Statement

Assume AC and DC. Let $A / k$ be an abelian variety over any field and $L$ an invertible sheaf on $A$ . For every integer $n$ , with $[n] : A \to A$ denoting multiplication by $n$ , there is an isomorphism $[n]^{*} L ≅ L^{\otimes n (n + 1) / 2} \otimes ([- 1]^{*} L)^{\otimes n (n - 1) / 2} .$ In particular, if $L$ is symmetric, meaning $[- 1]^{*} L ≅ L$ , then $[n]^{*} L ≅ L^{\otimes n^{2}}$ . Negative tensor powers mean powers of the dual; these are isomorphisms of line bundles, without a claim of canonical trivialization at the identity.

Facts & Assumptions

[F1]

The group law of $A$ is commutative under AC. Thus the integer multiplication maps are homomorphisms, $[r] + [s] = [r + s]$ , $[r] \circ [s] = [r s]$ , and $[- 1]^{2} = {id}_{A}$ . (Abelian varieties over a field, A proper geometrically connected group variety is commutative)

[F2]

For any invertible sheaf $L$ , the alternating tensor product of the seven sum pullbacks on $A^{3}$ is trivial, under AC and DC. (The theorem of the cube for an abelian variety)

Proof

Given: AC, DC, $A / k$ , an invertible sheaf $L$ , and an integer $n$ .

1.1F1F2givenalgebra

Write $P_{r} = [r]^{*} L$ and $J = [- 1]^{*} L$ . The constant map $[0]$ pulls back $L$ to $O_{A} \otimes_{k} e^{*} L ≅ O_{A}$ , since $e^{*} L$ is one-dimensional. Thus the formula holds at $r = 0, 1, - 1$ . Pulling [F2] back along $x \mapsto (x, x, - x)$ gives $L^{\otimes 3} \otimes J ≅ P_{2}$ , because the two zero sum maps pull back to trivial bundles. This proves the formula at $r = 2$ .

2.1F1F2step 1.1algebra

For $r \geq 2$ pull [F2] back along $x \mapsto (x, x, [r - 1] x)$ . The resulting relation is $P_{r + 1} \otimes L^{\otimes 2} \otimes P_{r - 1} ≅ P_{2} \otimes P_{r}^{\otimes 2}$ . Suppose the formula holds at $r$ and $r - 1$ . Substituting it and the formula for $P_{2}$ , then cancelling invertible factors, gives the exponents $3 + 2 r (r + 1) / 2 - 2 - (r - 1) r / 2 = (r + 1) (r + 2) / 2$ on $L$ and $1 + 2 r (r - 1) / 2 - (r - 1) (r - 2) / 2 = r (r + 1) / 2$ on $J$ . Induction proves the assertion for all positive integers.

3.1F1step 1.1step 2.1algebra∎

If $n = - r$ with $r > 0$ , then $P_{- r} = [- 1]^{*} P_{r}$ by [F1]. Pulling the proved formula back by $[- 1]$ interchanges $L$ and $J$ and yields the exponents $r (r - 1) / 2 = n (n + 1) / 2$ on $L$ and $r (r + 1) / 2 = n (n - 1) / 2$ on $J$ . This proves every integer case. If $J ≅ L$ , the two exponents add to $n^{2}$ , giving the symmetric formula. All equalities use line-bundle tensor cancellation and morphism identities, which apply in every characteristic, including when $n$ vanishes in $k$ .

Depends on

Used by

Nonzero multiplication on an abelian variety is finite and faithfully flat Theorem

Dependency tree · two levels

22 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, Lemma 39.9.7 (standard reference, not scraped)