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.
Dual of a line bundle is its tensor inverse
Statement
Let be a scheme and let be an invertible -module (Invertible sheaves), with dual (The internal Hom sheaf of two module sheaves). Then the evaluation pairing is an isomorphism of -modules, so canonically; here is the tensor product of sheaves of modules (Tensor product of sheaves of modules).
Moreover the dual is described by transition data: if and are trivialisations, and are the units with equal to multiplication by , then the induced trivialisations of have transition units , and is a trivialisation of whose transition units are , compatible with the evaluation isomorphism. No choice principle is used.
Facts & Assumptions
Given: A scheme and an invertible -module , with a cover and trivialisations .
is locally free of rank : there is an open cover by sets with ; equivalently, on each such open a generator induces an isomorphism , (Invertible sheaves).
is finite locally free, and on a chart with one has (Dual and base change for finite locally free sheaves).
Sections of the internal Hom are homomorphisms: , with restrictions given by restriction of morphisms, and restriction of the Hom sheaf to is (The internal Hom sheaf of two module sheaves, Modules on a ringed space).
The tensor product sheaf is the sheafification of the presheaf ; a natural family of -bilinear maps therefore induces a morphism of sheaves (Tensor product of sheaves of modules, Sheafification of a presheaf, Sheafification is left adjoint to the inclusion of sheaves into presheaves).
Universal property of the module tensor product: a bilinear map over a commutative ring factors uniquely through ; in particular , , is an isomorphism with inverse (Universal property of the tensor product for balanced maps into abelian groups).
A morphism of -modules which restricts to an isomorphism on each member of an open cover is an isomorphism, because sections over an open set are determined by their restrictions to a cover and compatible families glue (A sheaf on a topological space).
For an -module and open , evaluation on the unit section gives an isomorphism , , with inverse ; in particular , and an endomorphism of is an isomorphism exactly when its value at is a unit (Modules on a ringed space).
Proof technique: direct; define evaluation on the presheaf tensor product, and check it is an isomorphism on a trivialising cover, where it becomes the multiplication map of the structure sheaf.
Proof
Evaluation is a morphism: for each open the map , , is well defined by [F3], is -bilinear by additivity and -linearity of homomorphisms of module sheaves, and is compatible with restrictions; by [F4] it induces a morphism of -modules with .
On a chart with trivialisation , the induced trivialisation of the dual is , , which is an isomorphism because corresponds under to the isomorphism of [F7]; moreover every automorphism of the trivial bundle is multiplication by a unit of , again by [F7].
On such a chart , transport the evaluation morphism along the trivialisations : the result is the map , , which is an isomorphism by [F5], with inverse . By [F1] such trivialising charts cover , so restricts to an isomorphism on every member of a cover of , and is therefore an isomorphism by [F6]; this proves the first claim.
Transition units: let be two trivialisations as in the Statement, and put ; by step 1.2 the automorphism of is multiplication by , which is a unit because the automorphism is invertible. Computing the transition of the duals, for and with one has , since is multiplication by ; so the transition unit of is .
Compatibility with evaluation: under the trivialisation the evaluation pairing becomes multiplication , , by step 2.1, and under the transitions of step 2.2 both sides transform by and respectively, so the transition unit of is and evaluation is the identity trivialisation on overlaps; all constructions are local and canonical, so no choice principle is used.
Depends on
Invertible sheaves
Dual and base change for finite locally free sheaves
The internal Hom sheaf of two module sheaves
Tensor product of sheaves of modules
Sheafification of a presheaf
Sheafification is left adjoint to the inclusion of sheaves into presheaves
Universal property of the tensor product for balanced maps into abelian groups
Modules on a ringed space
A sheaf on a topological space