Multiplication of ideal sheaves

For ideal sheaves I and J on a scheme X, products of local functions in I and J are local functions in the product ideal sheaf I * J. This file packages that multiplication, first on sections and then as a morphism I ⊗ J ⟶ I * J of 𝒪_X-modules out of the tensor product. It is the restriction of the multiplication 𝒪_X ⊗ 𝒪_X ≅ 𝒪_X of the structure sheaf along the inclusions of I, J and I * J into 𝒪_X. No hypothesis is placed on I or J; when J is the ideal sheaf of an effective Cartier divisor the multiplication is an isomorphism (Scheme.IdealSheafData.tensorProductSheafIso).

Main declarations

• Scheme.IdealSheafData.mul_mem_sections_mul: products of sections of I and J are sections of I * J, and Scheme.IdealSheafData.sectionsMul is the resulting multiplication map Γ(I, U) × Γ(J, U) → Γ(I * J, U);
• Scheme.IdealSheafData.tensorPresheafHom: the multiplication I ⊗ J ⟶ I * J on the sectionwise tensor product of presheaves of modules;
• Scheme.IdealSheafData.sheafMul: the multiplication morphism I ⊗ J ⟶ I * J of 𝒪_X-modules, characterized by sheafMul_sheafι as the restriction of the multiplication of 𝒪_X.

References

• The construction of the multiplication map follows the Cartier divisor version Scheme.CartierDivisor.tensorProductSheafIso in TauCeti/AlgebraicGeometry/CartierDivisor/TensorProduct.lean.

theorem AlgebraicGeometry.Scheme.IdealSheafData.mul_mem_sections_mul {X : Scheme} {I J : X.IdealSheafData} {U : X.Opens} {s t : ↑(X.presheaf.obj (Opposite.op U))} (hs : s ∈ I.sections U) (ht : t ∈ J.sections U) : s * t ∈ (I * J).sections U

