Rational trivializations of line bundles

A line bundle on an integral scheme is trivial on a dense open subset. Equivalently, it has a basis near the generic point. This is the first step in associating a divisor to an arbitrary line bundle: after fixing such a rational basis, its transition functions at codimension-one points give the coefficients of the divisor.

Main declaration

• SheafOfModules.exists_dense_open_trivialization produces a dense open subset containing the generic point on which an invertible sheaf is free of rank one.

theorem TauCeti.SheafOfModules.exists_dense_open_trivialization {X : AlgebraicGeometry.Scheme} [IrreducibleSpace ↥X] (M : X.Modules) [AlgebraicGeometry.SheafOfModules.isInvertible X M] : ∃ (U : X.Opens), genericPoint ↥X ∈ U ∧ Dense ↑U ∧ Nonempty (SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M U)

An invertible sheaf on an irreducible scheme is free of rank one on a dense open subset containing the generic point.

This is the rational trivialization used to associate a divisor to a line bundle: a local basis on an open neighbourhood of the generic point is a basis of the generic fibre.

theorem TauCeti.SheafOfModules.exists_dense_open_restrict_iso_unit {X : AlgebraicGeometry.Scheme} [IrreducibleSpace ↥X] (M : X.Modules) [AlgebraicGeometry.SheafOfModules.isInvertible X M] : ∃ (U : X.Opens), genericPoint ↥X ∈ U ∧ Dense ↑U ∧ Nonempty (M.restrict U.ι ≅ SheafOfModules.unit (↑U).ringCatSheaf)

An invertible sheaf on an irreducible scheme becomes the structure sheaf on a dense open subscheme containing the generic point.