The Cartier class group and the Picard group

For an integral scheme X, the Cartier class group CaCl(X) is the group of Cartier divisors modulo principal divisors. The map D ↦ [𝒪_X(D)] induces an additive equivalence CaCl(X) ≃+ Additive (LineBundleClass X). Thus two Cartier divisors define isomorphic line bundles exactly when their difference is principal.

The equivalence combines the tensor-product law, representation of every line bundle by a Cartier divisor, and the characterization of divisors with trivial associated line bundle. No Noetherian, regularity, dimension, or properness hypothesis is needed.

Main declarations

• Scheme.CartierDivisor.ClassGroup: Cartier divisors modulo principal divisors;
• Scheme.CartierDivisor.divisorClass: the additive quotient map;
• Scheme.CartierDivisor.ClassGroup.lift: descent of homomorphisms vanishing on principal divisors;
• Scheme.CartierDivisor.classGroupAddEquivLineBundleClass: the Cartier–Picard dictionary;
• Scheme.CartierDivisor.nonempty_iso_sheaf_iff: isomorphic divisor sheaves are characterized by a principal difference.

References

• R. Hartshorne, Algebraic Geometry, Proposition II.6.15.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.principalSubgroup (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] : AddSubgroup (CartierDivisor X)

The subgroup of principal Cartier divisors.

Equations

• TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.principalSubgroup X = (TauCeti.AlgebraicGeometry.Scheme.principalCartierDivisorAddHom X).range

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.mem_principalSubgroup {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D : CartierDivisor X} : D ∈ principalSubgroup X ↔ ∃ (f : (↑X.functionField)ˣ), principalCartierDivisor X f = D

A Cartier divisor belongs to the principal subgroup exactly when it is the divisor of a nonzero rational function.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.principalSubgroup_eq_ker {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] : principalSubgroup X = toLineBundleClassHom.ker

The principal Cartier divisors are precisely the kernel of D ↦ [𝒪_X(D)].

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.ClassGroup (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] : Type u

The Cartier class group CaCl(X), namely Cartier divisors modulo principal divisors.

Equations

• TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.ClassGroup X = (TauCeti.AlgebraicGeometry.Scheme.CartierDivisor X ⧸ TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.principalSubgroup X)

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.divisorClass {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] : CartierDivisor X →+ ClassGroup X

The additive quotient map from Cartier divisors to the Cartier class group.

Equations

• TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.divisorClass = QuotientAddGroup.mk' (TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.principalSubgroup X)

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.divisorClass_eq_mk' {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) : divisorClass D = (QuotientAddGroup.mk' (principalSubgroup X)) D

The Cartier divisor class is the canonical quotient projection.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.divisorClass_surjective {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] : Function.Surjective ⇑divisorClass

Every Cartier divisor class has a Cartier divisor representative.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.divisorClass_eq_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D E : CartierDivisor X} : divisorClass D = divisorClass E ↔ ∃ (f : (↑X.functionField)ˣ), principalCartierDivisor X f = D - E

Equal Cartier divisor classes are characterized by a principal difference.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.divisorClass_eq_zero_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D : CartierDivisor X} : divisorClass D = 0 ↔ ∃ (f : (↑X.functionField)ˣ), principalCartierDivisor X f = D

A Cartier divisor has zero class exactly when it is principal.

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.divisorClass_principalCartierDivisor {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (f : (↑X.functionField)ˣ) : divisorClass (principalCartierDivisor X f) = 0

Principal Cartier divisors have zero class.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.ClassGroup.lift {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {H : Type u_1} [AddMonoid H] (φ : CartierDivisor X →+ H) (hφ : ∀ (f : (↑X.functionField)ˣ), φ (principalCartierDivisor X f) = 0) : ClassGroup X →+ H

The universal property of the Cartier class group: an additive homomorphism that vanishes on principal Cartier divisors descends to the class group.

Equations

• TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.ClassGroup.lift φ hφ = QuotientAddGroup.lift (TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.principalSubgroup X) φ ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.ClassGroup.lift_divisorClass {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {H : Type u_1} [AddMonoid H] (φ : CartierDivisor X →+ H) (hφ : ∀ (f : (↑X.functionField)ˣ), φ (principalCartierDivisor X f) = 0) (D : CartierDivisor X) : (lift φ hφ) (divisorClass D) = φ D

The descended homomorphism evaluates on the class of a divisor as the original map.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.classGroupAddEquivLineBundleClass (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] : ClassGroup X ≃+ Additive (LineBundleClass X)

The Cartier–Picard dictionary. On any integral scheme, Cartier divisors modulo principal divisors form the Picard group of line-bundle classes under tensor product.

Equations

• TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.classGroupAddEquivLineBundleClass X = QuotientAddGroup.liftEquiv (TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.principalSubgroup X) ⋯ ⋯

@[simp]

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

The Cartier–Picard equivalence sends the class of D to the class of 𝒪_X(D).

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.classGroupAddEquivLineBundleClass_symm_toLineBundleClass {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) : (classGroupAddEquivLineBundleClass X).symm (Additive.ofMul D.toLineBundleClass) = divisorClass D

The inverse Cartier–Picard equivalence sends 𝒪_X(D) back to the class of D.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.toLineBundleClass_eq_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D E : CartierDivisor X} : D.toLineBundleClass = E.toLineBundleClass ↔ ∃ (f : (↑X.functionField)ˣ), principalCartierDivisor X f = D - E

Two Cartier divisors give the same line-bundle class exactly when their difference is principal.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.nonempty_iso_sheaf_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D E : CartierDivisor X} : Nonempty (D.sheaf ≅ E.sheaf) ↔ ∃ (f : (↑X.functionField)ˣ), principalCartierDivisor X f = D - E

Isomorphic Cartier divisor sheaves have a principal difference, and conversely.