Products of sections of two ideal sheaves are sections of their product.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.sectionsMul {X : Scheme} (I J : X.IdealSheafData) (U : X.Opens) (s : ↑(I.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(J.sheaf.presheaf.obj (Opposite.op U))) : ↑((I * J).sheaf.presheaf.obj (Opposite.op U))

Multiplication of local functions, as a map from sections of I and J to sections of I * J.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sheafι_app_sectionsMul {X : Scheme} (I J : X.IdealSheafData) (U : X.Opens) (s : ↑(I.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(J.sheaf.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (Modules.Hom.app (I * J).sheafι U)) (I.sectionsMul J U s t) = (CategoryTheory.ConcreteCategory.hom (Modules.Hom.app I.sheafι U)) s * (CategoryTheory.ConcreteCategory.hom (Modules.Hom.app J.sheafι U)) t

sectionsMul multiplies the underlying local functions.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sectionsMul_sectionMk {X : Scheme} (I J : X.IdealSheafData) (U : X.Opens) {a b : ↑(X.presheaf.obj (Opposite.op U))} (ha : a ∈ I.sections U) (hb : b ∈ J.sections U) : I.sectionsMul J U (I.sectionMk a ha) (J.sectionMk b hb) = (I * J).sectionMk (a * b) ⋯

On sections built from local functions a and b, sectionsMul is the product a * b.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sectionsMul_add_left {X : Scheme} {I J : X.IdealSheafData} {U : X.Opens} (s s' : ↑(I.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(J.sheaf.presheaf.obj (Opposite.op U))) : I.sectionsMul J U (s + s') t = I.sectionsMul J U s t + I.sectionsMul J U s' t

sectionsMul is additive in its first argument.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sectionsMul_add_right {X : Scheme} {I J : X.IdealSheafData} {U : X.Opens} (s : ↑(I.sheaf.presheaf.obj (Opposite.op U))) (t t' : ↑(J.sheaf.presheaf.obj (Opposite.op U))) : I.sectionsMul J U s (t + t') = I.sectionsMul J U s t + I.sectionsMul J U s t'

sectionsMul is additive in its second argument.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sectionsMul_smul_left {X : Scheme} {I J : X.IdealSheafData} {U : X.Opens} (r : ↑(X.presheaf.obj (Opposite.op U))) (s : ↑(I.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(J.sheaf.presheaf.obj (Opposite.op U))) : I.sectionsMul J U (r • s) t = r • I.sectionsMul J U s t

sectionsMul is Γ(X, U)-linear in its first argument.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sectionsMul_smul_right {X : Scheme} {I J : X.IdealSheafData} {U : X.Opens} (r : ↑(X.presheaf.obj (Opposite.op U))) (s : ↑(I.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(J.sheaf.presheaf.obj (Opposite.op U))) : I.sectionsMul J U s (r • t) = r • I.sectionsMul J U s t

sectionsMul is Γ(X, U)-linear in its second argument.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.sectionsMul_map {X : Scheme} {I J : X.IdealSheafData} {U V : X.Opens} (i : V ⟶ U) (s : ↑(I.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(J.sheaf.presheaf.obj (Opposite.op U))) : I.sectionsMul J V ((CategoryTheory.ConcreteCategory.hom (I.sheaf.presheaf.map i.op)) s) ((CategoryTheory.ConcreteCategory.hom (J.sheaf.presheaf.map i.op)) t) = (CategoryTheory.ConcreteCategory.hom ((I * J).sheaf.presheaf.map i.op)) (I.sectionsMul J U s t)

Restriction commutes with multiplication of sections.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.tensorPresheafHom {X : Scheme} (I J : X.IdealSheafData) : PresheafOfModulesOfCommRing.Monoidal.tensorObj I.sheaf.val J.sheaf.val ⟶ (I * J).sheaf.val

The multiplication morphism of presheaves of modules I ⊗ J ⟶ I * J.

theorem AlgebraicGeometry.Scheme.IdealSheafData.tensorPresheafHom_app_tmul {X : Scheme} (I J : X.IdealSheafData) (U : X.Opens) (s : ↑(I.sheaf.presheaf.obj (Opposite.op U))) (t : ↑(J.sheaf.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom ((I.tensorPresheafHom J).app (Opposite.op U))) (s ⊗ₜ[↑(X.sheaf.obj.obj (Opposite.op U))] t) = I.sectionsMul J U s t

On a pure tensor of sections over U, tensorPresheafHom is sectionsMul.

@[instance_reducible]

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.instMonoidalCategoryPresheafOfModulesOpensCarrierCarrierCommRingCatObjFunctorOppositeRingCatIsSheafGrothendieckTopologyRingCatSheafSheaf {X : Scheme} : CategoryTheory.MonoidalCategory (_root_.PresheafOfModules (TauCeti.SheafOfModules.ringCatSheaf X.sheaf).obj)

The sectionwise monoidal structure on presheaves of modules over the ring sheaf of X. Instance search does not find it, nor the two instances below, as it cannot unify the topological sheaf X.sheaf with a sheaf on a site; they are supplied here.

@[instance_reducible]

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.instMonoidalCategorySheafOfModulesOpensCarrierCarrierCommRingCatRingCatSheafSheaf {X : Scheme} : CategoryTheory.MonoidalCategory (SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf X.sheaf))

The monoidal structure on sheaves of modules over the ring sheaf of X, as on X.Modules.

@[instance_reducible]

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.instLaxMonoidalSheafOfModulesOpensCarrierCarrierCommRingCatRingCatSheafSheafPresheafOfModulesObjFunctorOppositeRingCatIsSheafGrothendieckTopologyForget {X : Scheme} : (SheafOfModules.forget (TauCeti.SheafOfModules.ringCatSheaf X.sheaf)).LaxMonoidal

The inclusion of sheaves of modules into presheaves of modules is lax monoidal.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.sheafMul {X : Scheme} (I J : X.IdealSheafData) : CategoryTheory.MonoidalCategoryStruct.tensorObj I.sheaf J.sheaf ⟶ (I * J).sheaf

Multiplication of local functions I ⊗ J ⟶ I * J, as a morphism of 𝒪_X-modules out of the tensor product. It is the restriction of the multiplication of 𝒪_X (sheafMul_sheafι).

theorem AlgebraicGeometry.Scheme.IdealSheafData.sheafMul_sheafι {X : Scheme} (I J : X.IdealSheafData) : CategoryTheory.CategoryStruct.comp (I.sheafMul J) (I * J).sheafι = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom I.sheafι J.sheafι) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)).hom

Multiplication I ⊗ J ⟶ I * J, followed by the inclusion I * J ⟶ 𝒪_X, is the inclusion I ⊗ J ⟶ 𝒪_X ⊗ 𝒪_X followed by the multiplication 𝒪_X ⊗ 𝒪_X ≅ 𝒪_X. As the inclusion is a monomorphism, this characterizes sheafMul.

theorem AlgebraicGeometry.Scheme.IdealSheafData.sheafMul_sheafι_assoc {X : Scheme} (I J : X.IdealSheafData) {Z : X.Modules} (h : SheafOfModules.unit X.ringCatSheaf ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (I.sheafMul J) (I * J).sheafι) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom I.sheafι J.sheafι) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)).hom) h

Multiplication I ⊗ J ⟶ I * J, followed by the inclusion I * J ⟶ 𝒪_X, is the inclusion I ⊗ J ⟶ 𝒪_X ⊗ 𝒪_X followed by the multiplication 𝒪_X ⊗ 𝒪_X ≅ 𝒪_X. As the inclusion is a monomorphism, this characterizes sheafMul.