Documentation

DerivedAlgGeo.AlgebraicGeometry.Divisors.Symmetric

Symmetry of the tensor product on invertible sheaves #

The presheaf braiding descends through module sheafification. Naturality and both hexagon identities reduce to the corresponding symmetric-monoidal identities for presheaves; the reverse hexagon is obtained from the forward hexagon using involutivity of the commutor.

source
@[implicit_reducible]
def AlgebraicGeometry.Scheme.Modules.instCategory_derivedAlgGeo_3 {X : Scheme} :
CategoryTheory.Category.{u, u + 1} X.Modules
Equations
Instances For
    source
    @[implicit_reducible]
    noncomputable def AlgebraicGeometry.Scheme.Modules.instMonoidalCategoryPresheafOfModules_derivedAlgGeo_2 {X : Scheme} :
    CategoryTheory.MonoidalCategory X.PresheafOfModules
    Equations
    Instances For
      source
      @[implicit_reducible]
      noncomputable def AlgebraicGeometry.Scheme.Modules.instSymmetricCategoryPresheafOfModules_derivedAlgGeo_2 {X : Scheme} :
      CategoryTheory.SymmetricCategory X.PresheafOfModules
      Equations
      Instances For
        source
        theorem AlgebraicGeometry.Scheme.Modules.tensorCommIso_naturality {X : Scheme} {L₁ L₂ M₁ M₂ : X.Modules} (f : L₁ ⟶ L₂) (g : M₁ ⟶ M₂) :
        CategoryTheory.CategoryStruct.comp (tensorHom f g) (L₂.tensorCommIso M₂).hom = CategoryTheory.CategoryStruct.comp (L₁.tensorCommIso M₁).hom (tensorHom g f)
        source
        theorem AlgebraicGeometry.Scheme.Modules.tensorCommIso_symmetry {X : Scheme} (L M : X.Modules) :
        CategoryTheory.CategoryStruct.comp (L.tensorCommIso M).hom (M.tensorCommIso L).hom = CategoryTheory.CategoryStruct.id (L.tensorObj M)
        source
        theorem AlgebraicGeometry.Scheme.Modules.tensorCommIso_inv {X : Scheme} (L M : X.Modules) :
        (L.tensorCommIso M).inv = (M.tensorCommIso L).hom
        source
        @[implicit_reducible]
        noncomputable instance AlgebraicGeometry.Scheme.Modules.invertibleSheafBraidedCategory {X : Scheme} :
        CategoryTheory.BraidedCategory (InvertibleSheaf X)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[implicit_reducible]
        noncomputable instance AlgebraicGeometry.Scheme.Modules.invertibleSheafSymmetricCategory {X : Scheme} :
        CategoryTheory.SymmetricCategory (InvertibleSheaf X)
        Equations