Tensor products of presentations of sheaves of modules

Let R be a sheaf of commutative rings on a small site. If M is the cokernel of f : free ι ⟶ free σ and N is the cokernel of g : free κ ⟶ free τ, then M ⊗ N is the cokernel of the morphism

(free ι ⊗ free τ) ⨿ (free σ ⊗ free κ) ⟶ free σ ⊗ free τ

given by f ▷ free τ and free σ ◁ g, and the tensor product of two free sheaves of modules is free on the product of the index types. Hence a presentation of M and a presentation of N give a presentation of M ⊗ N, with generators indexed by σ × τ and relations indexed by ι × τ ⊕ σ × κ. This is the local input for the tensor product of quasi-coherent sheaves.

The right exactness of the tensor product comes from its closed structure, and the cokernel computation is Mathlib's CategoryTheory.Limits.CokernelCofork.isColimitTensor. The generator-and-relation construction is the sheaf-level analogue of Mathlib's Module.Presentation.tensor in Mathlib.Algebra.Module.Presentation.Tensor, by Joël Riou.

Main declarations

• TauCeti.SheafOfModules.freeTensorFreeIso: free I ⊗ free I' ≅ free (I × I');
• SheafOfModules.Presentation.tensor: the presentation of M ⊗ N built from presentations of M and N; it is finite when both presentations are finite, and its generating morphism is an isomorphism when both generating morphisms are (SheafOfModules.Presentation.isIso_tensor_generators_π).

