The associated sheaf of a Cartier divisor

This file owns the construction of O_X(D). It defines local equations of a Cartier divisor, the fractional subpresheaf of the rational presheaf generated by their inverses, and the associated sheaf as its module sheafification.

Local equations trivialize the result, so the associated sheaf is invertible; equationTransitionIso gives the canonical change of trivialization and equationTransitionIso_trans records its cocycle law. Pointwise multiplication of rational functions gives the canonical additive comparison before sheafification, and it is proved to be a local equivalence, which yields the tensor comparison associatedTensorAddIso.

The construction is intrinsic: the fractional presheaf is generated by every local equation. The scaffolding lemmas that establish the local surjectivity and injectivity conditions are private to this module; only the resulting sheaves, isomorphisms, and their defining data are exported.

def AlgebraicGeometry.Scheme.CartierDivisor.IsEquationOn {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) (U : X.Opens) (f : Additive (↑X.functionField)ˣ) : Prop

A rational function is an equation for D throughout U.

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.IsEquationOn D U f = ∀ x ∈ U, ↑D x = (X.localCartierClass x) f

theorem AlgebraicGeometry.Scheme.CartierDivisor.IsEquationOn.mono {X : Scheme} [IsIntegral X] {D : ↥X.CartierDivisor} {U V : X.Opens} {f : Additive (↑X.functionField)ˣ} (hf : IsEquationOn D U f) (h : V ≤ U) : IsEquationOn D V f

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.fractionalPresheaf {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) : X.PresheafOfModules

The fractional module presheaf attached to a Cartier divisor.

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.fractionalPresheaf D = (AlgebraicGeometry.Scheme.CartierDivisor.fractionalPresheafSubmodule✝ D).toPresheafOfModules

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.associatedSheaf {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) : X.Modules

The associated sheaf O_X(D), obtained by sheafifying the fractional presheaf.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.equationIso {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) (U : X.Opens) (f : Additive (↑X.functionField)ˣ) (hf : IsEquationOn D U f) : SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf U) ≅ SheafOfModules.over (associatedSheaf D) U

A local equation trivializes the associated sheaf on its domain.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.equationTransitionIso {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) (U : X.Opens) (f : Additive (↑X.functionField)ˣ) (hf : IsEquationOn D U f) (g : Additive (↑X.functionField)ˣ) (hg : IsEquationOn D U g) : SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf U) ≅ SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf U)

The canonical change of trivialization between two equations for the same divisor on an open.

Equations

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

theorem AlgebraicGeometry.Scheme.CartierDivisor.equationTransitionIso_trans {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) (U : X.Opens) (f : Additive (↑X.functionField)ˣ) (hf : IsEquationOn D U f) (g : Additive (↑X.functionField)ˣ) (hg : IsEquationOn D U g) (h : Additive (↑X.functionField)ˣ) (hh : IsEquationOn D U h) : equationTransitionIso D U f hf g hg ≪≫ equationTransitionIso D U g hg h hh = equationTransitionIso D U f hf h hh

Changes of local equation satisfy the cocycle law.

instance AlgebraicGeometry.Scheme.CartierDivisor.associatedSheaf_isInvertible {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) : (have this := associatedSheaf D; this).IsInvertible

The associated sheaf of a Cartier divisor is invertible.

@[implicit_reducible]

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.instMonoidalCategoryPresheafOfModules {X : Scheme} : CategoryTheory.MonoidalCategory X.PresheafOfModules

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.instMonoidalCategoryPresheafOfModules = PresheafOfModules.monoidalCategory

@[implicit_reducible]

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.instMonoidalCategoryPresheafOfModulesOverOpensCarrierCarrierCommRingCatObjFunctorOppositeRingCatIsSheafOverGrothendieckTopologyOverRingCatSheaf {X : Scheme} (U : X.Opens) : CategoryTheory.MonoidalCategory (_root_.PresheafOfModules (CategoryTheory.Sheaf.over X.ringCatSheaf U).obj)

Equations

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

@[implicit_reducible]

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.instSymmetricCategoryPresheafOfModulesOverOpensCarrierCarrierCommRingCatObjFunctorOppositeRingCatIsSheafOverGrothendieckTopologyOverRingCatSheaf {X : Scheme} (U : X.Opens) : CategoryTheory.SymmetricCategory (_root_.PresheafOfModules (CategoryTheory.Sheaf.over X.ringCatSheaf U).obj)

Equations

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

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.multiplicationHom {X : Scheme} [IsIntegral X] (D E : ↥X.CartierDivisor) : CategoryTheory.MonoidalCategoryStruct.tensorObj (fractionalPresheaf D) (fractionalPresheaf E) ⟶ fractionalPresheaf (D + E)

Multiplication of fractional sections.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.fractionalTensorAddIso {X : Scheme} [IsIntegral X] (D E : ↥X.CartierDivisor) : (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (fractionalPresheaf D) (fractionalPresheaf E)) ≅ associatedSheaf (D + E)

Sheafified multiplication identifies the tensor of the two fractional models with the associated sheaf of the sum.

Equations

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

Tensor additivity for the associated sheaves

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.associatedTensorAddIso {X : Scheme} [IsIntegral X] (D E : ↥X.CartierDivisor) : (associatedSheaf D).tensorObj (associatedSheaf E) ≅ associatedSheaf (D + E)

The associated-sheaf construction converts addition of Cartier divisors into tensor product.

Equations

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

Global equations, zero, and tensor inverses

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.globalEquationIso {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) (f : Additive (↑X.functionField)ˣ) (hf : IsEquationOn D ⊤ f) : SheafOfModules.unit X.ringCatSheaf ≅ associatedSheaf D

A global equation trivializes its associated sheaf.

Equations

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