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;
• SheafOfModules.isInvertible_unit records that the structure sheaf 𝒪_X, as a sheaf of modules over itself, is invertible;
• SheafOfModules.isInvertible_iff_exists_isOpenCover characterizes invertible sheaves on a scheme as those whose restrictions to the open subschemes of some open cover are isomorphic to the structure sheaves of those open subschemes.

A free rank-one trivialization of an 𝒪_X-module M over an open V gives local coordinates:

• Scheme.Modules.trivializationCoordinate is the linear isomorphism Γ(M, W) ≃ Γ(X, W) it induces on every open W ≤ V, compatible with restriction in both directions (Scheme.Modules.trivializationCoordinate_map and Scheme.Modules.map_trivializationCoordinate_symm), and Scheme.Modules.trivializationGenerator is the basis section of M over V with coordinate one;
• Scheme.Modules.existsUnique_eq_smul_map_trivializationGenerator writes every section over W ≤ V uniquely as a regular multiple of the restricted basis section, and Scheme.Modules.existsUnique_map_trivializationGenerator_eq_smul shows that the basis sections of two trivializations differ by a unique regular unit on any common open subset.

These local rank-one coordinates describe transition functions between local bases and provide normal forms for sections used in line-bundle constructions.

noncomputable def TauCeti.AlgebraicGeometry.SheafOfModules.LocalTrivializations.ofIsOpenCover (X : AlgebraicGeometry.Scheme) {M : X.Modules} {ι : Type u} (W : ι → X.Opens) (hW : TopologicalSpace.IsOpenCover W) (e : (i : ι) → SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf (W i)) ≅ SheafOfModules.over M (W i)) : SheafOfModules.LocalTrivializations M

Construct a rank-one atlas from an open cover and a trivialization on each member.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.AlgebraicGeometry.SheafOfModules.LocalTrivializations.ofForallMem (X : AlgebraicGeometry.Scheme) {M : X.Modules} (V : ↥X → X.Opens) (hx : ∀ (x : ↥X), x ∈ V x) (e : (x : ↥X) → SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf (V x)) ≅ SheafOfModules.over M (V x)) : SheafOfModules.LocalTrivializations M

Construct a rank-one atlas from a neighbourhood of each point and a trivialization there.

Equations

• TauCeti.AlgebraicGeometry.SheafOfModules.LocalTrivializations.ofForallMem X V hx e = TauCeti.AlgebraicGeometry.SheafOfModules.LocalTrivializations.ofIsOpenCover X V ⋯ e

@[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

instance TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible_unit (X : AlgebraicGeometry.Scheme) : isInvertible X (SheafOfModules.unit X.ringCatSheaf)

The structure sheaf, regarded as a sheaf of modules over itself, is an invertible sheaf: it is the free sheaf on one generator.

@[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}

noncomputable def TauCeti.SheafOfModules.LocalTrivializations.unitIsoRestrict {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U : X.Opens} (e : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M U) : SheafOfModules.unit (↑U).ringCatSheaf ≅ M.restrict U.ι

A free rank-one trivialization over an open is an isomorphism from the structure sheaf of the open subscheme to the restricted module sheaf.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible_iff_exists_isOpenCover {X : AlgebraicGeometry.Scheme} {M : X.Modules} : isInvertible X M ↔ ∃ (ι : Type u) (W : ι → X.Opens), TopologicalSpace.IsOpenCover W ∧ ∀ (i : ι), Nonempty (SheafOfModules.unit (↑(W i)).ringCatSheaf ≅ M.restrict (W i).ι)

A sheaf of modules on a scheme is invertible exactly when an open cover of the scheme trivializes it: on every member W of the cover, its restriction to the open subscheme W is isomorphic to the structure sheaf 𝒪_W.

noncomputable def AlgebraicGeometry.Scheme.Modules.trivializationCoordinateIso {X : Scheme} (M : X.Modules) {U : X.Opens} (e : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M U) : SheafOfModules.over M U ≅ SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf U)

The coordinate isomorphism from a locally trivial rank-one module sheaf to the structure sheaf on the trivializing open subset.

Equations

• M.trivializationCoordinateIso e = e.symm ≪≫ TauCeti.SheafOfModules.freePUnitIsoUnit (CategoryTheory.Sheaf.over X.ringCatSheaf U)

noncomputable def AlgebraicGeometry.Scheme.Modules.trivializationCoordinate {X : Scheme} (M : X.Modules) {U W : X.Opens} (e : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M U) (i : W ⟶ U) : ↑(M.presheaf.obj (Opposite.op W)) ≃ₗ[↑(X.presheaf.obj (Opposite.op W))] ↑(X.presheaf.obj (Opposite.op W))

The coordinate of a free rank-one trivialization over U, read on an open subset W ≤ U: the linear isomorphism between sections of the module sheaf and regular functions on W.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Modules.trivializationCoordinate_apply {X : Scheme} (M : X.Modules) {U W : X.Opens} (e : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M U) (i : W ⟶ U) (s : ↑(M.presheaf.obj (Opposite.op W))) : (M.trivializationCoordinate e i) s = (CategoryTheory.ConcreteCategory.hom ((M.trivializationCoordinateIso e).hom.val.app (Opposite.op (CategoryTheory.Over.mk i)))) s

