From Cartier divisors to the Picard group

This file owns the specialized consequences of the associated-sheaf construction: the associated sheaf of the zero divisor is the structure sheaf, a principal divisor gives the structure sheaf, the associated sheaf of a sum is the tensor product, and the resulting map to the Picard group is an additive homomorphism that factors through the divisor class group.

No unconditional pullback theorem is stated. CartierPullbackData supplies a justified function-field pullback for divisors, but a comparison with pullback of module sheaves would also need compatibility between that data, rational sections, and module sheafification. That extra compatibility is not part of the current Mathlib API.

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.associatedSheafZeroIso {X : Scheme} [IsIntegral X] : associatedSheaf 0 ≅ SheafOfModules.unit X.ringCatSheaf

The associated sheaf of the zero divisor is the structure sheaf.

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.associatedSheafZeroIso = (AlgebraicGeometry.Scheme.CartierDivisor.globalEquationIso 0 0 ⋯).symm

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.associatedSheafPrincipalIso {X : Scheme} [IsIntegral X] (f : Additive (↑X.functionField)ˣ) : associatedSheaf ((principal X) f) ≅ SheafOfModules.unit X.ringCatSheaf

A principal divisor has trivial associated sheaf.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.associatedTensorInverseIso {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) : (associatedSheaf D).tensorObj (associatedSheaf (-D)) ≅ SheafOfModules.unit X.ringCatSheaf

O_X(-D) is an explicit tensor inverse of O_X(D).

Equations

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

From Cartier divisors to the Picard group

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

The Picard-group class represented by O_X(D), with O_X(-D) as its recorded inverse.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.CartierDivisor.coe_toPic {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) : ↑(toPic D) = Modules.PicardClass.mk (associatedSheaf D)

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.divisorToPicAdd {X : Scheme} [IsIntegral X] : ↥X.CartierDivisor →+ Additive (Modules.Pic X)

Before quotienting by principal divisors, D ↦ O_X(D) is additive after writing the Picard group additively.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.CartierDivisor.divisorToPicAdd_apply {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) : divisorToPicAdd D = Additive.ofMul (toPic D)

@[simp]

theorem AlgebraicGeometry.Scheme.CartierDivisor.divisorToPicAdd_principal {X : Scheme} [IsIntegral X] (f : Additive (↑X.functionField)ˣ) : divisorToPicAdd ((principal X) f) = 0

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.classToPicAdd {X : Scheme} [IsIntegral X] : ClassGroup X →+ Additive (Modules.Pic X)

Cartier divisor classes map additively to the Picard group. Principal divisors vanish by the canonical global-equation trivialization.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.classToPic {X : Scheme} [IsIntegral X] : Multiplicative (ClassGroup X) →* Modules.Pic X

Multiplicative form of the Cartier-class-to-Picard homomorphism.

Equations

• AlgebraicGeometry.Scheme.CartierDivisor.classToPic = AddMonoidHom.toMultiplicativeLeft AlgebraicGeometry.Scheme.CartierDivisor.classToPicAdd

@[simp]

theorem AlgebraicGeometry.Scheme.CartierDivisor.classToPic_toClass {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) : classToPic (Multiplicative.ofAdd ((toClass X) D)) = toPic D