Documentation

DerivedAlgGeo.AlgebraicGeometry.Modules.Tensor.ComplexColimits

Diagram colimits of complex tensor on scheme-module sheaves #

Ordinary sheaf tensor preserves colimits in either slot. The generic literal-total theorem transfers this to the two fixed-input slots of AlgebraicGeometry.Scheme.Modules.totalTensor for site-universe and small diagram categories. Sequential diagrams are a specialization.

Main definitions #

This module introduces no definitions. It studies the existing AlgebraicGeometry.Scheme.Modules.totalTensor.

Main results #

Implementation notes #

The sheaf tensor colimit theorems supply the partial-functor hypotheses at each term of the fixed complex. The generic cochain-total theorem handles the diagonal coproducts and the comparison to Mathlib's literal total. The site-universe theorem uses ordinary sheaf tensor preservation directly. Size-change instances supply small-shape preservation; the sequential corollaries then specialize to ℕ.

References #

The inputs are AlgebraicGeometry.Scheme.Modules.tensorLeft_preservesColimitsOfShape, AlgebraicGeometry.Scheme.Modules.tensorRight_preservesColimitsOfShape, and the generic CategoryTheory.Functor.preservesColimitsOfShape_map₂CochainComplex_obj and flipped-slot counterpart.

Tags #

scheme-module sheaf, total tensor, cochain complex, diagram colimit

source
theorem AlgebraicGeometry.Scheme.Modules.preservesColimitsOfShape_totalTensor_obj_site (X : Scheme) (K : CochainComplex X.Modules ℤ) (J : Type u) [CategoryTheory.Category.{u, u} J] :
CategoryTheory.Limits.PreservesColimitsOfShape J ((totalTensor X).obj K)

Literal total tensor preserves site-universe diagram colimits in the second complex when the first is fixed. No flatness or exactness is needed.

source
theorem AlgebraicGeometry.Scheme.Modules.preservesColimitsOfShape_totalTensor_flip_obj_site (X : Scheme) (K : CochainComplex X.Modules ℤ) (J : Type u) [CategoryTheory.Category.{u, u} J] :
CategoryTheory.Limits.PreservesColimitsOfShape J ((totalTensor X).flip.obj K)

Literal total tensor preserves site-universe diagram colimits in the first complex when the second is fixed. The bicomplex degree order is retained.

source
theorem AlgebraicGeometry.Scheme.Modules.preservesColimitsOfShape_totalTensor_obj_small (X : Scheme) (K : CochainComplex X.Modules ℤ) (J : Type) [CategoryTheory.Category.{0, 0} J] :
CategoryTheory.Limits.PreservesColimitsOfShape J ((totalTensor X).obj K)

Literal total tensor preserves colimits of any small diagram in the second complex with the first complex fixed. The size-change instances transfer ordinary sheaf tensor preservation to small shapes.

source
theorem AlgebraicGeometry.Scheme.Modules.preservesColimitsOfShape_totalTensor_flip_obj_small (X : Scheme) (K : CochainComplex X.Modules ℤ) (J : Type) [CategoryTheory.Category.{0, 0} J] :
CategoryTheory.Limits.PreservesColimitsOfShape J ((totalTensor X).flip.obj K)

Literal total tensor preserves colimits of any small diagram in the first complex with the second complex fixed. The bicomplex degree order is retained.

source
theorem AlgebraicGeometry.Scheme.Modules.preservesColimitsOfShape_totalTensor_obj_nat (X : Scheme) (K : CochainComplex X.Modules ℤ) :
CategoryTheory.Limits.PreservesColimitsOfShape ℕ ((totalTensor X).obj K)

The small-shape theorem at the sequential diagram category.

source
theorem AlgebraicGeometry.Scheme.Modules.preservesColimitsOfShape_totalTensor_flip_obj_nat (X : Scheme) (K : CochainComplex X.Modules ℤ) :
CategoryTheory.Limits.PreservesColimitsOfShape ℕ ((totalTensor X).flip.obj K)

The flipped small-shape theorem at the sequential diagram category.