Tensor descent for scheme module sheaves

This file compares restriction with module sheafification, proves closure of invertible scheme module sheaves under the sheafified tensor product, and constructs the resulting associator.

The intrinsic rank-one property and arbitrary-site tensor descent are imported from Algebra.Category.ModuleCat.Sheaf; the stronger stalkwise tensor result is imported from Topology.Sheaves.ModuleTensor. This module begins only when the scheme-indexed module category and its topological site enter the signatures.

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

noncomputable def AlgebraicGeometry.Scheme.Modules.instMonoidalCategoryPresheafOfModulesOpensCarrierCarrierCommRingCatObjFunctorOppositeRingCatIsSheafGrothendieckTopologyRingCatSheaf_derivedAlgGeo {X : Scheme} : CategoryTheory.MonoidalCategory (_root_.PresheafOfModules X.ringCatSheaf.obj)

Equations

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

@[implicit_reducible]

noncomputable def AlgebraicGeometry.Scheme.Modules.instSymmetricCategoryPresheafOfModulesOpensCarrierCarrierCommRingCatObjFunctorOppositeRingCatIsSheafGrothendieckTopologyRingCatSheaf_derivedAlgGeo {X : Scheme} : CategoryTheory.SymmetricCategory (_root_.PresheafOfModules X.ringCatSheaf.obj)

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.overSheafificationComparison {X : Scheme} (P : X.PresheafOfModules) (U : X.Opens) : (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (CategoryTheory.Sheaf.over X.ringCatSheaf U).obj)).obj ((AlgebraicGeometry.Scheme.Modules.overPresheafFunctor✝ X U).obj P) ⟶ ((AlgebraicGeometry.Scheme.Modules.associatedSheaf'✝ X).obj P).over U

Restriction of an associated module sheaf is the associated sheaf of the restriction.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.isIso_overSheafificationComparison {X : Scheme} (P : X.PresheafOfModules) (U : X.Opens) : CategoryTheory.IsIso (overSheafificationComparison P U)

noncomputable def AlgebraicGeometry.Scheme.Modules.overTensorPresheafIso {X : Scheme} (P Q : X.PresheafOfModules) (U : X.Opens) : (AlgebraicGeometry.Scheme.Modules.overPresheafFunctor✝ X U).obj (AlgebraicGeometry.Scheme.Modules.tensorPresheaf'✝ X P Q) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj ((AlgebraicGeometry.Scheme.Modules.overPresheafFunctor✝ X U).obj P) ((AlgebraicGeometry.Scheme.Modules.overPresheafFunctor✝ X U).obj Q)

Restriction of the objectwise tensor presheaf is the tensor of the restrictions.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.tensorOverIsoOfTrivializations {X : Scheme} (L M : X.Modules) (U : X.Opens) (eL : SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf U) ≅ SheafOfModules.over L U) (eM : SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf U) ≅ SheafOfModules.over M U) : SheafOfModules.over (L.tensorObj M) U ≅ SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf U)

The tensor product is trivial on an open where both factors are trivial.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.tensorOverIsoOfTrivializationRight {X : Scheme} (L M : X.Modules) (U : X.Opens) (eM : SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf U) ≅ SheafOfModules.over M U) : SheafOfModules.over (L.tensorObj M) U ≅ SheafOfModules.over L U

Tensoring with a sheaf that is trivial on U does nothing to the restriction to U.

The one-sided companion of tensorOverIsoOfTrivializations, which needs both factors trivial and lands on the unit. Here only the right factor is trivialized and the left one is arbitrary, so the right unitor replaces the left one and the result is L.over U rather than the unit.

This is the shape a twist consumes: F(n) = F ⊗ O(n) restricted to a chart where O(n) is trivial is just F restricted to that chart, with F arbitrary.

Equations

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

instance AlgebraicGeometry.Scheme.Modules.isInvertible_tensorObj {X : Scheme} (L M : X.Modules) [(have this := L; this).IsInvertible] [(have this := M; this).IsInvertible] : (have this := L.tensorObj M; this).IsInvertible

The sheafified tensor product of invertible sheaves is invertible.

theorem AlgebraicGeometry.Scheme.Modules.isIso_sheafification_map_whiskerLeft_unit {X : Scheme} (M P : X.PresheafOfModules) : CategoryTheory.IsIso ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M ((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id X.ringCatSheaf.obj)).unit.app P)))

Sheafification inverts M ◁ toSheafify for an arbitrary M.

The general form of SheafOfModules.isIso_sheafification_map_whiskerLeft_unit_of_rankOneData, with the rank-one hypothesis on the whiskering factor gone. It is available here and not over a general site because the proof is stalkwise; see PresheafOfModules.W_whiskerLeft_of_isIso_stalk.

noncomputable def AlgebraicGeometry.Scheme.Modules.tensorSheafificationComparisonLeft {X : Scheme} (L : X.Modules) (P : X.PresheafOfModules) : (AlgebraicGeometry.Scheme.Modules.associatedSheaf'✝ X).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj ((toPresheafOfModules X).obj L) P) ⟶ L.tensorObj ((AlgebraicGeometry.Scheme.Modules.associatedSheaf'✝ X).obj P)

Comparison from tensoring before sheafification to tensoring with the associated sheaf.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.tensorSheafificationComparisonRight {X : Scheme} (P : X.PresheafOfModules) (L : X.Modules) : (AlgebraicGeometry.Scheme.Modules.associatedSheaf'✝ X).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj P ((toPresheafOfModules X).obj L)) ⟶ tensorObj ((AlgebraicGeometry.Scheme.Modules.associatedSheaf'✝ X).obj P) L

Right-handed comparison from tensoring before sheafification.

Equations

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

instance AlgebraicGeometry.Scheme.Modules.isIso_tensorSheafificationComparisonLeft {X : Scheme} (L : X.Modules) (P : X.PresheafOfModules) : CategoryTheory.IsIso (L.tensorSheafificationComparisonLeft P)

The left comparison is an isomorphism for arbitrary L.

The invertibility hypothesis this carried until #833 was an artifact of proving local injectivity and local surjectivity separately: the injective half then needed L locally trivial. Going through stalks avoids the split — see isIso_sheafification_map_whiskerLeft_unit.

instance AlgebraicGeometry.Scheme.Modules.isIso_tensorSheafificationComparisonRight {X : Scheme} (P : X.PresheafOfModules) (L : X.Modules) : CategoryTheory.IsIso (tensorSheafificationComparisonRight P L)

The right comparison is an isomorphism for arbitrary L.

The left comparison is already invertible with no rank-one, finiteness, or flatness hypothesis, because its proof goes through stalks. Symmetry of the objectwise presheaf tensor then conjugates one whiskering into the other, and that conjugation holds on an arbitrary site: it is SheafOfModules.isIso_sheafification_map_whiskerRight_of_whiskerLeft, which lives with the rest of the arbitrary-site tensor descent. Only the stalkwise input it consumes is scheme-level, so nothing generic is restated here. This removes the last rank-one restriction from associativity of the sheafified tensor product.

noncomputable def AlgebraicGeometry.Scheme.Modules.tensorAssocIso {X : Scheme} (L M N : X.Modules) : (L.tensorObj M).tensorObj N ≅ L.tensorObj (M.tensorObj N)

Associativity of the sheafified tensor product for arbitrary module sheaves.

Equations

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