Tensor products of Cartier divisor line bundles

Multiplication of rational functions sends sections of 𝒪_X(D) and 𝒪_X(E) to sections of 𝒪_X(D + E). On an integral scheme this gives the tensor product isomorphism 𝒪_X(D) ⊗ 𝒪_X(E) ≅ 𝒪_X(D + E), and hence makes the Cartier divisor map to line-bundle classes additive. A local equation of E trivializes the multiplication map: multiplication by the equation and its inverse give its local inverse.

The multiplication isomorphism supplies the tensor law needed to construct the Picard group in CartierDivisor/Picard.lean.

Main declarations

• Scheme.CartierDivisor.tensorProductSheafIso: 𝒪_X(D) ⊗ 𝒪_X(E) ≅ 𝒪_X(D + E);
• Scheme.CartierDivisor.tensorProductSheafIso_hom_tmul: the action of the isomorphism on pure tensors of sections.

This is the Cartier divisor version of Hartshorne, Algebraic Geometry, II.6.13. The construction of the multiplication map follows the Weil divisor construction in TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/TensorProduct.lean.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.rationalFunctionsMulBilin_mem_sections {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D E : CartierDivisor X} {U : X.Opens} {s t : ↑((rationalFunctions X).presheaf.obj (Opposite.op U))} (hs : s ∈ D.sections U) (ht : t ∈ E.sections U) : ((rationalFunctionsMulBilin X U) s) t ∈ (D + E).sections U

Products of sections of two Cartier divisor sheaves are sections of their sum.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.sectionsMul {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D E : CartierDivisor X) (U : X.Opens) (s : ↑(D.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(E.sheaf.presheaf.obj (Opposite.op U))) : ↑((D + E).sheaf.presheaf.obj (Opposite.op U))

Multiplication inside the rational functions, as a section of 𝒪_X(D + E).

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.sheafι_app_sectionsMul {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D E : CartierDivisor X) (U : X.Opens) (s : ↑(D.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(E.sheaf.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app (D + E).sheafι U)) (D.sectionsMul E U s t) = ((rationalFunctionsMulBilin X U) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app D.sheafι U)) s)) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app E.sheafι U)) t)