noncomputable def TauCeti.SheafOfModules.freeTensorFreeIso {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} (I I' : Type u) : CategoryTheory.MonoidalCategoryStruct.tensorObj (SheafOfModules.free I) (SheafOfModules.free I') ≅ SheafOfModules.free (I × I')

The tensor product of the free sheaves of modules on I and on I' is the free sheaf of modules on I × I'. The generator indexed by (i, i') corresponds to the tensor product of the generators indexed by i and i' (ιFree_freeTensorFreeIso_inv).

Equations

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

@[simp]

theorem TauCeti.SheafOfModules.ιFree_freeTensorFreeIso_inv {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {I I' : Type u} (i : I) (i' : I') : CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree (i, i')) (freeTensorFreeIso I I').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (SheafOfModules.unit (ringCatSheaf R))).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (SheafOfModules.ιFree i) (SheafOfModules.ιFree i'))

Under freeTensorFreeIso, the generator indexed by (i, i') is the tensor product of the generators indexed by i and i'.

@[simp]

theorem TauCeti.SheafOfModules.ιFree_freeTensorFreeIso_inv_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {I I' : Type u} (i : I) (i' : I') {Z : SheafOfModules (ringCatSheaf R)} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (SheafOfModules.free I) (SheafOfModules.free I') ⟶ Z) : CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree (i, i')) (CategoryTheory.CategoryStruct.comp (freeTensorFreeIso I I').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (SheafOfModules.unit (ringCatSheaf R))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SheafOfModules.ιFree i) (SheafOfModules.ιFree i')) h)

Under freeTensorFreeIso, the generator indexed by (i, i') is the tensor product of the generators indexed by i and i'.

noncomputable def SheafOfModules.Presentation.tensor {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (P : M.Presentation) (Q : N.Presentation) : (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).Presentation

The tensor product of presentations of M and N is a presentation of M ⊗ N. Its generators are indexed by pairs of generators, and its relations by a relation of M paired with a generator of N, or a generator of M paired with a relation of N.

Equations

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

@[simp]

theorem SheafOfModules.Presentation.tensor_relations_I {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (P : M.Presentation) (Q : N.Presentation) : (P.tensor Q).relations.I = (P.relations.I × Q.generators.I ⊕ P.generators.I × Q.relations.I)

@[simp]

theorem SheafOfModules.Presentation.tensor_generators_I {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (P : M.Presentation) (Q : N.Presentation) : (P.tensor Q).generators.I = (P.generators.I × Q.generators.I)

@[simp]

theorem SheafOfModules.Presentation.tensor_relations_s {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (P : M.Presentation) (Q : N.Presentation) (a✝ : P.relations.I × Q.generators.I ⊕ P.generators.I × Q.relations.I) : (P.tensor Q).relations.s a✝ = (CategoryTheory.Limits.kernel (generatorsOfIsCokernelFree (CategoryTheory.CategoryStruct.comp (freeSumIso (P.relations.I × Q.generators.I) (P.generators.I × Q.relations.I)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (TauCeti.SheafOfModules.freeTensorFreeIso P.relations.I Q.generators.I).inv (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.relations.I).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.kernel P.generators.π).freeHomEquiv.symm P.relations.s) (CategoryTheory.Limits.kernel.ι P.generators.π)) (free Q.generators.I)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (free P.generators.I) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.kernel Q.generators.π).freeHomEquiv.symm Q.relations.s) (CategoryTheory.Limits.kernel.ι Q.generators.π)))) (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.generators.I).hom))) (CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.generators.I).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom P.generators.π Q.generators.π)) ⋯ (CategoryTheory.Limits.IsCokernel.ofIso (CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.kernel P.generators.π).freeHomEquiv.symm P.relations.s) (CategoryTheory.Limits.kernel.ι P.generators.π)) (free Q.generators.I)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (free P.generators.I) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.kernel Q.generators.π).freeHomEquiv.symm Q.relations.s) (CategoryTheory.Limits.kernel.ι Q.generators.π)))) (CategoryTheory.Limits.CokernelCofork.isColimitTensor P.isColimit Q.isColimit) (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.generators.I).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom P.generators.π Q.generators.π)) ⋯) (CategoryTheory.Limits.coprod.mapIso (TauCeti.SheafOfModules.freeTensorFreeIso P.relations.I Q.generators.I) (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.relations.I) ≪≫ freeSumIso (P.relations.I × Q.generators.I) (P.generators.I × Q.relations.I)) (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.generators.I) (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)) ⋯ ⋯)).π).freeHomEquiv (CategoryTheory.Limits.kernel.lift (generatorsOfIsCokernelFree (CategoryTheory.CategoryStruct.comp (freeSumIso (P.relations.I × Q.generators.I) (P.generators.I × Q.relations.I)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (TauCeti.SheafOfModules.freeTensorFreeIso P.relations.I Q.generators.I).inv (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.relations.I).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.kernel P.generators.π).freeHomEquiv.symm P.relations.s) (CategoryTheory.Limits.kernel.ι P.generators.π)) (free Q.generators.I)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (free P.generators.I) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.kernel Q.generators.π).freeHomEquiv.symm Q.relations.s) (CategoryTheory.Limits.kernel.ι Q.generators.π)))) (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.generators.I).hom))) (CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.generators.I).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom P.generators.π Q.generators.π)) ⋯ (CategoryTheory.Limits.IsCokernel.ofIso (CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.kernel P.generators.π).freeHomEquiv.symm P.relations.s) (CategoryTheory.Limits.kernel.ι P.generators.π)) (free Q.generators.I)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (free P.generators.I) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.kernel Q.generators.π).freeHomEquiv.symm Q.relations.s) (CategoryTheory.Limits.kernel.ι Q.generators.π)))) (CategoryTheory.Limits.CokernelCofork.isColimitTensor P.isColimit Q.isColimit) (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.generators.I).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom P.generators.π Q.generators.π)) ⋯) (CategoryTheory.Limits.coprod.mapIso (TauCeti.SheafOfModules.freeTensorFreeIso P.relations.I Q.generators.I) (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.relations.I) ≪≫ freeSumIso (P.relations.I × Q.generators.I) (P.generators.I × Q.relations.I)) (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.generators.I) (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)) ⋯ ⋯)).π (CategoryTheory.CategoryStruct.comp (freeSumIso (P.relations.I × Q.generators.I) (P.generators.I × Q.relations.I)).inv (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.freeTensorFreeIso P.relations.I Q.generators.I).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.Limits.kernel P.generators.π).freeHomEquiv.symm P.relations.s) (free Q.generators.I)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.kernel.ι P.generators.π) (free Q.generators.I)) (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.generators.I).hom))) (CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.relations.I).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (free P.generators.I) ((CategoryTheory.Limits.kernel Q.generators.π).freeHomEquiv.symm Q.relations.s)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (free P.generators.I) (CategoryTheory.Limits.kernel.ι Q.generators.π)) (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.generators.I).hom))))) ⋯) a✝

@[simp]

theorem SheafOfModules.Presentation.tensor_generators_π {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (P : M.Presentation) (Q : N.Presentation) : (P.tensor Q).generators.π = CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.freeTensorFreeIso P.generators.I Q.generators.I).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom P.generators.π Q.generators.π)

The generating morphism of the tensor presentation is the tensor product of the generating morphisms, read through freeTensorFreeIso.

theorem SheafOfModules.Presentation.isIso_tensor_generators_π {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (P : M.Presentation) (Q : N.Presentation) (hP : CategoryTheory.IsIso P.generators.π) (hQ : CategoryTheory.IsIso Q.generators.π) : CategoryTheory.IsIso (P.tensor Q).generators.π

If the generating morphisms of P and Q are isomorphisms, that is, P and Q exhibit M and N as free, then so is the generating morphism of P.tensor Q.

instance SheafOfModules.Presentation.isFinite_tensor {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (P : M.Presentation) (Q : N.Presentation) [P.IsFinite] [Q.IsFinite] : (P.tensor Q).IsFinite

The tensor product of two finite presentations is finite.