Documentation

TauCeti.AlgebraicGeometry.Modules.Quasicoherent.Basic

The monoidal category of quasicoherent sheaves #

For a scheme X, QuasicoherentSheaf X is the full subcategory of X.Modules on the quasicoherent sheaves. It inherits the symmetric monoidal structure of X.Modules.

Finite free sheaves give the basic dualizable objects in the quasicoherent category. The free sheaf on a finite type is self-dual there, with evaluation and coevaluation inherited from the corresponding exact pairing in X.Modules.

Quasi-coherence is stable under pullback along an arbitrary morphism of schemes, so pullback of modules restricts to quasicoherent sheaves.

Pullback of quasicoherent sheaves is compatible with identities and composition. In particular, an isomorphism of schemes induces an equivalence of their quasicoherent-sheaf categories.

Main declarations #

source
@[instance_reducible]
noncomputable def TauCeti.AlgebraicGeometry.symmetricCategorySheafOfModules (X : AlgebraicGeometry.Scheme) :
CategoryTheory.SymmetricCategory (SheafOfModules X.ringCatSheaf)

The symmetry of X.Modules, stated for the unfolded type SheafOfModules X.ringCatSheaf, which typeclass search does not see through the definition of Scheme.Modules.

Equations
Instances For
    source
    theorem TauCeti.AlgebraicGeometry.isMonoidalIsQuasicoherent (X : AlgebraicGeometry.Scheme) :
    (SheafOfModules.isQuasicoherent X.ringCatSheaf).IsMonoidal

    Quasi-coherence is a monoidal property of SheafOfModules X.ringCatSheaf, stated for that unfolded type rather than for X.Modules.

    source
    @[reducible, inline]
    abbrev TauCeti.AlgebraicGeometry.QuasicoherentSheaf (X : AlgebraicGeometry.Scheme) :
    Type (u + 1)

    The full category of quasicoherent sheaves of modules on a scheme.

    Equations
    Instances For
      source
      @[instance_reducible]
      noncomputable instance TauCeti.AlgebraicGeometry.instMonoidalCategoryQuasicoherentSheaf (X : AlgebraicGeometry.Scheme) :
      CategoryTheory.MonoidalCategory (QuasicoherentSheaf X)

      The symmetric monoidal structure on quasicoherent sheaves inherited from X.Modules.

      Equations
      source
      @[instance_reducible]
      noncomputable instance TauCeti.AlgebraicGeometry.instSymmetricCategoryQuasicoherentSheaf (X : AlgebraicGeometry.Scheme) :
      CategoryTheory.SymmetricCategory (QuasicoherentSheaf X)

      The symmetry on quasicoherent sheaves inherited from X.Modules.

      Equations
      source
      @[reducible, inline]
      noncomputable abbrev TauCeti.AlgebraicGeometry.QuasicoherentSheaf.free (X : AlgebraicGeometry.Scheme) (I : Type u) [Finite I] :
      QuasicoherentSheaf X

      The free sheaf on a finite type, as a quasicoherent sheaf.

      This is an abbreviation so that instance search sees its underlying finite free sheaf and hence the exact self-pairing on that sheaf.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.free_obj (X : AlgebraicGeometry.Scheme) (I : Type u) [Finite I] :
        (free X I).obj = SheafOfModules.free I
        source
        @[instance_reducible]
        noncomputable instance TauCeti.AlgebraicGeometry.QuasicoherentSheaf.exactPairingFree (X : AlgebraicGeometry.Scheme) (I : Type u) [Finite I] :
        CategoryTheory.ExactPairing (free X I) (free X I)

        The free quasicoherent sheaf on a finite type is self-dual.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[instance_reducible]
        noncomputable instance TauCeti.AlgebraicGeometry.QuasicoherentSheaf.hasLeftDualFree (X : AlgebraicGeometry.Scheme) (I : Type u) [Finite I] :
        CategoryTheory.HasLeftDual (free X I)

        The chosen left dual of a finite free quasicoherent sheaf is itself.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[instance_reducible]
        noncomputable instance TauCeti.AlgebraicGeometry.QuasicoherentSheaf.hasRightDualFree (X : AlgebraicGeometry.Scheme) (I : Type u) [Finite I] :
        CategoryTheory.HasRightDual (free X I)

        The chosen right dual of a finite free quasicoherent sheaf is itself.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.leftDual_free (X : AlgebraicGeometry.Scheme) (I : Type u) [Finite I] :
        ᘁ(free X I) = free X I
        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.rightDual_free (X : AlgebraicGeometry.Scheme) (I : Type u) [Finite I] :
        (free X I)ᘁ = free X I
        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.evaluation_free_hom (X : AlgebraicGeometry.Scheme) (I : Type u) [Finite I] :
        (ε_ (free X I) (free X I)).hom = ε_ (free X I).obj (free X I).obj

        The evaluation of the self-duality of a finite free quasicoherent sheaf is the evaluation of the underlying finite free sheaf of modules.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.coevaluation_free_hom (X : AlgebraicGeometry.Scheme) (I : Type u) [Finite I] :
        (η_ (free X I) (free X I)).hom = η_ (free X I).obj (free X I).obj

        The coevaluation of the self-duality of a finite free quasicoherent sheaf is the coevaluation of the underlying finite free sheaf of modules.

        source
        noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
        CategoryTheory.Functor (QuasicoherentSheaf Y) (QuasicoherentSheaf X)

        The pullback of quasicoherent sheaves along a morphism of schemes f : X ⟶ Y.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_obj_obj {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : QuasicoherentSheaf Y) :
          ((pullback f).obj E).obj = (AlgebraicGeometry.Scheme.Modules.pullback f).obj E.obj

          The underlying sheaf of the pullback of a quasicoherent sheaf is its pullback as an 𝒪_Y-module.

          source
          @[simp]
          theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullback_map_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {E F : QuasicoherentSheaf Y} (φ : E ⟶ F) :
          ((pullback f).map φ).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map φ.hom) (CategoryTheory.eqToHom ⋯))

          Pullback acts on a morphism of quasicoherent sheaves by the underlying pullback of modules.

          source
          noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullbackId (X : AlgebraicGeometry.Scheme) :
          pullback (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id (QuasicoherentSheaf X)

          Pullback of quasi-coherent modules along the identity is naturally the identity.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullbackId_hom_app_hom (X : AlgebraicGeometry.Scheme) (E : QuasicoherentSheaf X) :
            ((pullbackId X).hom.app E).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((AlgebraicGeometry.Scheme.Modules.pullbackId X).hom.app E.obj)

            The identity comparison is Mathlib's comparison on underlying modules.

            source
            @[simp]
            theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullbackId_inv_app_hom (X : AlgebraicGeometry.Scheme) (E : QuasicoherentSheaf X) :
            ((pullbackId X).inv.app E).hom = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackId X).inv.app E.obj) (CategoryTheory.eqToHom ⋯)

            The inverse identity comparison is Mathlib's inverse on underlying modules.

            source
            theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullbackComp_obj_obj {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (E : QuasicoherentSheaf Z) :
            (((pullback g).comp (pullback f)).obj E).obj = ((AlgebraicGeometry.Scheme.Modules.pullback g).comp (AlgebraicGeometry.Scheme.Modules.pullback f)).obj E.obj

            The underlying module of a composite restricted pullback is the composite module pullback.

            source
            noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullbackComp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) :
            (pullback g).comp (pullback f) ≅ pullback (CategoryTheory.CategoryStruct.comp f g)

            Pullback of quasi-coherent modules respects composition.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullbackComp_hom_app_hom {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (E : QuasicoherentSheaf Z) :
              ((pullbackComp f g).hom.app E).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).hom.app E.obj) (CategoryTheory.eqToHom ⋯))

              The composition comparison is Mathlib's comparison on underlying modules.

              source
              @[simp]
              theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.pullbackComp_inv_app_hom {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (E : QuasicoherentSheaf Z) :
              ((pullbackComp f g).inv.app E).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app E.obj) (CategoryTheory.eqToHom ⋯))

              The inverse composition comparison is Mathlib's inverse on underlying modules.

              source
              noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentSheaf.equivOfIso {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) :
              QuasicoherentSheaf Y ≌ QuasicoherentSheaf X

              An isomorphism of schemes induces an equivalence of quasi-coherent modules.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.equivOfIso_functor {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) :
                (equivOfIso e).functor = pullback e.hom

                The forward functor of the equivalence induced by a scheme isomorphism is pullback.

                source
                @[simp]
                theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.equivOfIso_inverse {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) :
                (equivOfIso e).inverse = pullback e.inv

                The inverse functor of the equivalence induced by a scheme isomorphism is pullback.