noncomputable def Corollary19.IsInvertibleSheaf {X : AlgebraicGeometry.Scheme} (ℒ : X.Modules) : Prop

An invertible sheaf (line bundle) on a scheme X: a sheaf of modules that is locally free of rank 1.

theorem Corollary19.isInvertibleSheaf_unit (X : AlgebraicGeometry.Scheme) : IsInvertibleSheaf (SheafOfModules.unit X.ringCatSheaf)

The structure sheaf 𝒪_X is invertible (trivially of rank 1).

def Corollary19.InvertibleSheaf (X : AlgebraicGeometry.Scheme) : Type (u + 1)

The type of invertible sheaves on X.

@[implicit_reducible]

instance Corollary19.invertibleSheafSetoid (X : AlgebraicGeometry.Scheme) : Setoid (InvertibleSheaf X)

Setoid identifying two invertible sheaves when they are isomorphic.

def Corollary19.PicardGroupScheme (X : AlgebraicGeometry.Scheme) : Type (u + 1)

The Picard group of a scheme X: isomorphism classes of invertible sheaves on X.

@[implicit_reducible]

noncomputable instance Corollary19.instCommGroupPicardGroupScheme (X : AlgebraicGeometry.Scheme) : CommGroup (PicardGroupScheme X)

Commutative group structure on PicardGroupScheme X via tensor product of line bundles, with identity given by 𝒪_X and inverses by duals.

def Corollary19.PicardGroupScheme.mk {X : AlgebraicGeometry.Scheme} (ℒ : X.Modules) (h : IsInvertibleSheaf ℒ) : PicardGroupScheme X

Class of an invertible sheaf in the Picard group.

theorem Corollary19.PicardGroupScheme.mk_eq_iff {X : AlgebraicGeometry.Scheme} (ℒ₁ ℒ₂ : X.Modules) (h₁ : IsInvertibleSheaf ℒ₁) (h₂ : IsInvertibleSheaf ℒ₂) : mk ℒ₁ h₁ = mk ℒ₂ h₂ ↔ Nonempty (ℒ₁ ≅ ℒ₂)

Two invertible sheaves represent the same Picard class iff they are isomorphic.

theorem Corollary19.PicardGroupScheme.mk_unit (X : AlgebraicGeometry.Scheme) : mk (SheafOfModules.unit X.ringCatSheaf) ⋯ = 1

The class of the structure sheaf is the identity of the Picard group.

@[implicit_reducible]

noncomputable instance Corollary19.picardGroup_affine_commGroup (R : Type u) [CommRing R] : CommGroup (CommRing.Pic R)

The Picard group of a commutative ring is naturally a commutative group.

noncomputable def Corollary19.picardGroupScheme_spec_equiv (R : Type u) [CommRing R] : PicardGroupScheme (AlgebraicGeometry.Spec (CommRingCat.of R)) ≃* CommRing.Pic R

Affine case of the Picard group: for X = Spec R, the scheme Picard group is naturally isomorphic to the ring Picard group Pic R.

theorem Corollary19.pic_mul_eq_tensor {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [Module.Invertible R M] [AddCommMonoid N] [Module R N] [Module.Invertible R N] : CommRing.Pic.mk R (TensorProduct R M N) = CommRing.Pic.mk R M * CommRing.Pic.mk R N

Multiplication in Pic R corresponds to tensor product of invertible modules.

theorem Corollary19.pic_identity {R : Type u} [CommSemiring R] : CommRing.Pic.mk R R = 1

The trivial line bundle R represents the identity in Pic R.

theorem Corollary19.pic_inv_eq_dual {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module.Invertible R M] : CommRing.Pic.mk R (Module.Dual R M) = (CommRing.Pic.mk R M)⁻¹

The inverse of a Picard class is represented by the dual module.

theorem Corollary19.pic_comm {R : Type u} [CommSemiring R] (a b : CommRing.Pic R) : a * b = b * a

Commutativity of multiplication in Pic R.

theorem Corollary19.pic_eq_iff_iso {R : Type u} [CommSemiring R] {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [Module R M] [Module.Invertible R M] [AddCommMonoid N] [Module R N] [Module.Invertible R N] : CommRing.Pic.mk R M = CommRing.Pic.mk R N ↔ Nonempty (M ≃ₗ[R] N)

Two invertible modules represent the same Picard class iff they are isomorphic as R-modules.

theorem Corollary19.pic_trivial_iff_free {R : Type u} [CommSemiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] [Module.Invertible R M] : CommRing.Pic.mk R M = 1 ↔ Module.Free R M

A Picard class is trivial iff the underlying invertible module is free.