The coordinate on W ≤ U is the component of the coordinate isomorphism at W.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.trivializationCoordinate_map {X : Scheme} (M : X.Modules) {U W W' : X.Opens} (e : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M U) (i : W ⟶ U) (j : W' ⟶ W) (s : ↑(M.presheaf.obj (Opposite.op W))) : (M.trivializationCoordinate e (CategoryTheory.CategoryStruct.comp j i)) ((CategoryTheory.ConcreteCategory.hom (M.presheaf.map j.op)) s) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map j.op)) ((M.trivializationCoordinate e i) s)

The coordinate of a free rank-one trivialization commutes with restriction to a smaller open subset.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.map_trivializationCoordinate_symm {X : Scheme} (M : X.Modules) {U W W' : X.Opens} (e : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M U) (i : W ⟶ U) (j : W' ⟶ W) (r : ↑(X.presheaf.obj (Opposite.op W))) : (CategoryTheory.ConcreteCategory.hom (M.presheaf.map j.op)) ((M.trivializationCoordinate e i).symm r) = (M.trivializationCoordinate e (CategoryTheory.CategoryStruct.comp j i)).symm ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map j.op)) r)

The inverse coordinate of a free rank-one trivialization commutes with restriction to a smaller open subset.

noncomputable def AlgebraicGeometry.Scheme.Modules.trivializationGenerator {X : Scheme} (M : X.Modules) {V : X.Opens} (t : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V) : ↑(M.presheaf.obj (Opposite.op V))

The basis section of a line bundle over an open subset carrying a chosen rank-one trivialization.

Equations

• M.trivializationGenerator t = (M.trivializationCoordinate t (CategoryTheory.CategoryStruct.id V)).symm 1

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.trivializationCoordinate_map_trivializationGenerator {X : Scheme} (M : X.Modules) {V W : X.Opens} (t : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V) (i : W ⟶ V) : (M.trivializationCoordinate t i) ((CategoryTheory.ConcreteCategory.hom (M.presheaf.map i.op)) (M.trivializationGenerator t)) = 1

The chosen trivialization reads the restriction of its basis section to any open subset W ≤ V as the constant coordinate one.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.trivializationCoordinate_trivializationGenerator {X : Scheme} (M : X.Modules) {V : X.Opens} (t : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V) : (M.trivializationCoordinate t (CategoryTheory.CategoryStruct.id V)) (M.trivializationGenerator t) = 1

The basis section of a rank-one trivialization has coordinate one.

theorem AlgebraicGeometry.Scheme.Modules.eq_trivializationCoordinate_smul_map_trivializationGenerator {X : Scheme} (M : X.Modules) {V W : X.Opens} (t : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V) (i : W ⟶ V) (s : ↑(M.presheaf.obj (Opposite.op W))) : s = (M.trivializationCoordinate t i) s • (CategoryTheory.ConcreteCategory.hom (M.presheaf.map i.op)) (M.trivializationGenerator t)

A section is its coordinate times the restricted basis section of a rank-one trivialization.

theorem AlgebraicGeometry.Scheme.Modules.existsUnique_eq_smul_map_trivializationGenerator {X : Scheme} (M : X.Modules) {V W : X.Opens} (t : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V) (i : W ⟶ V) (s : ↑(M.presheaf.obj (Opposite.op W))) : ∃! r : ↑(X.presheaf.obj (Opposite.op W)), s = r • (CategoryTheory.ConcreteCategory.hom (M.presheaf.map i.op)) (M.trivializationGenerator t)

On an open subset W ≤ V, every section is a unique regular-function multiple of the restriction of the basis section of a rank-one trivialization over V.

theorem AlgebraicGeometry.Scheme.Modules.existsUnique_map_trivializationGenerator_eq_smul {X : Scheme} (M : X.Modules) {V₁ V₂ W : X.Opens} (t₁ : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V₁) (t₂ : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V₂) (i₁ : W ⟶ V₁) (i₂ : W ⟶ V₂) : ∃! u : (↑(X.presheaf.obj (Opposite.op W)))ˣ, (CategoryTheory.ConcreteCategory.hom (M.presheaf.map i₁.op)) (M.trivializationGenerator t₁) = ↑u • (CategoryTheory.ConcreteCategory.hom (M.presheaf.map i₂.op)) (M.trivializationGenerator t₂)

On an open subset W contained in the domains of two rank-one trivializations, the restrictions of their basis sections differ by a unique unit of the regular functions on W.

theorem AlgebraicGeometry.Scheme.Modules.trivializationGenerator_ne_zero {X : Scheme} (M : X.Modules) {V : X.Opens} (t : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V) [Nonempty ↥↑V] : M.trivializationGenerator t ≠ 0

The distinguished basis section of a rank-one trivialization is nonzero on a nonempty open subset.

theorem AlgebraicGeometry.Scheme.Modules.exists_mem_trivialization {X : Scheme} (M : X.Modules) [TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X M] (x : ↥X) : ∃ (V : X.Opens) (x_1 : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V), x ∈ V

Every point of a scheme lies in the domain of a rank-one trivialization of an invertible sheaf.