The monoidal category of scheme-module sheaves

The sheafified tensor product equips all scheme-module sheaves with a monoidal structure. Its associator is natural and satisfies the triangle and pentagon identities because the comparison maps cancel, reducing the coherence diagrams to those for the objectwise tensor product of presheaves. Intrinsic invertibility is closed under this tensor, so invertible sheaves inherit the same structure as a full monoidal subcategory.

@[implicit_reducible]

def AlgebraicGeometry.Scheme.Modules.instCategory_derivedAlgGeo_2 {X : Scheme} : CategoryTheory.Category.{u, u + 1} X.Modules

Equations

• AlgebraicGeometry.Scheme.Modules.instCategory_derivedAlgGeo_2 = { toCategoryStruct := AlgebraicGeometry.Scheme.Modules.instCategory.toCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

@[implicit_reducible]

noncomputable def AlgebraicGeometry.Scheme.Modules.instMonoidalCategoryPresheafOfModules_derivedAlgGeo_1 {X : Scheme} : CategoryTheory.MonoidalCategory X.PresheafOfModules

Equations

• AlgebraicGeometry.Scheme.Modules.instMonoidalCategoryPresheafOfModules_derivedAlgGeo_1 = PresheafOfModules.monoidalCategory

@[implicit_reducible]

noncomputable def AlgebraicGeometry.Scheme.Modules.instSymmetricCategoryPresheafOfModules_derivedAlgGeo_1 {X : Scheme} : CategoryTheory.SymmetricCategory X.PresheafOfModules

Equations

• AlgebraicGeometry.Scheme.Modules.instSymmetricCategoryPresheafOfModules_derivedAlgGeo_1 = PresheafOfModules.symmetricCategory

theorem AlgebraicGeometry.Scheme.Modules.tensorSheafificationComparisonRight_naturality {X : Scheme} {P Q : X.PresheafOfModules} (f : P ⟶ Q) {L M : X.Modules} (g : L ⟶ M) : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f ((toPresheafOfModules X).map g))) (tensorSheafificationComparisonRight Q M) = CategoryTheory.CategoryStruct.comp (tensorSheafificationComparisonRight P L) (tensorHom ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).map f) g)

theorem AlgebraicGeometry.Scheme.Modules.tensorSheafificationComparisonLeft_naturality {X : Scheme} {L M : X.Modules} (f : L ⟶ M) {P Q : X.PresheafOfModules} (g : P ⟶ Q) : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).map (CategoryTheory.MonoidalCategoryStruct.tensorHom ((toPresheafOfModules X).map f) g)) (M.tensorSheafificationComparisonLeft Q) = CategoryTheory.CategoryStruct.comp (L.tensorSheafificationComparisonLeft P) (tensorHom f ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).map g))

theorem AlgebraicGeometry.Scheme.Modules.tensorAssocIso_naturality {X : Scheme} {L₁ L₂ M₁ M₂ N₁ N₂ : X.Modules} (f : L₁ ⟶ L₂) (g : M₁ ⟶ M₂) (h : N₁ ⟶ N₂) : CategoryTheory.CategoryStruct.comp (tensorHom (tensorHom f g) h) (L₂.tensorAssocIso M₂ N₂).hom = CategoryTheory.CategoryStruct.comp (L₁.tensorAssocIso M₁ N₁).hom (tensorHom f (tensorHom g h))

Naturality of the associator on arbitrary module sheaves.

theorem AlgebraicGeometry.Scheme.Modules.tensorHom_id_id {X : Scheme} (L M : X.Modules) : tensorHom (CategoryTheory.CategoryStruct.id L) (CategoryTheory.CategoryStruct.id M) = CategoryTheory.CategoryStruct.id (L.tensorObj M)

theorem AlgebraicGeometry.Scheme.Modules.tensorHom_comp_tensorHom {X : Scheme} {L₁ L₂ L₃ M₁ M₂ M₃ : X.Modules} (f₁ : L₁ ⟶ L₂) (f₂ : M₁ ⟶ M₂) (g₁ : L₂ ⟶ L₃) (g₂ : M₂ ⟶ M₃) : CategoryTheory.CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂) = tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂)

noncomputable def AlgebraicGeometry.Scheme.Modules.tensorObjIso {X : Scheme} {L L' M M' : X.Modules} (e : L ≅ L') (g : M ≅ M') : L.tensorObj M ≅ L'.tensorObj M'

Tensoring is functorial in each argument, so an isomorphism transports through it.

This is the objectwise form of the tensor bifunctor's action on isomorphisms.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.tensorSheafificationComparisonRight_comp_tensorAssocIso {X : Scheme} (L M N : X.Modules) : CategoryTheory.CategoryStruct.comp (tensorSheafificationComparisonRight (CategoryTheory.MonoidalCategoryStruct.tensorObj ((toPresheafOfModules X).obj L) ((toPresheafOfModules X).obj M)) N) (L.tensorAssocIso M N).hom = CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).map (CategoryTheory.MonoidalCategoryStruct.associator ((toPresheafOfModules X).obj L) ((toPresheafOfModules X).obj M) ((toPresheafOfModules X).obj N)).hom) (L.tensorSheafificationComparisonLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj ((toPresheafOfModules X).obj M) ((toPresheafOfModules X).obj N)))

The right comparison composed with the associator.

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.modulesMonoidalCategoryStruct {X : Scheme} : CategoryTheory.MonoidalCategoryStruct X.Modules

The canonical tensor on all scheme-module sheaves.

Equations

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

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.modulesMonoidalCategory {X : Scheme} : CategoryTheory.MonoidalCategory X.Modules

Scheme-module sheaves form a monoidal category under the sheafified tensor product.

This is the canonical ambient root. Invertible sheaves inherit their monoidal structure as a full monoidal subcategory, so the tensor, associator, and unitors are definitionally shared rather than reimplemented at the leaf.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.tensorLeftFunctor {X : Scheme} (L : X.Modules) : CategoryTheory.Functor X.Modules X.Modules

The historical tensor-left functor is the canonical functor of the monoidal structure on scheme-module sheaves.

Equations

• L.tensorLeftFunctor = CategoryTheory.MonoidalCategory.tensorLeft L

instance AlgebraicGeometry.Scheme.Modules.isInvertibleIsMonoidal {X : Scheme} : (isInvertible X).IsMonoidal

Intrinsic invertibility is a monoidal object property of scheme-module sheaves.

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.invertibleSheafMonoidalCategoryStruct {X : Scheme} : CategoryTheory.MonoidalCategoryStruct (InvertibleSheaf X)

Compatibility name for the inherited monoidal-category structure on invertible sheaves.

Equations

• AlgebraicGeometry.Scheme.Modules.invertibleSheafMonoidalCategoryStruct = (AlgebraicGeometry.Scheme.Modules.isInvertible X).instMonoidalCategoryStructFullSubcategory

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.invertibleSheafMonoidalCategory {X : Scheme} : CategoryTheory.MonoidalCategory (InvertibleSheaf X)

Compatibility name for the monoidal structure inherited by invertible sheaves.

Equations

• AlgebraicGeometry.Scheme.Modules.invertibleSheafMonoidalCategory = (AlgebraicGeometry.Scheme.Modules.isInvertible X).fullMonoidalSubcategory