The image of the product in the rational-function sheaf is the product of the images.

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.sectionsMul_add_left {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D E : CartierDivisor X} {U : X.Opens} (s s' : ↑(D.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(E.sheaf.presheaf.obj (Opposite.op U))) : D.sectionsMul E U (s + s') t = D.sectionsMul E U s t + D.sectionsMul E U s' t

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.sectionsMul_add_right {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D E : CartierDivisor X} {U : X.Opens} (s : ↑(D.sheaf.presheaf.obj (Opposite.op U))) (t t' : ↑(E.sheaf.presheaf.obj (Opposite.op U))) : D.sectionsMul E U s (t + t') = D.sectionsMul E U s t + D.sectionsMul E U s t'

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.sectionsMul_smul_left {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D E : CartierDivisor X} {U : X.Opens} (r : ↑(X.presheaf.obj (Opposite.op U))) (s : ↑(D.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(E.sheaf.presheaf.obj (Opposite.op U))) : D.sectionsMul E U (r • s) t = r • D.sectionsMul E U s t

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.sectionsMul_smul_right {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D E : CartierDivisor X} {U : X.Opens} (r : ↑(X.presheaf.obj (Opposite.op U))) (s : ↑(D.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(E.sheaf.presheaf.obj (Opposite.op U))) : D.sectionsMul E U s (r • t) = r • D.sectionsMul E U s t

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.sectionsMul_map {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D E : CartierDivisor X} {U V : X.Opens} (i : V ⟶ U) (s : ↑(D.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(E.sheaf.presheaf.obj (Opposite.op U))) : D.sectionsMul E V ((CategoryTheory.ConcreteCategory.hom (D.sheaf.presheaf.map i.op)) s) ((CategoryTheory.ConcreteCategory.hom (E.sheaf.presheaf.map i.op)) t) = (CategoryTheory.ConcreteCategory.hom ((D + E).sheaf.presheaf.map i.op)) (D.sectionsMul E U s t)

Restriction commutes with multiplication of sections.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.sectionsMulLift {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D E : CartierDivisor X) (U : X.Opens) : TensorProduct ↑(X.presheaf.obj (Opposite.op U)) ↑(D.sheaf.presheaf.obj (Opposite.op U)) ↑(E.sheaf.presheaf.obj (Opposite.op U)) →ₗ[↑(X.presheaf.obj (Opposite.op U))] ↑((D + E).sheaf.presheaf.obj (Opposite.op U))

Multiplication, linear on the tensor product of the sections.

Equations

• D.sectionsMulLift E U = TensorProduct.lift (LinearMap.mk₂ (↑(X.presheaf.obj (Opposite.op U))) (D.sectionsMul E U) ⋯ ⋯ ⋯ ⋯)

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.sectionsMulLift_tmul {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D E : CartierDivisor X) (U : X.Opens) (s : ↑(D.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(E.sheaf.presheaf.obj (Opposite.op U))) : (D.sectionsMulLift E U) (s ⊗ₜ[↑(X.presheaf.obj (Opposite.op U))] t) = D.sectionsMul E U s t

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.tensorPresheafHom {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D E : CartierDivisor X) : PresheafOfModulesOfCommRing.Monoidal.tensorObj D.sheaf.val E.sheaf.val ⟶ (D + E).sheaf.val

The multiplication morphism of presheaves of modules.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.tensorPresheafHom_app {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D E : CartierDivisor X) (U : X.Opens) : ModuleCat.Hom.hom ((D.tensorPresheafHom E).app (Opposite.op U)) = D.sectionsMulLift E U

The morphism on an open subset is the multiplication map on tensor products of sections.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.inv_localEquation_mem_sections {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {E : CartierDivisor X} {V : X.Opens} [Nonempty ↥↑V] {g : (↑X.functionField)ˣ} (hg : (rationalUnitClass X V) (Additive.ofMul g) = TopCat.Presheaf.restrictOpen E V ⋯) : (rationalFunctionsEquiv V).symm (↑g)⁻¹ ∈ E.sections V

The inverse of an equation of E is a section of 𝒪_X(E) on its domain.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.localEquation_mem_sections_neg {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {E : CartierDivisor X} {V : X.Opens} [Nonempty ↥↑V] {g : (↑X.functionField)ˣ} (hg : (rationalUnitClass X V) (Additive.ofMul g) = TopCat.Presheaf.restrictOpen E V ⋯) : (rationalFunctionsEquiv V).symm ↑g ∈ (-E).sections V

An equation of E is a section of 𝒪_X(-E) on its domain.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.mul_localEquation_mem_sections {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {E : CartierDivisor X} {V : X.Opens} [Nonempty ↥↑V] {g : (↑X.functionField)ˣ} (hg : (rationalUnitClass X V) (Additive.ofMul g) = TopCat.Presheaf.restrictOpen E V ⋯) (D : CartierDivisor X) (s : ↑((D + E).sheaf.presheaf.obj (Opposite.op V))) : ((rationalFunctionsMulBilin X V) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app (D + E).sheafι V)) s)) ((rationalFunctionsEquiv V).symm ↑g) ∈ D.sections V

Multiplying a section of 𝒪_X(D+E) by an equation of E produces a section of 𝒪_X(D).

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.exists_sectionsMul_eq {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {E : CartierDivisor X} {V : X.Opens} [Nonempty ↥↑V] {g : (↑X.functionField)ˣ} (hg : (rationalUnitClass X V) (Additive.ofMul g) = TopCat.Presheaf.restrictOpen E V ⋯) (D : CartierDivisor X) (s : ↑((D + E).sheaf.presheaf.obj (Opposite.op V))) : ∃ (a : ↑(D.sheaf.presheaf.obj (Opposite.op V))) (b : ↑(E.sheaf.presheaf.obj (Opposite.op V))), D.sectionsMul E V a b = s

Multiplication of divisor sheaf sections is locally surjective.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.tensorProductSheafIso {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D E : CartierDivisor X) : SheafOfModules.tensorProduct X.sheaf D.sheaf E.sheaf ≅ (D + E).sheaf

The tensor product of the line bundles of two Cartier divisors is the line bundle of their sum.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.tensorProductSheafIso_hom_tmul {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D E : CartierDivisor X) (U : X.Opens) (s : ↑(D.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(E.sheaf.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app (CategoryTheory.CategoryStruct.comp (SheafOfModules.tensorProductIso X.sheaf D.sheaf E.sheaf).inv (D.tensorProductSheafIso E).hom) U)) ((CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).unit.app (PresheafOfModulesOfCommRing.Monoidal.tensorObj D.sheaf.val E.sheaf.val)).app (Opposite.op U))) (s ⊗ₜ[↑(X.sheaf.obj.obj (Opposite.op U))] t)) = D.sectionsMul E U s t

On a pure tensor of local sections, the tensor-product isomorphism multiplies the corresponding rational functions. The sheafification unit sends the sectionwise pure tensor into the tensor product sheaf.