Invertible sheaves on a scheme

This file begins the scheme-level line-bundle lane of the Jacobian challenge. An invertible sheaf on a scheme X is an 𝒪_X-module which is locally free of rank one.

The rank-one condition itself is not specific to schemes: it is TauCeti.SheafOfModules.IsInvertible from TauCeti/Algebra/Category/ModuleCat/Sheaf/Invertible/Basic.lean, stated for a sheaf of modules over an arbitrary site. This file only packages it over a scheme:

• TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X is the ObjectProperty on X.Modules cut out by the predicate (closed under isomorphisms, by the site-level transport theorem, so ObjectProperty.prop_of_iso and ObjectProperty.prop_iff_of_iso apply to it);
• TauCeti.AlgebraicGeometry.InvertibleSheaf X is the full subcategory it cuts out;
• InvertibleSheaf.free X I is the free sheaf on an indexing type with exactly one element, and InvertibleSheaf.trivial X is the globally free rank-one sheaf.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, item "Invertible sheaves on a scheme; the Picard group Pic X under ⊗". The tensor product and Picard group require a monoidal structure on sheaves of modules and are left to subsequent files. No formalization is vendored.

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible (X : AlgebraicGeometry.Scheme) : CategoryTheory.ObjectProperty X.Modules

The object property of being an invertible sheaf on a scheme.

Equations

• TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X = TauCeti.SheafOfModules.IsInvertible

instance TauCeti.AlgebraicGeometry.SheafOfModules.instIsClosedUnderIsomorphismsModulesIsInvertible (X : AlgebraicGeometry.Scheme) : (isInvertible X).IsClosedUnderIsomorphisms

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.InvertibleSheaf (X : AlgebraicGeometry.Scheme) : Type (u + 1)

The full category of invertible sheaves on X. Its morphisms are morphisms of 𝒪_X-modules.

Equations

• TauCeti.AlgebraicGeometry.InvertibleSheaf X = (TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X).FullSubcategory

instance TauCeti.AlgebraicGeometry.InvertibleSheaf.instIsInvertibleObjModules {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) : SheafOfModules.isInvertible X L.obj

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.free (X : AlgebraicGeometry.Scheme) (I : Type u) [Nonempty I] [Subsingleton I] : InvertibleSheaf X

The invertible sheaf given by the free sheaf on an indexing type with exactly one element.

Equations

• TauCeti.AlgebraicGeometry.InvertibleSheaf.free X I = { obj := SheafOfModules.free I, property := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.free_obj (X : AlgebraicGeometry.Scheme) (I : Type u) [Nonempty I] [Subsingleton I] : (free X I).obj = SheafOfModules.free I

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial (X : AlgebraicGeometry.Scheme) : InvertibleSheaf X

The globally free rank-one invertible sheaf.

Equations

• TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X = TauCeti.AlgebraicGeometry.InvertibleSheaf.free X PUnit.{?u.1 + 1}

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial_obj (X : AlgebraicGeometry.Scheme) : (trivial X).obj = SheafOfModules.free PUnit.{u + 1}