Line bundles on local and discrete schemes are trivial

If every point of a scheme X specializes to a single point x, then the only open subset of X containing x is X itself. A line bundle is trivial on some open neighbourhood of x, so it is trivial on X, and the Picard group of X is trivial. This applies to the spectrum of a local ring, and in particular to the spectrum of a field.

If instead the underlying space of X is discrete, as for a scheme finite over a field, each point is an open subset on which a line bundle has a basis, and these bases glue to a global basis; so the Picard group of X is again trivial.

The triviality of Pic(Spec K) for a field K is what makes invariants of line bundles computed on the fibres Spec K ×_T X_T of a base change insensitive to line bundles pulled back from the base T.

Main declarations

• TauCeti.AlgebraicGeometry.LineBundleClass.eq_one_of_forall_specializes: on a scheme in which every point specializes to a fixed point, every line-bundle class is trivial;
• TauCeti.AlgebraicGeometry.LineBundleClass.subsingleton_spec_of_isLocalRing: the Picard group of the spectrum of a local ring is trivial;
• TauCeti.AlgebraicGeometry.LineBundleClass.eq_one_of_discreteTopology and TauCeti.AlgebraicGeometry.LineBundleClass.subsingleton_of_discreteTopology: the Picard group of a scheme with discrete underlying space is trivial.

References

• R. Hartshorne, Algebraic Geometry, Chapter II, Section 6.

theorem TauCeti.AlgebraicGeometry.LineBundleClass.eq_one_of_forall_specializes {X : AlgebraicGeometry.Scheme} {x : ↥X} (hx : ∀ (y : ↥X), y ⤳ x) (a : LineBundleClass X) : a = 1

Line bundles on a local scheme are trivial. If every point of X specializes to x, then every line-bundle class on X is the identity.

instance TauCeti.AlgebraicGeometry.LineBundleClass.subsingleton_spec_of_isLocalRing (R : Type u) [CommRing R] [IsLocalRing R] : Subsingleton (LineBundleClass (AlgebraicGeometry.Spec ↧R))

The Picard group of the spectrum of a local ring is trivial. In particular every line bundle on the spectrum of a field is trivial.

theorem TauCeti.AlgebraicGeometry.LineBundleClass.eq_one_of_discreteTopology {X : AlgebraicGeometry.Scheme} [DiscreteTopology ↥X] (a : LineBundleClass X) : a = 1

Line bundles on a discrete scheme are trivial. If the underlying space of X is discrete, as it is for a locally Artinian scheme such as a scheme finite over a field, then every line-bundle class on X is the identity.

instance TauCeti.AlgebraicGeometry.LineBundleClass.subsingleton_of_discreteTopology {X : AlgebraicGeometry.Scheme} [DiscreteTopology ↥X] : Subsingleton (LineBundleClass X)

The Picard group of a discrete scheme is trivial.