theorem InvertibleSheaves.dual_tensor_self_equiv (R : Type u) [CommSemiring R] (M : Type u_1) [AddCommMonoid M] [Module R M] [Module.Invertible R M] : Nonempty (TensorProduct R (Module.Dual R M) M ≃ₗ[R] R)

For an invertible module M over R, the natural evaluation M^∨ ⊗ M → R is an isomorphism, witnessing M as a unit in the Picard group.

instance InvertibleSheaves.invertible_tensor (R : Type u) [CommSemiring R] (M : Type u_1) [AddCommMonoid M] [Module R M] [Module.Invertible R M] (N : Type u_2) [AddCommMonoid N] [Module R N] [Module.Invertible R N] : Module.Invertible R (TensorProduct R M N)

The tensor product of two invertible modules is invertible (Pic is closed under multiplication).

instance InvertibleSheaves.invertible_dual (R : Type u) [CommSemiring R] (M : Type u_1) [AddCommMonoid M] [Module R M] [Module.Invertible R M] : Module.Invertible R (Module.Dual R M)

The dual of an invertible module is invertible: this gives inverses in Pic.

instance InvertibleSheaves.invertible_self (R : Type u) [CommSemiring R] : Module.Invertible R R

R itself is invertible as an R-module, serving as the identity element of Pic.

@[implicit_reducible]

noncomputable instance InvertibleSheaves.picardGroup_commGroup (R : Type u) [CommSemiring R] : CommGroup (CommRing.Pic R)

The Picard group of R is a commutative group under tensor product (Corollary 19, Lecture 14/15).

theorem InvertibleSheaves.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 the Picard group is given by tensor product of invertible modules.

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

The class of R is the identity element 1 of Pic(R).

theorem InvertibleSheaves.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 in Pic of the class of M is the class of its dual M^∨.

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

Commutativity of Pic: the group law (tensor product) is commutative.

theorem InvertibleSheaves.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 Pic class iff they are linearly isomorphic.

theorem InvertibleSheaves.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

An invertible module is trivial in Pic iff it is free as an R-module.