Cartier divisors and the Picard group

The Cartier divisor tensor-product isomorphism makes the class map additive. Negation of Cartier divisors corresponds to inversion in the Picard group.

Main declarations

• Scheme.CartierDivisor.toLineBundleClass_add and toLineBundleClassHom: the additive comparison from Cartier divisors to line-bundle classes;
• Scheme.CartierDivisor.toLineBundleClass_neg: negation corresponds to the inverse class.

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.toLineBundleClass_add {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D E : CartierDivisor X) : (D + E).toLineBundleClass = D.toLineBundleClass * E.toLineBundleClass

The class of the sheaf of D + E is the tensor product of the two divisor classes.

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.toLineBundleClass_neg {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) : (-D).toLineBundleClass = D.toLineBundleClass⁻¹

Negating a Cartier divisor gives the inverse line-bundle class.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.toLineBundleClassHom {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] : CartierDivisor X →+ Additive (LineBundleClass X)

The Cartier divisor map to the tensor-product Picard group, as an additive homomorphism.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.toLineBundleClassHom_apply {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) : toLineBundleClassHom D = Additive.ofMul D.toLineBundleClass

The bundled Cartier divisor comparison sends D to the class of 𝒪_X(D).