Isomorphism classes of line bundles

The Picard group of a scheme consists of line bundles up to isomorphism, with tensor product as its operation. This file constructs the type of isomorphism classes and descends tensor product, the trivial line bundle, and duality to it. Tensor symmetry, associativity, the unit isomorphisms, and evaluation against the dual give the commutative group laws.

Main declarations

• LineBundleClass X is the type of line bundles on X up to isomorphism;
• LineBundleClass.mk sends a line bundle to its isomorphism class, and every class arises this way (LineBundleClass.mk_surjective);
• LineBundleClass.lift descends an isomorphism-invariant function to line-bundle classes;
• LineBundleClass.mk_eq_mk_iff characterizes equality by an isomorphism of the underlying sheaves;
• multiplication is induced by InvertibleSheaf.tensorProduct, and 1 is the class of the trivial line bundle, so that LineBundleClass.mk_eq_one_iff characterizes the classes of line bundles isomorphic to the structure sheaf;
• inversion is induced by InvertibleSheaf.dual;
• tensor product makes LineBundleClass X a commutative group.

The construction uses Mathlib's CategoryTheory.Skeleton, its standard implementation of the isomorphism classes of objects of a category.

def TauCeti.AlgebraicGeometry.LineBundleClass (X : AlgebraicGeometry.Scheme) : Type (u + 1)

The type of isomorphism classes of line bundles on a scheme.

Equations

• TauCeti.AlgebraicGeometry.LineBundleClass X = CategoryTheory.Skeleton (TauCeti.AlgebraicGeometry.InvertibleSheaf X)

def TauCeti.AlgebraicGeometry.LineBundleClass.mk {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) : LineBundleClass X

The isomorphism class of a line bundle.

Equations

• TauCeti.AlgebraicGeometry.LineBundleClass.mk L = CategoryTheory.toSkeleton L

noncomputable def TauCeti.AlgebraicGeometry.LineBundleClass.lift {X : AlgebraicGeometry.Scheme} {α : Sort v} (f : InvertibleSheaf X → α) (hf : ∀ (L M : InvertibleSheaf X), Nonempty (L.obj ≅ M.obj) → f L = f M) : LineBundleClass X → α

Descend a function on invertible sheaves that is invariant under isomorphism to line-bundle classes.

Equations

• TauCeti.AlgebraicGeometry.LineBundleClass.lift f hf = (TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X).skeletonLift f hf

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.lift_mk {X : AlgebraicGeometry.Scheme} {α : Sort v} {f : InvertibleSheaf X → α} {hf : ∀ (L M : InvertibleSheaf X), Nonempty (L.obj ≅ M.obj) → f L = f M} (L : InvertibleSheaf X) : lift f hf (mk L) = f L

Applying lift to the class represented by L recovers the original function at L.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.mk_eq_mk_iff {X : AlgebraicGeometry.Scheme} {L K : InvertibleSheaf X} : mk L = mk K ↔ Nonempty (L.obj ≅ K.obj)

Two line bundles have the same class exactly when their underlying sheaves are isomorphic.

theorem TauCeti.AlgebraicGeometry.LineBundleClass.mk_surjective {X : AlgebraicGeometry.Scheme} : Function.Surjective mk

Every line-bundle class is the class of a line bundle.

noncomputable def TauCeti.AlgebraicGeometry.LineBundleClass.dual {X : AlgebraicGeometry.Scheme} (a : LineBundleClass X) : LineBundleClass X

Duality of line bundles descends to their isomorphism classes.

Equations

• a.dual = TauCeti.AlgebraicGeometry.LineBundleClass.lift (fun (L : TauCeti.AlgebraicGeometry.InvertibleSheaf X) => TauCeti.AlgebraicGeometry.LineBundleClass.mk L.dual) ⋯ a

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.LineBundleClass.instInv {X : AlgebraicGeometry.Scheme} : Inv (LineBundleClass X)

Equations

• TauCeti.AlgebraicGeometry.LineBundleClass.instInv = { inv := TauCeti.AlgebraicGeometry.LineBundleClass.dual }

theorem TauCeti.AlgebraicGeometry.LineBundleClass.inv_eq_dual {X : AlgebraicGeometry.Scheme} (a : LineBundleClass X) : a⁻¹ = a.dual

Inversion of line-bundle classes is induced by duality.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.inv_mk {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) : (mk L)⁻¹ = mk L.dual

The inverse of the class of a line bundle is the class of its dual.

noncomputable def TauCeti.AlgebraicGeometry.LineBundleClass.tensorProduct {X : AlgebraicGeometry.Scheme} (a b : LineBundleClass X) : LineBundleClass X

Tensor product of line bundles descends to their isomorphism classes.

Equations

• a.tensorProduct b = Quotient.map₂ TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProduct ⋯ a b

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.LineBundleClass.instMul {X : AlgebraicGeometry.Scheme} : Mul (LineBundleClass X)

Equations

• TauCeti.AlgebraicGeometry.LineBundleClass.instMul = { mul := TauCeti.AlgebraicGeometry.LineBundleClass.tensorProduct }

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.mk_tensorProduct {X : AlgebraicGeometry.Scheme} (L K : InvertibleSheaf X) : mk (L.tensorProduct K) = mk L * mk K

The class of a tensor product is the product of the two classes.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.LineBundleClass.instOne {X : AlgebraicGeometry.Scheme} : One (LineBundleClass X)

The unit for tensor product is the class of the trivial line bundle.

Equations

• TauCeti.AlgebraicGeometry.LineBundleClass.instOne = { one := TauCeti.AlgebraicGeometry.LineBundleClass.mk (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X) }

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.mk_trivial {X : AlgebraicGeometry.Scheme} : mk (InvertibleSheaf.trivial X) = 1

The class of the trivial line bundle is the tensor unit.

@[simp]

theorem TauCeti.AlgebraicGeometry.LineBundleClass.mk_eq_one_iff {X : AlgebraicGeometry.Scheme} {L : InvertibleSheaf X} : mk L = 1 ↔ Nonempty (L.obj ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)

The class of a line bundle is the tensor unit exactly when the line bundle is isomorphic to the structure sheaf.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.LineBundleClass.instCommGroup {X : AlgebraicGeometry.Scheme} : CommGroup (LineBundleClass X)

Tensor product and duality make line-bundle classes a commutative group.

Equations

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