The Picard group of a scheme

The symmetric monoidal category of locally free rank-one sheaves makes PicardClass X a commutative monoid. Pic X is its group of units: an element records an isomorphism class and an explicit tensor-inverse class. Pic.mkOfTensorInverse is the downstream constructor for line bundles such as O_X(D) and O_X(-D).

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.picardClassCommMonoid (X : Scheme) : CommMonoid (PicardClass X)

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.PicardClass.one_eq_one (X : Scheme) : one X = 1

theorem AlgebraicGeometry.Scheme.Modules.PicardClass.mk_mul_mk {X : Scheme} (L M : X.Modules) [hL : (have this := L; this).IsInvertible] [hM : (have this := M; this).IsInvertible] : mk L * mk M = mk (L.tensorObj M)

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Modules.Pic (X : Scheme) : Type (u + 1)

The Picard group: tensor-invertible isomorphism classes of locally free rank-one sheaves.

Equations

• AlgebraicGeometry.Scheme.Modules.Pic X = (AlgebraicGeometry.Scheme.Modules.PicardClass X)ˣ

noncomputable def AlgebraicGeometry.Scheme.Modules.Pic.mkOfTensorInverse {X : Scheme} (L M : X.Modules) [hL : (have this := L; this).IsInvertible] [hM : (have this := M; this).IsInvertible] (e : L.tensorObj M ≅ SheafOfModules.unit X.ringCatSheaf) : Pic X

Construct a Picard-group element from an explicit tensor inverse.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.Pic.coe_mkOfTensorInverse {X : Scheme} (L M : X.Modules) [(have this := L; this).IsInvertible] [(have this := M; this).IsInvertible] (e : L.tensorObj M ≅ SheafOfModules.unit X.ringCatSheaf) : ↑(mkOfTensorInverse L M e) = PicardClass.mk L

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.Pic.coe_one {X : Scheme} : ↑1 = PicardClass.one X