Morphisms from a line bundle onto local bases

Let L be an invertible sheaf on a scheme X and φ : L ⟶ N a morphism of 𝒪_X-modules. Suppose that every point of X has an open neighbourhood V and a section s of L over V whose image φ(s) is a basis of N over V: on every open W ⊆ V, every section of N is a unique regular multiple of the restriction of φ(s). Then φ is an isomorphism.

Near a point, write s = r • e for a basis section e of L. Then φ(e) = c • φ(s) for a regular function c, and φ(s) = r c • φ(s) forces r c = 1, so φ sends the basis e of L to the basis c • φ(s) of N. Hence φ is bijective on sections over every small enough open, and being an isomorphism is local.

This recognizes a morphism of line bundles as an isomorphism from the image of a single local section, without knowing the sections of the source L explicitly. It applies when L is a pullback, whose sections are not described concretely.

theorem AlgebraicGeometry.Scheme.Modules.isIso_of_forall_exists_bijective_smul {X : Scheme} {L N : X.Modules} [TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X L] (φ : L ⟶ N) (h : ∀ (x : ↥X), ∃ (V : X.Opens) (_ : x ∈ V) (s : ↑(L.presheaf.obj (Opposite.op V))), ∀ (W : X.Opens) (i : W ⟶ V), Function.Bijective fun (r : ↑(X.presheaf.obj (Opposite.op W))) => r • (CategoryTheory.ConcreteCategory.hom (N.presheaf.map i.op)) ((CategoryTheory.ConcreteCategory.hom (Hom.app φ V)) s)) : CategoryTheory.IsIso φ

A morphism from a line bundle onto local bases is an isomorphism. Let L be an invertible sheaf. If every point has an open neighbourhood V and a section s of L over V such that φ(s) is a basis of N over V, in the sense that for every open W ⊆ V every section of N over W is a unique regular multiple of the restriction of φ(s), then φ : L ⟶ N is an isomorphism.